<!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.cpp 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.cpp</div> </div>
</div>
<div class="contents">
<a href="search__impl__base_8cpp.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.cpp</span>
<a name="l00004"></a>00004 <span class="comment"> * </span>
<a name="l00005"></a>00005 <span class="comment"> * Author: Clark Barrett, Vijay Ganesh (CNF Converter)</span>
<a name="l00006"></a>00006 <span class="comment"> * </span>
<a name="l00007"></a>00007 <span class="comment"> * Created: Fri Jan 17 14:19:54 2003</span>
<a name="l00008"></a>00008 <span class="comment"> *</span>
<a name="l00009"></a>00009 <span class="comment"> * <hr></span>
<a name="l00010"></a>00010 <span class="comment"> *</span>
<a name="l00011"></a>00011 <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span>
<a name="l00012"></a>00012 <span class="comment"> * and its documentation for any purpose is hereby granted without</span>
<a name="l00013"></a>00013 <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span>
<a name="l00014"></a>00014 <span class="comment"> * LICENSE file provided with this distribution.</span>
<a name="l00015"></a>00015 <span class="comment"> * </span>
<a name="l00016"></a>00016 <span class="comment"> * <hr></span>
<a name="l00017"></a>00017 <span class="comment"> * </span>
<a name="l00018"></a>00018 <span class="comment"> */</span>
<a name="l00019"></a>00019 <span class="comment">/*****************************************************************************/</span>
<a name="l00020"></a>00020
<a name="l00021"></a>00021
<a name="l00022"></a>00022 <span class="preprocessor">#include "<a class="code" href="search__impl__base_8h.html" title="Abstract API to the proof search engine.">search_impl_base.h</a>"</span>
<a name="l00023"></a>00023 <span class="preprocessor">#include "<a class="code" href="theory_8h.html" title="Generic API for Theories plus methods commonly used by theories.">theory.h</a>"</span>
<a name="l00024"></a>00024 <span class="preprocessor">#include "<a class="code" href="eval__exception_8h.html">eval_exception.h</a>"</span>
<a name="l00025"></a>00025 <span class="preprocessor">#include "<a class="code" href="search__rules_8h.html" title="Abstract proof rules interface to the simple search engine.">search_rules.h</a>"</span>
<a name="l00026"></a>00026 <span class="preprocessor">#include "<a class="code" href="variable_8h.html">variable.h</a>"</span>
<a name="l00027"></a>00027 <span class="preprocessor">#include "<a class="code" href="command__line__flags_8h.html">command_line_flags.h</a>"</span>
<a name="l00028"></a>00028 <span class="preprocessor">#include "<a class="code" href="statistics_8h.html" title="Description: Counters and flags for collecting run-time statistics.">statistics.h</a>"</span>
<a name="l00029"></a>00029 <span class="preprocessor">#include "<a class="code" href="theorem__manager_8h.html">theorem_manager.h</a>"</span>
<a name="l00030"></a>00030 <span class="preprocessor">#include "<a class="code" href="expr__transform_8h.html" title="Generally Useful Expression Transformations.">expr_transform.h</a>"</span>
<a name="l00031"></a>00031 <span class="preprocessor">#include "<a class="code" href="assumptions_8h.html">assumptions.h</a>"</span>
<a name="l00032"></a>00032
<a name="l00033"></a>00033
<a name="l00034"></a>00034 <span class="keyword">using namespace </span>std;
<a name="l00035"></a>00035
<a name="l00036"></a>00036
<a name="l00037"></a>00037 <span class="keyword">namespace </span>CVC3 {
<a name="l00038"></a>00038
<a name="l00039"></a>00039
<a name="l00040"></a><a class="code" href="classCVC3_1_1CoreSatAPI__implBase.html">00040</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1CoreSatAPI__implBase.html">CoreSatAPI_implBase</a> :<span class="keyword">public</span> <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>::CoreSatAPI {
<a name="l00041"></a><a class="code" href="classCVC3_1_1CoreSatAPI__implBase.html#a5e73a31f4fe51b66e5a7fd0f799ed6c0">00041</a> <a class="code" href="classCVC3_1_1SearchImplBase.html" title="API to to a generic proof search engine (a.k.a. SAT solver)">SearchImplBase</a>* <a class="code" href="classCVC3_1_1CoreSatAPI__implBase.html#a5e73a31f4fe51b66e5a7fd0f799ed6c0">d_se</a>;
<a name="l00042"></a>00042 <span class="keyword">public</span>:
<a name="l00043"></a><a class="code" href="classCVC3_1_1CoreSatAPI__implBase.html#a23f5c8b714a78e79204017d6565cf265">00043</a> <a class="code" href="classCVC3_1_1CoreSatAPI__implBase.html#a23f5c8b714a78e79204017d6565cf265">CoreSatAPI_implBase</a>(<a class="code" href="classCVC3_1_1SearchImplBase.html" title="API to to a generic proof search engine (a.k.a. SAT solver)">SearchImplBase</a>* se) : d_se(se) {}
<a name="l00044"></a><a class="code" href="classCVC3_1_1CoreSatAPI__implBase.html#ae93e65ef87f385accf77189dfe21a740">00044</a> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1CoreSatAPI__implBase.html#ae93e65ef87f385accf77189dfe21a740">~CoreSatAPI_implBase</a>() {}
<a name="l00045"></a><a class="code" href="classCVC3_1_1CoreSatAPI__implBase.html#a0f161d12f8d1c2c6920e747cc6551be0">00045</a> <span class="keyword">virtual</span> <span class="keywordtype">void</span> addLemma(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm, <span class="keywordtype">int</span> priority, <span class="keywordtype">bool</span> atBottomScope)
<a name="l00046"></a>00046 { d_se->addFact(thm); }
<a name="l00047"></a><a class="code" href="classCVC3_1_1CoreSatAPI__implBase.html#a5447590e73ee5be03de304fb0925bf58">00047</a> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> addAssumption(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& assump)
<a name="l00048"></a>00048 { <span class="keywordflow">return</span> d_se->newIntAssumption(assump); }
<a name="l00049"></a><a class="code" href="classCVC3_1_1CoreSatAPI__implBase.html#aa2bdec86d7df97040c41f32b6354b89a">00049</a> <span class="keyword">virtual</span> <span class="keywordtype">void</span> addSplitter(<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="l00050"></a>00050 { d_se->addSplitter(e, priority); }
<a name="l00051"></a>00051 <span class="keyword">virtual</span> <span class="keywordtype">bool</span> check(<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="l00052"></a>00052 };
<a name="l00053"></a>00053
<a name="l00054"></a><a class="code" href="classCVC3_1_1CoreSatAPI__implBase.html#a81efe1d5fd1132b8a4bbea200a51ff48">00054</a> <span class="keywordtype">bool</span> CoreSatAPI_implBase::check(<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="l00055"></a>00055 {
<a name="l00056"></a>00056 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> thm;
<a name="l00057"></a>00057 <span class="keywordtype">int</span> scope = d_se->theoryCore()->getCM()->scopeLevel();
<a name="l00058"></a>00058 d_se->theoryCore()->getCM()->push();
<a name="l00059"></a>00059 <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> res = d_se->checkValid(e, thm);
<a name="l00060"></a>00060 d_se->theoryCore()->getCM()->popto(scope);
<a name="l00061"></a>00061 <span class="keywordflow">return</span> res == <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498ba24f8f4860dbe6fd65883a9d7cbd2f576">VALID</a>;
<a name="l00062"></a>00062 }
<a name="l00063"></a>00063
<a name="l00064"></a>00064
<a name="l00065"></a>00065
<a name="l00066"></a>00066 }
<a name="l00067"></a>00067
<a name="l00068"></a>00068
<a name="l00069"></a>00069 <span class="keyword">using namespace </span>CVC3;
<a name="l00070"></a>00070
<a name="l00071"></a>00071
<a name="l00072"></a>00072 <span class="comment">// class SearchImplBase::Splitter methods</span>
<a name="l00073"></a>00073
<a name="l00074"></a>00074 <span class="comment">// Constructor</span>
<a name="l00075"></a><a class="code" href="classCVC3_1_1SearchImplBase_1_1Splitter.html#a59ee8b0fa0185678e86266e6159bf69a">00075</a> SearchImplBase::Splitter::Splitter(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Literal.html">Literal</a>& lit): d_lit(lit) {
<a name="l00076"></a>00076 <a class="code" href="classCVC3_1_1SearchImplBase_1_1Splitter.html#a5a12e90f92f58ac61e1525f8a8099def">d_lit</a>.<a class="code" href="classCVC3_1_1Literal.html#a4823b2e9ec3a6a13a28c209d22269564">count</a>()++;
<a name="l00077"></a>00077 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"Splitter"</span>, <span class="stringliteral">"Splitter("</span>, <a class="code" href="classCVC3_1_1SearchImplBase_1_1Splitter.html#a5a12e90f92f58ac61e1525f8a8099def">d_lit</a>, <span class="stringliteral">")"</span>);
<a name="l00078"></a>00078 }
<a name="l00079"></a>00079
<a name="l00080"></a>00080 <span class="comment">// Copy constructor</span>
<a name="l00081"></a><a class="code" href="classCVC3_1_1SearchImplBase_1_1Splitter.html#a19fc6bdd8f6563e416be12945c7bdd23">00081</a> <a class="code" href="classCVC3_1_1SearchImplBase_1_1Splitter.html#a59ee8b0fa0185678e86266e6159bf69a" title="Constructor.">SearchImplBase::Splitter::Splitter</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1SearchImplBase_1_1Splitter.html" title="Representation of a DP-suggested splitter.">SearchImplBase::Splitter</a>& s)
<a name="l00082"></a>00082 : d_lit(s.d_lit) {
<a name="l00083"></a>00083 <a class="code" href="classCVC3_1_1SearchImplBase_1_1Splitter.html#a5a12e90f92f58ac61e1525f8a8099def">d_lit</a>.<a class="code" href="classCVC3_1_1Literal.html#a4823b2e9ec3a6a13a28c209d22269564">count</a>()++;
<a name="l00084"></a>00084 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"Splitter"</span>, <span class="stringliteral">"Splitter[copy]("</span>, <a class="code" href="classCVC3_1_1SearchImplBase_1_1Splitter.html#a5a12e90f92f58ac61e1525f8a8099def">d_lit</a>, <span class="stringliteral">")"</span>);
<a name="l00085"></a>00085 }
<a name="l00086"></a>00086
<a name="l00087"></a>00087 <span class="comment">// Assignment</span>
<a name="l00088"></a>00088 <a class="code" href="classCVC3_1_1SearchImplBase_1_1Splitter.html" title="Representation of a DP-suggested splitter.">SearchImplBase::Splitter</a>&
<a name="l00089"></a><a class="code" href="classCVC3_1_1SearchImplBase_1_1Splitter.html#a5ba159e6e31410ed42bb5edfe2d7020b">00089</a> <a class="code" href="classCVC3_1_1SearchImplBase_1_1Splitter.html#a5ba159e6e31410ed42bb5edfe2d7020b" title="Assignment.">SearchImplBase::Splitter::operator=</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1SearchImplBase_1_1Splitter.html" title="Representation of a DP-suggested splitter.">SearchImplBase::Splitter</a>& s) {
<a name="l00090"></a>00090 <span class="keywordflow">if</span>(<span class="keyword">this</span> == &s) <span class="keywordflow">return</span> *<span class="keyword">this</span>; <span class="comment">// Self-assignment</span>
<a name="l00091"></a>00091 d_lit.count()--;
<a name="l00092"></a>00092 d_lit = s.<a class="code" href="classCVC3_1_1SearchImplBase_1_1Splitter.html#a5a12e90f92f58ac61e1525f8a8099def">d_lit</a>;
<a name="l00093"></a>00093 d_lit.<a class="code" href="classCVC3_1_1Literal.html#a4823b2e9ec3a6a13a28c209d22269564">count</a>()++;
<a name="l00094"></a>00094 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"Splitter"</span>, <span class="stringliteral">"Splitter[assign]("</span>, d_lit, <span class="stringliteral">")"</span>);
<a name="l00095"></a>00095 <span class="keywordflow">return</span> *<span class="keyword">this</span>;
<a name="l00096"></a>00096 }
<a name="l00097"></a>00097
<a name="l00098"></a>00098 <span class="comment">// Destructor</span>
<a name="l00099"></a><a class="code" href="classCVC3_1_1SearchImplBase_1_1Splitter.html#a41e072e9644325ae849a1602c31d9d36">00099</a> <a class="code" href="classCVC3_1_1SearchImplBase_1_1Splitter.html#a41e072e9644325ae849a1602c31d9d36" title="Descructor.">SearchImplBase::Splitter::~Splitter</a>() {
<a name="l00100"></a>00100 d_lit.count()--;
<a name="l00101"></a>00101 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"Splitter"</span>, <span class="stringliteral">"~Splitter("</span>, d_lit, <span class="stringliteral">")"</span>);
<a name="l00102"></a>00102 }
<a name="l00103"></a>00103
<a name="l00104"></a>00104
<a name="l00105"></a>00105 <span class="comment"></span>
<a name="l00106"></a>00106 <span class="comment">//! Constructor</span>
<a name="l00107"></a><a class="code" href="group__SE.html#gaa6e44780a3c5e714f4fd5d8ee41bb1fb">00107</a> <span class="comment"></span><a class="code" href="group__SE.html#gaa6e44780a3c5e714f4fd5d8ee41bb1fb" title="Constructor.">SearchImplBase::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)
<a name="l00108"></a>00108 : <a class="code" href="classCVC3_1_1SearchEngine.html" title="API to to a generic proof search engine.">SearchEngine</a>(core),
<a name="l00109"></a>00109 <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>(core->getCM()->getCurrentContext()),
<a name="l00110"></a>00110 <a class="code" href="group__SE.html#ga8ea9b2ab9f50d3ddf595595b1f3d7974" title="Backtracking ordered set of DP-suggested splitters.">d_dpSplitters</a>(core->getCM()->getCurrentContext()),
<a name="l00111"></a>00111 <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 class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>->trueTheorem()),
<a name="l00112"></a>00112 <a class="code" href="group__SE.html#ga83dfe2d2d85bacf5e4aa10c0320a140b" title="Maintain the list of current assumptions (user asserts and splitters) for getAssumptions().">d_assumptions</a>(core->getCM()->getCurrentContext()),
<a name="l00113"></a>00113 <a class="code" href="group__SE.html#gab60a7d204ed01875c98629e874575cd6" title="Backtracking cache for the CNF generator.">d_cnfCache</a>(core->getCM()->getCurrentContext()),
<a name="l00114"></a>00114 <a class="code" href="group__SE.html#ga1c64a37d94b4cadedce29f3e4b98a3af" title="Backtracking set of new variables generated by CNF translator.">d_cnfVars</a>(core->getCM()->getCurrentContext()),
<a name="l00115"></a>00115 <a class="code" href="group__SE.html#gae3b8b3cfd965e7d5138320d26808767a" title="Command line flag whether to convert to CNF.">d_cnfOption</a>(&(core->getFlags()[<span class="stringliteral">"cnf"</span>].getBool())),
<a name="l00116"></a>00116 <a class="code" href="group__SE.html#gaa28d7e60bbe1df69ffb304f939b984b7" title="Flag: whether to convert term ITEs into CNF.">d_ifLiftOption</a>(&(core->getFlags()[<span class="stringliteral">"iflift"</span>].getBool())),
<a name="l00117"></a>00117 <a class="code" href="group__SE.html#gafc2c782e4f24b55c8af7cb0189d281d8" title="Flag: ignore auxiliary CNF variables when searching for a splitter.">d_ignoreCnfVarsOption</a>(&(core->getFlags()[<span class="stringliteral">"ignore-cnf-vars"</span>].getBool())),
<a name="l00118"></a>00118 <a class="code" href="group__SE.html#ga2287fd23d4250cc74db446983b2c3274" title="Flag: Preserve the original formula with +cnf (for splitter heuristics)">d_origFormulaOption</a>(&(core->getFlags()[<span class="stringliteral">"orig-formula"</span>].getBool())),
<a name="l00119"></a>00119 <a class="code" href="group__SE.html#ga9dc16eb11f046d9a615aff3018957c6d" title="Cache for enqueueCNF()">d_enqueueCNFCache</a>(core->getCM()->getCurrentContext()),
<a name="l00120"></a>00120 <a class="code" href="group__SE.html#ga401319b3ede7162504e979aaf2119deb" title="Cache for applyCNFRules()">d_applyCNFRulesCache</a>(core->getCM()->getCurrentContext()),
<a name="l00121"></a>00121 <a class="code" href="group__SE.html#ga0c829909b9e3ab2b59ba40e681905c4b" title="Cache for replaceITE()">d_replaceITECache</a>(core->getCM()->getCurrentContext())
<a name="l00122"></a>00122 {
<a name="l00123"></a>00123 <a class="code" href="group__SE.html#ga626a0fe24f363d007d729e16d13349e5" title="Variable manager for classes Variable and Literal.">d_vm</a> = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1VariableManager.html">VariableManager</a>(core-><a class="code" href="classCVC3_1_1TheoryCore.html#a9377f423f4fd59fdac396794363733a6">getCM</a>(), <a class="code" href="group__SE.html#ga879b68112123e2b4ae7175d85a03bfec" title="Proof rules for the search engine.">d_rules</a>,
<a name="l00124"></a>00124 core-><a class="code" href="classCVC3_1_1TheoryCore.html#a46b2792a5c24f95ccfc3fbfc0456b09f">getFlags</a>()[<span class="stringliteral">"mm"</span>].getString());
<a name="l00125"></a>00125 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</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>.setName(<span class="stringliteral">"CDList[SearchImplBase::d_assumptions]"</span>);)
<a name="l00126"></a>00126 <a class="code" href="group__SE.html#ga02f72989536076eab8c55e452a6662d9">d_coreSatAPI_implBase</a> = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1CoreSatAPI__implBase.html">CoreSatAPI_implBase</a>(<span class="keyword">this</span>);
<a name="l00127"></a>00127 core-><a class="code" href="classCVC3_1_1TheoryCore.html#afb6629080bceb44023f1bb3a44f9136f" title="Register a SatAPI for TheoryCore.">registerCoreSatAPI</a>(<a class="code" href="group__SE.html#ga02f72989536076eab8c55e452a6662d9">d_coreSatAPI_implBase</a>);
<a name="l00128"></a>00128 }
<a name="l00129"></a>00129
<a name="l00130"></a>00130 <span class="comment"></span>
<a name="l00131"></a>00131 <span class="comment">//! Destructor</span>
<a name="l00132"></a><a class="code" href="group__SE.html#ga139d4116c2b14d5357f2696dc8f29cac">00132</a> <span class="comment"></span><a class="code" href="group__SE.html#ga139d4116c2b14d5357f2696dc8f29cac" title="Destructor.">SearchImplBase::~SearchImplBase</a>()
<a name="l00133"></a>00133 {
<a name="l00134"></a>00134 <span class="keyword">delete</span> <a class="code" href="group__SE.html#ga02f72989536076eab8c55e452a6662d9">d_coreSatAPI_implBase</a>;
<a name="l00135"></a>00135 <span class="keyword">delete</span> <a class="code" href="group__SE.html#ga626a0fe24f363d007d729e16d13349e5" title="Variable manager for classes Variable and Literal.">d_vm</a>;
<a name="l00136"></a>00136 }
<a name="l00137"></a>00137
<a name="l00138"></a>00138
<a name="l00139"></a>00139 <span class="comment">// Returns a new theorem if e has not already been asserted, otherwise returns</span>
<a name="l00140"></a>00140 <span class="comment">// a NULL theorem.</span>
<a name="l00141"></a><a class="code" href="group__SE.html#gaf46a82b16f76c9e97cfe252d4398eac7">00141</a> <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...">SearchImplBase::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) {
<a name="l00142"></a>00142 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> thm;
<a name="l00143"></a>00143 <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr,Theorem>::iterator</a> i(<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 class="code" href="classCVC3_1_1CDMap.html#a1cadecbd2d6fa614a2f2e9419aa43f33">find</a>(e));
<a name="l00144"></a>00144 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(<span class="keywordflow">if</span>(debugger.trace(<span class="stringliteral">"search verbose"</span>)) {
<a name="l00145"></a>00145 ostream& os(debugger.getOS());
<a name="l00146"></a>00146 os << <span class="stringliteral">"d_assumptions = ["</span>;
<a name="l00147"></a>00147 <span class="keywordflow">for</span>(<a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr,Theorem>::iterator</a> i=<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 class="code" href="classCVC3_1_1CDMap.html#a5d57eb1210dab2fadcd85a2f01e6d6d1">begin</a>(),
<a name="l00148"></a>00148 iend=<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 class="code" href="classCVC3_1_1CDMap.html#a2a26c7cc4db12cb17d273db5cfa5a890">end</a>(); i!=iend; ++i) {
<a name="l00149"></a>00149 debugger.getOS() << <span class="stringliteral">"("</span> << (*i).first << <span class="stringliteral">" => "</span> << (*i).second << <span class="stringliteral">"), "</span>;
<a name="l00150"></a>00150 }
<a name="l00151"></a>00151 os << <span class="stringliteral">"]"</span> << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00152"></a>00152 })
<a name="l00153"></a>00153 <span class="keywordflow">if</span>(i!=<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 class="code" href="classCVC3_1_1CDMap.html#a2a26c7cc4db12cb17d273db5cfa5a890">end</a>()) {
<a name="l00154"></a>00154 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"search verbose"</span>, <span class="stringliteral">"newUserAssumption("</span>, e,
<a name="l00155"></a>00155 <span class="stringliteral">"): assumption already exists"</span>);
<a name="l00156"></a>00156 } <span class="keywordflow">else</span> {
<a name="l00157"></a>00157 thm = <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#ab4527c48e9f88d94d7ca076757a6f3ba">assumpRule</a>(e);
<a name="l00158"></a>00158 <a class="code" href="group__SE.html#ga83dfe2d2d85bacf5e4aa10c0320a140b" title="Maintain the list of current assumptions (user asserts and splitters) for getAssumptions().">d_assumptions</a>[e] = thm;
<a name="l00159"></a>00159 e.<a class="code" href="group__ExprPkg.html#ga63eb3b8c124654cf056b2814794c4236">setUserAssumption</a>();
<a name="l00160"></a>00160 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"search verbose"</span>, <span class="stringliteral">"newUserAssumption("</span>, thm,
<a name="l00161"></a>00161 <span class="stringliteral">"): created new assumption"</span>);
<a name="l00162"></a>00162 }
<a name="l00163"></a>00163 <span class="keywordflow">if</span> (!thm.<a class="code" href="classCVC3_1_1Theorem.html#afc6fdb0507eb3669e28d9be5ed0bd333">isNull</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#aecef2465eb761f7f112ddce77f93d081" title="Add a new assertion to the core from the user or a SAT solver. Do NOT use it in a decision procedure;...">addFact</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#acc963fd43994f06d3647394b731e835c">getExprTrans</a>()-><a class="code" href="classCVC3_1_1ExprTransform.html#a39652560061ab1172040113d9dfa25f6">preprocess</a>(thm));
<a name="l00164"></a>00164 <span class="keywordflow">return</span> thm;
<a name="l00165"></a>00165 }
<a name="l00166"></a>00166
<a name="l00167"></a>00167
<a name="l00168"></a>00168 <span class="comment">// Same as newUserAssertion, except it's an error to assert something that's</span>
<a name="l00169"></a>00169 <span class="comment">// already been asserted.</span>
<a name="l00170"></a><a class="code" href="group__SE.html#ga635768498a239f0193de5f1445676f65">00170</a> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="group__SE.html#ga635768498a239f0193de5f1445676f65" title="Add a new internal asserion.">SearchImplBase::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) {
<a name="l00171"></a>00171 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> thm = <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#ab4527c48e9f88d94d7ca076757a6f3ba">assumpRule</a>(e);
<a name="l00172"></a>00172 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> atom = e.<a class="code" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a>() ? e[0] : e;
<a name="l00173"></a>00173 thm.<a class="code" href="classCVC3_1_1Theorem.html#ab3309c937f827595d1d92fa48cb5a471" title="Set the quantification level for this theorem.">setQuantLevel</a>(<a class="code" href="group__SE.html#ga895a3150e972fb79a7a3ab26100dd31e" title="Accessor for TheoryCore.">theoryCore</a>()->getQuantLevelForTerm(atom));
<a name="l00174"></a>00174 <a class="code" href="group__SE.html#ga635768498a239f0193de5f1445676f65" title="Add a new internal asserion.">newIntAssumption</a>(thm);
<a name="l00175"></a>00175 <span class="keywordflow">return</span> thm;
<a name="l00176"></a>00176 }
<a name="l00177"></a>00177
<a name="l00178"></a>00178
<a name="l00179"></a><a class="code" href="group__SE.html#gab6852f32844435f73f86665c40d2fda8">00179</a> <span class="keywordtype">void</span> <a class="code" href="group__SE.html#ga635768498a239f0193de5f1445676f65" title="Add a new internal asserion.">SearchImplBase::newIntAssumption</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm) {
<a name="l00180"></a>00180 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</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 class="code" href="classCVC3_1_1CDMap.html#af5f700035db0db798c645e36dd0b31bd">count</a>(thm.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>()),
<a name="l00181"></a>00181 <span class="stringliteral">"newIntAssumption: repeated assertion: "</span>+thm.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>().<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00182"></a>00182 <a class="code" href="group__SE.html#ga83dfe2d2d85bacf5e4aa10c0320a140b" title="Maintain the list of current assumptions (user asserts and splitters) for getAssumptions().">d_assumptions</a>[thm.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>()] = thm;
<a name="l00183"></a>00183 thm.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>().<a class="code" href="group__ExprPkg.html#ga8b1ac81529d2ebee895a385a35460d39">setIntAssumption</a>();
<a name="l00184"></a>00184 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"search verbose"</span>, <span class="stringliteral">"newIntAssumption("</span>, thm,
<a name="l00185"></a>00185 <span class="stringliteral">"): new assumption"</span>);
<a name="l00186"></a>00186 }
<a name="l00187"></a>00187
<a name="l00188"></a>00188
<a name="l00189"></a><a class="code" href="group__SE.html#gab730f3f048637996f532f77af932fe55">00189</a> <span class="keywordtype">void</span> <a class="code" href="group__SE.html#gab730f3f048637996f532f77af932fe55" title="Get all assumptions made in this and all previous contexts.">SearchImplBase::getUserAssumptions</a>(vector<Expr>& assumptions)
<a name="l00190"></a>00190 {
<a name="l00191"></a>00191 <span class="keywordflow">for</span>(<a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr,Theorem>::orderedIterator</a> i=<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 class="code" href="classCVC3_1_1CDMap.html#a691443b59a497f6223eae64a2801f5d4">orderedBegin</a>(),
<a name="l00192"></a>00192 iend=<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 class="code" href="classCVC3_1_1CDMap.html#aac337d308e248fd61acf392c7151c9e3">orderedEnd</a>(); i!=iend; ++i)
<a name="l00193"></a>00193 <span class="keywordflow">if</span> ((*i).first.isUserAssumption()) assumptions.push_back((*i).first);
<a name="l00194"></a>00194 }
<a name="l00195"></a>00195
<a name="l00196"></a>00196
<a name="l00197"></a><a class="code" href="group__SE.html#gae65e0921e9ef2b475242b1a284a413ad">00197</a> <span class="keywordtype">void</span> <a class="code" href="group__SE.html#gae65e0921e9ef2b475242b1a284a413ad" title="Get assumptions made internally in this and all previous contexts.">SearchImplBase::getInternalAssumptions</a>(std::vector<Expr>& assumptions)
<a name="l00198"></a>00198 {
<a name="l00199"></a>00199 <span class="keywordflow">for</span>(<a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr,Theorem>::orderedIterator</a> i=<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 class="code" href="classCVC3_1_1CDMap.html#a691443b59a497f6223eae64a2801f5d4">orderedBegin</a>(),
<a name="l00200"></a>00200 iend=<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 class="code" href="classCVC3_1_1CDMap.html#aac337d308e248fd61acf392c7151c9e3">orderedEnd</a>(); i!=iend; ++i)
<a name="l00201"></a>00201 <span class="keywordflow">if</span> ((*i).first.isIntAssumption()) assumptions.push_back((*i).first);
<a name="l00202"></a>00202 }
<a name="l00203"></a>00203
<a name="l00204"></a>00204
<a name="l00205"></a><a class="code" href="group__SE.html#gadadf46fa5200744c9f30ca548080d35d">00205</a> <span class="keywordtype">void</span> <a class="code" href="group__SE.html#gadadf46fa5200744c9f30ca548080d35d" title="Get all assumptions made in this and all previous contexts.">SearchImplBase::getAssumptions</a>(std::vector<Expr>& assumptions)
<a name="l00206"></a>00206 {
<a name="l00207"></a>00207 <span class="keywordflow">for</span>(<a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr,Theorem>::orderedIterator</a> i=<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 class="code" href="classCVC3_1_1CDMap.html#a691443b59a497f6223eae64a2801f5d4">orderedBegin</a>(),
<a name="l00208"></a>00208 iend=<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 class="code" href="classCVC3_1_1CDMap.html#aac337d308e248fd61acf392c7151c9e3">orderedEnd</a>(); i!=iend; ++i)
<a name="l00209"></a>00209 assumptions.push_back((*i).first);
<a name="l00210"></a>00210 }
<a name="l00211"></a>00211
<a name="l00212"></a>00212
<a name="l00213"></a><a class="code" href="group__SE.html#ga38ec2c19ebab8525ebc3c6249bf97442">00213</a> <span class="keywordtype">bool</span> <a class="code" href="group__SE.html#ga38ec2c19ebab8525ebc3c6249bf97442" title="Check if the formula has been assumed.">SearchImplBase::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="l00214"></a>00214 <span class="keywordflow">return</span> <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 class="code" href="classCVC3_1_1CDMap.html#af5f700035db0db798c645e36dd0b31bd">count</a>(e) > 0;
<a name="l00215"></a>00215 }
<a name="l00216"></a>00216
<a name="l00217"></a>00217
<a name="l00218"></a><a class="code" href="group__SE.html#gadebc5b605b4a358789b697e44065a97e">00218</a> <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.">SearchImplBase::addCNFFact</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm, <span class="keywordtype">bool</span> fromCore) {
<a name="l00219"></a>00219 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"addCNFFact"</span>, <span class="stringliteral">"addCNFFact("</span>, thm.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>(), <span class="stringliteral">") {"</span>);
<a name="l00220"></a>00220 <span class="keywordflow">if</span>(thm.<a class="code" href="classCVC3_1_1Theorem.html#aed1590a02166f6099e5538dbf681a60c" title="Check if the theorem is a literal.">isAbsLiteral</a>()) {
<a name="l00221"></a>00221 <a class="code" href="group__SE.html#gaed2d918b4d0eb14d99bf63882fe2df1a" title="Notify the search engine about a new literal fact.">addLiteralFact</a>(thm);
<a name="l00222"></a>00222 <span class="comment">// These literals are derived, and should also be reported to the core. </span>
<a name="l00223"></a>00223 <span class="keywordflow">if</span>(!fromCore) <a class="code" href="group__SE.html#ga3772c6af7eac91b9ed7fc278edf5ef90" title="Access to theory reasoning.">d_core</a>-><a class="code" href="classCVC3_1_1TheoryCore.html#a479141bc26a125b758a2acc6420274f9" title="Enqueue a new fact.">enqueueFact</a>(thm);
<a name="l00224"></a>00224 } <span class="keywordflow">else</span> {
<a name="l00225"></a>00225 <a class="code" href="group__SE.html#gae95c78de94900637db19e3b7dee5d7c3" title="Notify the search engine about a new non-literal fact.">addNonLiteralFact</a>(thm);
<a name="l00226"></a>00226 }
<a name="l00227"></a>00227 <a class="code" href="debug_8h.html#ad64155edafde9f067f4868817cd04bdf">TRACE_MSG</a>(<span class="stringliteral">"addCNFFact"</span>, <span class="stringliteral">"addCNFFact => }"</span>);
<a name="l00228"></a>00228 }
<a name="l00229"></a>00229
<a name="l00230"></a>00230
<a name="l00231"></a><a class="code" href="group__SE.html#gac6e807418fb26dee354f7f934eb432ba">00231</a> <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.">SearchImplBase::addFact</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm) {
<a name="l00232"></a>00232 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"search addFact"</span>, <span class="stringliteral">"SearchImplBase::addFact("</span>, thm.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>(), <span class="stringliteral">") {"</span>);
<a name="l00233"></a>00233 <span class="keywordflow">if</span>(*<a class="code" href="group__SE.html#gae3b8b3cfd965e7d5138320d26808767a" title="Command line flag whether to convert to CNF.">d_cnfOption</a>)
<a name="l00234"></a>00234 <a class="code" href="group__SE.html#ga4bcd481c70362c589aa7e712a8cc746d" title="Translate theta to CNF and enqueue the new clauses.">enqueueCNF</a>(thm);
<a name="l00235"></a>00235 <span class="keywordflow">else</span>
<a name="l00236"></a>00236 <a class="code" href="group__SE.html#gadebc5b605b4a358789b697e44065a97e" title="Add a new fact to the search engine bypassing CNF converter.">addCNFFact</a>(thm, <span class="keyword">true</span>);
<a name="l00237"></a>00237 <a class="code" href="debug_8h.html#ad64155edafde9f067f4868817cd04bdf">TRACE_MSG</a>(<span class="stringliteral">"search addFact"</span>, <span class="stringliteral">"SearchImplBase::addFact => }"</span>);
<a name="l00238"></a>00238 }
<a name="l00239"></a>00239
<a name="l00240"></a>00240
<a name="l00241"></a><a class="code" href="group__SE.html#ga6c1448b58fb299bc084aa9c522faf36d">00241</a> <span class="keywordtype">void</span> <a class="code" href="group__SE.html#ga6c1448b58fb299bc084aa9c522faf36d" title="Suggest a splitter to the SearchEngine.">SearchImplBase::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="l00242"></a>00242 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(e.<a class="code" href="group__ExprPkg.html#gaac535dae48f02fcd093a5b1b1a062211" title="Test if e is an abstract literal.">isAbsLiteral</a>(), <span class="stringliteral">"SearchImplBase::addSplitter("</span>+e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>()+<span class="stringliteral">")"</span>);
<a name="l00243"></a>00243 <a class="code" href="group__SE.html#ga8ea9b2ab9f50d3ddf595595b1f3d7974" title="Backtracking ordered set of DP-suggested splitters.">d_dpSplitters</a>.<a class="code" href="classCVC3_1_1CDList.html#aa1e8d3591c596d1b9c585dec955b519b">push_back</a>(<a class="code" href="classCVC3_1_1SearchImplBase_1_1Splitter.html" title="Representation of a DP-suggested splitter.">Splitter</a>(<a class="code" href="group__SE.html#gaf0dbbb1806723760ab8744e96a8c6657" title="Construct a Literal out of an Expr or return an existing one.">newLiteral</a>(e)));
<a name="l00244"></a>00244 }
<a name="l00245"></a>00245
<a name="l00246"></a>00246
<a name="l00247"></a><a class="code" href="group__SE.html#gacf93ae1a488573c6d34dee7721007351">00247</a> <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.">SearchImplBase::getCounterExample</a>(vector<Expr>& assertions, <span class="keywordtype">bool</span> inOrder)
<a name="l00248"></a>00248 {
<a name="l00249"></a>00249 <span class="keywordflow">if</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#af3077cff0601b8ae28e420ef5ce2ea37">getTM</a>()-><a class="code" href="classCVC3_1_1TheoremManager.html#a0a4f7d2aac078ca32b1dacb5d0af25c4">withAssumptions</a>())
<a name="l00250"></a>00250 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1EvalException.html">EvalException</a>
<a name="l00251"></a>00251 (<span class="stringliteral">"Method getCounterExample() (or command COUNTEREXAMPLE) cannot be used\n"</span>
<a name="l00252"></a>00252 <span class="stringliteral">" without assumptions activated"</span>);
<a name="l00253"></a>00253 <span class="keywordflow">if</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 class="code" href="classCVC3_1_1Theorem.html#afc6fdb0507eb3669e28d9be5ed0bd333">isNull</a>())
<a name="l00254"></a>00254 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1EvalException.html">EvalException</a>
<a name="l00255"></a>00255 (<span class="stringliteral">"Method getCounterExample() (or command COUNTEREXAMPLE)\n"</span>
<a name="l00256"></a>00256 <span class="stringliteral">" must be called only after failed QUERY"</span>);
<a name="l00257"></a>00257 <a class="code" href="group__SE.html#gae65e0921e9ef2b475242b1a284a413ad" title="Get assumptions made internally in this and all previous contexts.">getInternalAssumptions</a>(assertions);
<a name="l00258"></a>00258 <span class="comment">/*</span>
<a name="l00259"></a>00259 <span class="comment"></span>
<a name="l00260"></a>00260 <span class="comment"> if(!d_lastCounterExample.empty()) {</span>
<a name="l00261"></a>00261 <span class="comment"> if (inOrder) {</span>
<a name="l00262"></a>00262 <span class="comment"> for(CDMap<Expr,Theorem>::orderedIterator i=d_assumptions.orderedBegin(),</span>
<a name="l00263"></a>00263 <span class="comment"> iend=d_assumptions.orderedEnd(); i!=iend; ++i) {</span>
<a name="l00264"></a>00264 <span class="comment"> if (d_lastCounterExample.find((*i).first) != d_lastCounterExample.end()) {</span>
<a name="l00265"></a>00265 <span class="comment"> assertions.push_back((*i).first);</span>
<a name="l00266"></a>00266 <span class="comment"> }</span>
<a name="l00267"></a>00267 <span class="comment"> }</span>
<a name="l00268"></a>00268 <span class="comment"> DebugAssert(assertions.size()==d_lastCounterExample.size(),</span>
<a name="l00269"></a>00269 <span class="comment"> "getCounterExample: missing assertion");</span>
<a name="l00270"></a>00270 <span class="comment"> }</span>
<a name="l00271"></a>00271 <span class="comment"> else {</span>
<a name="l00272"></a>00272 <span class="comment"> ExprHashMap<bool>::iterator i=d_lastCounterExample.begin(),</span>
<a name="l00273"></a>00273 <span class="comment"> iend = d_lastCounterExample.end();</span>
<a name="l00274"></a>00274 <span class="comment"> for(; i!=iend; ++i) assertions.push_back((*i).first);</span>
<a name="l00275"></a>00275 <span class="comment"> }</span>
<a name="l00276"></a>00276 <span class="comment"> }</span>
<a name="l00277"></a>00277 <span class="comment"> */</span>
<a name="l00278"></a>00278 }
<a name="l00279"></a>00279
<a name="l00280"></a>00280
<a name="l00281"></a>00281 <a class="code" href="classCVC3_1_1Proof.html">Proof</a>
<a name="l00282"></a><a class="code" href="group__SE.html#gaf90e8ae5cd67dc6c43787a9d3ebdca53">00282</a> <a class="code" href="group__SE.html#gaf90e8ae5cd67dc6c43787a9d3ebdca53" title="Returns the proof term for the last proven query.">SearchImplBase::getProof</a>()
<a name="l00283"></a>00283 {
<a name="l00284"></a>00284 <span class="keywordflow">if</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#af3077cff0601b8ae28e420ef5ce2ea37">getTM</a>()-><a class="code" href="classCVC3_1_1TheoremManager.html#a462f27eb0eca420b334354a9ddc7a257">withProof</a>())
<a name="l00285"></a>00285 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1EvalException.html">EvalException</a>
<a name="l00286"></a>00286 (<span class="stringliteral">"DUMP_PROOF cannot be used without proofs activated"</span>);
<a name="l00287"></a>00287 <span class="keywordflow">if</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 class="code" href="classCVC3_1_1Theorem.html#afc6fdb0507eb3669e28d9be5ed0bd333">isNull</a>())
<a name="l00288"></a>00288 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1EvalException.html">EvalException</a>
<a name="l00289"></a>00289 (<span class="stringliteral">"DUMP_PROOF must be called only after successful QUERY"</span>);
<a name="l00290"></a>00290 <span class="comment">// Double-check for optimized version</span>
<a name="l00291"></a>00291 <span class="keywordflow">if</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 class="code" href="classCVC3_1_1Theorem.html#afc6fdb0507eb3669e28d9be5ed0bd333">isNull</a>()) <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Proof.html">Proof</a>();
<a name="l00292"></a>00292 <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 class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>();
<a name="l00293"></a>00293 }
<a name="l00294"></a>00294
<a name="l00295"></a>00295
<a name="l00296"></a>00296 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a>&
<a name="l00297"></a><a class="code" href="group__SE.html#ga24dc510f27c40d8044f461308bcdb62d">00297</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().">SearchImplBase::getAssumptionsUsed</a>()
<a name="l00298"></a>00298 {
<a name="l00299"></a>00299 <span class="keywordflow">if</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#af3077cff0601b8ae28e420ef5ce2ea37">getTM</a>()-><a class="code" href="classCVC3_1_1TheoremManager.html#a0a4f7d2aac078ca32b1dacb5d0af25c4">withAssumptions</a>())
<a name="l00300"></a>00300 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1EvalException.html">EvalException</a>
<a name="l00301"></a>00301 (<span class="stringliteral">"DUMP_ASSUMPTIONS cannot be used without assumptions activated"</span>);
<a name="l00302"></a>00302 <span class="keywordflow">if</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 class="code" href="classCVC3_1_1Theorem.html#afc6fdb0507eb3669e28d9be5ed0bd333">isNull</a>())
<a name="l00303"></a>00303 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1EvalException.html">EvalException</a>
<a name="l00304"></a>00304 (<span class="stringliteral">"DUMP_ASSUMPTIONS must be called only after successful QUERY"</span>);
<a name="l00305"></a>00305 <span class="comment">// Double-check for optimized version</span>
<a name="l00306"></a>00306 <span class="keywordflow">if</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 class="code" href="classCVC3_1_1Theorem.html#afc6fdb0507eb3669e28d9be5ed0bd333">isNull</a>()) <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Assumptions.html#af309a39e2e013cc62b6d94c5812ad86b">Assumptions::emptyAssump</a>();
<a name="l00307"></a>00307 <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 class="code" href="classCVC3_1_1Theorem.html#a5e9ab00a613df15cc02f55edb55a67b3">getAssumptionsRef</a>();
<a name="l00308"></a>00308 }
<a name="l00309"></a>00309 <span class="comment"></span>
<a name="l00310"></a>00310 <span class="comment">/*! </span>
<a name="l00311"></a>00311 <span class="comment"> * Given a proof of FALSE ('res') from an assumption 'e', derive the</span>
<a name="l00312"></a>00312 <span class="comment"> * proof of the inverse of e.</span>
<a name="l00313"></a>00313 <span class="comment"> *</span>
<a name="l00314"></a>00314 <span class="comment"> * \param res is a proof of FALSE</span>
<a name="l00315"></a>00315 <span class="comment"> * \param e is the assumption used in the above proof</span>
<a name="l00316"></a>00316 <span class="comment"> */</span>
<a name="l00317"></a><a class="code" href="group__SE.html#ga0d509e38a03048dcbdb9e28f3f5da724">00317</a> <span class="keywordtype">void</span> <a class="code" href="group__SE.html#ga0d509e38a03048dcbdb9e28f3f5da724" title="Process result of checkValid.">SearchImplBase::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="l00318"></a>00318 {
<a name="l00319"></a>00319 <span class="comment">// Result must be either Null (== SAT) or false (== unSAT)</span>
<a name="l00320"></a>00320 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(res.<a class="code" href="classCVC3_1_1Theorem.html#afc6fdb0507eb3669e28d9be5ed0bd333">isNull</a>() || res.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>().<a class="code" href="group__ExprPkg.html#ga6173f64b22cba76472cd0c814bbf6dae">isFalse</a>(),
<a name="l00321"></a>00321 <span class="stringliteral">"processResult: bad input"</span>
<a name="l00322"></a>00322 + res.<a class="code" href="classCVC3_1_1Theorem.html#ac4b1c9570ffb9cc901627ef2abb9ff77">toString</a>());
<a name="l00323"></a>00323 <span class="keywordflow">if</span>(res.<a class="code" href="classCVC3_1_1Theorem.html#afc6fdb0507eb3669e28d9be5ed0bd333">isNull</a>()) {
<a name="l00324"></a>00324 <span class="comment">// Didn't prove valid (if CVC-lite is complete, it means invalid).</span>
<a name="l00325"></a>00325 <span class="comment">// The assumptions for the counterexample must have been already</span>
<a name="l00326"></a>00326 <span class="comment">// set by checkSAT().</span>
<a name="l00327"></a>00327 <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 class="code" href="classCVC3_1_1Theorem.html">Theorem</a>(); <span class="comment">// Reset last proof</span>
<a name="l00328"></a>00328 <span class="comment">// Remove !e, keep just the counterexample</span>
<a name="l00329"></a>00329 <a class="code" href="group__SE.html#gaf6841e86841006b6917d46664de64d21" title="Assumptions from the last unsuccessful checkValid call. These are used by getCounterExample.">d_lastCounterExample</a>.<a class="code" href="classCVC3_1_1ExprHashMap.html#a77637e1f3754b7153cbd1b903a5acb76">erase</a>(!e);
<a name="l00330"></a>00330 <span class="keywordflow">if</span> (e.<a class="code" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</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>.<a class="code" href="classCVC3_1_1ExprHashMap.html#a77637e1f3754b7153cbd1b903a5acb76">erase</a>(e[0]);
<a name="l00331"></a>00331 } <span class="keywordflow">else</span> {
<a name="l00332"></a>00332 <span class="comment">// Proved valid</span>
<a name="l00333"></a>00333 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> res2 =
<a name="l00334"></a>00334 <a class="code" href="group__SE.html#ga879b68112123e2b4ae7175d85a03bfec" title="Proof rules for the search engine.">d_rules</a>-><a class="code" href="group__SE__Rules.html#ga3ddf95924d2ff2efb59e84dc78a19821">eliminateSkolemAxioms</a>(res, <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#ac773341edabcc5091ca25af74fcb7653">getSkolemAxioms</a>());
<a name="l00335"></a>00335 <span class="keywordflow">if</span>(e.<a class="code" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a>())
<a name="l00336"></a>00336 <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 class="code" href="group__SE.html#ga879b68112123e2b4ae7175d85a03bfec" title="Proof rules for the search engine.">d_rules</a>-><a class="code" href="group__SE__Rules.html#ga846c2bdc33f6ff2080e76637ea618626" title="Negation introduction: .">negIntro</a>(e, res2);
<a name="l00337"></a>00337 <span class="keywordflow">else</span>
<a name="l00338"></a>00338 <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 class="code" href="group__SE.html#ga879b68112123e2b4ae7175d85a03bfec" title="Proof rules for the search engine.">d_rules</a>-><a class="code" href="group__SE__Rules.html#ga64c9fb7058e52c324ce76f15fcea37e2" title="Proof by contradiction: .">proofByContradiction</a>(e, res2);
<a name="l00339"></a>00339 <a class="code" href="group__SE.html#gaf6841e86841006b6917d46664de64d21" title="Assumptions from the last unsuccessful checkValid call. These are used by getCounterExample.">d_lastCounterExample</a>.<a class="code" href="classCVC3_1_1ExprHashMap.html#aa20f14dba09537171af45bf479b99c66">clear</a>(); <span class="comment">// Reset counterexample</span>
<a name="l00340"></a>00340 }
<a name="l00341"></a>00341 }
<a name="l00342"></a>00342
<a name="l00343"></a>00343
<a name="l00344"></a><a class="code" href="group__SE.html#ga83d82b8cf43e9dc8240e762b180f6343">00344</a> <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.">SearchImplBase::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) {
<a name="l00345"></a>00345 <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#a6f8068606f30fe7b2c405ddf5ce1a53b">clearSkolemAxioms</a>();
<a name="l00346"></a>00346 <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> qres = <a class="code" href="group__SE.html#ga1e6282534845cfe93f245d9983d58761" title="Checks the validity of a formula in the current context.">checkValidInternal</a>(e);
<a name="l00347"></a>00347 result = <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="l00348"></a>00348 <span class="keywordflow">return</span> qres;
<a name="l00349"></a>00349 }
<a name="l00350"></a>00350
<a name="l00351"></a>00351
<a name="l00352"></a><a class="code" href="group__SE.html#gad4a8edbe5a6520fc9f564ec1c65d4729">00352</a> <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.">SearchImplBase::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="l00353"></a>00353 <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> qres = <a class="code" href="group__SE.html#gaf89e6b914a2099b366258953fccb6277" title="Reruns last check with e as an additional assumption.">restartInternal</a>(e);
<a name="l00354"></a>00354 result = <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="l00355"></a>00355 <span class="keywordflow">return</span> qres;
<a name="l00356"></a>00356 }
<a name="l00357"></a>00357
<a name="l00358"></a>00358
<a name="l00359"></a>00359 <span class="keywordtype">void</span>
<a name="l00360"></a><a class="code" href="group__SE.html#ga4bcd481c70362c589aa7e712a8cc746d">00360</a> <a class="code" href="group__SE.html#ga4bcd481c70362c589aa7e712a8cc746d" title="Translate theta to CNF and enqueue the new clauses.">SearchImplBase::enqueueCNF</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& beta) {
<a name="l00361"></a>00361 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"mycnf"</span>, <span class="stringliteral">"enqueueCNF("</span>, beta, <span class="stringliteral">") {"</span>);
<a name="l00362"></a>00362 <span class="keywordflow">if</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="l00363"></a>00363 <a class="code" href="group__SE.html#gadebc5b605b4a358789b697e44065a97e" title="Add a new fact to the search engine bypassing CNF converter.">addCNFFact</a>(beta);
<a name="l00364"></a>00364
<a name="l00365"></a>00365 <a class="code" href="group__SE.html#ga62e31e3c4dbadb6cc5fddc3b0b73e047" title="Recursive version of enqueueCNF()">enqueueCNFrec</a>(beta);
<a name="l00366"></a>00366 <a class="code" href="debug_8h.html#ad64155edafde9f067f4868817cd04bdf">TRACE_MSG</a>(<span class="stringliteral">"mycnf"</span>, <span class="stringliteral">"enqueueCNF => }"</span>);
<a name="l00367"></a>00367 }
<a name="l00368"></a>00368
<a name="l00369"></a>00369
<a name="l00370"></a>00370 <span class="keywordtype">void</span>
<a name="l00371"></a><a class="code" href="group__SE.html#ga62e31e3c4dbadb6cc5fddc3b0b73e047">00371</a> <a class="code" href="group__SE.html#ga62e31e3c4dbadb6cc5fddc3b0b73e047" title="Recursive version of enqueueCNF()">SearchImplBase::enqueueCNFrec</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& beta) {
<a name="l00372"></a>00372 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> theta = beta;
<a name="l00373"></a>00373
<a name="l00374"></a>00374 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"mycnf"</span>,<span class="stringliteral">"enqueueCNFrec("</span>, theta.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>(), <span class="stringliteral">") { "</span>);
<a name="l00375"></a>00375 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"cnf-clauses"</span>, <span class="stringliteral">"enqueueCNF call"</span>, theta.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>(), <span class="stringliteral">""</span>);
<a name="l00376"></a>00376 <span class="comment">// The theorem scope shouldn't be higher than current</span>
<a name="l00377"></a>00377 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(theta.<a class="code" href="classCVC3_1_1Theorem.html#a112466d9793abcf97015233ffdc4ec5e">getScope</a>() <= <a class="code" href="group__SE.html#gab267d9f29c30c8e26b5c7bcc4d15306a" title="Return the current scope level (for convenience)">scopeLevel</a>(),
<a name="l00378"></a>00378 <span class="stringliteral">"\n theta.getScope()="</span>+<a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(theta.<a class="code" href="classCVC3_1_1Theorem.html#a112466d9793abcf97015233ffdc4ec5e">getScope</a>())
<a name="l00379"></a>00379 +<span class="stringliteral">"\n scopeLevel="</span>+<a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(<a class="code" href="group__SE.html#gab267d9f29c30c8e26b5c7bcc4d15306a" title="Return the current scope level (for convenience)">scopeLevel</a>())
<a name="l00380"></a>00380 +<span class="stringliteral">"\n e = "</span>+theta.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>().<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00381"></a>00381
<a name="l00382"></a>00382 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> thetaExpr = theta.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>();
<a name="l00383"></a>00383
<a name="l00384"></a>00384 <span class="keywordflow">if</span>(<a class="code" href="group__SE.html#ga9dc16eb11f046d9a615aff3018957c6d" title="Cache for enqueueCNF()">d_enqueueCNFCache</a>.<a class="code" href="classCVC3_1_1CDMap.html#af5f700035db0db798c645e36dd0b31bd">count</a>(thetaExpr) > 0) {
<a name="l00385"></a>00385 <a class="code" href="debug_8h.html#ad64155edafde9f067f4868817cd04bdf">TRACE_MSG</a>(<span class="stringliteral">"mycnf"</span>, <span class="stringliteral">"enqueueCNFrec[cached] => }"</span>);
<a name="l00386"></a>00386 <span class="keywordflow">return</span>;
<a name="l00387"></a>00387 }
<a name="l00388"></a>00388
<a name="l00389"></a>00389 <a class="code" href="group__SE.html#ga9dc16eb11f046d9a615aff3018957c6d" title="Cache for enqueueCNF()">d_enqueueCNFCache</a>[thetaExpr] = <span class="keyword">true</span>;
<a name="l00390"></a>00390
<a name="l00391"></a>00391 <span class="comment">// // Strip double negations first</span>
<a name="l00392"></a>00392 <span class="keywordflow">while</span>(thetaExpr.isNot() && thetaExpr[0].isNot()) {
<a name="l00393"></a>00393 theta = <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#ace6786234994faf89bc1b0ac8575278a">notNotElim</a>(theta);
<a name="l00394"></a>00394 thetaExpr = theta.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>();
<a name="l00395"></a>00395 <span class="comment">// Cache all the derived theorems too</span>
<a name="l00396"></a>00396 <a class="code" href="group__SE.html#ga9dc16eb11f046d9a615aff3018957c6d" title="Cache for enqueueCNF()">d_enqueueCNFCache</a>[thetaExpr] = <span class="keyword">true</span>;
<a name="l00397"></a>00397 }
<a name="l00398"></a>00398
<a name="l00399"></a>00399 <span class="comment">// Check for a propositional literal</span>
<a name="l00400"></a>00400 <span class="keywordflow">if</span>(thetaExpr.isPropLiteral()) {
<a name="l00401"></a>00401 theta = <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#aebbcd4a194e4fdca0bcd16143fb03a75">iffMP</a>(theta, <a class="code" href="group__SE.html#ga687e32d21d7fe7e4b26873ae86a47ae5" title="Replaces ITE subexpressions in e with variables.">replaceITE</a>(thetaExpr));
<a name="l00402"></a>00402 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!*<a class="code" href="group__SE.html#gaa28d7e60bbe1df69ffb304f939b984b7" title="Flag: whether to convert term ITEs into CNF.">d_ifLiftOption</a> || theta.<a class="code" href="classCVC3_1_1Theorem.html#aed1590a02166f6099e5538dbf681a60c" title="Check if the theorem is a literal.">isAbsLiteral</a>(),
<a name="l00403"></a>00403 <span class="stringliteral">"Must be a literal: theta = "</span>
<a name="l00404"></a>00404 +theta.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>().<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00405"></a>00405 <a class="code" href="group__SE.html#gadebc5b605b4a358789b697e44065a97e" title="Add a new fact to the search engine bypassing CNF converter.">addCNFFact</a>(theta);
<a name="l00406"></a>00406 <a class="code" href="debug_8h.html#ad64155edafde9f067f4868817cd04bdf">TRACE_MSG</a>(<span class="stringliteral">"mycnf"</span>, <span class="stringliteral">"enqueueCNFrec[literal] => }"</span>);
<a name="l00407"></a>00407 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"cnf-clauses"</span>, <span class="stringliteral">"literal with proofs("</span>, theta.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>(), <span class="stringliteral">")"</span>);
<a name="l00408"></a>00408 <span class="keywordflow">return</span>;
<a name="l00409"></a>00409 }
<a name="l00410"></a>00410
<a name="l00411"></a>00411 thetaExpr = theta.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>();
<a name="l00412"></a>00412 <span class="comment">// Obvious optimizations for AND and OR </span>
<a name="l00413"></a>00413 <span class="keywordflow">switch</span>(thetaExpr.getKind()) {
<a name="l00414"></a>00414 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba865555c9f2e0458a7078486aa1b3254f">AND</a>:
<a name="l00415"></a>00415 <span class="comment">// Split up the top-level conjunction and translate individually</span>
<a name="l00416"></a>00416 <span class="keywordflow">for</span>(<span class="keywordtype">int</span> i=0; i<thetaExpr.arity(); i++)
<a name="l00417"></a>00417 <a class="code" href="group__SE.html#ga62e31e3c4dbadb6cc5fddc3b0b73e047" title="Recursive version of enqueueCNF()">enqueueCNFrec</a>(<a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#a3f3592ac74d0aa0caa3b9224ea7e61f4">andElim</a>(theta, i));
<a name="l00418"></a>00418 <a class="code" href="debug_8h.html#ad64155edafde9f067f4868817cd04bdf">TRACE_MSG</a>(<span class="stringliteral">"mycnf"</span>, <span class="stringliteral">"enqueueCNFrec[AND] => }"</span>);
<a name="l00419"></a>00419 <span class="keywordflow">return</span>;
<a name="l00420"></a>00420 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba96727447c0ad447987df1c6415aef074">OR</a>: {
<a name="l00421"></a>00421 <span class="comment">// Check if we are already in CNF (ignoring ITEs in the terms),</span>
<a name="l00422"></a>00422 <span class="comment">// and if we are, translate term ITEs on the way</span>
<a name="l00423"></a>00423 <span class="keywordtype">bool</span> cnf(<span class="keyword">true</span>);
<a name="l00424"></a>00424 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"bv mycnf"</span>, <span class="stringliteral">"enqueueCNFrec[OR] ( "</span>, theta.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>().<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>(), <span class="stringliteral">")"</span>);
<a name="l00425"></a>00425 <span class="keywordflow">for</span>(<a class="code" href="classCVC3_1_1Expr_1_1iterator.html">Expr::iterator</a> i=thetaExpr.begin(),iend=thetaExpr.end();
<a name="l00426"></a>00426 i!=iend && cnf; i++) {
<a name="l00427"></a>00427 <span class="keywordflow">if</span>(!(*i).isPropLiteral())
<a name="l00428"></a>00428 cnf = <span class="keyword">false</span>;
<a name="l00429"></a>00429 }
<a name="l00430"></a>00430 <span class="keywordflow">if</span>(cnf) {
<a name="l00431"></a>00431 vector<Theorem> thms;
<a name="l00432"></a>00432 vector<unsigned int> changed;
<a name="l00433"></a>00433 <span class="keywordtype">unsigned</span> <span class="keywordtype">int</span> cc=0;
<a name="l00434"></a>00434 <span class="keywordflow">for</span>(<a class="code" href="classCVC3_1_1Expr_1_1iterator.html">Expr::iterator</a> i=thetaExpr.begin(),iend=thetaExpr.end();
<a name="l00435"></a>00435 i!=iend; i++,cc++) {
<a name="l00436"></a>00436 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> thm = <a class="code" href="group__SE.html#ga687e32d21d7fe7e4b26873ae86a47ae5" title="Replaces ITE subexpressions in e with variables.">replaceITE</a>(*i);
<a name="l00437"></a>00437 <span class="keywordflow">if</span>(thm.<a class="code" href="classCVC3_1_1Theorem.html#a206c04f39fbbcacef2337148675553f4">getLHS</a>() != thm.<a class="code" href="classCVC3_1_1Theorem.html#a97d957fcbf9094480851b1d2e5d3729f">getRHS</a>()) {
<a name="l00438"></a>00438 thms.push_back(thm);
<a name="l00439"></a>00439 changed.push_back(cc);
<a name="l00440"></a>00440 }
<a name="l00441"></a>00441 }
<a name="l00442"></a>00442 <span class="keywordflow">if</span>(changed.size() > 0) {
<a name="l00443"></a>00443 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> rewrite =
<a name="l00444"></a>00444 <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#a776c827bb6e3b889234429c49ae9ad6f" title="Optimized case for expr with one child.">substitutivityRule</a>(theta.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>(), changed, thms);
<a name="l00445"></a>00445 theta = <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#aebbcd4a194e4fdca0bcd16143fb03a75">iffMP</a>(theta, rewrite);
<a name="l00446"></a>00446 }
<a name="l00447"></a>00447 <a class="code" href="group__SE.html#gadebc5b605b4a358789b697e44065a97e" title="Add a new fact to the search engine bypassing CNF converter.">addCNFFact</a>(theta);
<a name="l00448"></a>00448 <a class="code" href="debug_8h.html#ad64155edafde9f067f4868817cd04bdf">TRACE_MSG</a>(<span class="stringliteral">"mycnf"</span>, <span class="stringliteral">"enqueueCNFrec[cnf] => }"</span>);
<a name="l00449"></a>00449 <span class="keywordflow">return</span>;
<a name="l00450"></a>00450 }
<a name="l00451"></a>00451 <span class="keywordflow">break</span>;
<a name="l00452"></a>00452 }
<a name="l00453"></a>00453 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>: { <span class="comment">// Check for "var <=> phi" and "phi <=> var"</span>
<a name="l00454"></a>00454 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t0 = thetaExpr[0];
<a name="l00455"></a>00455 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1 = thetaExpr[1];
<a name="l00456"></a>00456 <span class="keywordflow">if</span>(t1.<a class="code" href="group__ExprPkg.html#gaccf96ea73570e38c5c7e4ad39ed8b509" title="PropAtom or negation of PropAtom.">isPropLiteral</a>()) {
<a name="l00457"></a>00457 <span class="keywordflow">if</span>(!t1.<a class="code" href="group__ExprPkg.html#gaac535dae48f02fcd093a5b1b1a062211" title="Test if e is an abstract literal.">isAbsLiteral</a>())
<a name="l00458"></a>00458 theta = <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#a4a4e90cd69ce24e83ba2c217907c277a" title=" (same for IFF)">transitivityRule</a>(theta, <a class="code" href="group__SE.html#ga687e32d21d7fe7e4b26873ae86a47ae5" title="Replaces ITE subexpressions in e with variables.">replaceITE</a>(t1));
<a name="l00459"></a>00459 <a class="code" href="group__SE.html#gaa7bf3c385bae481d4ea35179e818a09a" title="FIXME: write a comment.">applyCNFRules</a>(theta);
<a name="l00460"></a>00460 <span class="keywordflow">return</span>;
<a name="l00461"></a>00461 } <span class="keywordflow">else</span> <span class="keywordflow">if</span>(thetaExpr[0].isPropLiteral()) {
<a name="l00462"></a>00462 theta = <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#a0a87e88508f49b73037e0024afa841bf" title=" (same for IFF)">symmetryRule</a>(theta);
<a name="l00463"></a>00463 <span class="keywordflow">if</span>(!t0.<a class="code" href="group__ExprPkg.html#gaac535dae48f02fcd093a5b1b1a062211" title="Test if e is an abstract literal.">isAbsLiteral</a>())
<a name="l00464"></a>00464 theta = <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#a4a4e90cd69ce24e83ba2c217907c277a" title=" (same for IFF)">transitivityRule</a>(theta, <a class="code" href="group__SE.html#ga687e32d21d7fe7e4b26873ae86a47ae5" title="Replaces ITE subexpressions in e with variables.">replaceITE</a>(t0));
<a name="l00465"></a>00465 <a class="code" href="group__SE.html#gaa7bf3c385bae481d4ea35179e818a09a" title="FIXME: write a comment.">applyCNFRules</a>(theta);
<a name="l00466"></a>00466 <span class="keywordflow">return</span>;
<a name="l00467"></a>00467 }
<a name="l00468"></a>00468 <span class="keywordflow">break</span>;
<a name="l00469"></a>00469 }
<a name="l00470"></a>00470 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3a4cfaf3eae8eac1dc2fd27d9f0994dc">ITE</a>:
<a name="l00471"></a>00471 <span class="keywordflow">if</span>(thetaExpr[0].isPropLiteral() && thetaExpr[1].isPropLiteral()
<a name="l00472"></a>00472 && thetaExpr[2].isPropLiteral()) {
<a name="l00473"></a>00473 <span class="comment">// Replace ITEs</span>
<a name="l00474"></a>00474 vector<Theorem> thms;
<a name="l00475"></a>00475 vector<unsigned int> changed;
<a name="l00476"></a>00476 <span class="keywordflow">for</span>(<span class="keywordtype">int</span> c=0, cend=thetaExpr.arity(); c<cend; ++c) {
<a name="l00477"></a>00477 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> thm = <a class="code" href="group__SE.html#ga687e32d21d7fe7e4b26873ae86a47ae5" title="Replaces ITE subexpressions in e with variables.">replaceITE</a>(thetaExpr[c]);
<a name="l00478"></a>00478 <span class="keywordflow">if</span>(thm.<a class="code" href="classCVC3_1_1Theorem.html#a206c04f39fbbcacef2337148675553f4">getLHS</a>() != thm.<a class="code" href="classCVC3_1_1Theorem.html#a97d957fcbf9094480851b1d2e5d3729f">getRHS</a>()) {
<a name="l00479"></a>00479 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!*<a class="code" href="group__SE.html#gaa28d7e60bbe1df69ffb304f939b984b7" title="Flag: whether to convert term ITEs into CNF.">d_ifLiftOption</a> || thm.<a class="code" href="classCVC3_1_1Theorem.html#a97d957fcbf9094480851b1d2e5d3729f">getRHS</a>().<a class="code" href="group__ExprPkg.html#gaac535dae48f02fcd093a5b1b1a062211" title="Test if e is an abstract literal.">isAbsLiteral</a>(),
<a name="l00480"></a>00480 <span class="stringliteral">"thm = "</span>+thm.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>().<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00481"></a>00481 thms.push_back(thm);
<a name="l00482"></a>00482 changed.push_back(c);
<a name="l00483"></a>00483 }
<a name="l00484"></a>00484 }
<a name="l00485"></a>00485 <span class="keywordflow">if</span>(changed.size() > 0) {
<a name="l00486"></a>00486 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> rewrite =
<a name="l00487"></a>00487 <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#a776c827bb6e3b889234429c49ae9ad6f" title="Optimized case for expr with one child.">substitutivityRule</a>(theta.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>(), changed, thms);
<a name="l00488"></a>00488 theta = <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#aebbcd4a194e4fdca0bcd16143fb03a75">iffMP</a>(theta, rewrite);
<a name="l00489"></a>00489 }
<a name="l00490"></a>00490 <span class="comment">// Convert to clauses</span>
<a name="l00491"></a>00491 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> thm = <a class="code" href="group__SE.html#ga879b68112123e2b4ae7175d85a03bfec" title="Proof rules for the search engine.">d_rules</a>-><a class="code" href="group__SE__Rules.html#ga9b9c0fe62505477b6ec9774c1b5b2494" title="ITE(c, f1, f2) |- (NOT c OR f1) AND (c OR f2)">iteToClauses</a>(theta);
<a name="l00492"></a>00492 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(thm.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>().<a class="code" href="group__ExprPkg.html#ga383260cf4f8919728e2712e6e11f21fa">isAnd</a>() && thm.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>().<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>()==2,
<a name="l00493"></a>00493 <span class="stringliteral">"enqueueCNFrec [ITE over literals]\n thm = "</span>
<a name="l00494"></a>00494 +thm.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>().<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00495"></a>00495 <a class="code" href="group__SE.html#gadebc5b605b4a358789b697e44065a97e" title="Add a new fact to the search engine bypassing CNF converter.">addCNFFact</a>(<a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#a3f3592ac74d0aa0caa3b9224ea7e61f4">andElim</a>(thm, 0));
<a name="l00496"></a>00496 <a class="code" href="group__SE.html#gadebc5b605b4a358789b697e44065a97e" title="Add a new fact to the search engine bypassing CNF converter.">addCNFFact</a>(<a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#a3f3592ac74d0aa0caa3b9224ea7e61f4">andElim</a>(thm, 1));
<a name="l00497"></a>00497 <span class="keywordflow">return</span>;
<a name="l00498"></a>00498 }
<a name="l00499"></a>00499 <span class="keywordflow">break</span>;
<a name="l00500"></a>00500 <span class="keywordflow">default</span>:
<a name="l00501"></a>00501 <span class="keywordflow">break</span>;
<a name="l00502"></a>00502 }
<a name="l00503"></a>00503
<a name="l00504"></a>00504 <span class="comment">// Now do the real work</span>
<a name="l00505"></a>00505 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> res = <a class="code" href="group__SE.html#ga298ad740ab490d5b3337445573b8c4d7" title="Find a theorem phi <=> v by phi, where v is a literal.">findInCNFCache</a>(theta.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00506"></a>00506 <span class="keywordflow">if</span>(!res.<a class="code" href="classCVC3_1_1Theorem.html#afc6fdb0507eb3669e28d9be5ed0bd333">isNull</a>()) {
<a name="l00507"></a>00507 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> thm = <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#aebbcd4a194e4fdca0bcd16143fb03a75">iffMP</a>(theta, res);
<a name="l00508"></a>00508 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(thm.<a class="code" href="classCVC3_1_1Theorem.html#aed1590a02166f6099e5538dbf681a60c" title="Check if the theorem is a literal.">isAbsLiteral</a>(), <span class="stringliteral">"thm = "</span>+thm.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>().<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00509"></a>00509 <a class="code" href="group__SE.html#gadebc5b605b4a358789b697e44065a97e" title="Add a new fact to the search engine bypassing CNF converter.">addCNFFact</a>(thm);
<a name="l00510"></a>00510 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"cnf-clauses"</span>, <span class="stringliteral">"enqueueCNFrec call[cache hit]:("</span>,
<a name="l00511"></a>00511 thm.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>(), <span class="stringliteral">")"</span>);
<a name="l00512"></a>00512 <a class="code" href="group__SE.html#gaa7bf3c385bae481d4ea35179e818a09a" title="FIXME: write a comment.">applyCNFRules</a>(res);
<a name="l00513"></a>00513 <a class="code" href="debug_8h.html#ad64155edafde9f067f4868817cd04bdf">TRACE_MSG</a>(<span class="stringliteral">"mycnf"</span>, <span class="stringliteral">"enqueueCNFrec[cached] => }"</span>);
<a name="l00514"></a>00514 <span class="keywordflow">return</span>;
<a name="l00515"></a>00515 }
<a name="l00516"></a>00516
<a name="l00517"></a>00517 <span class="comment">// std::vector<Theorem> clauses;</span>
<a name="l00518"></a>00518 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> result;
<a name="l00519"></a>00519 <span class="comment">// (\phi <==> v)</span>
<a name="l00520"></a>00520 result = <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#a10fa187373ec24079c10874d8e804ecb" title="Retrun a theorem "|- e = v" for a new Skolem constant v.">varIntroSkolem</a>(theta.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00521"></a>00521
<a name="l00522"></a>00522 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"mycnf"</span>, <span class="stringliteral">"enqueueCNFrec: varIntroSkolem => "</span>, result.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>(),
<a name="l00523"></a>00523 <span class="stringliteral">" @ "</span>+<a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(result.<a class="code" href="classCVC3_1_1Theorem.html#a112466d9793abcf97015233ffdc4ec5e">getScope</a>())
<a name="l00524"></a>00524 +<span class="stringliteral">" (current="</span>+<a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(<a class="code" href="group__SE.html#gab267d9f29c30c8e26b5c7bcc4d15306a" title="Return the current scope level (for convenience)">scopeLevel</a>())+<span class="stringliteral">")"</span>);
<a name="l00525"></a>00525
<a name="l00526"></a>00526 <span class="comment">//result = skolemize(result, false);</span>
<a name="l00527"></a>00527
<a name="l00528"></a>00528 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"mycnf"</span>, <span class="stringliteral">"enqueueCNFrec: skolemize => "</span>, result.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>(),
<a name="l00529"></a>00529 <span class="stringliteral">" @ "</span>+<a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(result.<a class="code" href="classCVC3_1_1Theorem.html#a112466d9793abcf97015233ffdc4ec5e">getScope</a>())
<a name="l00530"></a>00530 +<span class="stringliteral">" (current="</span>+<a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(<a class="code" href="group__SE.html#gab267d9f29c30c8e26b5c7bcc4d15306a" title="Return the current scope level (for convenience)">scopeLevel</a>())+<span class="stringliteral">")"</span>);
<a name="l00531"></a>00531 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(result.<a class="code" href="classCVC3_1_1Theorem.html#a362c1d70e03803d804bbe300e5f6dc87">isRewrite</a>(),
<a name="l00532"></a>00532 <span class="stringliteral">"SearchImplBase::CNF(): result = "</span>+result.<a class="code" href="classCVC3_1_1Theorem.html#ac4b1c9570ffb9cc901627ef2abb9ff77">toString</a>());
<a name="l00533"></a>00533 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!result.<a class="code" href="classCVC3_1_1Theorem.html#a206c04f39fbbcacef2337148675553f4">getLHS</a>().<a class="code" href="group__ExprPkg.html#gaccf96ea73570e38c5c7e4ad39ed8b509" title="PropAtom or negation of PropAtom.">isPropLiteral</a>() &&
<a name="l00534"></a>00534 result.<a class="code" href="classCVC3_1_1Theorem.html#a97d957fcbf9094480851b1d2e5d3729f">getRHS</a>().<a class="code" href="group__ExprPkg.html#gaccf96ea73570e38c5c7e4ad39ed8b509" title="PropAtom or negation of PropAtom.">isPropLiteral</a>(),
<a name="l00535"></a>00535 <span class="stringliteral">"SearchImplBase::CNF(): result = "</span>+result.<a class="code" href="classCVC3_1_1Theorem.html#ac4b1c9570ffb9cc901627ef2abb9ff77">toString</a>());
<a name="l00536"></a>00536 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(result.<a class="code" href="classCVC3_1_1Theorem.html#a206c04f39fbbcacef2337148675553f4">getLHS</a>() == theta.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>(),
<a name="l00537"></a>00537 <span class="stringliteral">"SearchImplBase::CNF(): result = "</span>+result.<a class="code" href="classCVC3_1_1Theorem.html#ac4b1c9570ffb9cc901627ef2abb9ff77">toString</a>()
<a name="l00538"></a>00538 +<span class="stringliteral">"\n theta = "</span>+theta.<a class="code" href="classCVC3_1_1Theorem.html#ac4b1c9570ffb9cc901627ef2abb9ff77">toString</a>());
<a name="l00539"></a>00539
<a name="l00540"></a>00540 <span class="comment">//enqueue v</span>
<a name="l00541"></a>00541 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> var(<a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#aebbcd4a194e4fdca0bcd16143fb03a75">iffMP</a>(theta, result));
<a name="l00542"></a>00542 <span class="comment">// Add variable to the set of CNF vars</span>
<a name="l00543"></a>00543 <a class="code" href="group__SE.html#ga1c64a37d94b4cadedce29f3e4b98a3af" title="Backtracking set of new variables generated by CNF translator.">d_cnfVars</a>[var.getExpr()] = <span class="keyword">true</span>;
<a name="l00544"></a>00544 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"mycnf"</span>, <span class="stringliteral">"enqueueCNFrec: theta = "</span>, theta.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>(),
<a name="l00545"></a>00545 <span class="stringliteral">" @ "</span>+<a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(theta.<a class="code" href="classCVC3_1_1Theorem.html#a112466d9793abcf97015233ffdc4ec5e">getScope</a>())
<a name="l00546"></a>00546 +<span class="stringliteral">" (current="</span>+<a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(<a class="code" href="group__SE.html#gab267d9f29c30c8e26b5c7bcc4d15306a" title="Return the current scope level (for convenience)">scopeLevel</a>())+<span class="stringliteral">")"</span>);
<a name="l00547"></a>00547 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"mycnf"</span>, <span class="stringliteral">"enqueueCNFrec: var = "</span>, var.getExpr(),
<a name="l00548"></a>00548 <span class="stringliteral">" @ "</span>+<a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(var.getScope())
<a name="l00549"></a>00549 +<span class="stringliteral">" (current="</span>+<a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(<a class="code" href="group__SE.html#gab267d9f29c30c8e26b5c7bcc4d15306a" title="Return the current scope level (for convenience)">scopeLevel</a>())+<span class="stringliteral">")"</span>);
<a name="l00550"></a>00550 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(var.isAbsLiteral(), <span class="stringliteral">"var = "</span>+var.getExpr().toString());
<a name="l00551"></a>00551 <a class="code" href="group__SE.html#gadebc5b605b4a358789b697e44065a97e" title="Add a new fact to the search engine bypassing CNF converter.">addCNFFact</a>(var);
<a name="l00552"></a>00552 <span class="comment">// phi <=> v</span>
<a name="l00553"></a>00553 <a class="code" href="group__SE.html#gaa78fb38536d0a2e34ad140f3ec865f2b" title="Cache a theorem phi <=> v by phi, where v is a literal.">addToCNFCache</a>(result);
<a name="l00554"></a>00554 <a class="code" href="group__SE.html#gaa7bf3c385bae481d4ea35179e818a09a" title="FIXME: write a comment.">applyCNFRules</a>(result);
<a name="l00555"></a>00555 <a class="code" href="debug_8h.html#ad64155edafde9f067f4868817cd04bdf">TRACE_MSG</a>(<span class="stringliteral">"mycnf"</span>, <span class="stringliteral">"enqueueCNFrec => }"</span>);
<a name="l00556"></a>00556 }
<a name="l00557"></a>00557
<a name="l00558"></a>00558 <span class="comment"></span>
<a name="l00559"></a>00559 <span class="comment">/*!</span>
<a name="l00560"></a>00560 <span class="comment"> * \param thm is the input of the form phi <=> v</span>
<a name="l00561"></a>00561 <span class="comment"> */</span>
<a name="l00562"></a>00562 <span class="keywordtype">void</span>
<a name="l00563"></a><a class="code" href="group__SE.html#gaa7bf3c385bae481d4ea35179e818a09a">00563</a> <a class="code" href="group__SE.html#gaa7bf3c385bae481d4ea35179e818a09a" title="FIXME: write a comment.">SearchImplBase::applyCNFRules</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm) {
<a name="l00564"></a>00564 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"mycnf"</span>, <span class="stringliteral">"applyCNFRules("</span>, thm.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>(), <span class="stringliteral">") { "</span>);
<a name="l00565"></a>00565
<a name="l00566"></a>00566 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> result = thm;
<a name="l00567"></a>00567 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(result.isRewrite(),
<a name="l00568"></a>00568 <span class="stringliteral">"SearchImplBase::applyCNFRules: input must be an iff: "</span> +
<a name="l00569"></a>00569 result.getExpr().toString());
<a name="l00570"></a>00570 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> lhs = result.getLHS();
<a name="l00571"></a>00571 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> rhs = result.getRHS();
<a name="l00572"></a>00572 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(rhs.<a class="code" href="group__ExprPkg.html#gaac535dae48f02fcd093a5b1b1a062211" title="Test if e is an abstract literal.">isAbsLiteral</a>(),
<a name="l00573"></a>00573 <span class="stringliteral">"SearchImplBase::applyCNFRules: rhs of input must be literal: "</span> +
<a name="l00574"></a>00574 result.getExpr().toString());
<a name="l00575"></a>00575
<a name="l00576"></a>00576 <span class="comment">// Eliminate negation first</span>
<a name="l00577"></a>00577 <span class="keywordflow">while</span>(result.getLHS().isNot())
<a name="l00578"></a>00578 result = <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#af38f25446a561384c3de66392c4d3544" title="e1 <=> e2 ==> ~e1 <=> ~e2">iffContrapositive</a>(result);
<a name="l00579"></a>00579 lhs = result.<a class="code" href="classCVC3_1_1Theorem.html#a206c04f39fbbcacef2337148675553f4">getLHS</a>();
<a name="l00580"></a>00580 rhs = result.getRHS();
<a name="l00581"></a>00581
<a name="l00582"></a>00582 <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr,bool>::iterator</a> it = <a class="code" href="group__SE.html#ga401319b3ede7162504e979aaf2119deb" title="Cache for applyCNFRules()">d_applyCNFRulesCache</a>.<a class="code" href="classCVC3_1_1CDMap.html#a1cadecbd2d6fa614a2f2e9419aa43f33">find</a>(lhs);
<a name="l00583"></a>00583 <span class="keywordflow">if</span>(it == <a class="code" href="group__SE.html#ga401319b3ede7162504e979aaf2119deb" title="Cache for applyCNFRules()">d_applyCNFRulesCache</a>.<a class="code" href="classCVC3_1_1CDMap.html#a2a26c7cc4db12cb17d273db5cfa5a890">end</a>())
<a name="l00584"></a>00584 <a class="code" href="group__SE.html#ga401319b3ede7162504e979aaf2119deb" title="Cache for applyCNFRules()">d_applyCNFRulesCache</a>[lhs] = <span class="keyword">true</span>;
<a name="l00585"></a>00585 <span class="keywordflow">else</span> {
<a name="l00586"></a>00586 <a class="code" href="debug_8h.html#ad64155edafde9f067f4868817cd04bdf">TRACE_MSG</a>(<span class="stringliteral">"mycnf"</span>,<span class="stringliteral">"applyCNFRules[temp cache] => }"</span>);
<a name="l00587"></a>00587 <span class="keywordflow">return</span>;
<a name="l00588"></a>00588 }
<a name="l00589"></a>00589
<a name="l00590"></a>00590 <span class="comment">// Catch the trivial case v1 <=> v2</span>
<a name="l00591"></a>00591 <span class="keywordflow">if</span>(lhs.isPropLiteral()) {
<a name="l00592"></a>00592 <span class="keywordflow">if</span>(!lhs.isAbsLiteral()) {
<a name="l00593"></a>00593 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> replaced = <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#a0a87e88508f49b73037e0024afa841bf" title=" (same for IFF)">symmetryRule</a>(<a class="code" href="group__SE.html#ga687e32d21d7fe7e4b26873ae86a47ae5" title="Replaces ITE subexpressions in e with variables.">replaceITE</a>(lhs));
<a name="l00594"></a>00594 result = <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#a4a4e90cd69ce24e83ba2c217907c277a" title=" (same for IFF)">transitivityRule</a>(replaced, result);
<a name="l00595"></a>00595 lhs = result.<a class="code" href="classCVC3_1_1Theorem.html#a206c04f39fbbcacef2337148675553f4">getLHS</a>();
<a name="l00596"></a>00596 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(rhs == result.getRHS(),
<a name="l00597"></a>00597 <span class="stringliteral">"applyCNFRules [literal lhs]\n result = "</span>
<a name="l00598"></a>00598 +result.getExpr().<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>()
<a name="l00599"></a>00599 +<span class="stringliteral">"\n rhs = "</span>+rhs.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00600"></a>00600 }
<a name="l00601"></a>00601 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> thm = <a class="code" href="group__SE.html#ga879b68112123e2b4ae7175d85a03bfec" title="Proof rules for the search engine.">d_rules</a>-><a class="code" href="group__SE__Rules.html#ga356cd5a36ede50921fbaa3bc7e222d4f" title="e1 <=> e2 |- (NOT e1 OR e2) AND (e1 OR NOT e2)">iffToClauses</a>(result);
<a name="l00602"></a>00602 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(thm.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>().<a class="code" href="group__ExprPkg.html#ga383260cf4f8919728e2712e6e11f21fa">isAnd</a>() && thm.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>().<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>()==2,
<a name="l00603"></a>00603 <span class="stringliteral">"applyCNFRules [literal lhs]\n thm = "</span>
<a name="l00604"></a>00604 +thm.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>().<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00605"></a>00605 <a class="code" href="group__SE.html#gadebc5b605b4a358789b697e44065a97e" title="Add a new fact to the search engine bypassing CNF converter.">addCNFFact</a>(<a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#a3f3592ac74d0aa0caa3b9224ea7e61f4">andElim</a>(thm, 0));
<a name="l00606"></a>00606 <a class="code" href="group__SE.html#gadebc5b605b4a358789b697e44065a97e" title="Add a new fact to the search engine bypassing CNF converter.">addCNFFact</a>(<a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#a3f3592ac74d0aa0caa3b9224ea7e61f4">andElim</a>(thm, 1));
<a name="l00607"></a>00607 <span class="keywordflow">return</span>;
<a name="l00608"></a>00608 }
<a name="l00609"></a>00609
<a name="l00610"></a>00610 <span class="comment">// Check the kids in e[0], replace them with cache[e[0][i]], rebuild thm</span>
<a name="l00611"></a>00611 vector<unsigned> changed;
<a name="l00612"></a>00612 vector<Theorem> substitutions;
<a name="l00613"></a>00613 <span class="keywordtype">int</span> c=0;
<a name="l00614"></a>00614 <span class="keywordflow">for</span>(<a class="code" href="classCVC3_1_1Expr_1_1iterator.html">Expr::iterator</a> j = lhs.begin(), jend = lhs.end(); j!=jend; ++c,++j) {
<a name="l00615"></a>00615 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& phi = *j;
<a name="l00616"></a>00616 <span class="keywordflow">if</span>(!phi.<a class="code" href="group__ExprPkg.html#gaccf96ea73570e38c5c7e4ad39ed8b509" title="PropAtom or negation of PropAtom.">isPropLiteral</a>()) {
<a name="l00617"></a>00617 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> phiIffVar = <a class="code" href="group__SE.html#ga298ad740ab490d5b3337445573b8c4d7" title="Find a theorem phi <=> v by phi, where v is a literal.">findInCNFCache</a>(phi);
<a name="l00618"></a>00618 <span class="keywordflow">if</span>(phiIffVar.<a class="code" href="classCVC3_1_1Theorem.html#afc6fdb0507eb3669e28d9be5ed0bd333">isNull</a>()) {
<a name="l00619"></a>00619 <span class="comment">// Create a new variable for this child</span>
<a name="l00620"></a>00620 phiIffVar = <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#a10fa187373ec24079c10874d8e804ecb" title="Retrun a theorem "|- e = v" for a new Skolem constant v.">varIntroSkolem</a>(phi);
<a name="l00621"></a>00621 <a class="code" href="group__SE.html#gaa78fb38536d0a2e34ad140f3ec865f2b" title="Cache a theorem phi <=> v by phi, where v is a literal.">addToCNFCache</a>(phiIffVar);
<a name="l00622"></a>00622 }
<a name="l00623"></a>00623 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(phiIffVar.<a class="code" href="classCVC3_1_1Theorem.html#a362c1d70e03803d804bbe300e5f6dc87">isRewrite</a>(),
<a name="l00624"></a>00624 <span class="stringliteral">"SearchImplBase::applyCNFRules: result = "</span> +
<a name="l00625"></a>00625 result.toString());
<a name="l00626"></a>00626 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(phi == phiIffVar.<a class="code" href="classCVC3_1_1Theorem.html#a206c04f39fbbcacef2337148675553f4">getLHS</a>(),
<a name="l00627"></a>00627 <span class="stringliteral">"SearchImplBase::applyCNFRules:\n phi = "</span> +
<a name="l00628"></a>00628 phi.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>()
<a name="l00629"></a>00629 + <span class="stringliteral">"\n\n phiIffVar = "</span> + phiIffVar.<a class="code" href="classCVC3_1_1Theorem.html#ac4b1c9570ffb9cc901627ef2abb9ff77">toString</a>());
<a name="l00630"></a>00630 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(phiIffVar.<a class="code" href="classCVC3_1_1Theorem.html#a97d957fcbf9094480851b1d2e5d3729f">getRHS</a>().<a class="code" href="group__ExprPkg.html#gaac535dae48f02fcd093a5b1b1a062211" title="Test if e is an abstract literal.">isAbsLiteral</a>(),
<a name="l00631"></a>00631 <span class="stringliteral">"SearchImplBase::applyCNFRules: phiIffVar = "</span> +
<a name="l00632"></a>00632 phiIffVar.<a class="code" href="classCVC3_1_1Theorem.html#ac4b1c9570ffb9cc901627ef2abb9ff77">toString</a>());
<a name="l00633"></a>00633 changed.push_back(c);
<a name="l00634"></a>00634 substitutions.push_back(phiIffVar);
<a name="l00635"></a>00635 <a class="code" href="group__SE.html#gaa7bf3c385bae481d4ea35179e818a09a" title="FIXME: write a comment.">applyCNFRules</a>(phiIffVar);
<a name="l00636"></a>00636 }
<a name="l00637"></a>00637 }
<a name="l00638"></a>00638 <span class="keywordflow">if</span>(changed.size() > 0) {
<a name="l00639"></a>00639 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> subst =
<a name="l00640"></a>00640 <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#a776c827bb6e3b889234429c49ae9ad6f" title="Optimized case for expr with one child.">substitutivityRule</a>(lhs, changed, substitutions);
<a name="l00641"></a>00641 subst = <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#a0a87e88508f49b73037e0024afa841bf" title=" (same for IFF)">symmetryRule</a>(subst);
<a name="l00642"></a>00642 result = <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#a4a4e90cd69ce24e83ba2c217907c277a" title=" (same for IFF)">transitivityRule</a>(subst, result);
<a name="l00643"></a>00643 }
<a name="l00644"></a>00644
<a name="l00645"></a>00645 <span class="keywordflow">switch</span>(result.getLHS().getKind()) {
<a name="l00646"></a>00646 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba865555c9f2e0458a7078486aa1b3254f">AND</a>:
<a name="l00647"></a>00647 result = <a class="code" href="group__SE.html#ga879b68112123e2b4ae7175d85a03bfec" title="Proof rules for the search engine.">d_rules</a>-><a class="code" href="group__SE__Rules.html#gab183ff7d1013729d0d3e2dbe28686e3c" title="AND(x1,...,xn) <=> v |- CNF[AND(x1,...,xn) <=> v].">andCNFRule</a>(result);
<a name="l00648"></a>00648 <span class="keywordflow">break</span>;
<a name="l00649"></a>00649 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba96727447c0ad447987df1c6415aef074">OR</a>:
<a name="l00650"></a>00650 result = <a class="code" href="group__SE.html#ga879b68112123e2b4ae7175d85a03bfec" title="Proof rules for the search engine.">d_rules</a>-><a class="code" href="group__SE__Rules.html#ga7086aa693d2a3421bc349eca8e9938ba" title="OR(x1,...,xn) <=> v |- CNF[OR(x1,...,xn) <=> v].">orCNFRule</a>(result);
<a name="l00651"></a>00651 <span class="keywordflow">break</span>;
<a name="l00652"></a>00652 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>:
<a name="l00653"></a>00653 result = <a class="code" href="group__SE.html#ga879b68112123e2b4ae7175d85a03bfec" title="Proof rules for the search engine.">d_rules</a>-><a class="code" href="group__SE__Rules.html#ga4ab7606744594db9050cb83fe6b73668" title="(x1 <=> x2) <=> v |- CNF[(x1 <=> x2) <=> v]">iffCNFRule</a>(result);
<a name="l00654"></a>00654 <span class="keywordflow">break</span>;
<a name="l00655"></a>00655 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7338bb59b9aa936104a6d2f631d4d8db">IMPLIES</a>:
<a name="l00656"></a>00656 result = <a class="code" href="group__SE.html#ga879b68112123e2b4ae7175d85a03bfec" title="Proof rules for the search engine.">d_rules</a>-><a class="code" href="group__SE__Rules.html#ga25f7b95c8ebce2be117d03a1c93d715f" title="(x1 => x2) <=> v |- CNF[(x1 => x2) <=> v]">impCNFRule</a>(result);
<a name="l00657"></a>00657 <span class="keywordflow">break</span>;
<a name="l00658"></a>00658 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3a4cfaf3eae8eac1dc2fd27d9f0994dc">ITE</a>:
<a name="l00659"></a>00659 result = <a class="code" href="group__SE.html#ga879b68112123e2b4ae7175d85a03bfec" title="Proof rules for the search engine.">d_rules</a>-><a class="code" href="group__SE__Rules.html#gae9263cbcedf5def99b3c49ee6978497a" title="ITE(c, x1, x2) <=> v |- CNF[ITE(c, x1, x2) <=> v].">iteCNFRule</a>(result);
<a name="l00660"></a>00660 <span class="keywordflow">break</span>;
<a name="l00661"></a>00661 <span class="keywordflow">default</span>:
<a name="l00662"></a>00662 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<span class="keyword">false</span>,
<a name="l00663"></a>00663 <span class="stringliteral">"SearchImplBase::applyCNFRules: "</span>
<a name="l00664"></a>00664 <span class="stringliteral">"the input operator must be and|or|iff|imp|ite\n result = "</span> +
<a name="l00665"></a>00665 result.getLHS().toString());
<a name="l00666"></a>00666 <span class="keywordflow">break</span>;
<a name="l00667"></a>00667 }
<a name="l00668"></a>00668
<a name="l00669"></a>00669 <span class="comment">// FIXME: eliminate this once debugged</span>
<a name="l00670"></a>00670 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> clauses(result);
<a name="l00671"></a>00671
<a name="l00672"></a>00672 <span class="comment">// Enqueue the clauses</span>
<a name="l00673"></a>00673 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!clauses.<a class="code" href="classCVC3_1_1Theorem.html#afc6fdb0507eb3669e28d9be5ed0bd333">isNull</a>(), <span class="stringliteral">"Oops!.."</span>);
<a name="l00674"></a>00674 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(clauses.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>().<a class="code" href="group__ExprPkg.html#ga383260cf4f8919728e2712e6e11f21fa">isAnd</a>(), <span class="stringliteral">"clauses = "</span>
<a name="l00675"></a>00675 +clauses.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>().<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00676"></a>00676
<a name="l00677"></a>00677 <span class="comment">// The clauses may containt term ITEs, and we need to translate those</span>
<a name="l00678"></a>00678
<a name="l00679"></a>00679 <span class="keywordflow">for</span>(<span class="keywordtype">int</span> i=0, iend=clauses.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>().<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>(); i<iend; ++i) {
<a name="l00680"></a>00680 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> clause(<a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#a3f3592ac74d0aa0caa3b9224ea7e61f4">andElim</a>(clauses,i));
<a name="l00681"></a>00681 <a class="code" href="group__SE.html#gadebc5b605b4a358789b697e44065a97e" title="Add a new fact to the search engine bypassing CNF converter.">addCNFFact</a>(clause);
<a name="l00682"></a>00682 }
<a name="l00683"></a>00683 <a class="code" href="debug_8h.html#ad64155edafde9f067f4868817cd04bdf">TRACE_MSG</a>(<span class="stringliteral">"mycnf"</span>,<span class="stringliteral">"applyCNFRules => }"</span>);
<a name="l00684"></a>00684 }
<a name="l00685"></a>00685
<a name="l00686"></a>00686
<a name="l00687"></a><a class="code" href="group__SE.html#ga9babda9b0bcd226dd4d0a736cd433893">00687</a> <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)">SearchImplBase::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="l00688"></a>00688 <span class="keywordflow">if</span>(e.<a class="code" href="group__ExprPkg.html#gaac535dae48f02fcd093a5b1b1a062211" title="Test if e is an abstract literal.">isAbsLiteral</a>()) <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00689"></a>00689 <span class="keywordflow">if</span>(!e.<a class="code" href="group__ExprPkg.html#ga36f1eff876808586db368dc1b6da5f56">isOr</a>()) <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00690"></a>00690
<a name="l00691"></a>00691 <span class="keywordtype">bool</span> cnf(<span class="keyword">true</span>);
<a name="l00692"></a>00692 <span class="keywordflow">for</span>(<a class="code" href="classCVC3_1_1Expr_1_1iterator.html">Expr::iterator</a> i=e.<a class="code" href="group__ExprPkg.html#gac890e13db184610276fc533fa4b4fe99" title="Begin iterator.">begin</a>(), iend=e.<a class="code" href="group__ExprPkg.html#gaf6048a5030c8fa2511bf5dfee868e653" title="End iterator.">end</a>(); i!=iend && cnf; ++i)
<a name="l00693"></a>00693 cnf = (*i).isAbsLiteral();
<a name="l00694"></a>00694 <span class="keywordflow">return</span> cnf;
<a name="l00695"></a>00695 }
<a name="l00696"></a>00696
<a name="l00697"></a>00697
<a name="l00698"></a>00698 <span class="keywordtype">bool</span>
<a name="l00699"></a><a class="code" href="group__SE.html#ga9db77121699fbbdbff209014b8ab26c3">00699</a> <a class="code" href="group__SE.html#ga9db77121699fbbdbff209014b8ab26c3" title="Check if e is a propositional clause.">SearchImplBase::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) {
<a name="l00700"></a>00700 <span class="keywordflow">if</span>(e.<a class="code" href="group__ExprPkg.html#gaccf96ea73570e38c5c7e4ad39ed8b509" title="PropAtom or negation of PropAtom.">isPropLiteral</a>()) <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00701"></a>00701 <span class="keywordflow">if</span>(!e.<a class="code" href="group__ExprPkg.html#ga36f1eff876808586db368dc1b6da5f56">isOr</a>()) <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00702"></a>00702
<a name="l00703"></a>00703 <span class="keywordtype">bool</span> cnf(<span class="keyword">true</span>);
<a name="l00704"></a>00704 <span class="keywordflow">for</span>(<a class="code" href="classCVC3_1_1Expr_1_1iterator.html">Expr::iterator</a> i=e.<a class="code" href="group__ExprPkg.html#gac890e13db184610276fc533fa4b4fe99" title="Begin iterator.">begin</a>(), iend=e.<a class="code" href="group__ExprPkg.html#gaf6048a5030c8fa2511bf5dfee868e653" title="End iterator.">end</a>(); i!=iend && cnf; ++i)
<a name="l00705"></a>00705 cnf = (*i).isPropLiteral();
<a name="l00706"></a>00706 <span class="keywordflow">return</span> cnf;
<a name="l00707"></a>00707 }
<a name="l00708"></a>00708
<a name="l00709"></a>00709
<a name="l00710"></a>00710 <span class="keywordtype">bool</span>
<a name="l00711"></a><a class="code" href="group__SE.html#gaed4079f44a18e496b87366ce65b20d99">00711</a> <a class="code" href="group__SE.html#gaed4079f44a18e496b87366ce65b20d99" title="Check if a splitter is required for completeness.">SearchImplBase::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="l00712"></a>00712 <span class="keywordflow">if</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="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00713"></a>00713 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"isGoodSplitter"</span>, <span class="stringliteral">"isGoodSplitter("</span>, e, <span class="stringliteral">") {"</span>);
<a name="l00714"></a>00714 <span class="comment">// Check for var being an auxiliary CNF variable</span>
<a name="l00715"></a>00715 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& var = e.<a class="code" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a>()? e[0] : e;
<a name="l00716"></a>00716 <span class="keywordtype">bool</span> res(!<a class="code" href="group__SE.html#ga92018736294ba073bc5db887467944ad" title="Check whether e is a fresh variable introduced by the CNF converter.">isCNFVar</a>(var));
<a name="l00717"></a>00717 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"isGoodSplitter"</span>, <span class="stringliteral">"isGoodSplitter => "</span>, res? <span class="stringliteral">"true"</span> : <span class="stringliteral">"false"</span>, <span class="stringliteral">" }"</span>);
<a name="l00718"></a>00718 <span class="keywordflow">return</span> res;
<a name="l00719"></a>00719 }
<a name="l00720"></a>00720
<a name="l00721"></a>00721
<a name="l00722"></a>00722 <span class="keywordtype">void</span>
<a name="l00723"></a><a class="code" href="group__SE.html#gaa78fb38536d0a2e34ad140f3ec865f2b">00723</a> <a class="code" href="group__SE.html#gaa78fb38536d0a2e34ad140f3ec865f2b" title="Cache a theorem phi <=> v by phi, where v is a literal.">SearchImplBase::addToCNFCache</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm) {
<a name="l00724"></a>00724 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"mycnf"</span>, <span class="stringliteral">"addToCNFCache("</span>, thm.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>(), <span class="stringliteral">")"</span>);
<a name="l00725"></a>00725
<a name="l00726"></a>00726 <a class="code" href="group__SE.html#ga3772c6af7eac91b9ed7fc278edf5ef90" title="Access to theory reasoning.">d_core</a>-><a class="code" href="classCVC3_1_1TheoryCore.html#a7f119c4fa5313b72feca7dd441e045f0">getStatistics</a>().<a class="code" href="classCVC3_1_1Statistics.html#a9b2503d33c8c41b768f40b1a43c2d3bf">counter</a>(<span class="stringliteral">"CNF New Vars"</span>)++;
<a name="l00727"></a>00727
<a name="l00728"></a>00728 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> result = thm;
<a name="l00729"></a>00729 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(result.<a class="code" href="classCVC3_1_1Theorem.html#a362c1d70e03803d804bbe300e5f6dc87">isRewrite</a>(),
<a name="l00730"></a>00730 <span class="stringliteral">"SearchImplBase::addToCNFCache: input must be an iff: "</span> +
<a name="l00731"></a>00731 result.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>().<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00732"></a>00732 <span class="comment">// Record the CNF variable</span>
<a name="l00733"></a>00733 <a class="code" href="group__SE.html#ga1c64a37d94b4cadedce29f3e4b98a3af" title="Backtracking set of new variables generated by CNF translator.">d_cnfVars</a>[thm.<a class="code" href="classCVC3_1_1Theorem.html#a97d957fcbf9094480851b1d2e5d3729f">getRHS</a>()] = <span class="keyword">true</span>;
<a name="l00734"></a>00734
<a name="l00735"></a>00735 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> t(thm);
<a name="l00736"></a>00736 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> phi = thm.<a class="code" href="classCVC3_1_1Theorem.html#a206c04f39fbbcacef2337148675553f4">getLHS</a>();
<a name="l00737"></a>00737 <span class="keywordflow">while</span>(phi.<a class="code" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a>()) {
<a name="l00738"></a>00738 t = <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#af38f25446a561384c3de66392c4d3544" title="e1 <=> e2 ==> ~e1 <=> ~e2">iffContrapositive</a>(thm);
<a name="l00739"></a>00739 phi = phi[0];
<a name="l00740"></a>00740 }
<a name="l00741"></a>00741 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="group__SE.html#gab60a7d204ed01875c98629e874575cd6" title="Backtracking cache for the CNF generator.">d_cnfCache</a>.<a class="code" href="classCVC3_1_1CDMap.html#af5f700035db0db798c645e36dd0b31bd">count</a>(phi) == 0,
<a name="l00742"></a>00742 <span class="stringliteral">"thm = "</span>+thm.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>().<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>() +
<a name="l00743"></a>00743 <span class="stringliteral">"\n t = "</span>+ t.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>().<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00744"></a>00744 <span class="comment">//d_cnfCache.insert(phi, t);</span>
<a name="l00745"></a>00745 <a class="code" href="group__SE.html#gab60a7d204ed01875c98629e874575cd6" title="Backtracking cache for the CNF generator.">d_cnfCache</a>.<a class="code" href="classCVC3_1_1CDMap.html#a664a15046de83b0af599f488cb420022">insert</a>(phi, t, <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="l00746"></a>00746 }
<a name="l00747"></a>00747
<a name="l00748"></a>00748
<a name="l00749"></a>00749 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l00750"></a><a class="code" href="group__SE.html#ga298ad740ab490d5b3337445573b8c4d7">00750</a> <a class="code" href="group__SE.html#ga298ad740ab490d5b3337445573b8c4d7" title="Find a theorem phi <=> v by phi, where v is a literal.">SearchImplBase::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="l00751"></a>00751 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"mycnf"</span>, <span class="stringliteral">"findInCNFCache("</span>, e, <span class="stringliteral">") { "</span>);
<a name="l00752"></a>00752 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> phi(e);
<a name="l00753"></a>00753
<a name="l00754"></a>00754 <span class="keywordtype">int</span> numNegs(0);
<a name="l00755"></a>00755 <span class="comment">// Strip all the top-level negations from e</span>
<a name="l00756"></a>00756 <span class="keywordflow">while</span>(phi.<a class="code" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a>()) {
<a name="l00757"></a>00757 phi = phi[0]; numNegs++;
<a name="l00758"></a>00758 }
<a name="l00759"></a>00759 <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr,Theorem>::iterator</a> it = <a class="code" href="group__SE.html#gab60a7d204ed01875c98629e874575cd6" title="Backtracking cache for the CNF generator.">d_cnfCache</a>.<a class="code" href="classCVC3_1_1CDMap.html#a1cadecbd2d6fa614a2f2e9419aa43f33">find</a>(phi);
<a name="l00760"></a>00760 <span class="keywordflow">if</span>(it != <a class="code" href="group__SE.html#gab60a7d204ed01875c98629e874575cd6" title="Backtracking cache for the CNF generator.">d_cnfCache</a>.<a class="code" href="classCVC3_1_1CDMap.html#a2a26c7cc4db12cb17d273db5cfa5a890">end</a>()) {
<a name="l00761"></a>00761 <span class="comment">// IF_DEBUG(debugger.counter("CNF cache hits")++;)</span>
<a name="l00762"></a>00762 <a class="code" href="group__SE.html#ga3772c6af7eac91b9ed7fc278edf5ef90" title="Access to theory reasoning.">d_core</a>-><a class="code" href="classCVC3_1_1TheoryCore.html#a7f119c4fa5313b72feca7dd441e045f0">getStatistics</a>().<a class="code" href="classCVC3_1_1Statistics.html#a9b2503d33c8c41b768f40b1a43c2d3bf">counter</a>(<span class="stringliteral">"CNF cache hits"</span>)++;
<a name="l00763"></a>00763 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> thm = (*it).second;
<a name="l00764"></a>00764
<a name="l00765"></a>00765 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(thm.<a class="code" href="classCVC3_1_1Theorem.html#a362c1d70e03803d804bbe300e5f6dc87">isRewrite</a>() && thm.<a class="code" href="classCVC3_1_1Theorem.html#a206c04f39fbbcacef2337148675553f4">getLHS</a>() == phi,
<a name="l00766"></a>00766 <span class="stringliteral">"SearchImplBase::findInCNFCache: thm must be an iff: "</span> +
<a name="l00767"></a>00767 thm.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>().<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00768"></a>00768
<a name="l00769"></a>00769 <span class="comment">// Now put all the negations back. If the number of negations is</span>
<a name="l00770"></a>00770 <span class="comment">// odd, first transform phi<=>v into !phi<=>!v. Then apply</span>
<a name="l00771"></a>00771 <span class="comment">// !!phi<=>phi rewrite as many times as needed.</span>
<a name="l00772"></a>00772 <span class="keywordflow">if</span>(numNegs % 2 != 0) {
<a name="l00773"></a>00773 thm = <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#af38f25446a561384c3de66392c4d3544" title="e1 <=> e2 ==> ~e1 <=> ~e2">iffContrapositive</a>(thm);
<a name="l00774"></a>00774 numNegs--;
<a name="l00775"></a>00775 }
<a name="l00776"></a>00776 <span class="keywordflow">for</span>(; numNegs > 0; numNegs-=2) {
<a name="l00777"></a>00777 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> t = <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#a8a04ff29591a019d4d4cf073c0987316" title="==> NOT NOT e IFF e, takes !!e">rewriteNotNot</a>(!!(thm.<a class="code" href="classCVC3_1_1Theorem.html#a206c04f39fbbcacef2337148675553f4">getLHS</a>()));
<a name="l00778"></a>00778 thm = <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#a4a4e90cd69ce24e83ba2c217907c277a" title=" (same for IFF)">transitivityRule</a>(t,thm);
<a name="l00779"></a>00779 }
<a name="l00780"></a>00780
<a name="l00781"></a>00781 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(numNegs == 0, <span class="stringliteral">"numNegs = "</span>+<a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(numNegs));
<a name="l00782"></a>00782 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"mycnf"</span>, <span class="stringliteral">"findInCNFCache => "</span>, thm.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>(), <span class="stringliteral">" }"</span>);
<a name="l00783"></a>00783 <span class="keywordflow">return</span> thm;
<a name="l00784"></a>00784 }
<a name="l00785"></a>00785 <a class="code" href="debug_8h.html#ad64155edafde9f067f4868817cd04bdf">TRACE_MSG</a>(<span class="stringliteral">"mycnf"</span>, <span class="stringliteral">"findInCNFCache => null }"</span>);
<a name="l00786"></a>00786 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>();
<a name="l00787"></a>00787 }
<a name="l00788"></a>00788 <span class="comment"></span>
<a name="l00789"></a>00789 <span class="comment">/*!</span>
<a name="l00790"></a>00790 <span class="comment"> * Strategy:</span>
<a name="l00791"></a>00791 <span class="comment"> *</span>
<a name="l00792"></a>00792 <span class="comment"> * For a given atomic formula phi(ite(c, t1, t2)) which depends on a</span>
<a name="l00793"></a>00793 <span class="comment"> * term ITE, generate an equisatisfiable formula:</span>
<a name="l00794"></a>00794 <span class="comment"> *</span>
<a name="l00795"></a>00795 <span class="comment"> * phi(x) & ite(c, t1=x, t2=x),</span>
<a name="l00796"></a>00796 <span class="comment"> *</span>
<a name="l00797"></a>00797 <span class="comment"> * where x is a new variable.</span>
<a name="l00798"></a>00798 <span class="comment"> *</span>
<a name="l00799"></a>00799 <span class="comment"> * The phi(x) part will be generated by the caller, and our job is to</span>
<a name="l00800"></a>00800 <span class="comment"> * assert the 'ite(c, t1=x, t2=x)', and return a rewrite theorem</span>
<a name="l00801"></a>00801 <span class="comment"> * phi(ite(c, t1, t2)) <=> phi(x).</span>
<a name="l00802"></a>00802 <span class="comment"> */</span>
<a name="l00803"></a>00803 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l00804"></a><a class="code" href="group__SE.html#ga687e32d21d7fe7e4b26873ae86a47ae5">00804</a> <a class="code" href="group__SE.html#ga687e32d21d7fe7e4b26873ae86a47ae5" title="Replaces ITE subexpressions in e with variables.">SearchImplBase::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="l00805"></a>00805 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"replaceITE"</span>,<span class="stringliteral">"replaceITE("</span>, e, <span class="stringliteral">") { "</span>);
<a name="l00806"></a>00806 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> res;
<a name="l00807"></a>00807
<a name="l00808"></a>00808 <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr,Theorem>::iterator</a> i=<a class="code" href="group__SE.html#ga0c829909b9e3ab2b59ba40e681905c4b" title="Cache for replaceITE()">d_replaceITECache</a>.<a class="code" href="classCVC3_1_1CDMap.html#a1cadecbd2d6fa614a2f2e9419aa43f33">find</a>(e),
<a name="l00809"></a>00809 iend=<a class="code" href="group__SE.html#ga0c829909b9e3ab2b59ba40e681905c4b" title="Cache for replaceITE()">d_replaceITECache</a>.<a class="code" href="classCVC3_1_1CDMap.html#a2a26c7cc4db12cb17d273db5cfa5a890">end</a>();
<a name="l00810"></a>00810 <span class="keywordflow">if</span>(i!=iend) {
<a name="l00811"></a>00811 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"replaceITE"</span>, <span class="stringliteral">"replaceITE[cached] => "</span>, (*i).second, <span class="stringliteral">" }"</span>);
<a name="l00812"></a>00812 <span class="keywordflow">return</span> (*i).second;
<a name="l00813"></a>00813 }
<a name="l00814"></a>00814
<a name="l00815"></a>00815 <span class="keywordflow">if</span>(e.<a class="code" href="group__ExprPkg.html#gaac535dae48f02fcd093a5b1b1a062211" title="Test if e is an abstract literal.">isAbsLiteral</a>())
<a name="l00816"></a>00816 res = <a class="code" href="group__SE.html#ga3772c6af7eac91b9ed7fc278edf5ef90" title="Access to theory reasoning.">d_core</a>-><a class="code" href="classCVC3_1_1TheoryCore.html#a586e77e855946fd0b5f541ec06f7decd" title="Called by search engine.">rewriteLiteral</a>(e);
<a name="l00817"></a>00817 <span class="keywordflow">else</span>
<a name="l00818"></a>00818 res = <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#a61c1fe56b4ed9744006883a7784ddb71">reflexivityRule</a>(e);
<a name="l00819"></a>00819
<a name="l00820"></a>00820
<a name="l00821"></a>00821 <span class="comment">// If 'res' is e<=>phi, and the resulting formula phi is not a</span>
<a name="l00822"></a>00822 <span class="comment">// literal, introduce a new variable x, enqueue phi<=>x, and return</span>
<a name="l00823"></a>00823 <span class="comment">// e<=>x.</span>
<a name="l00824"></a>00824 <span class="keywordflow">if</span>(!res.<a class="code" href="classCVC3_1_1Theorem.html#a97d957fcbf9094480851b1d2e5d3729f">getRHS</a>().<a class="code" href="group__ExprPkg.html#gaccf96ea73570e38c5c7e4ad39ed8b509" title="PropAtom or negation of PropAtom.">isPropLiteral</a>()) {
<a name="l00825"></a>00825 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> varThm(<a class="code" href="group__SE.html#ga298ad740ab490d5b3337445573b8c4d7" title="Find a theorem phi <=> v by phi, where v is a literal.">findInCNFCache</a>(res.<a class="code" href="classCVC3_1_1Theorem.html#a97d957fcbf9094480851b1d2e5d3729f">getRHS</a>()));
<a name="l00826"></a>00826 <span class="keywordflow">if</span>(varThm.<a class="code" href="classCVC3_1_1Theorem.html#afc6fdb0507eb3669e28d9be5ed0bd333">isNull</a>()) {
<a name="l00827"></a>00827 varThm = <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#a10fa187373ec24079c10874d8e804ecb" title="Retrun a theorem "|- e = v" for a new Skolem constant v.">varIntroSkolem</a>(res.<a class="code" href="classCVC3_1_1Theorem.html#a97d957fcbf9094480851b1d2e5d3729f">getRHS</a>());
<a name="l00828"></a>00828 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> var;
<a name="l00829"></a>00829 <span class="keywordflow">if</span>(res.<a class="code" href="classCVC3_1_1Theorem.html#a362c1d70e03803d804bbe300e5f6dc87">isRewrite</a>())
<a name="l00830"></a>00830 var = <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#a4a4e90cd69ce24e83ba2c217907c277a" title=" (same for IFF)">transitivityRule</a>(res,varThm);
<a name="l00831"></a>00831 <span class="keywordflow">else</span>
<a name="l00832"></a>00832 var = <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#aebbcd4a194e4fdca0bcd16143fb03a75">iffMP</a>(res,varThm);
<a name="l00833"></a>00833 <span class="comment">//d_cnfVars[var.getExpr()] = true;</span>
<a name="l00834"></a>00834 <span class="comment">//addCNFFact(var);</span>
<a name="l00835"></a>00835 <a class="code" href="group__SE.html#gaa78fb38536d0a2e34ad140f3ec865f2b" title="Cache a theorem phi <=> v by phi, where v is a literal.">addToCNFCache</a>(varThm);
<a name="l00836"></a>00836 }
<a name="l00837"></a>00837 <a class="code" href="group__SE.html#gaa7bf3c385bae481d4ea35179e818a09a" title="FIXME: write a comment.">applyCNFRules</a>(varThm);
<a name="l00838"></a>00838 <span class="comment">//enqueueCNFrec(varThm);</span>
<a name="l00839"></a>00839 res = <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>-><a class="code" href="classCVC3_1_1CommonProofRules.html#a4a4e90cd69ce24e83ba2c217907c277a" title=" (same for IFF)">transitivityRule</a>(res, varThm);
<a name="l00840"></a>00840 }
<a name="l00841"></a>00841
<a name="l00842"></a>00842 <a class="code" href="group__SE.html#ga0c829909b9e3ab2b59ba40e681905c4b" title="Cache for replaceITE()">d_replaceITECache</a>[e] = res;
<a name="l00843"></a>00843
<a name="l00844"></a>00844 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"replaceITE"</span>, <span class="stringliteral">"replaceITE => "</span>, res, <span class="stringliteral">" }"</span>);
<a name="l00845"></a>00845 <span class="keywordflow">return</span> res;
<a name="l00846"></a>00846 }
</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>
