<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<title>CVC3: search_impl_base.h Source File</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li><a href="annotated.html"><span>Classes</span></a></li>
<li class="current"><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="files.html"><span>File List</span></a></li>
<li><a href="globals.html"><span>File Members</span></a></li>
</ul>
</div>
<div class="header">
<div class="headertitle">
<div class="title">search_impl_base.h</div> </div>
</div>
<div class="contents">
<a href="search__impl__base_8h.html">Go to the documentation of this file.</a><div class="fragment"><pre class="fragment"><a name="l00001"></a>00001 <span class="comment">/*****************************************************************************/</span><span class="comment"></span>
<a name="l00002"></a>00002 <span class="comment">/*!</span>
<a name="l00003"></a>00003 <span class="comment"> * \file search_impl_base.h</span>
<a name="l00004"></a>00004 <span class="comment"> * \brief Abstract API to the proof search engine</span>
<a name="l00005"></a>00005 <span class="comment"> * </span>
<a name="l00006"></a>00006 <span class="comment"> * Author: Clark Barrett, Vijay Ganesh (Clausal Normal Form Converter)</span>
<a name="l00007"></a>00007 <span class="comment"> * </span>
<a name="l00008"></a>00008 <span class="comment"> * Created: Fri Jan 17 13:35:03 2003</span>
<a name="l00009"></a>00009 <span class="comment"> *</span>
<a name="l00010"></a>00010 <span class="comment"> * <hr></span>
<a name="l00011"></a>00011 <span class="comment"> *</span>
<a name="l00012"></a>00012 <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span>
<a name="l00013"></a>00013 <span class="comment"> * and its documentation for any purpose is hereby granted without</span>
<a name="l00014"></a>00014 <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span>
<a name="l00015"></a>00015 <span class="comment"> * LICENSE file provided with this distribution.</span>
<a name="l00016"></a>00016 <span class="comment"> * </span>
<a name="l00017"></a>00017 <span class="comment"> * <hr></span>
<a name="l00018"></a>00018 <span class="comment"> * </span>
<a name="l00019"></a>00019 <span class="comment"> */</span>
<a name="l00020"></a>00020 <span class="comment">/*****************************************************************************/</span>
<a name="l00021"></a>00021
<a name="l00022"></a>00022 <span class="preprocessor">#ifndef _cvc3__include__search_impl_base_h_</span>
<a name="l00023"></a>00023 <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__include__search_impl_base_h_</span>
<a name="l00024"></a>00024 <span class="preprocessor"></span>
<a name="l00025"></a>00025 <span class="preprocessor">#include "<a class="code" href="search_8h.html" title="Abstract API to the proof search engine.">search.h</a>"</span>
<a name="l00026"></a>00026 <span class="preprocessor">#include "<a class="code" href="theory__core_8h.html">theory_core.h</a>"</span>
<a name="l00027"></a>00027 <span class="preprocessor">#include "<a class="code" href="variable_8h.html">variable.h</a>"</span>
<a name="l00028"></a>00028 <span class="preprocessor">#include "<a class="code" href="formula__value_8h.html" title="enumerated type for value of formulas">formula_value.h</a>"</span>
<a name="l00029"></a>00029
<a name="l00030"></a>00030 <span class="keyword">namespace </span>CVC3 {
<a name="l00031"></a>00031
<a name="l00032"></a>00032 <span class="keyword">class </span>SearchEngineRules;
<a name="l00033"></a>00033 <span class="keyword">class </span>VariableManager;
<a name="l00034"></a>00034 <span class="comment"></span>
<a name="l00035"></a>00035 <span class="comment"> //! API to to a generic proof search engine (a.k.a. SAT solver) </span>
<a name="l00036"></a>00036 <span class="comment"></span><span class="comment"> /*! \ingroup SE */</span>
<a name="l00037"></a><a class="code" href="classCVC3_1_1SearchImplBase.html">00037</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1SearchImplBase.html" title="API to to a generic proof search engine (a.k.a. SAT solver)">SearchImplBase</a> :<span class="keyword">public</span> <a class="code" href="classCVC3_1_1SearchEngine.html" title="API to to a generic proof search engine.">SearchEngine</a> {
<a name="l00038"></a><a class="code" href="classCVC3_1_1SearchImplBase.html#a224d899d0f44bb19868fa244a59d1577">00038</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1DecisionEngine.html">DecisionEngine</a>;
<a name="l00039"></a>00039 <span class="keyword">protected</span>:<span class="comment"></span>
<a name="l00040"></a>00040 <span class="comment"> /*! \addtogroup SE </span>
<a name="l00041"></a>00041 <span class="comment"> * @{</span>
<a name="l00042"></a>00042 <span class="comment"> */</span><span class="comment"></span>
<a name="l00043"></a>00043 <span class="comment"> //! Variable manager for classes Variable and Literal</span>
<a name="l00044"></a><a class="code" href="group__SE.html#ga626a0fe24f363d007d729e16d13349e5">00044</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1VariableManager.html">VariableManager</a>* <a class="code" href="group__SE.html#ga626a0fe24f363d007d729e16d13349e5" title="Variable manager for classes Variable and Literal.">d_vm</a>;
<a name="l00045"></a>00045 <span class="comment"></span>
<a name="l00046"></a>00046 <span class="comment"> /*! @brief The bottom-most scope for the current call to checkSAT (where conflict</span>
<a name="l00047"></a>00047 <span class="comment"> clauses are still valid).</span>
<a name="l00048"></a>00048 <span class="comment"> */</span>
<a name="l00049"></a><a class="code" href="group__SE.html#ga640e08e2b051e08f2abdd4111b9a2e71">00049</a> <a class="code" href="classCVC3_1_1CDO.html">CDO<int></a> <a class="code" href="group__SE.html#ga640e08e2b051e08f2abdd4111b9a2e71" title="The bottom-most scope for the current call to checkSAT (where conflict clauses are still valid)...">d_bottomScope</a>;
<a name="l00050"></a>00050
<a name="l00051"></a><a class="code" href="group__SE.html#ga02f72989536076eab8c55e452a6662d9">00051</a> <a class="code" href="classCVC3_1_1TheoryCore_1_1CoreSatAPI.html" title="Interface class for callbacks to SAT from Core.">TheoryCore::CoreSatAPI</a>* <a class="code" href="group__SE.html#ga02f72989536076eab8c55e452a6662d9">d_coreSatAPI_implBase</a>;
<a name="l00052"></a>00052 <span class="comment"></span>
<a name="l00053"></a>00053 <span class="comment"> //! Representation of a DP-suggested splitter</span>
<a name="l00054"></a><a class="code" href="classCVC3_1_1SearchImplBase_1_1Splitter.html">00054</a> <span class="comment"></span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1SearchImplBase_1_1Splitter.html" title="Representation of a DP-suggested splitter.">Splitter</a> {
<a name="l00055"></a><a class="code" href="classCVC3_1_1SearchImplBase_1_1Splitter.html#a5a12e90f92f58ac61e1525f8a8099def">00055</a> <a class="code" href="classCVC3_1_1Literal.html">Literal</a> <a class="code" href="classCVC3_1_1SearchImplBase_1_1Splitter.html#a5a12e90f92f58ac61e1525f8a8099def">d_lit</a>;
<a name="l00056"></a>00056 <span class="keyword">public</span>:
<a name="l00057"></a>00057 <span class="comment">// int priority;</span><span class="comment"></span>
<a name="l00058"></a>00058 <span class="comment"> //! Constructor</span>
<a name="l00059"></a>00059 <span class="comment"></span> <a class="code" href="classCVC3_1_1SearchImplBase_1_1Splitter.html#a59ee8b0fa0185678e86266e6159bf69a" title="Constructor.">Splitter</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Literal.html">Literal</a>& lit);<span class="comment"></span>
<a name="l00060"></a>00060 <span class="comment"> //! Copy constructor</span>
<a name="l00061"></a>00061 <span class="comment"></span> <a class="code" href="classCVC3_1_1SearchImplBase_1_1Splitter.html#a59ee8b0fa0185678e86266e6159bf69a" title="Constructor.">Splitter</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1SearchImplBase_1_1Splitter.html" title="Representation of a DP-suggested splitter.">Splitter</a>& s);<span class="comment"></span>
<a name="l00062"></a>00062 <span class="comment"> //! Assignment</span>
<a name="l00063"></a>00063 <span class="comment"></span> <a class="code" href="classCVC3_1_1SearchImplBase_1_1Splitter.html" title="Representation of a DP-suggested splitter.">Splitter</a>& <a class="code" href="classCVC3_1_1SearchImplBase_1_1Splitter.html#a5ba159e6e31410ed42bb5edfe2d7020b" title="Assignment.">operator=</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1SearchImplBase_1_1Splitter.html" title="Representation of a DP-suggested splitter.">Splitter</a>& s);<span class="comment"></span>
<a name="l00064"></a>00064 <span class="comment"> //! Descructor</span>
<a name="l00065"></a>00065 <span class="comment"></span> <a class="code" href="classCVC3_1_1SearchImplBase_1_1Splitter.html#a41e072e9644325ae849a1602c31d9d36" title="Descructor.">~Splitter</a>();
<a name="l00066"></a><a class="code" href="classCVC3_1_1SearchImplBase_1_1Splitter.html#a2d93d367e7ad35f828fafb931827380d">00066</a> <a class="code" href="classCVC3_1_1SearchImplBase_1_1Splitter.html#a2d93d367e7ad35f828fafb931827380d">operator Literal</a>() { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1SearchImplBase_1_1Splitter.html#a5a12e90f92f58ac61e1525f8a8099def">d_lit</a>; }<span class="comment"></span>
<a name="l00067"></a>00067 <span class="comment"> //! The order is descending by priority ("reversed", highest first)</span>
<a name="l00068"></a>00068 <span class="comment"></span><span class="comment">// friend bool operator<(const Splitter& s1, const Splitter& s2) {</span>
<a name="l00069"></a>00069 <span class="comment">// return (s1.priority > s2.priority</span>
<a name="l00070"></a>00070 <span class="comment">// || (s1.priority == s2.priority && s1.expr > s2.expr));</span>
<a name="l00071"></a>00071 <span class="comment">// }</span>
<a name="l00072"></a>00072 };<span class="comment"></span>
<a name="l00073"></a>00073 <span class="comment"> //! Backtracking ordered set of DP-suggested splitters</span>
<a name="l00074"></a><a class="code" href="group__SE.html#ga8ea9b2ab9f50d3ddf595595b1f3d7974">00074</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Splitter></a> <a class="code" href="group__SE.html#ga8ea9b2ab9f50d3ddf595595b1f3d7974" title="Backtracking ordered set of DP-suggested splitters.">d_dpSplitters</a>;
<a name="l00075"></a>00075 <span class="comment"></span>
<a name="l00076"></a>00076 <span class="comment"> /*! @brief Theorem from the last successful checkValid call. It is</span>
<a name="l00077"></a>00077 <span class="comment"> used by getProof and getAssumptions. */</span>
<a name="l00078"></a><a class="code" href="group__SE.html#ga88ba664573602ecfca1d6eadc14a30af">00078</a> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="group__SE.html#ga88ba664573602ecfca1d6eadc14a30af" title="Theorem from the last successful checkValid call. It is used by getProof and getAssumptions.">d_lastValid</a>;<span class="comment"></span>
<a name="l00079"></a>00079 <span class="comment"> /*! @brief Assumptions from the last unsuccessful checkValid call.</span>
<a name="l00080"></a>00080 <span class="comment"> These are used by getCounterExample. */</span>
<a name="l00081"></a><a class="code" href="group__SE.html#gaf6841e86841006b6917d46664de64d21">00081</a> <a class="code" href="classCVC3_1_1ExprHashMap.html">ExprHashMap<bool></a> <a class="code" href="group__SE.html#gaf6841e86841006b6917d46664de64d21" title="Assumptions from the last unsuccessful checkValid call. These are used by getCounterExample.">d_lastCounterExample</a>;<span class="comment"></span>
<a name="l00082"></a>00082 <span class="comment"> /*! @brief Maintain the list of current assumptions (user asserts and</span>
<a name="l00083"></a>00083 <span class="comment"> splitters) for getAssumptions(). */</span>
<a name="l00084"></a><a class="code" href="group__SE.html#ga83dfe2d2d85bacf5e4aa10c0320a140b">00084</a> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr,Theorem></a> <a class="code" href="group__SE.html#ga83dfe2d2d85bacf5e4aa10c0320a140b" title="Maintain the list of current assumptions (user asserts and splitters) for getAssumptions().">d_assumptions</a>;
<a name="l00085"></a>00085 <span class="comment"></span>
<a name="l00086"></a>00086 <span class="comment"> //! Backtracking cache for the CNF generator</span>
<a name="l00087"></a><a class="code" href="group__SE.html#gab60a7d204ed01875c98629e874575cd6">00087</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr, Theorem></a> <a class="code" href="group__SE.html#gab60a7d204ed01875c98629e874575cd6" title="Backtracking cache for the CNF generator.">d_cnfCache</a>;<span class="comment"></span>
<a name="l00088"></a>00088 <span class="comment"> //! Backtracking set of new variables generated by CNF translator</span>
<a name="l00089"></a>00089 <span class="comment"></span><span class="comment"> /*! Specific search engines do not have to split on these variables */</span>
<a name="l00090"></a><a class="code" href="group__SE.html#ga1c64a37d94b4cadedce29f3e4b98a3af">00090</a> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr, bool></a> <a class="code" href="group__SE.html#ga1c64a37d94b4cadedce29f3e4b98a3af" title="Backtracking set of new variables generated by CNF translator.">d_cnfVars</a>;<span class="comment"></span>
<a name="l00091"></a>00091 <span class="comment"> //! Command line flag whether to convert to CNF</span>
<a name="l00092"></a><a class="code" href="group__SE.html#gae3b8b3cfd965e7d5138320d26808767a">00092</a> <span class="comment"></span> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="group__SE.html#gae3b8b3cfd965e7d5138320d26808767a" title="Command line flag whether to convert to CNF.">d_cnfOption</a>;<span class="comment"></span>
<a name="l00093"></a>00093 <span class="comment"> //! Flag: whether to convert term ITEs into CNF</span>
<a name="l00094"></a><a class="code" href="group__SE.html#gaa28d7e60bbe1df69ffb304f939b984b7">00094</a> <span class="comment"></span> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="group__SE.html#gaa28d7e60bbe1df69ffb304f939b984b7" title="Flag: whether to convert term ITEs into CNF.">d_ifLiftOption</a>;<span class="comment"></span>
<a name="l00095"></a>00095 <span class="comment"> //! Flag: ignore auxiliary CNF variables when searching for a splitter</span>
<a name="l00096"></a><a class="code" href="group__SE.html#gafc2c782e4f24b55c8af7cb0189d281d8">00096</a> <span class="comment"></span> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="group__SE.html#gafc2c782e4f24b55c8af7cb0189d281d8" title="Flag: ignore auxiliary CNF variables when searching for a splitter.">d_ignoreCnfVarsOption</a>;<span class="comment"></span>
<a name="l00097"></a>00097 <span class="comment"> //! Flag: Preserve the original formula with +cnf (for splitter heuristics)</span>
<a name="l00098"></a><a class="code" href="group__SE.html#ga2287fd23d4250cc74db446983b2c3274">00098</a> <span class="comment"></span> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="group__SE.html#ga2287fd23d4250cc74db446983b2c3274" title="Flag: Preserve the original formula with +cnf (for splitter heuristics)">d_origFormulaOption</a>;
<a name="l00099"></a>00099 <span class="comment"></span>
<a name="l00100"></a>00100 <span class="comment"> /*!</span>
<a name="l00101"></a>00101 <span class="comment"> * \name CNF Caches </span>
<a name="l00102"></a>00102 <span class="comment"> *</span>
<a name="l00103"></a>00103 <span class="comment"> * These caches are for subexpressions of the translated formula</span>
<a name="l00104"></a>00104 <span class="comment"> * phi, to avoid expanding phi into a tree. We cannot use</span>
<a name="l00105"></a>00105 <span class="comment"> * d_cnfCache for that, since it is effectively non-backtracking,</span>
<a name="l00106"></a>00106 <span class="comment"> * and we do not know if a subexpression of phi was translated at</span>
<a name="l00107"></a>00107 <span class="comment"> * the current level, or at some other (inactive) branch of the</span>
<a name="l00108"></a>00108 <span class="comment"> * decision tree.</span>
<a name="l00109"></a>00109 <span class="comment"> * @{</span>
<a name="l00110"></a>00110 <span class="comment"> */</span><span class="comment"></span>
<a name="l00111"></a>00111 <span class="comment"> //! Cache for enqueueCNF()</span>
<a name="l00112"></a><a class="code" href="group__SE.html#ga9dc16eb11f046d9a615aff3018957c6d">00112</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr,bool></a> <a class="code" href="group__SE.html#ga9dc16eb11f046d9a615aff3018957c6d" title="Cache for enqueueCNF()">d_enqueueCNFCache</a>;<span class="comment"></span>
<a name="l00113"></a>00113 <span class="comment"> //! Cache for applyCNFRules()</span>
<a name="l00114"></a><a class="code" href="group__SE.html#ga401319b3ede7162504e979aaf2119deb">00114</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr,bool></a> <a class="code" href="group__SE.html#ga401319b3ede7162504e979aaf2119deb" title="Cache for applyCNFRules()">d_applyCNFRulesCache</a>;<span class="comment"></span>
<a name="l00115"></a>00115 <span class="comment"> //! Cache for replaceITE()</span>
<a name="l00116"></a><a class="code" href="group__SE.html#ga0c829909b9e3ab2b59ba40e681905c4b">00116</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr,Theorem></a> <a class="code" href="group__SE.html#ga0c829909b9e3ab2b59ba40e681905c4b" title="Cache for replaceITE()">d_replaceITECache</a>;<span class="comment"></span>
<a name="l00117"></a>00117 <span class="comment"> /*@}*/</span> <span class="comment">// End of CNF Caches</span>
<a name="l00118"></a>00118 <span class="comment"></span>
<a name="l00119"></a>00119 <span class="comment"> //! Construct a Literal out of an Expr or return an existing one</span>
<a name="l00120"></a><a class="code" href="group__SE.html#gaf0dbbb1806723760ab8744e96a8c6657">00120</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1Literal.html">Literal</a> <a class="code" href="group__SE.html#gaf0dbbb1806723760ab8744e96a8c6657" title="Construct a Literal out of an Expr or return an existing one.">newLiteral</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Literal.html">Literal</a>(<a class="code" href="group__SE.html#ga626a0fe24f363d007d729e16d13349e5" title="Variable manager for classes Variable and Literal.">d_vm</a>, e); }
<a name="l00121"></a>00121 <span class="comment"></span>
<a name="l00122"></a>00122 <span class="comment"> /*! @brief Our version of simplifier: take Theorem(e), apply</span>
<a name="l00123"></a>00123 <span class="comment"> simplifier to get Theorem(e==e'), return Theorem(e') */</span>
<a name="l00124"></a><a class="code" href="group__SE.html#gaaa621df0c7e2a2043139e6451eab7072">00124</a> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="group__SE.html#gaaa621df0c7e2a2043139e6451eab7072" title="Our version of simplifier: take Theorem(e), apply simplifier to get Theorem(e==e'), return Theorem(e')">simplify</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e)
<a name="l00125"></a>00125 { <span class="keywordflow">return</span> <a class="code" href="group__SE.html#ga3772c6af7eac91b9ed7fc278edf5ef90" title="Access to theory reasoning.">d_core</a>-><a class="code" href="classCVC3_1_1Theory.html#aeda4c57dfbe357a80a348da9ffa71072" title="e1 AND (e1 IFF e2) ==> e2">iffMP</a>(e, <a class="code" href="group__SE.html#ga3772c6af7eac91b9ed7fc278edf5ef90" title="Access to theory reasoning.">d_core</a>-><a class="code" href="classCVC3_1_1TheoryCore.html#a8a66da5ca687474a3a725448a3be8c41" title="Top-level simplifier.">simplify</a>(e.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>())); }
<a name="l00126"></a>00126 <span class="comment"></span>
<a name="l00127"></a>00127 <span class="comment"> //! Notify the search engine about a new literal fact.</span>
<a name="l00128"></a>00128 <span class="comment"></span><span class="comment"> /*! It should be called by SearchEngine::addFact() only.</span>
<a name="l00129"></a>00129 <span class="comment"> * Must be implemented by the subclasses of SearchEngine.</span>
<a name="l00130"></a>00130 <span class="comment"> *</span>
<a name="l00131"></a>00131 <span class="comment"> * IMPORTANT: do not call addFact() from this function; use</span>
<a name="l00132"></a>00132 <span class="comment"> * enqueueFact() or setInconsistent() instead.</span>
<a name="l00133"></a>00133 <span class="comment"> */</span>
<a name="l00134"></a>00134 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="group__SE.html#gaed2d918b4d0eb14d99bf63882fe2df1a" title="Notify the search engine about a new literal fact.">addLiteralFact</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm) = 0;<span class="comment"></span>
<a name="l00135"></a>00135 <span class="comment"> //! Notify the search engine about a new non-literal fact.</span>
<a name="l00136"></a>00136 <span class="comment"></span><span class="comment"> /*! It should be called by SearchEngine::addFact() only.</span>
<a name="l00137"></a>00137 <span class="comment"> * Must be implemented by the subclasses of SearchEngine.</span>
<a name="l00138"></a>00138 <span class="comment"> *</span>
<a name="l00139"></a>00139 <span class="comment"> * IMPORTANT: do not call addFact() from this function; use</span>
<a name="l00140"></a>00140 <span class="comment"> * enqueueFact() or setInconsistent() instead.</span>
<a name="l00141"></a>00141 <span class="comment"> */</span>
<a name="l00142"></a>00142 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="group__SE.html#gae95c78de94900637db19e3b7dee5d7c3" title="Notify the search engine about a new non-literal fact.">addNonLiteralFact</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm) = 0;<span class="comment"></span>
<a name="l00143"></a>00143 <span class="comment"> //! Add a new fact to the search engine bypassing CNF converter</span>
<a name="l00144"></a>00144 <span class="comment"></span><span class="comment"> /*! Calls either addLiteralFact() or addNonLiteralFact()</span>
<a name="l00145"></a>00145 <span class="comment"> * appropriately, and converts to CNF when d_cnfOption is set. If</span>
<a name="l00146"></a>00146 <span class="comment"> * fromCore==true, this fact already comes from the core, and</span>
<a name="l00147"></a>00147 <span class="comment"> * doesn't need to be reported back to the core.</span>
<a name="l00148"></a>00148 <span class="comment"> */</span>
<a name="l00149"></a>00149 <span class="keywordtype">void</span> <a class="code" href="group__SE.html#gadebc5b605b4a358789b697e44065a97e" title="Add a new fact to the search engine bypassing CNF converter.">addCNFFact</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm, <span class="keywordtype">bool</span> fromCore=<span class="keyword">false</span>);
<a name="l00150"></a>00150
<a name="l00151"></a>00151 <span class="keyword">public</span>:
<a name="l00152"></a>00152
<a name="l00153"></a><a class="code" href="group__SE.html#ga12db60dd52e1223d009f6b51b654f70e">00153</a> <span class="keywordtype">int</span> <a class="code" href="group__SE.html#ga12db60dd52e1223d009f6b51b654f70e">getBottomScope</a>() { <span class="keywordflow">return</span> <a class="code" href="group__SE.html#ga640e08e2b051e08f2abdd4111b9a2e71" title="The bottom-most scope for the current call to checkSAT (where conflict clauses are still valid)...">d_bottomScope</a>; }
<a name="l00154"></a>00154 <span class="comment"></span>
<a name="l00155"></a>00155 <span class="comment"> //! Check if e is a clause (a literal, or a disjunction of literals)</span>
<a name="l00156"></a>00156 <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="group__SE.html#ga9babda9b0bcd226dd4d0a736cd433893" title="Check if e is a clause (a literal, or a disjunction of literals)">isClause</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);
<a name="l00157"></a>00157 <span class="comment"></span>
<a name="l00158"></a>00158 <span class="comment"> //! Check if e is a propositional clause</span>
<a name="l00159"></a>00159 <span class="comment"></span><span class="comment"> /*! \sa isPropAtom() */</span>
<a name="l00160"></a>00160 <span class="keywordtype">bool</span> <a class="code" href="group__SE.html#ga9db77121699fbbdbff209014b8ab26c3" title="Check if e is a propositional clause.">isPropClause</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span>
<a name="l00161"></a>00161 <span class="comment"> //! Check whether e is a fresh variable introduced by the CNF converter</span>
<a name="l00162"></a>00162 <span class="comment"></span><span class="comment"> /*! Search engines do not need to split on those variables in order</span>
<a name="l00163"></a>00163 <span class="comment"> * to be complete</span>
<a name="l00164"></a>00164 <span class="comment"> */</span>
<a name="l00165"></a><a class="code" href="group__SE.html#ga92018736294ba073bc5db887467944ad">00165</a> <span class="keywordtype">bool</span> <a class="code" href="group__SE.html#ga92018736294ba073bc5db887467944ad" title="Check whether e is a fresh variable introduced by the CNF converter.">isCNFVar</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) { <span class="keywordflow">return</span> (<a class="code" href="group__SE.html#ga1c64a37d94b4cadedce29f3e4b98a3af" title="Backtracking set of new variables generated by CNF translator.">d_cnfVars</a>.<a class="code" href="classCVC3_1_1CDMap.html#af5f700035db0db798c645e36dd0b31bd">count</a>(e) > 0); }<span class="comment"></span>
<a name="l00166"></a>00166 <span class="comment"> //! Check if a splitter is required for completeness</span>
<a name="l00167"></a>00167 <span class="comment"></span><span class="comment"> /*! Currently, it checks that 'e' is not an auxiliary CNF variable */</span>
<a name="l00168"></a>00168 <span class="keywordtype">bool</span> <a class="code" href="group__SE.html#gaed4079f44a18e496b87366ce65b20d99" title="Check if a splitter is required for completeness.">isGoodSplitter</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);
<a name="l00169"></a>00169
<a name="l00170"></a>00170 <span class="keyword">private</span>:
<a name="l00171"></a>00171 <span class="comment"></span>
<a name="l00172"></a>00172 <span class="comment"> //! Translate theta to CNF and enqueue the new clauses</span>
<a name="l00173"></a>00173 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="group__SE.html#ga4bcd481c70362c589aa7e712a8cc746d" title="Translate theta to CNF and enqueue the new clauses.">enqueueCNF</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& theta);<span class="comment"></span>
<a name="l00174"></a>00174 <span class="comment"> //! Recursive version of enqueueCNF()</span>
<a name="l00175"></a>00175 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="group__SE.html#ga62e31e3c4dbadb6cc5fddc3b0b73e047" title="Recursive version of enqueueCNF()">enqueueCNFrec</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& theta);<span class="comment"></span>
<a name="l00176"></a>00176 <span class="comment"> //! FIXME: write a comment</span>
<a name="l00177"></a>00177 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="group__SE.html#gaa7bf3c385bae481d4ea35179e818a09a" title="FIXME: write a comment.">applyCNFRules</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e);
<a name="l00178"></a>00178 <span class="comment"></span>
<a name="l00179"></a>00179 <span class="comment"> //! Cache a theorem phi <=> v by phi, where v is a literal.</span>
<a name="l00180"></a>00180 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="group__SE.html#gaa78fb38536d0a2e34ad140f3ec865f2b" title="Cache a theorem phi <=> v by phi, where v is a literal.">addToCNFCache</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);
<a name="l00181"></a>00181 <span class="comment"></span>
<a name="l00182"></a>00182 <span class="comment"> //! Find a theorem phi <=> v by phi, where v is a literal.</span>
<a name="l00183"></a>00183 <span class="comment"></span><span class="comment"> /*! \return Null Theorem if not found. */</span>
<a name="l00184"></a>00184 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="group__SE.html#ga298ad740ab490d5b3337445573b8c4d7" title="Find a theorem phi <=> v by phi, where v is a literal.">findInCNFCache</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);
<a name="l00185"></a>00185 <span class="comment"></span>
<a name="l00186"></a>00186 <span class="comment"> //! Replaces ITE subexpressions in e with variables</span>
<a name="l00187"></a>00187 <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="group__SE.html#ga687e32d21d7fe7e4b26873ae86a47ae5" title="Replaces ITE subexpressions in e with variables.">replaceITE</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);
<a name="l00188"></a>00188
<a name="l00189"></a>00189 <span class="keyword">protected</span>:
<a name="l00190"></a>00190 <span class="comment"></span>
<a name="l00191"></a>00191 <span class="comment"> //! Return the current scope level (for convenience)</span>
<a name="l00192"></a><a class="code" href="group__SE.html#gab267d9f29c30c8e26b5c7bcc4d15306a">00192</a> <span class="comment"></span> <span class="keywordtype">int</span> <a class="code" href="group__SE.html#gab267d9f29c30c8e26b5c7bcc4d15306a" title="Return the current scope level (for convenience)">scopeLevel</a>() { <span class="keywordflow">return</span> <a class="code" href="group__SE.html#ga3772c6af7eac91b9ed7fc278edf5ef90" title="Access to theory reasoning.">d_core</a>-><a class="code" href="classCVC3_1_1TheoryCore.html#a9377f423f4fd59fdac396794363733a6">getCM</a>()-><a class="code" href="classCVC3_1_1ContextManager.html#a194f7ddd794eaa876544a45006a3ff6f">scopeLevel</a>(); }
<a name="l00193"></a>00193
<a name="l00194"></a>00194 <span class="keyword">public</span>:<span class="comment"></span>
<a name="l00195"></a>00195 <span class="comment"> //! Constructor</span>
<a name="l00196"></a>00196 <span class="comment"></span> <a class="code" href="group__SE.html#gaa6e44780a3c5e714f4fd5d8ee41bb1fb" title="Constructor.">SearchImplBase</a>(<a class="code" href="classCVC3_1_1TheoryCore.html" title="This theory handles the built-in logical connectives plus equality. It also handles the registration ...">TheoryCore</a>* core);<span class="comment"></span>
<a name="l00197"></a>00197 <span class="comment"> //! Destructor</span>
<a name="l00198"></a>00198 <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="group__SE.html#ga139d4116c2b14d5357f2696dc8f29cac" title="Destructor.">~SearchImplBase</a>();
<a name="l00199"></a>00199
<a name="l00200"></a><a class="code" href="group__SE.html#gac4e5351fec1964bf7571d67e90a1538d">00200</a> <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="group__SE.html#gac4e5351fec1964bf7571d67e90a1538d" title="Register an atomic formula of interest.">registerAtom</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e)
<a name="l00201"></a>00201 { <a class="code" href="group__SE.html#ga3772c6af7eac91b9ed7fc278edf5ef90" title="Access to theory reasoning.">d_core</a>-><a class="code" href="classCVC3_1_1Theory.html#a01fa8047ed1f649dc98831cb536187e4" title="Return the theory associated with a kind.">theoryOf</a>(e)-><a class="code" href="group__Theory__API.html#gafb1431aa8258f6663ad948ebb08e5330">registerAtom</a>(e, <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>()); }
<a name="l00202"></a><a class="code" href="group__SE.html#ga65ca9e33c2ac0807f0ef680415457c45">00202</a> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="group__SE.html#ga65ca9e33c2ac0807f0ef680415457c45" title="Return next literal implied by last assertion. Null Expr if none.">getImpliedLiteral</a>() { <span class="keywordflow">return</span> <a class="code" href="group__SE.html#ga3772c6af7eac91b9ed7fc278edf5ef90" title="Access to theory reasoning.">d_core</a>-><a class="code" href="classCVC3_1_1TheoryCore.html#a464a49882cbd94a3c48428ed60d3a365" title="Return the next implied literal (NULL Theorem if none)">getImpliedLiteral</a>(); }
<a name="l00203"></a><a class="code" href="group__SE.html#gae987ab9ab6129f83efb0b5649cc2003c">00203</a> <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="group__SE.html#gae987ab9ab6129f83efb0b5649cc2003c" title="Push a checkpoint.">push</a>() { <a class="code" href="group__SE.html#ga3772c6af7eac91b9ed7fc278edf5ef90" title="Access to theory reasoning.">d_core</a>-><a class="code" href="classCVC3_1_1TheoryCore.html#a9377f423f4fd59fdac396794363733a6">getCM</a>()-><a class="code" href="classCVC3_1_1ContextManager.html#a90e301927cc935d561b81761d4ab2ee8">push</a>(); }
<a name="l00204"></a><a class="code" href="group__SE.html#ga84ceb5e9dcc4e57c1f48f77f4b2f8db5">00204</a> <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="group__SE.html#ga84ceb5e9dcc4e57c1f48f77f4b2f8db5" title="Restore last checkpoint.">pop</a>() { <a class="code" href="group__SE.html#ga3772c6af7eac91b9ed7fc278edf5ef90" title="Access to theory reasoning.">d_core</a>-><a class="code" href="classCVC3_1_1TheoryCore.html#a9377f423f4fd59fdac396794363733a6">getCM</a>()-><a class="code" href="classCVC3_1_1ContextManager.html#ae74b114a270baff44940a8916d958e9c">pop</a>(); }
<a name="l00205"></a>00205 <span class="comment"></span>
<a name="l00206"></a>00206 <span class="comment"> ///////////////////////////////////////////////////////////////////////////</span>
<a name="l00207"></a>00207 <span class="comment"></span> <span class="comment">// checkValid() is the method that subclasses must implement.</span><span class="comment"></span>
<a name="l00208"></a>00208 <span class="comment"> ///////////////////////////////////////////////////////////////////////////</span>
<a name="l00209"></a>00209 <span class="comment"></span><span class="comment"></span>
<a name="l00210"></a>00210 <span class="comment"> //! Checks the validity of a formula in the current context</span>
<a name="l00211"></a>00211 <span class="comment"></span><span class="comment"> /*! The method that actually calls the SAT solver (implemented in a</span>
<a name="l00212"></a>00212 <span class="comment"> subclass). It should maintain d_assumptions (add all asserted</span>
<a name="l00213"></a>00213 <span class="comment"> splitters to it), and set d_lastValid and d_lastCounterExample</span>
<a name="l00214"></a>00214 <span class="comment"> appropriately before exiting. */</span>
<a name="l00215"></a>00215 <span class="keyword">virtual</span> <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="code" href="group__SE.html#ga1e6282534845cfe93f245d9983d58761" title="Checks the validity of a formula in the current context.">checkValidInternal</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) = 0;<span class="comment"></span>
<a name="l00216"></a>00216 <span class="comment"> //! Similar to checkValidInternal(), only returns Theorem(e) or Null</span>
<a name="l00217"></a>00217 <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="code" href="group__SE.html#ga83d82b8cf43e9dc8240e762b180f6343" title="Similar to checkValidInternal(), only returns Theorem(e) or Null.">checkValid</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& result);<span class="comment"></span>
<a name="l00218"></a>00218 <span class="comment"> //! Reruns last check with e as an additional assumption</span>
<a name="l00219"></a>00219 <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="code" href="group__SE.html#gaf89e6b914a2099b366258953fccb6277" title="Reruns last check with e as an additional assumption.">restartInternal</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) = 0;<span class="comment"></span>
<a name="l00220"></a>00220 <span class="comment"> //! Reruns last check with e as an additional assumption</span>
<a name="l00221"></a>00221 <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="code" href="group__SE.html#gad4a8edbe5a6520fc9f564ec1c65d4729" title="Reruns last check with e as an additional assumption.">restart</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& result);
<a name="l00222"></a><a class="code" href="group__SE.html#ga7d62893d0d19ed50cc1f616a92d536c0">00222</a> <span class="keywordtype">void</span> <a class="code" href="group__SE.html#ga7d62893d0d19ed50cc1f616a92d536c0" title="Returns to context immediately before last call to checkValid.">returnFromCheck</a>()
<a name="l00223"></a>00223 { <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> thm; <a class="code" href="group__SE.html#gad4a8edbe5a6520fc9f564ec1c65d4729" title="Reruns last check with e as an additional assumption.">restart</a>(<a class="code" href="group__SE.html#ga3772c6af7eac91b9ed7fc278edf5ef90" title="Access to theory reasoning.">d_core</a>-><a class="code" href="classCVC3_1_1Theory.html#a0bbf7c5b6079fc99a0f759e5809fe6f5" title="Return FALSE Expr.">falseExpr</a>(), thm); }
<a name="l00224"></a><a class="code" href="group__SE.html#ga95428fe99c7a85e5e90ba6b2dce0e024">00224</a> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="group__SE.html#ga95428fe99c7a85e5e90ba6b2dce0e024" title="Returns the result of the most recent valid theorem.">lastThm</a>() { <span class="keywordflow">return</span> <a class="code" href="group__SE.html#ga88ba664573602ecfca1d6eadc14a30af" title="Theorem from the last successful checkValid call. It is used by getProof and getAssumptions.">d_lastValid</a>; }
<a name="l00225"></a>00225 <span class="comment"></span>
<a name="l00226"></a>00226 <span class="comment"> ///////////////////////////////////////////////////////////////////////////</span>
<a name="l00227"></a>00227 <span class="comment"></span> <span class="comment">// The following methods are provided by the base class, and in most</span>
<a name="l00228"></a>00228 <span class="comment">// cases should be sufficient. However, they are virtual so that</span>
<a name="l00229"></a>00229 <span class="comment">// subclasses can add functionality to them if needed.</span><span class="comment"></span>
<a name="l00230"></a>00230 <span class="comment"> ///////////////////////////////////////////////////////////////////////////</span>
<a name="l00231"></a>00231 <span class="comment"></span><span class="comment"></span>
<a name="l00232"></a>00232 <span class="comment"> /*! @brief Generate and add a new assertion to the set of assertions</span>
<a name="l00233"></a>00233 <span class="comment"> in the current context. This should only be used by class VCL in</span>
<a name="l00234"></a>00234 <span class="comment"> assertFormula(). */</span>
<a name="l00235"></a>00235 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="group__SE.html#gaf46a82b16f76c9e97cfe252d4398eac7" title="Generate and add a new assertion to the set of assertions in the current context. This should only be...">newUserAssumption</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span>
<a name="l00236"></a>00236 <span class="comment"> //! Add a new internal asserion</span>
<a name="l00237"></a>00237 <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="group__SE.html#ga635768498a239f0193de5f1445676f65" title="Add a new internal asserion.">newIntAssumption</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span>
<a name="l00238"></a>00238 <span class="comment"> //! Helper for above function</span>
<a name="l00239"></a>00239 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="group__SE.html#ga635768498a239f0193de5f1445676f65" title="Add a new internal asserion.">newIntAssumption</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);<span class="comment"></span>
<a name="l00240"></a>00240 <span class="comment"> //! Get all assumptions made in this and all previous contexts.</span>
<a name="l00241"></a>00241 <span class="comment"></span><span class="comment"> /*! \param assumptions should be an empty vector which will be filled \</span>
<a name="l00242"></a>00242 <span class="comment"> with the assumptions */</span>
<a name="l00243"></a>00243 <span class="keywordtype">void</span> <a class="code" href="group__SE.html#gab730f3f048637996f532f77af932fe55" title="Get all assumptions made in this and all previous contexts.">getUserAssumptions</a>(std::vector<Expr>& assumptions);
<a name="l00244"></a>00244 <span class="keywordtype">void</span> <a class="code" href="group__SE.html#gae65e0921e9ef2b475242b1a284a413ad" title="Get assumptions made internally in this and all previous contexts.">getInternalAssumptions</a>(std::vector<Expr>& assumptions);
<a name="l00245"></a>00245 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="group__SE.html#gadadf46fa5200744c9f30ca548080d35d" title="Get all assumptions made in this and all previous contexts.">getAssumptions</a>(std::vector<Expr>& assumptions);<span class="comment"></span>
<a name="l00246"></a>00246 <span class="comment"> //! Check if the formula has been assumed</span>
<a name="l00247"></a>00247 <span class="comment"></span> <span class="keyword">virtual</span> <span class="keywordtype">bool</span> <a class="code" href="group__SE.html#ga38ec2c19ebab8525ebc3c6249bf97442" title="Check if the formula has been assumed.">isAssumption</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);
<a name="l00248"></a>00248 <span class="comment"></span>
<a name="l00249"></a>00249 <span class="comment"> //! Add a new fact to the search engine from the core</span>
<a name="l00250"></a>00250 <span class="comment"></span><span class="comment"> /*! It should be called by TheoryCore::assertFactCore(). */</span>
<a name="l00251"></a>00251 <span class="keywordtype">void</span> <a class="code" href="group__SE.html#gac6e807418fb26dee354f7f934eb432ba" title="Add a new fact to the search engine from the core.">addFact</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);
<a name="l00252"></a>00252 <span class="comment"></span>
<a name="l00253"></a>00253 <span class="comment"> //! Suggest a splitter to the SearchEngine</span>
<a name="l00254"></a>00254 <span class="comment"></span><span class="comment"> /*! The higher is the priority, the sooner the SAT solver will split</span>
<a name="l00255"></a>00255 <span class="comment"> * on it. It can be positive or negative (default is 0).</span>
<a name="l00256"></a>00256 <span class="comment"> *</span>
<a name="l00257"></a>00257 <span class="comment"> * The set of suggested splitters is backtracking; that is, a</span>
<a name="l00258"></a>00258 <span class="comment"> * splitter is "forgotten" once the scope is backtracked.</span>
<a name="l00259"></a>00259 <span class="comment"> *</span>
<a name="l00260"></a>00260 <span class="comment"> * This method can be used either to change the priority</span>
<a name="l00261"></a>00261 <span class="comment"> * of existing splitters, or to introduce new splitters that DPs</span>
<a name="l00262"></a>00262 <span class="comment"> * consider relevant, even though they do not appear in existing</span>
<a name="l00263"></a>00263 <span class="comment"> * formulas.</span>
<a name="l00264"></a>00264 <span class="comment"> */</span>
<a name="l00265"></a>00265 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="group__SE.html#ga6c1448b58fb299bc084aa9c522faf36d" title="Suggest a splitter to the SearchEngine.">addSplitter</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <span class="keywordtype">int</span> priority);
<a name="l00266"></a>00266
<a name="l00267"></a>00267 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="group__SE.html#gacf93ae1a488573c6d34dee7721007351" title="Will return the set of assertions which make the queried formula false.">getCounterExample</a>(std::vector<Expr>& assertions, <span class="keywordtype">bool</span> inOrder = <span class="keyword">true</span>);
<a name="l00268"></a>00268
<a name="l00269"></a>00269 <span class="comment">// The following two methods should be called only after a checkValid</span>
<a name="l00270"></a>00270 <span class="comment">// which returns true. In any other case, they return Null values.</span>
<a name="l00271"></a>00271 <span class="comment"></span>
<a name="l00272"></a>00272 <span class="comment"> //! Returns the proof term for the last proven query</span>
<a name="l00273"></a>00273 <span class="comment"></span><span class="comment"> /*! It should be called only after a checkValid which returns true.</span>
<a name="l00274"></a>00274 <span class="comment"> In any other case, it returns Null. */</span>
<a name="l00275"></a>00275 <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Proof.html">Proof</a> <a class="code" href="group__SE.html#gaf90e8ae5cd67dc6c43787a9d3ebdca53" title="Returns the proof term for the last proven query.">getProof</a>();<span class="comment"></span>
<a name="l00276"></a>00276 <span class="comment"> /*! @brief Returns the set of assumptions used in the proof. It</span>
<a name="l00277"></a>00277 <span class="comment"> should be a subset of getAssumptions(). */</span><span class="comment"></span>
<a name="l00278"></a>00278 <span class="comment"> /*! It should be called only after a checkValid which returns true.</span>
<a name="l00279"></a>00279 <span class="comment"> In any other case, it returns Null. */</span>
<a name="l00280"></a>00280 <span class="keyword">virtual</span> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a>& <a class="code" href="group__SE.html#ga24dc510f27c40d8044f461308bcdb62d" title="Returns the set of assumptions used in the proof. It should be a subset of getAssumptions().">getAssumptionsUsed</a>();
<a name="l00281"></a>00281 <span class="comment"></span>
<a name="l00282"></a>00282 <span class="comment"> //! Process result of checkValid</span>
<a name="l00283"></a>00283 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="group__SE.html#ga0d509e38a03048dcbdb9e28f3f5da724" title="Process result of checkValid.">processResult</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& res, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);
<a name="l00284"></a>00284
<a name="l00285"></a>00285 <span class="comment">//:ALEX:</span>
<a name="l00286"></a><a class="code" href="group__SE.html#gadf867c70d67d05d72a11895a2cc13971">00286</a> <span class="keyword">inline</span> <span class="keyword">virtual</span> <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bf">FormulaValue</a> <a class="code" href="group__SE.html#gadf867c70d67d05d72a11895a2cc13971">getValue</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">CVC3::Expr</a>& e) {
<a name="l00287"></a>00287 <a class="code" href="debug_8h.html#a2637b2fffa22e3c9fad40cda8fcc3bce" title="If something goes horribly wrong, print a message and abort immediately with exit(1).">FatalAssert</a>(<span class="keyword">false</span>, <span class="stringliteral">"not implemented"</span>);
<a name="l00288"></a>00288 <span class="keywordflow">return</span> <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfadb6455bbcb14daca672dfcc52df342d7">UNKNOWN_VAL</a>;
<a name="l00289"></a>00289 }
<a name="l00290"></a>00290
<a name="l00291"></a>00291 <span class="comment">/* @} */</span> <span class="comment">// end of group SE</span>
<a name="l00292"></a>00292
<a name="l00293"></a>00293 };
<a name="l00294"></a>00294
<a name="l00295"></a>00295
<a name="l00296"></a>00296 }
<a name="l00297"></a>00297
<a name="l00298"></a>00298 <span class="preprocessor">#endif</span>
</pre></div></div>
</div>
<hr class="footer"/><address class="footer"><small>Generated on Wed Sep 7 2011 for CVC3 by 
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>
