<!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_sat.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_sat.cpp</div> </div>
</div>
<div class="contents">
<a href="search__sat_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_sat.cpp</span>
<a name="l00004"></a>00004 <span class="comment"> *\brief Implementation of Search engine with generic external sat solver</span>
<a name="l00005"></a>00005 <span class="comment"> *</span>
<a name="l00006"></a>00006 <span class="comment"> * Author: Clark Barrett</span>
<a name="l00007"></a>00007 <span class="comment"> *</span>
<a name="l00008"></a>00008 <span class="comment"> * Created: Wed Dec 7 21:00:24 2005</span>
<a name="l00009"></a>00009 <span class="comment"> *</span>
<a name="l00010"></a>00010 <span class="comment"> * <hr></span>
<a name="l00011"></a>00011 <span class="comment"> *</span>
<a name="l00012"></a>00012 <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span>
<a name="l00013"></a>00013 <span class="comment"> * and its documentation for any purpose is hereby granted without</span>
<a name="l00014"></a>00014 <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span>
<a name="l00015"></a>00015 <span class="comment"> * LICENSE file provided with this distribution.</span>
<a name="l00016"></a>00016 <span class="comment"> * </span>
<a name="l00017"></a>00017 <span class="comment"> * <hr></span>
<a name="l00018"></a>00018 <span class="comment"> */</span>
<a name="l00019"></a>00019 <span class="comment">/*****************************************************************************/</span>
<a name="l00020"></a>00020
<a name="l00021"></a>00021
<a name="l00022"></a>00022 <span class="preprocessor">#include "<a class="code" href="search__sat_8h.html" title="Search engine that uses an external SAT engine.">search_sat.h</a>"</span>
<a name="l00023"></a>00023 <span class="preprocessor">#ifdef DPLL_BASIC</span>
<a name="l00024"></a>00024 <span class="preprocessor"></span><span class="preprocessor">#include "<a class="code" href="dpllt__basic_8h.html" title="Basic implementation of dpllt module.">dpllt_basic.h</a>"</span>
<a name="l00025"></a>00025 <span class="preprocessor">#endif</span>
<a name="l00026"></a>00026 <span class="preprocessor"></span><span class="preprocessor">#include "<a class="code" href="dpllt__minisat_8h.html" title="Implementation of dpllt module based on minisat.">dpllt_minisat.h</a>"</span>
<a name="l00027"></a>00027 <span class="preprocessor">#include "<a class="code" href="theory__core_8h.html">theory_core.h</a>"</span>
<a name="l00028"></a>00028 <span class="preprocessor">#include "<a class="code" href="eval__exception_8h.html">eval_exception.h</a>"</span>
<a name="l00029"></a>00029 <span class="preprocessor">#include "<a class="code" href="typecheck__exception_8h.html" title="An exception to be thrown at typecheck error.">typecheck_exception.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="search__rules_8h.html" title="Abstract proof rules interface to the simple search engine.">search_rules.h</a>"</span>
<a name="l00032"></a>00032 <span class="preprocessor">#include "<a class="code" href="command__line__flags_8h.html">command_line_flags.h</a>"</span>
<a name="l00033"></a>00033 <span class="preprocessor">#include "<a class="code" href="theorem__manager_8h.html">theorem_manager.h</a>"</span>
<a name="l00034"></a>00034 <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="l00035"></a>00035 <span class="preprocessor">#include "<a class="code" href="debug_8h.html" title="Description: Collection of debugging macros and functions.">debug.h</a>"</span>
<a name="l00036"></a>00036
<a name="l00037"></a>00037
<a name="l00038"></a>00038 <span class="keyword">using namespace </span>std;
<a name="l00039"></a>00039 <span class="keyword">using namespace </span>CVC3;
<a name="l00040"></a>00040 <span class="keyword">using namespace </span>SAT;
<a name="l00041"></a>00041
<a name="l00042"></a>00042
<a name="l00043"></a>00043 <span class="keyword">namespace </span>CVC3 {
<a name="l00044"></a>00044
<a name="l00045"></a>00045
<a name="l00046"></a><a class="code" href="classCVC3_1_1SearchSatCoreSatAPI.html">00046</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1SearchSatCoreSatAPI.html">SearchSatCoreSatAPI</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="l00047"></a><a class="code" href="classCVC3_1_1SearchSatCoreSatAPI.html#ae81499ebac0b86e35ff1bcb79a7dc1e2">00047</a> <a class="code" href="classCVC3_1_1SearchSat.html" title="Search engine that connects to a generic SAT reasoning module.">SearchSat</a>* <a class="code" href="classCVC3_1_1SearchSatCoreSatAPI.html#ae81499ebac0b86e35ff1bcb79a7dc1e2">d_ss</a>;
<a name="l00048"></a>00048 <span class="keyword">public</span>:
<a name="l00049"></a><a class="code" href="classCVC3_1_1SearchSatCoreSatAPI.html#a6609c8ddc5e6273087b0171d3e3a6141">00049</a> <a class="code" href="classCVC3_1_1SearchSatCoreSatAPI.html#a6609c8ddc5e6273087b0171d3e3a6141">SearchSatCoreSatAPI</a>(<a class="code" href="classCVC3_1_1SearchSat.html" title="Search engine that connects to a generic SAT reasoning module.">SearchSat</a>* ss) : d_ss(ss) {}
<a name="l00050"></a><a class="code" href="classCVC3_1_1SearchSatCoreSatAPI.html#a5a1b12f3189fb9cd97d9694515bd4ae7">00050</a> <a class="code" href="classCVC3_1_1SearchSatCoreSatAPI.html#a5a1b12f3189fb9cd97d9694515bd4ae7">~SearchSatCoreSatAPI</a>() {}
<a name="l00051"></a><a class="code" href="classCVC3_1_1SearchSatCoreSatAPI.html#ae2f398e9ebdca22f7dbbe12380f34151">00051</a> <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="l00052"></a>00052 { d_ss->addLemma(thm, priority, atBottomScope); }
<a name="l00053"></a><a class="code" href="classCVC3_1_1SearchSatCoreSatAPI.html#a09cc89d4a36875de81fbd58b1c35f7bf">00053</a> <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="l00054"></a>00054 { <span class="keywordflow">return</span> d_ss->newUserAssumption(assump); }
<a name="l00055"></a><a class="code" href="classCVC3_1_1SearchSatCoreSatAPI.html#a17e68b9c4e83489e11099b9f5f60be63">00055</a> <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="l00056"></a>00056 { d_ss->addSplitter(e, priority); }
<a name="l00057"></a>00057 <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="l00058"></a>00058
<a name="l00059"></a>00059 };
<a name="l00060"></a>00060
<a name="l00061"></a>00061
<a name="l00062"></a><a class="code" href="classCVC3_1_1SearchSatCoreSatAPI.html#a20b83a72494dd9dec49f37457e2ac5ac">00062</a> <span class="keywordtype">bool</span> SearchSatCoreSatAPI::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="l00063"></a>00063 {
<a name="l00064"></a>00064 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> thm;
<a name="l00065"></a>00065 d_ss->push();
<a name="l00066"></a>00066 <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> res = d_ss->check(e, thm);
<a name="l00067"></a>00067 d_ss->pop();
<a name="l00068"></a>00068 <span class="keywordflow">return</span> res == <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498ba24f8f4860dbe6fd65883a9d7cbd2f576">VALID</a>;
<a name="l00069"></a>00069 }
<a name="l00070"></a>00070
<a name="l00071"></a>00071
<a name="l00072"></a><a class="code" href="classCVC3_1_1SearchSatTheoryAPI.html">00072</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1SearchSatTheoryAPI.html">SearchSatTheoryAPI</a> :<span class="keyword">public</span> <a class="code" href="classSAT_1_1DPLLT.html">DPLLT</a>::TheoryAPI {
<a name="l00073"></a><a class="code" href="classCVC3_1_1SearchSatTheoryAPI.html#a23c983838f09ca499abe23c09381292c">00073</a> <a class="code" href="classCVC3_1_1ContextManager.html" title="Manager for multiple contexts. Also holds current context.">ContextManager</a>* <a class="code" href="classCVC3_1_1SearchSatTheoryAPI.html#a23c983838f09ca499abe23c09381292c">d_cm</a>;
<a name="l00074"></a><a class="code" href="classCVC3_1_1SearchSatTheoryAPI.html#ac1c134629294189ad3728762588c51cd">00074</a> <a class="code" href="classCVC3_1_1SearchSat.html" title="Search engine that connects to a generic SAT reasoning module.">SearchSat</a>* <a class="code" href="classCVC3_1_1SearchSatTheoryAPI.html#ac1c134629294189ad3728762588c51cd">d_ss</a>;
<a name="l00075"></a>00075 <span class="keyword">public</span>:
<a name="l00076"></a><a class="code" href="classCVC3_1_1SearchSatTheoryAPI.html#ae37ebadf06bdc0116ff7850bc2ea5dc6">00076</a> <a class="code" href="classCVC3_1_1SearchSatTheoryAPI.html">SearchSatTheoryAPI</a>(<a class="code" href="classCVC3_1_1SearchSat.html" title="Search engine that connects to a generic SAT reasoning module.">SearchSat</a>* ss)
<a name="l00077"></a>00077 : d_cm(ss->theoryCore()->getCM()), d_ss(ss) {}
<a name="l00078"></a><a class="code" href="classCVC3_1_1SearchSatTheoryAPI.html#a4fe19299e276955c5c2f653510b98ef3">00078</a> <a class="code" href="classCVC3_1_1SearchSatTheoryAPI.html#a4fe19299e276955c5c2f653510b98ef3">~SearchSatTheoryAPI</a>() {}
<a name="l00079"></a><a class="code" href="classCVC3_1_1SearchSatTheoryAPI.html#ab315cba0a7157225c0355b1136b511fc">00079</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchSatTheoryAPI.html#ab315cba0a7157225c0355b1136b511fc" title="Set a checkpoint for backtracking.">push</a>() { <span class="keywordflow">return</span> d_cm->push(); }
<a name="l00080"></a><a class="code" href="classCVC3_1_1SearchSatTheoryAPI.html#a22e462ee6d70a81cdf6610921068c9ed">00080</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchSatTheoryAPI.html#a22e462ee6d70a81cdf6610921068c9ed" title="Restore most recent checkpoint.">pop</a>() { <span class="keywordflow">return</span> d_cm->pop(); }
<a name="l00081"></a><a class="code" href="classCVC3_1_1SearchSatTheoryAPI.html#a11363a1236f9d2520119a0d4533087a6">00081</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchSatTheoryAPI.html#a11363a1236f9d2520119a0d4533087a6" title="Notify theory when a literal is set to true.">assertLit</a>(<a class="code" href="classSAT_1_1Lit.html">Lit</a> l) { d_ss->assertLit(l); }
<a name="l00082"></a><a class="code" href="classCVC3_1_1SearchSatTheoryAPI.html#a5f294c37fc9ba581b542a0639e47865f">00082</a> <a class="code" href="classSAT_1_1DPLLT.html#ac612908684032ffe76ad97f04afd0ca8">SAT::DPLLT::ConsistentResult</a> checkConsistent(<a class="code" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a>& cnf, <span class="keywordtype">bool</span> fullEffort)
<a name="l00083"></a>00083 { <span class="keywordflow">return</span> d_ss->checkConsistent(cnf, fullEffort); }
<a name="l00084"></a><a class="code" href="classCVC3_1_1SearchSatTheoryAPI.html#aad2fecc1799c5b79199995cf02fcd3fb">00084</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1SearchSatTheoryAPI.html#aad2fecc1799c5b79199995cf02fcd3fb" title="Check if the work budget has been exceeded.">outOfResources</a>() { <span class="keywordflow">return</span> d_ss->theoryCore()->outOfResources(); }
<a name="l00085"></a><a class="code" href="classCVC3_1_1SearchSatTheoryAPI.html#a06f33ae2c4b9020c9dd5c05b4dc3345f">00085</a> <a class="code" href="classSAT_1_1Lit.html">Lit</a> <a class="code" href="classCVC3_1_1SearchSatTheoryAPI.html#a06f33ae2c4b9020c9dd5c05b4dc3345f" title="Get a literal that is implied by the current assignment.">getImplication</a>() { <span class="keywordflow">return</span> d_ss->getImplication(); }
<a name="l00086"></a><a class="code" href="classCVC3_1_1SearchSatTheoryAPI.html#a5faff1f37c64447f406fbd6c377f6cd2">00086</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchSatTheoryAPI.html#a5faff1f37c64447f406fbd6c377f6cd2" title="Get an explanation for a literal that was implied.">getExplanation</a>(<a class="code" href="classSAT_1_1Lit.html">Lit</a> l, <a class="code" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a>& cnf) { <span class="keywordflow">return</span> d_ss->getExplanation(l, cnf); }
<a name="l00087"></a><a class="code" href="classCVC3_1_1SearchSatTheoryAPI.html#a2e715dfb82483c9a78e80eea7dbb97aa">00087</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1SearchSatTheoryAPI.html#a2e715dfb82483c9a78e80eea7dbb97aa" title="Get new clauses from the theory.">getNewClauses</a>(<a class="code" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a>& cnf) { <span class="keywordflow">return</span> d_ss->getNewClauses(cnf); }
<a name="l00088"></a>00088 };
<a name="l00089"></a>00089
<a name="l00090"></a>00090
<a name="l00091"></a><a class="code" href="classCVC3_1_1SearchSatDecider.html">00091</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1SearchSatDecider.html">SearchSatDecider</a> :<span class="keyword">public</span> <a class="code" href="classSAT_1_1DPLLT.html">DPLLT</a>::Decider {
<a name="l00092"></a><a class="code" href="classCVC3_1_1SearchSatDecider.html#a1f0f6fe9b711ecc89ac06edfe1c52aed">00092</a> <a class="code" href="classCVC3_1_1SearchSat.html" title="Search engine that connects to a generic SAT reasoning module.">SearchSat</a>* <a class="code" href="classCVC3_1_1SearchSatDecider.html#a1f0f6fe9b711ecc89ac06edfe1c52aed">d_ss</a>;
<a name="l00093"></a>00093 <span class="keyword">public</span>:
<a name="l00094"></a><a class="code" href="classCVC3_1_1SearchSatDecider.html#aea531ab8aa5fe7c8ebdd094585ac862d">00094</a> <a class="code" href="classCVC3_1_1SearchSatDecider.html#aea531ab8aa5fe7c8ebdd094585ac862d">SearchSatDecider</a>(<a class="code" href="classCVC3_1_1SearchSat.html" title="Search engine that connects to a generic SAT reasoning module.">SearchSat</a>* ss) : d_ss(ss) {}
<a name="l00095"></a><a class="code" href="classCVC3_1_1SearchSatDecider.html#a53dcf26ae3f6000c25fd41f7cfb6a15f">00095</a> <a class="code" href="classCVC3_1_1SearchSatDecider.html#a53dcf26ae3f6000c25fd41f7cfb6a15f">~SearchSatDecider</a>() {}
<a name="l00096"></a>00096
<a name="l00097"></a><a class="code" href="classCVC3_1_1SearchSatDecider.html#ad58d3667503de13c9921d751f8663e00">00097</a> <a class="code" href="classSAT_1_1Lit.html">Lit</a> <a class="code" href="classCVC3_1_1SearchSatDecider.html#ad58d3667503de13c9921d751f8663e00" title="Make a decision.">makeDecision</a>() { <span class="keywordflow">return</span> d_ss->makeDecision(); }
<a name="l00098"></a>00098 };
<a name="l00099"></a>00099
<a name="l00100"></a>00100
<a name="l00101"></a><a class="code" href="classCVC3_1_1SearchSatCNFCallback.html">00101</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1SearchSatCNFCallback.html">SearchSatCNFCallback</a> :<span class="keyword">public</span> <a class="code" href="classSAT_1_1CNF__Manager.html">CNF_Manager</a>::CNFCallback {
<a name="l00102"></a><a class="code" href="classCVC3_1_1SearchSatCNFCallback.html#a5b4909ba2c06dbe79d2c38f61958cbb0">00102</a> <a class="code" href="classCVC3_1_1SearchSat.html" title="Search engine that connects to a generic SAT reasoning module.">SearchSat</a>* <a class="code" href="classCVC3_1_1SearchSatCNFCallback.html#a5b4909ba2c06dbe79d2c38f61958cbb0">d_ss</a>;
<a name="l00103"></a>00103 <span class="keyword">public</span>:
<a name="l00104"></a><a class="code" href="classCVC3_1_1SearchSatCNFCallback.html#a62053b1f6dfa61fb0f2ab225b2886580">00104</a> <a class="code" href="classCVC3_1_1SearchSatCNFCallback.html#a62053b1f6dfa61fb0f2ab225b2886580">SearchSatCNFCallback</a>(<a class="code" href="classCVC3_1_1SearchSat.html" title="Search engine that connects to a generic SAT reasoning module.">SearchSat</a>* ss) : d_ss(ss) {}
<a name="l00105"></a><a class="code" href="classCVC3_1_1SearchSatCNFCallback.html#a0a5b3b1176357230a9e6055e13b521c9">00105</a> <a class="code" href="classCVC3_1_1SearchSatCNFCallback.html#a0a5b3b1176357230a9e6055e13b521c9">~SearchSatCNFCallback</a>() {}
<a name="l00106"></a>00106
<a name="l00107"></a><a class="code" href="classCVC3_1_1SearchSatCNFCallback.html#aedf8407f7bd6e3b1eceba553acd5bbf9">00107</a> <span class="keywordtype">void</span> registerAtom(<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="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm)
<a name="l00108"></a>00108 { d_ss->theoryCore()->theoryOf(e)->registerAtom(e, thm); }
<a name="l00109"></a>00109 };
<a name="l00110"></a>00110
<a name="l00111"></a>00111
<a name="l00112"></a>00112 }
<a name="l00113"></a>00113
<a name="l00114"></a>00114
<a name="l00115"></a><a class="code" href="classCVC3_1_1SearchSat.html#aff33fe25d0761167062aa871e1992ded">00115</a> <span class="keywordtype">void</span> SearchSat::restorePre()
<a name="l00116"></a>00116 {
<a name="l00117"></a>00117 <span class="keywordflow">if</span> (d_core->getCM()->scopeLevel() == d_bottomScope) {
<a name="l00118"></a>00118 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(d_prioritySetBottomEntriesSizeStack.size() > 0, <span class="stringliteral">"Expected non-empty stack"</span>);
<a name="l00119"></a>00119 d_prioritySetBottomEntriesSize = d_prioritySetBottomEntriesSizeStack.back();
<a name="l00120"></a>00120 d_prioritySetBottomEntriesSizeStack.pop_back();
<a name="l00121"></a>00121 <span class="keywordflow">while</span> (d_prioritySetBottomEntriesSize < d_prioritySetBottomEntries.size()) {
<a name="l00122"></a>00122 d_prioritySet.erase(d_prioritySetBottomEntries.back());
<a name="l00123"></a>00123 d_prioritySetBottomEntries.pop_back();
<a name="l00124"></a>00124 }
<a name="l00125"></a>00125 }
<a name="l00126"></a>00126 }
<a name="l00127"></a>00127
<a name="l00128"></a>00128
<a name="l00129"></a><a class="code" href="classCVC3_1_1SearchSat.html#a41d79aff18a635a5cdc2c789bb784a0a">00129</a> <span class="keywordtype">void</span> SearchSat::restore()
<a name="l00130"></a>00130 {
<a name="l00131"></a>00131 <span class="keywordflow">while</span> (d_prioritySetEntriesSize < d_prioritySetEntries.size()) {
<a name="l00132"></a>00132 d_prioritySet.erase(d_prioritySetEntries.back());
<a name="l00133"></a>00133 d_prioritySetEntries.pop_back();
<a name="l00134"></a>00134 }
<a name="l00135"></a>00135 <span class="keywordflow">while</span> (d_pendingLemmasSize < d_pendingLemmas.size()) {
<a name="l00136"></a>00136 d_pendingLemmas.pop_back();
<a name="l00137"></a>00137 d_pendingScopes.pop_back();
<a name="l00138"></a>00138 }
<a name="l00139"></a>00139 <span class="keywordflow">while</span> (d_varsUndoListSize < d_varsUndoList.size()) {
<a name="l00140"></a>00140 d_vars[d_varsUndoList.back()] = <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">SAT::Var::UNKNOWN</a>;
<a name="l00141"></a>00141 d_varsUndoList.pop_back();
<a name="l00142"></a>00142 }
<a name="l00143"></a>00143 }
<a name="l00144"></a>00144
<a name="l00145"></a>00145
<a name="l00146"></a><a class="code" href="classCVC3_1_1SearchSat.html#a0f3b2311296e520c22aea55c68c4b477">00146</a> <span class="keywordtype">bool</span> SearchSat::recordNewRootLit(<a class="code" href="classSAT_1_1Lit.html">Lit</a> lit, <span class="keywordtype">int</span> priority, <span class="keywordtype">bool</span> atBottomScope)
<a name="l00147"></a>00147 {
<a name="l00148"></a>00148 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(d_prioritySetEntriesSize == d_prioritySetEntries.size() &&
<a name="l00149"></a>00149 d_prioritySetBottomEntriesSize == d_prioritySetBottomEntries.size(),
<a name="l00150"></a>00150 <span class="stringliteral">"Size mismatch"</span>);
<a name="l00151"></a>00151 pair<set<LitPriorityPair>::iterator,<span class="keywordtype">bool</span>> status =
<a name="l00152"></a>00152 d_prioritySet.insert(<a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html" title="Pair of Lit and priority of this Lit.">LitPriorityPair</a>(lit, priority));
<a name="l00153"></a>00153 <span class="keywordflow">if</span> (!status.second) <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00154"></a>00154 <span class="keywordflow">if</span> (!atBottomScope || d_bottomScope == d_core->getCM()->scopeLevel()) {
<a name="l00155"></a>00155 d_prioritySetEntries.push_back(status.first);
<a name="l00156"></a>00156 d_prioritySetEntriesSize = d_prioritySetEntriesSize + 1;
<a name="l00157"></a>00157 }
<a name="l00158"></a>00158 <span class="keywordflow">else</span> {
<a name="l00159"></a>00159 d_prioritySetBottomEntries.push_back(status.first);
<a name="l00160"></a>00160 ++d_prioritySetBottomEntriesSize;
<a name="l00161"></a>00161 }
<a name="l00162"></a>00162
<a name="l00163"></a>00163 <span class="keywordflow">if</span> (d_prioritySetStart.get() == d_prioritySet.end() ||
<a name="l00164"></a>00164 ((*status.first) < (*(d_prioritySetStart.get()))))
<a name="l00165"></a>00165 d_prioritySetStart = status.first;
<a name="l00166"></a>00166 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00167"></a>00167 }
<a name="l00168"></a>00168
<a name="l00169"></a>00169
<a name="l00170"></a><a class="code" href="classCVC3_1_1SearchSat.html#ad7abbaa4ca4528eb0cdfcbce26d05ea4">00170</a> <span class="keywordtype">void</span> SearchSat::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="l00171"></a>00171 {
<a name="l00172"></a>00172 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(
<a name="l00173"></a>00173 <span class="keywordtype">string</span> indentStr(theoryCore()->getCM()->scopeLevel(), <span class="charliteral">' '</span>);
<a name="l00174"></a>00174 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"addLemma"</span>, indentStr, <span class="stringliteral">"AddLemma: "</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 class="code" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0eaa315c228d5c3290ce37df81524ed8e9a" title="Nice SAL-like language for manually written specs.">PRESENTATION_LANG</a>));
<a name="l00175"></a>00175 )
<a name="l00176"></a>00176 <span class="comment">// DebugAssert(!thm.getExpr().isAbsLiteral(), "Expected non-literal");</span>
<a name="l00177"></a>00177 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(d_pendingLemmasSize == d_pendingLemmas.size(), <span class="stringliteral">"Size mismatch"</span>);
<a name="l00178"></a>00178 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(d_pendingLemmasSize == d_pendingScopes.size(), <span class="stringliteral">"Size mismatch"</span>);
<a name="l00179"></a>00179 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(d_pendingLemmasNext <= d_pendingLemmas.size(), <span class="stringliteral">"Size mismatch"</span>);
<a name="l00180"></a>00180 d_pendingLemmas.push_back(pair<Theorem,int>(thm, priority));
<a name="l00181"></a>00181 d_pendingScopes.push_back(atBottomScope);
<a name="l00182"></a>00182 d_pendingLemmasSize = d_pendingLemmasSize + 1;
<a name="l00183"></a>00183 }
<a name="l00184"></a>00184
<a name="l00185"></a>00185
<a name="l00186"></a><a class="code" href="classCVC3_1_1SearchSat.html#a98359a6ceb891ac5d12030aa42210b3d">00186</a> <span class="keywordtype">void</span> SearchSat::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="l00187"></a>00187 {
<a name="l00188"></a>00188 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!e.<a class="code" href="group__ExprPkg.html#gac4af2026c180da0f18d66ac616f61f3a">isEq</a>() || e[0] != e[1], <span class="stringliteral">"Expected non-trivial splitter"</span>);
<a name="l00189"></a>00189 addLemma(d_commonRules->excludedMiddle(e), priority);
<a name="l00190"></a>00190 }
<a name="l00191"></a>00191
<a name="l00192"></a>00192
<a name="l00193"></a><a class="code" href="classCVC3_1_1SearchSat.html#a14cf6695839ff6ac2a0fc0f134c26d47">00193</a> <span class="keywordtype">void</span> SearchSat::assertLit(<a class="code" href="classSAT_1_1Lit.html">Lit</a> l)
<a name="l00194"></a>00194 {
<a name="l00195"></a>00195 <span class="comment">// DebugAssert(d_inCheckSat, "Should only be used as a call-back");</span>
<a name="l00196"></a>00196 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e = d_cnfManager->concreteLit(l);
<a name="l00197"></a>00197
<a name="l00198"></a>00198 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(
<a name="l00199"></a>00199 <span class="keywordtype">string</span> indentStr(theoryCore()->getCM()->scopeLevel(), <span class="charliteral">' '</span>);
<a name="l00200"></a>00200 <span class="keywordtype">string</span> val = <span class="stringliteral">" := "</span>;
<a name="l00201"></a>00201
<a name="l00202"></a>00202 std::stringstream ss;
<a name="l00203"></a>00203 ss<<theoryCore()->getCM()->scopeLevel();
<a name="l00204"></a>00204 std::string temp;
<a name="l00205"></a>00205 ss>>temp;
<a name="l00206"></a>00206
<a name="l00207"></a>00207 <span class="keywordflow">if</span> (l.<a class="code" href="classSAT_1_1Lit.html#ada14f3ca2b88500b5c2500d60e7f554b">isPositive</a>()) val += <span class="stringliteral">"1"</span>; <span class="keywordflow">else</span> val += <span class="stringliteral">"0"</span>;
<a name="l00208"></a>00208 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"assertLit"</span>, <span class="stringliteral">""</span>, <span class="stringliteral">""</span>, <span class="stringliteral">""</span>);
<a name="l00209"></a>00209 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"assertLitScope"</span>, indentStr, <span class="stringliteral">"Scope level = "</span>, temp);
<a name="l00210"></a>00210 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"assertLit"</span>, indentStr, l.<a class="code" href="classSAT_1_1Lit.html#a57e2e6e37cad9595c3edbea88a41262f">getVar</a>(), val+<span class="stringliteral">": "</span>+e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00211"></a>00211 )
<a name="l00212"></a>00212
<a name="l00213"></a>00213 <span class="comment">//=======</span>
<a name="l00214"></a>00214 <span class="comment">// IF_DEBUG(</span>
<a name="l00215"></a>00215 <span class="comment">// string indentStr(theoryCore()->getCM()->scopeLevel(), ' ');</span>
<a name="l00216"></a>00216 <span class="comment">// string val = " := ";</span>
<a name="l00217"></a>00217 <span class="comment">// if (l.isPositive()) val += "1"; else val += "0";</span>
<a name="l00218"></a>00218 <span class="comment">// TRACE("assertLit", indentStr, l.getVar(), val);</span>
<a name="l00219"></a>00219 <span class="comment">// )</span>
<a name="l00220"></a>00220
<a name="l00221"></a>00221 <span class="comment">// This can happen if the SAT solver propagates a learned unit clause from a p</span>
<a name="l00222"></a>00222 <span class="keywordtype">bool</span> isSATLemma = <span class="keyword">false</span>;
<a name="l00223"></a>00223 <span class="keywordflow">if</span> (e.<a class="code" href="group__ExprPkg.html#ga0265d1ca42fa59c95aaff3ca675b6504">isNull</a>()) {
<a name="l00224"></a>00224 e = d_cnfManager->concreteLit(l, <span class="keyword">false</span>);
<a name="l00225"></a>00225 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!e.<a class="code" href="group__ExprPkg.html#ga0265d1ca42fa59c95aaff3ca675b6504">isNull</a>(), <span class="stringliteral">"Expected known expr"</span>);
<a name="l00226"></a>00226 isSATLemma = <span class="keyword">true</span>;
<a name="l00227"></a>00227 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"quant-level"</span>, <span class="stringliteral">"found null expr "</span>,e, <span class="stringliteral">""</span>);
<a name="l00228"></a>00228 }
<a name="l00229"></a>00229
<a name="l00230"></a>00230 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!e.<a class="code" href="group__ExprPkg.html#ga0265d1ca42fa59c95aaff3ca675b6504">isNull</a>(), <span class="stringliteral">"Expected known expr"</span>);
<a name="l00231"></a>00231 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!e.<a class="code" href="group__ExprPkg.html#gaf42121131fd56040faef7a64d9e67729">isIntAssumption</a>() || getValue(l) == <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfafbdc0d362f5bc36703903ef24ebbd30b">SAT::Var::TRUE_VAL</a>,
<a name="l00232"></a>00232 <span class="stringliteral">"internal assumptions should be true"</span>);
<a name="l00233"></a>00233 <span class="comment">// This happens if the SAT solver has been restarted--it re-asserts its old assumptions</span>
<a name="l00234"></a>00234 <span class="keywordflow">if</span> (e.<a class="code" href="group__ExprPkg.html#gaf42121131fd56040faef7a64d9e67729">isIntAssumption</a>()) <span class="keywordflow">return</span>;
<a name="l00235"></a>00235 <span class="keywordflow">if</span> (getValue(l) == <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">SAT::Var::UNKNOWN</a>) {
<a name="l00236"></a>00236 setValue(l.<a class="code" href="classSAT_1_1Lit.html#a57e2e6e37cad9595c3edbea88a41262f">getVar</a>(), l.<a class="code" href="classSAT_1_1Lit.html#ada14f3ca2b88500b5c2500d60e7f554b">isPositive</a>() ? <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfafbdc0d362f5bc36703903ef24ebbd30b">Var::TRUE_VAL</a> : <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfa047662472190c5c32f81cb409b2139bc">Var::FALSE_VAL</a>);
<a name="l00237"></a>00237 }
<a name="l00238"></a>00238 <span class="keywordflow">else</span> {
<a name="l00239"></a>00239 <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">"invariant violated"</span>);
<a name="l00240"></a>00240 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(getValue(l) == <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfafbdc0d362f5bc36703903ef24ebbd30b">Var::TRUE_VAL</a>, <span class="stringliteral">"invariant violated"</span>);
<a name="l00241"></a>00241 <span class="keywordflow">return</span>;
<a name="l00242"></a>00242 }
<a name="l00243"></a>00243 <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>;
<a name="l00244"></a>00244 e.<a class="code" href="group__ExprPkg.html#ga8b1ac81529d2ebee895a385a35460d39">setIntAssumption</a>();
<a name="l00245"></a>00245
<a name="l00246"></a>00246 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> thm = d_commonRules->assumpRule(e);
<a name="l00247"></a>00247 <span class="keywordflow">if</span> (isSATLemma) {
<a name="l00248"></a>00248 <a class="code" href="classSAT_1_1CNF__Formula__Impl.html">CNF_Formula_Impl</a> cnf;
<a name="l00249"></a>00249 d_cnfManager->addAssumption(thm, cnf);
<a name="l00250"></a>00250 }
<a name="l00251"></a>00251
<a name="l00252"></a>00252 thm.<a class="code" href="classCVC3_1_1Theorem.html#ab3309c937f827595d1d92fa48cb5a471" title="Set the quantification level for this theorem.">setQuantLevel</a>(theoryCore()->getQuantLevelForTerm(e.<a class="code" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a>() ? e[0] : e));
<a name="l00253"></a>00253 d_intAssumptions.push_back(thm);
<a name="l00254"></a>00254 d_core->addFact(thm);
<a name="l00255"></a>00255 }
<a name="l00256"></a>00256
<a name="l00257"></a>00257
<a name="l00258"></a><a class="code" href="classCVC3_1_1SearchSat.html#aba13a4e3105c6d8ed6ae960a35ac0831">00258</a> <a class="code" href="classSAT_1_1DPLLT.html#ac612908684032ffe76ad97f04afd0ca8">SAT::DPLLT::ConsistentResult</a> SearchSat::checkConsistent(<a class="code" href="classSAT_1_1CNF__Formula.html">SAT::CNF_Formula</a>& cnf, <span class="keywordtype">bool</span> fullEffort)
<a name="l00259"></a>00259 {
<a name="l00260"></a>00260 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(d_inCheckSat, <span class="stringliteral">"Should only be used as a call-back"</span>);
<a name="l00261"></a>00261 <span class="keywordflow">if</span> (d_core->inconsistent()) {
<a name="l00262"></a>00262 d_cnfManager->convertLemma(d_core->inconsistentThm(), cnf);
<a name="l00263"></a>00263 <span class="keywordflow">if</span> (d_cnfManager->numVars() > d_vars.size()) {
<a name="l00264"></a>00264 d_vars.resize(d_cnfManager->numVars(), <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">SAT::Var::UNKNOWN</a>);
<a name="l00265"></a>00265 }
<a name="l00266"></a>00266 <span class="keywordflow">return</span> DPLLT::INCONSISTENT;
<a name="l00267"></a>00267 }
<a name="l00268"></a>00268 <span class="keywordflow">if</span> (fullEffort) {
<a name="l00269"></a>00269 <span class="keywordflow">if</span> (d_core->checkSATCore() && d_pendingLemmasNext == d_pendingLemmas.size() && d_lemmasNext == d_lemmas.numClauses()) {
<a name="l00270"></a>00270 <span class="keywordflow">if</span> (d_core->inconsistent()) {
<a name="l00271"></a>00271 d_cnfManager->convertLemma(d_core->inconsistentThm(), cnf);
<a name="l00272"></a>00272 <span class="keywordflow">if</span> (d_cnfManager->numVars() > d_vars.size()) {
<a name="l00273"></a>00273 d_vars.resize(d_cnfManager->numVars(), <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">SAT::Var::UNKNOWN</a>);
<a name="l00274"></a>00274 }
<a name="l00275"></a>00275 <span class="keywordflow">return</span> DPLLT::INCONSISTENT;
<a name="l00276"></a>00276 }
<a name="l00277"></a>00277 <span class="keywordflow">else</span> <span class="keywordflow">return</span> DPLLT::CONSISTENT;
<a name="l00278"></a>00278 }
<a name="l00279"></a>00279 }
<a name="l00280"></a>00280 <span class="keywordflow">return</span> DPLLT::MAYBE_CONSISTENT;
<a name="l00281"></a>00281 }
<a name="l00282"></a>00282
<a name="l00283"></a>00283
<a name="l00284"></a><a class="code" href="classCVC3_1_1SearchSat.html#a87c52cad8178ab644a84e31ab0290f95">00284</a> <a class="code" href="classSAT_1_1Lit.html">Lit</a> SearchSat::getImplication()
<a name="l00285"></a>00285 {
<a name="l00286"></a>00286 <span class="comment">// DebugAssert(d_inCheckSat, "Should only be used as a call-back");</span>
<a name="l00287"></a>00287 <a class="code" href="classSAT_1_1Lit.html">Lit</a> l;
<a name="l00288"></a>00288 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> imp = d_core->getImpliedLiteral();
<a name="l00289"></a>00289 <span class="keywordflow">while</span> (!imp.<a class="code" href="classCVC3_1_1Theorem.html#afc6fdb0507eb3669e28d9be5ed0bd333">isNull</a>()) {
<a name="l00290"></a>00290 l = d_cnfManager->getCNFLit(imp.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00291"></a>00291 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!l.<a class="code" href="classSAT_1_1Lit.html#ad5f6236c582c95356d720a7401623f36">isNull</a>() || imp.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>().<a class="code" href="group__ExprPkg.html#ga39070a3fb12c398dc5bb7526d6aeb7f3" title="Remove leading NOT if any.">unnegate</a>().<a class="code" href="group__ExprPkg.html#ga8296386eb481a436937b6f0b140f8af0">isUserRegisteredAtom</a>(),
<a name="l00292"></a>00292 <span class="stringliteral">"implied literals should be registered by cnf or by user"</span>);
<a name="l00293"></a>00293 <span class="keywordflow">if</span> (!l.<a class="code" href="classSAT_1_1Lit.html#ad5f6236c582c95356d720a7401623f36">isNull</a>() && getValue(l) != <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfafbdc0d362f5bc36703903ef24ebbd30b">Var::TRUE_VAL</a>) {
<a name="l00294"></a>00294 d_theorems.insert(imp.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>(), imp);
<a name="l00295"></a>00295 <span class="keywordflow">break</span>;
<a name="l00296"></a>00296 }
<a name="l00297"></a>00297 l.<a class="code" href="classSAT_1_1Lit.html#a3bb64db99db01facd58c54e48b3f7800">reset</a>();
<a name="l00298"></a>00298 imp = d_core->getImpliedLiteral();
<a name="l00299"></a>00299 }
<a name="l00300"></a>00300 <span class="keywordflow">return</span> l;
<a name="l00301"></a>00301 }
<a name="l00302"></a>00302
<a name="l00303"></a>00303
<a name="l00304"></a><a class="code" href="classCVC3_1_1SearchSat.html#a6347fa89942c705786dece8175c2bf6c">00304</a> <span class="keywordtype">void</span> SearchSat::getExplanation(<a class="code" href="classSAT_1_1Lit.html">Lit</a> l, <a class="code" href="classSAT_1_1CNF__Formula.html">SAT::CNF_Formula</a>& cnf)
<a name="l00305"></a>00305 {
<a name="l00306"></a>00306 <span class="comment">// DebugAssert(d_inCheckSat, "Should only be used as a call-back");</span>
<a name="l00307"></a>00307 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(cnf.<a class="code" href="classSAT_1_1CNF__Formula.html#a15e2d3d65a38c23558a0ae8cf35f1938">empty</a>(), <span class="stringliteral">"Expected empty cnf"</span>);
<a name="l00308"></a>00308 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e = d_cnfManager->concreteLit(l);
<a name="l00309"></a>00309 <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr, Theorem>::iterator</a> i = d_theorems.<a class="code" href="classCVC3_1_1CDMap.html#a1cadecbd2d6fa614a2f2e9419aa43f33">find</a>(e);
<a name="l00310"></a>00310 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(i != d_theorems.<a class="code" href="classCVC3_1_1CDMap.html#a2a26c7cc4db12cb17d273db5cfa5a890">end</a>(), <span class="stringliteral">"getExplanation: no explanation found"</span>);
<a name="l00311"></a>00311 d_cnfManager->convertLemma((*i).second, cnf);
<a name="l00312"></a>00312 <span class="keywordflow">if</span> (d_cnfManager->numVars() > d_vars.size()) {
<a name="l00313"></a>00313 d_vars.resize(d_cnfManager->numVars(), <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">SAT::Var::UNKNOWN</a>);
<a name="l00314"></a>00314 }
<a name="l00315"></a>00315 }
<a name="l00316"></a>00316
<a name="l00317"></a>00317
<a name="l00318"></a><a class="code" href="classCVC3_1_1SearchSat.html#a858da2f6e8aefe2aeb124eececd45e3a">00318</a> <span class="keywordtype">bool</span> SearchSat::getNewClauses(<a class="code" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a>& cnf)
<a name="l00319"></a>00319 {
<a name="l00320"></a>00320 <span class="keywordtype">unsigned</span> i;
<a name="l00321"></a>00321
<a name="l00322"></a>00322 <a class="code" href="classSAT_1_1Lit.html">Lit</a> l;
<a name="l00323"></a>00323 <span class="keywordflow">for</span> (i = d_pendingLemmasNext; i < d_pendingLemmas.size(); ++i) {
<a name="l00324"></a>00324 l = d_cnfManager->addLemma(d_pendingLemmas[i].first, d_lemmas);
<a name="l00325"></a>00325 <span class="keywordflow">if</span> (!recordNewRootLit(l, d_pendingLemmas[i].second, d_pendingScopes[i])) {
<a name="l00326"></a>00326 <span class="comment">// Already have this lemma: delete it</span>
<a name="l00327"></a>00327 d_lemmas.deleteLast();
<a name="l00328"></a>00328 }
<a name="l00329"></a>00329 }
<a name="l00330"></a>00330 d_pendingLemmasNext = d_pendingLemmas.size();
<a name="l00331"></a>00331
<a name="l00332"></a>00332 <span class="keywordflow">if</span> (d_cnfManager->numVars() > d_vars.size()) {
<a name="l00333"></a>00333 d_vars.resize(d_cnfManager->numVars(), <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">SAT::Var::UNKNOWN</a>);
<a name="l00334"></a>00334 }
<a name="l00335"></a>00335
<a name="l00336"></a>00336 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(d_lemmasNext <= d_lemmas.numClauses(), <span class="stringliteral">""</span>);
<a name="l00337"></a>00337 <span class="keywordflow">if</span> (d_lemmasNext == d_lemmas.numClauses()) <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00338"></a>00338 <span class="keywordflow">do</span> {
<a name="l00339"></a>00339 cnf += d_lemmas[d_lemmasNext];
<a name="l00340"></a>00340 d_lemmasNext = d_lemmasNext + 1;
<a name="l00341"></a>00341 } <span class="keywordflow">while</span> (d_lemmasNext < d_lemmas.numClauses());
<a name="l00342"></a>00342 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00343"></a>00343 }
<a name="l00344"></a>00344
<a name="l00345"></a>00345
<a name="l00346"></a><a class="code" href="classCVC3_1_1SearchSat.html#afa9bdddd9bef64500f6a958d90682c37">00346</a> <a class="code" href="classSAT_1_1Lit.html">Lit</a> SearchSat::makeDecision()
<a name="l00347"></a>00347 {
<a name="l00348"></a>00348 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(d_inCheckSat, <span class="stringliteral">"Should only be used as a call-back"</span>);
<a name="l00349"></a>00349 <a class="code" href="classSAT_1_1Lit.html">Lit</a> litDecision;
<a name="l00350"></a>00350
<a name="l00351"></a>00351 set<LitPriorityPair>::const_iterator i, iend;
<a name="l00352"></a>00352 <a class="code" href="classSAT_1_1Lit.html">Lit</a> lit;
<a name="l00353"></a>00353 <span class="keywordflow">for</span> (i = d_prioritySetStart, iend = d_prioritySet.end(); i != iend; ++i) {
<a name="l00354"></a>00354 lit = (*i).getLit();
<a name="l00355"></a>00355 <span class="keywordflow">if</span> (findSplitterRec(lit, getValue(lit), &litDecision)) {
<a name="l00356"></a>00356 <span class="keywordflow">break</span>;
<a name="l00357"></a>00357 }
<a name="l00358"></a>00358 }
<a name="l00359"></a>00359 d_prioritySetStart = i;
<a name="l00360"></a>00360 <span class="keywordflow">return</span> litDecision;
<a name="l00361"></a>00361 }
<a name="l00362"></a>00362
<a name="l00363"></a>00363
<a name="l00364"></a><a class="code" href="classCVC3_1_1SearchSat.html#a9b9c34dcc6d7deab8d54c1d03e5b7a2e">00364</a> <span class="keywordtype">bool</span> SearchSat::findSplitterRec(<a class="code" href="classSAT_1_1Lit.html">Lit</a> lit, <a class="code" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">Var::Val</a> value, <a class="code" href="classSAT_1_1Lit.html">Lit</a>* litDecision)
<a name="l00365"></a>00365 {
<a name="l00366"></a>00366 <span class="keywordflow">if</span> (lit.<a class="code" href="classSAT_1_1Lit.html#ab866c8154de88e5285f166f53cdf2d33">isFalse</a>() || lit.<a class="code" href="classSAT_1_1Lit.html#a770e1901858f699490f50e9d2ff1d070">isTrue</a>()) <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00367"></a>00367
<a name="l00368"></a>00368 <span class="keywordtype">unsigned</span> i, n;
<a name="l00369"></a>00369 <a class="code" href="classSAT_1_1Lit.html">Lit</a> litTmp;
<a name="l00370"></a>00370 <a class="code" href="classSAT_1_1Var.html">Var</a> varTmp;
<a name="l00371"></a>00371 <span class="keywordtype">bool</span> ret;
<a name="l00372"></a>00372 <a class="code" href="classSAT_1_1Var.html">Var</a> v = lit.<a class="code" href="classSAT_1_1Lit.html#a57e2e6e37cad9595c3edbea88a41262f">getVar</a>();
<a name="l00373"></a>00373
<a name="l00374"></a>00374 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(value != <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">Var::UNKNOWN</a>, <span class="stringliteral">"expected known value"</span>);
<a name="l00375"></a>00375 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(getValue(lit) == value || getValue(lit) == <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">Var::UNKNOWN</a>,
<a name="l00376"></a>00376 <span class="stringliteral">"invariant violated"</span>);
<a name="l00377"></a>00377
<a name="l00378"></a>00378 <span class="keywordflow">if</span> (checkJustified(v)) <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00379"></a>00379
<a name="l00380"></a>00380 <span class="keywordflow">if</span> (lit.<a class="code" href="classSAT_1_1Lit.html#ae6fbaf94176fd32347ff14ba3cbc3363">isInverted</a>()) {
<a name="l00381"></a>00381 value = Var::invertValue(value);
<a name="l00382"></a>00382 }
<a name="l00383"></a>00383
<a name="l00384"></a>00384 <span class="keywordflow">if</span> (d_cnfManager->numFanins(v) == 0) {
<a name="l00385"></a>00385 <span class="keywordflow">if</span> (getValue(v) != <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">Var::UNKNOWN</a>) {
<a name="l00386"></a>00386 setJustified(v);
<a name="l00387"></a>00387 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00388"></a>00388 }
<a name="l00389"></a>00389 <span class="keywordflow">else</span> {
<a name="l00390"></a>00390 *litDecision = <a class="code" href="classSAT_1_1Lit.html">Lit</a>(v, value == <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfafbdc0d362f5bc36703903ef24ebbd30b">Var::TRUE_VAL</a>);
<a name="l00391"></a>00391 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00392"></a>00392 }
<a name="l00393"></a>00393 }
<a name="l00394"></a>00394 <span class="keywordflow">else</span> <span class="keywordflow">if</span> (d_cnfManager->concreteVar(v).isAbsAtomicFormula()) {
<a name="l00395"></a>00395 <span class="comment">// This node represents a predicate with embedded ITE's</span>
<a name="l00396"></a>00396 <span class="comment">// We handle this case specially in order to catch the</span>
<a name="l00397"></a>00397 <span class="comment">// corner case when a variable is in its own fanin.</span>
<a name="l00398"></a>00398 n = d_cnfManager->numFanins(v);
<a name="l00399"></a>00399 <span class="keywordflow">for</span> (i=0; i < n; ++i) {
<a name="l00400"></a>00400 litTmp = d_cnfManager->getFanin(v, i);
<a name="l00401"></a>00401 varTmp = litTmp.<a class="code" href="classSAT_1_1Lit.html#a57e2e6e37cad9595c3edbea88a41262f">getVar</a>();
<a name="l00402"></a>00402 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!litTmp.<a class="code" href="classSAT_1_1Lit.html#ae6fbaf94176fd32347ff14ba3cbc3363">isInverted</a>(),<span class="stringliteral">"Expected positive fanin"</span>);
<a name="l00403"></a>00403 <span class="keywordflow">if</span> (checkJustified(varTmp)) <span class="keywordflow">continue</span>;
<a name="l00404"></a>00404 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(d_cnfManager->concreteVar(varTmp).getKind() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3a4cfaf3eae8eac1dc2fd27d9f0994dc">ITE</a>,
<a name="l00405"></a>00405 <span class="stringliteral">"Expected ITE"</span>);
<a name="l00406"></a>00406 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(getValue(varTmp) == <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfafbdc0d362f5bc36703903ef24ebbd30b">Var::TRUE_VAL</a>,<span class="stringliteral">"Expected TRUE"</span>);
<a name="l00407"></a>00407 <a class="code" href="classSAT_1_1Lit.html">Lit</a> cIf = d_cnfManager->getFanin(varTmp,0);
<a name="l00408"></a>00408 <a class="code" href="classSAT_1_1Lit.html">Lit</a> cThen = d_cnfManager->getFanin(varTmp,1);
<a name="l00409"></a>00409 <a class="code" href="classSAT_1_1Lit.html">Lit</a> cElse = d_cnfManager->getFanin(varTmp,2);
<a name="l00410"></a>00410 <span class="keywordflow">if</span> (getValue(cIf) == <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">Var::UNKNOWN</a>) {
<a name="l00411"></a>00411 <span class="keywordflow">if</span> (getValue(cElse) == <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfafbdc0d362f5bc36703903ef24ebbd30b">Var::TRUE_VAL</a> ||
<a name="l00412"></a>00412 getValue(cThen) == <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfa047662472190c5c32f81cb409b2139bc">Var::FALSE_VAL</a>) {
<a name="l00413"></a>00413 ret = findSplitterRec(cIf, <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfa047662472190c5c32f81cb409b2139bc">Var::FALSE_VAL</a>, litDecision);
<a name="l00414"></a>00414 }
<a name="l00415"></a>00415 <span class="keywordflow">else</span> {
<a name="l00416"></a>00416 ret = findSplitterRec(cIf, <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfafbdc0d362f5bc36703903ef24ebbd30b">Var::TRUE_VAL</a>, litDecision);
<a name="l00417"></a>00417 }
<a name="l00418"></a>00418 <span class="keywordflow">if</span> (!ret) {
<a name="l00419"></a>00419 cout << d_cnfManager->concreteVar(cIf.<a class="code" href="classSAT_1_1Lit.html#a57e2e6e37cad9595c3edbea88a41262f">getVar</a>()) << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00420"></a>00420 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<span class="keyword">false</span>,<span class="stringliteral">"No controlling input found (1)"</span>);
<a name="l00421"></a>00421 }
<a name="l00422"></a>00422 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00423"></a>00423 }
<a name="l00424"></a>00424 <span class="keywordflow">else</span> <span class="keywordflow">if</span> (getValue(cIf) == <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfafbdc0d362f5bc36703903ef24ebbd30b">Var::TRUE_VAL</a>) {
<a name="l00425"></a>00425 <span class="keywordflow">if</span> (findSplitterRec(cIf, <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfafbdc0d362f5bc36703903ef24ebbd30b">Var::TRUE_VAL</a>, litDecision)) {
<a name="l00426"></a>00426 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00427"></a>00427 }
<a name="l00428"></a>00428 <span class="keywordflow">if</span> (cThen.<a class="code" href="classSAT_1_1Lit.html#a57e2e6e37cad9595c3edbea88a41262f">getVar</a>() != v &&
<a name="l00429"></a>00429 (getValue(cThen) == <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">Var::UNKNOWN</a> ||
<a name="l00430"></a>00430 getValue(cThen) == <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfafbdc0d362f5bc36703903ef24ebbd30b">Var::TRUE_VAL</a>) &&
<a name="l00431"></a>00431 findSplitterRec(cThen, <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfafbdc0d362f5bc36703903ef24ebbd30b">Var::TRUE_VAL</a>, litDecision)) {
<a name="l00432"></a>00432 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00433"></a>00433 }
<a name="l00434"></a>00434 }
<a name="l00435"></a>00435 <span class="keywordflow">else</span> {
<a name="l00436"></a>00436 <span class="keywordflow">if</span> (findSplitterRec(cIf, <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfa047662472190c5c32f81cb409b2139bc">Var::FALSE_VAL</a>, litDecision)) {
<a name="l00437"></a>00437 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00438"></a>00438 }
<a name="l00439"></a>00439 <span class="keywordflow">if</span> (cElse.<a class="code" href="classSAT_1_1Lit.html#a57e2e6e37cad9595c3edbea88a41262f">getVar</a>() != v &&
<a name="l00440"></a>00440 (getValue(cElse) == <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">Var::UNKNOWN</a> ||
<a name="l00441"></a>00441 getValue(cElse) == <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfafbdc0d362f5bc36703903ef24ebbd30b">Var::TRUE_VAL</a>) &&
<a name="l00442"></a>00442 findSplitterRec(cElse, <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfafbdc0d362f5bc36703903ef24ebbd30b">Var::TRUE_VAL</a>, litDecision)) {
<a name="l00443"></a>00443 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00444"></a>00444 }
<a name="l00445"></a>00445 }
<a name="l00446"></a>00446 setJustified(varTmp);
<a name="l00447"></a>00447 }
<a name="l00448"></a>00448 <span class="keywordflow">if</span> (getValue(v) != <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">Var::UNKNOWN</a>) {
<a name="l00449"></a>00449 setJustified(v);
<a name="l00450"></a>00450 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00451"></a>00451 }
<a name="l00452"></a>00452 <span class="keywordflow">else</span> {
<a name="l00453"></a>00453 *litDecision = <a class="code" href="classSAT_1_1Lit.html">Lit</a>(v, value == <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfafbdc0d362f5bc36703903ef24ebbd30b">Var::TRUE_VAL</a>);
<a name="l00454"></a>00454 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00455"></a>00455 }
<a name="l00456"></a>00456 }
<a name="l00457"></a>00457
<a name="l00458"></a>00458 <span class="keywordtype">int</span> kind = d_cnfManager->concreteVar(v).getKind();
<a name="l00459"></a>00459 <a class="code" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">Var::Val</a> valHard = <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfa047662472190c5c32f81cb409b2139bc">Var::FALSE_VAL</a>;
<a name="l00460"></a>00460 <span class="keywordflow">switch</span> (kind) {
<a name="l00461"></a>00461 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba865555c9f2e0458a7078486aa1b3254f">AND</a>:
<a name="l00462"></a>00462 valHard = <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfafbdc0d362f5bc36703903ef24ebbd30b">Var::TRUE_VAL</a>;
<a name="l00463"></a>00463 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba96727447c0ad447987df1c6415aef074">OR</a>:
<a name="l00464"></a>00464 <span class="keywordflow">if</span> (value == valHard) {
<a name="l00465"></a>00465 n = d_cnfManager->numFanins(v);
<a name="l00466"></a>00466 <span class="keywordflow">for</span> (i=0; i < n; ++i) {
<a name="l00467"></a>00467 litTmp = d_cnfManager->getFanin(v, i);
<a name="l00468"></a>00468 <span class="keywordflow">if</span> (findSplitterRec(litTmp, valHard, litDecision)) {
<a name="l00469"></a>00469 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00470"></a>00470 }
<a name="l00471"></a>00471 }
<a name="l00472"></a>00472 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(getValue(v) == valHard, <span class="stringliteral">"Output should be justified"</span>);
<a name="l00473"></a>00473 setJustified(v);
<a name="l00474"></a>00474 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00475"></a>00475 }
<a name="l00476"></a>00476 <span class="keywordflow">else</span> {
<a name="l00477"></a>00477 <a class="code" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">Var::Val</a> valEasy = Var::invertValue(valHard);
<a name="l00478"></a>00478 n = d_cnfManager->numFanins(v);
<a name="l00479"></a>00479 <span class="keywordflow">for</span> (i=0; i < n; ++i) {
<a name="l00480"></a>00480 litTmp = d_cnfManager->getFanin(v, i);
<a name="l00481"></a>00481 <span class="keywordflow">if</span> (getValue(litTmp) != valHard) {
<a name="l00482"></a>00482 <span class="keywordflow">if</span> (findSplitterRec(litTmp, valEasy, litDecision)) {
<a name="l00483"></a>00483 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00484"></a>00484 }
<a name="l00485"></a>00485 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(getValue(v) == valEasy, <span class="stringliteral">"Output should be justified"</span>);
<a name="l00486"></a>00486 setJustified(v);
<a name="l00487"></a>00487 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00488"></a>00488 }
<a name="l00489"></a>00489 }
<a name="l00490"></a>00490 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<span class="keyword">false</span>, <span class="stringliteral">"No controlling input found (2)"</span>);
<a name="l00491"></a>00491 }
<a name="l00492"></a>00492 <span class="keywordflow">break</span>;
<a name="l00493"></a>00493 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7338bb59b9aa936104a6d2f631d4d8db">IMPLIES</a>:
<a name="l00494"></a>00494 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(d_cnfManager->numFanins(v) == 2, <span class="stringliteral">"Expected 2 fanins"</span>);
<a name="l00495"></a>00495 <span class="keywordflow">if</span> (value == <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfa047662472190c5c32f81cb409b2139bc">Var::FALSE_VAL</a>) {
<a name="l00496"></a>00496 litTmp = d_cnfManager->getFanin(v, 0);
<a name="l00497"></a>00497 <span class="keywordflow">if</span> (findSplitterRec(litTmp, <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfafbdc0d362f5bc36703903ef24ebbd30b">Var::TRUE_VAL</a>, litDecision)) {
<a name="l00498"></a>00498 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00499"></a>00499 }
<a name="l00500"></a>00500 litTmp = d_cnfManager->getFanin(v, 1);
<a name="l00501"></a>00501 <span class="keywordflow">if</span> (findSplitterRec(litTmp, <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfa047662472190c5c32f81cb409b2139bc">Var::FALSE_VAL</a>, litDecision)) {
<a name="l00502"></a>00502 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00503"></a>00503 }
<a name="l00504"></a>00504 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(getValue(v) == <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfa047662472190c5c32f81cb409b2139bc">Var::FALSE_VAL</a>, <span class="stringliteral">"Output should be justified"</span>);
<a name="l00505"></a>00505 setJustified(v);
<a name="l00506"></a>00506 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00507"></a>00507 }
<a name="l00508"></a>00508 <span class="keywordflow">else</span> {
<a name="l00509"></a>00509 litTmp = d_cnfManager->getFanin(v, 0);
<a name="l00510"></a>00510 <span class="keywordflow">if</span> (getValue(litTmp) != <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfafbdc0d362f5bc36703903ef24ebbd30b">Var::TRUE_VAL</a>) {
<a name="l00511"></a>00511 <span class="keywordflow">if</span> (findSplitterRec(litTmp, <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfa047662472190c5c32f81cb409b2139bc">Var::FALSE_VAL</a>, litDecision)) {
<a name="l00512"></a>00512 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00513"></a>00513 }
<a name="l00514"></a>00514 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(getValue(v) == <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfafbdc0d362f5bc36703903ef24ebbd30b">Var::TRUE_VAL</a>, <span class="stringliteral">"Output should be justified"</span>);
<a name="l00515"></a>00515 setJustified(v);
<a name="l00516"></a>00516 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00517"></a>00517 }
<a name="l00518"></a>00518 litTmp = d_cnfManager->getFanin(v, 1);
<a name="l00519"></a>00519 <span class="keywordflow">if</span> (getValue(litTmp) != <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfa047662472190c5c32f81cb409b2139bc">Var::FALSE_VAL</a>) {
<a name="l00520"></a>00520 <span class="keywordflow">if</span> (findSplitterRec(litTmp, <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfafbdc0d362f5bc36703903ef24ebbd30b">Var::TRUE_VAL</a>, litDecision)) {
<a name="l00521"></a>00521 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00522"></a>00522 }
<a name="l00523"></a>00523 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(getValue(v) == <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfafbdc0d362f5bc36703903ef24ebbd30b">Var::TRUE_VAL</a>, <span class="stringliteral">"Output should be justified"</span>);
<a name="l00524"></a>00524 setJustified(v);
<a name="l00525"></a>00525 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00526"></a>00526 }
<a name="l00527"></a>00527 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<span class="keyword">false</span>, <span class="stringliteral">"No controlling input found (3)"</span>);
<a name="l00528"></a>00528 }
<a name="l00529"></a>00529 <span class="keywordflow">break</span>;
<a name="l00530"></a>00530 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>: {
<a name="l00531"></a>00531 litTmp = d_cnfManager->getFanin(v, 0);
<a name="l00532"></a>00532 <a class="code" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">Var::Val</a> val = getValue(litTmp);
<a name="l00533"></a>00533 <span class="keywordflow">if</span> (val != <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">Var::UNKNOWN</a>) {
<a name="l00534"></a>00534 <span class="keywordflow">if</span> (findSplitterRec(litTmp, val, litDecision)) {
<a name="l00535"></a>00535 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00536"></a>00536 }
<a name="l00537"></a>00537 <span class="keywordflow">if</span> (value == <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfa047662472190c5c32f81cb409b2139bc">Var::FALSE_VAL</a>) val = Var::invertValue(val);
<a name="l00538"></a>00538 litTmp = d_cnfManager->getFanin(v, 1);
<a name="l00539"></a>00539
<a name="l00540"></a>00540 <span class="keywordflow">if</span> (findSplitterRec(litTmp, val, litDecision)) {
<a name="l00541"></a>00541 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00542"></a>00542 }
<a name="l00543"></a>00543 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(getValue(v) == value, <span class="stringliteral">"Output should be justified"</span>);
<a name="l00544"></a>00544 setJustified(v);
<a name="l00545"></a>00545 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00546"></a>00546 }
<a name="l00547"></a>00547 <span class="keywordflow">else</span> {
<a name="l00548"></a>00548 val = getValue(d_cnfManager->getFanin(v, 1));
<a name="l00549"></a>00549 <span class="keywordflow">if</span> (val == <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">Var::UNKNOWN</a>) val = <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfa047662472190c5c32f81cb409b2139bc">Var::FALSE_VAL</a>;
<a name="l00550"></a>00550 <span class="keywordflow">if</span> (value == <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfa047662472190c5c32f81cb409b2139bc">Var::FALSE_VAL</a>) val = Var::invertValue(val);
<a name="l00551"></a>00551 <span class="keywordflow">if</span> (findSplitterRec(litTmp, val, litDecision)) {
<a name="l00552"></a>00552 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00553"></a>00553 }
<a name="l00554"></a>00554 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<span class="keyword">false</span>, <span class="stringliteral">"Unable to find controlling input (4)"</span>);
<a name="l00555"></a>00555 }
<a name="l00556"></a>00556 <span class="keywordflow">break</span>;
<a name="l00557"></a>00557 }
<a name="l00558"></a>00558 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bac62338ffb5de22369c75caa565b5da1a">XOR</a>: {
<a name="l00559"></a>00559 litTmp = d_cnfManager->getFanin(v, 0);
<a name="l00560"></a>00560 <a class="code" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">Var::Val</a> val = getValue(litTmp);
<a name="l00561"></a>00561 <span class="keywordflow">if</span> (val != <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">Var::UNKNOWN</a>) {
<a name="l00562"></a>00562 <span class="keywordflow">if</span> (findSplitterRec(litTmp, val, litDecision)) {
<a name="l00563"></a>00563 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00564"></a>00564 }
<a name="l00565"></a>00565 <span class="keywordflow">if</span> (value == <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfafbdc0d362f5bc36703903ef24ebbd30b">Var::TRUE_VAL</a>) val = Var::invertValue(val);
<a name="l00566"></a>00566 litTmp = d_cnfManager->getFanin(v, 1);
<a name="l00567"></a>00567 <span class="keywordflow">if</span> (findSplitterRec(litTmp, val, litDecision)) {
<a name="l00568"></a>00568 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00569"></a>00569 }
<a name="l00570"></a>00570 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(getValue(v) == value, <span class="stringliteral">"Output should be justified"</span>);
<a name="l00571"></a>00571 setJustified(v);
<a name="l00572"></a>00572 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00573"></a>00573 }
<a name="l00574"></a>00574 <span class="keywordflow">else</span> {
<a name="l00575"></a>00575 val = getValue(d_cnfManager->getFanin(v, 1));
<a name="l00576"></a>00576 <span class="keywordflow">if</span> (val == <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">Var::UNKNOWN</a>) val = <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfa047662472190c5c32f81cb409b2139bc">Var::FALSE_VAL</a>;
<a name="l00577"></a>00577 <span class="keywordflow">if</span> (value == <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfafbdc0d362f5bc36703903ef24ebbd30b">Var::TRUE_VAL</a>) val = Var::invertValue(val);
<a name="l00578"></a>00578 <span class="keywordflow">if</span> (findSplitterRec(litTmp, val, litDecision)) {
<a name="l00579"></a>00579 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00580"></a>00580 }
<a name="l00581"></a>00581 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<span class="keyword">false</span>, <span class="stringliteral">"Unable to find controlling input (5)"</span>);
<a name="l00582"></a>00582 }
<a name="l00583"></a>00583 <span class="keywordflow">break</span>;
<a name="l00584"></a>00584 }
<a name="l00585"></a>00585 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3a4cfaf3eae8eac1dc2fd27d9f0994dc">ITE</a>: {
<a name="l00586"></a>00586 <a class="code" href="classSAT_1_1Lit.html">Lit</a> cIf = d_cnfManager->getFanin(v, 0);
<a name="l00587"></a>00587 <a class="code" href="classSAT_1_1Lit.html">Lit</a> cThen = d_cnfManager->getFanin(v, 1);
<a name="l00588"></a>00588 <a class="code" href="classSAT_1_1Lit.html">Lit</a> cElse = d_cnfManager->getFanin(v, 2);
<a name="l00589"></a>00589 <span class="keywordflow">if</span> (getValue(cIf) == <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">Var::UNKNOWN</a>) {
<a name="l00590"></a>00590 <span class="keywordflow">if</span> (getValue(cElse) == value ||
<a name="l00591"></a>00591 getValue(cThen) == Var::invertValue(value)) {
<a name="l00592"></a>00592 ret = findSplitterRec(cIf, <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfa047662472190c5c32f81cb409b2139bc">Var::FALSE_VAL</a>, litDecision);
<a name="l00593"></a>00593 }
<a name="l00594"></a>00594 <span class="keywordflow">else</span> {
<a name="l00595"></a>00595 ret = findSplitterRec(cIf, <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfafbdc0d362f5bc36703903ef24ebbd30b">Var::TRUE_VAL</a>, litDecision);
<a name="l00596"></a>00596 }
<a name="l00597"></a>00597 <span class="keywordflow">if</span> (!ret) {
<a name="l00598"></a>00598 cout << d_cnfManager->concreteVar(cIf.<a class="code" href="classSAT_1_1Lit.html#a57e2e6e37cad9595c3edbea88a41262f">getVar</a>()) << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00599"></a>00599 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<span class="keyword">false</span>,<span class="stringliteral">"No controlling input found (6)"</span>);
<a name="l00600"></a>00600 }
<a name="l00601"></a>00601 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00602"></a>00602 }
<a name="l00603"></a>00603 <span class="keywordflow">else</span> <span class="keywordflow">if</span> (getValue(cIf) == <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfafbdc0d362f5bc36703903ef24ebbd30b">Var::TRUE_VAL</a>) {
<a name="l00604"></a>00604 <span class="keywordflow">if</span> (findSplitterRec(cIf, <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfafbdc0d362f5bc36703903ef24ebbd30b">Var::TRUE_VAL</a>, litDecision)) {
<a name="l00605"></a>00605 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00606"></a>00606 }
<a name="l00607"></a>00607 <span class="keywordflow">if</span> (cThen.<a class="code" href="classSAT_1_1Lit.html#aeb84cef22c7dbf459f95dff9b7cbb4a7">isVar</a>() && cThen.<a class="code" href="classSAT_1_1Lit.html#a57e2e6e37cad9595c3edbea88a41262f">getVar</a>() != v &&
<a name="l00608"></a>00608 (getValue(cThen) == <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">Var::UNKNOWN</a> ||
<a name="l00609"></a>00609 getValue(cThen) == value) &&
<a name="l00610"></a>00610 findSplitterRec(cThen, value, litDecision)) {
<a name="l00611"></a>00611 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00612"></a>00612 }
<a name="l00613"></a>00613 }
<a name="l00614"></a>00614 <span class="keywordflow">else</span> {
<a name="l00615"></a>00615 <span class="keywordflow">if</span> (findSplitterRec(cIf, <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfa047662472190c5c32f81cb409b2139bc">Var::FALSE_VAL</a>, litDecision)) {
<a name="l00616"></a>00616 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00617"></a>00617 }
<a name="l00618"></a>00618 <span class="keywordflow">if</span> (cElse.<a class="code" href="classSAT_1_1Lit.html#aeb84cef22c7dbf459f95dff9b7cbb4a7">isVar</a>() && cElse.<a class="code" href="classSAT_1_1Lit.html#a57e2e6e37cad9595c3edbea88a41262f">getVar</a>() != v &&
<a name="l00619"></a>00619 (getValue(cElse) == <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">Var::UNKNOWN</a> ||
<a name="l00620"></a>00620 getValue(cElse) == value) &&
<a name="l00621"></a>00621 findSplitterRec(cElse, value, litDecision)) {
<a name="l00622"></a>00622 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00623"></a>00623 }
<a name="l00624"></a>00624 }
<a name="l00625"></a>00625 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(getValue(v) == value, <span class="stringliteral">"Output should be justified"</span>);
<a name="l00626"></a>00626 setJustified(v);
<a name="l00627"></a>00627 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00628"></a>00628 }
<a name="l00629"></a>00629 <span class="keywordflow">default</span>:
<a name="l00630"></a>00630 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<span class="keyword">false</span>, <span class="stringliteral">"Unexpected Boolean operator"</span>);
<a name="l00631"></a>00631 <span class="keywordflow">break</span>;
<a name="l00632"></a>00632 }
<a name="l00633"></a>00633 <a class="code" href="debug_8h.html#a2637b2fffa22e3c9fad40cda8fcc3bce" title="If something goes horribly wrong, print a message and abort immediately with exit(1).">FatalAssert</a>(<span class="keyword">false</span>, <span class="stringliteral">"Should be unreachable"</span>);
<a name="l00634"></a>00634 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00635"></a>00635 }
<a name="l00636"></a>00636
<a name="l00637"></a>00637
<a name="l00638"></a><a class="code" href="classCVC3_1_1SearchSat.html#a720aba611f6cf6fd78bc3a0ede54564b">00638</a> <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> SearchSat::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 class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& result, <span class="keywordtype">bool</span> isRestart)
<a name="l00639"></a>00639 {
<a name="l00640"></a>00640 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(d_dplltReady, <span class="stringliteral">"SAT solver is not ready"</span>);
<a name="l00641"></a>00641 <span class="keywordflow">if</span> (isRestart && d_lastCheck.get().isNull()) {
<a name="l00642"></a>00642 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1Exception.html">Exception</a>
<a name="l00643"></a>00643 (<span class="stringliteral">"restart called without former call to checkValid"</span>);
<a name="l00644"></a>00644 }
<a name="l00645"></a>00645
<a name="l00646"></a>00646 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!d_inCheckSat, <span class="stringliteral">"checkValid should not be called recursively"</span>);
<a name="l00647"></a>00647 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"searchsat"</span>, <span class="stringliteral">"checkValid: "</span>, e, <span class="stringliteral">""</span>);
<a name="l00648"></a>00648
<a name="l00649"></a>00649 <span class="keywordflow">if</span> (!e.<a class="code" href="group__ExprPkg.html#ga42929221eb172250697b72c28af6de07" title="Get the type. Recursively compute if necessary.">getType</a>().<a class="code" href="classCVC3_1_1Type.html#a38bba404056eadf3c283a67ab2347e02">isBool</a>())
<a name="l00650"></a>00650 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1TypecheckException.html">TypecheckException</a>
<a name="l00651"></a>00651 (<span class="stringliteral">"checking validity of a non-Boolean expression:\n\n "</span>
<a name="l00652"></a>00652 + e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>()
<a name="l00653"></a>00653 + <span class="stringliteral">"\n\nwhich has the following type:\n\n "</span>
<a name="l00654"></a>00654 + e.<a class="code" href="group__ExprPkg.html#ga42929221eb172250697b72c28af6de07" title="Get the type. Recursively compute if necessary.">getType</a>().<a class="code" href="classCVC3_1_1Type.html#a2f5ce4b1973ec02b2f2b2eba8ce3cc50">toString</a>());
<a name="l00655"></a>00655
<a name="l00656"></a>00656 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e2 = e;
<a name="l00657"></a>00657
<a name="l00658"></a>00658 <span class="comment">// Set up and quick exits</span>
<a name="l00659"></a>00659 <span class="keywordflow">if</span> (isRestart) {
<a name="l00660"></a>00660 <span class="keywordflow">while</span> (e2.<a class="code" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a>() && e2[0].<a class="code" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a>()) e2 = e2[0][0];
<a name="l00661"></a>00661 <span class="keywordflow">if</span> (e2.<a class="code" href="group__ExprPkg.html#gadf8596df73fa69ff8e6a22b9321f5c34">isTrue</a>() || (e2.<a class="code" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a>() && e2[0].<a class="code" href="group__ExprPkg.html#ga6173f64b22cba76472cd0c814bbf6dae">isFalse</a>())) {
<a name="l00662"></a>00662 result = d_lastValid;
<a name="l00663"></a>00663 <span class="keywordflow">return</span> <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498baa6ad39c124f561d934d94b371db2d819">INVALID</a>;
<a name="l00664"></a>00664 }
<a name="l00665"></a>00665 <span class="keywordflow">if</span> (e2.<a class="code" href="group__ExprPkg.html#ga6173f64b22cba76472cd0c814bbf6dae">isFalse</a>() || (e2.<a class="code" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a>() && e2[0].<a class="code" href="group__ExprPkg.html#gadf8596df73fa69ff8e6a22b9321f5c34">isTrue</a>())) {
<a name="l00666"></a>00666 <a class="code" href="group__ExprStream__Manip.html#gaddb050a787be87116afc51791293d3be" title="Restore the indentation.">pop</a>();
<a name="l00667"></a>00667 <span class="comment">//TODO: real theorem</span>
<a name="l00668"></a>00668 d_lastValid = d_commonRules->assumpRule(d_lastCheck);
<a name="l00669"></a>00669 result = d_lastValid;
<a name="l00670"></a>00670 <span class="keywordflow">return</span> <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498ba24f8f4860dbe6fd65883a9d7cbd2f576">VALID</a>;
<a name="l00671"></a>00671 }
<a name="l00672"></a>00672 }
<a name="l00673"></a>00673 <span class="keywordflow">else</span> {
<a name="l00674"></a>00674 <span class="keywordflow">if</span> (e.<a class="code" href="group__ExprPkg.html#gadf8596df73fa69ff8e6a22b9321f5c34">isTrue</a>()) {
<a name="l00675"></a>00675 d_lastValid = d_commonRules->trueTheorem();
<a name="l00676"></a>00676 result = d_lastValid;
<a name="l00677"></a>00677 <span class="keywordflow">return</span> <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498ba24f8f4860dbe6fd65883a9d7cbd2f576">VALID</a>;
<a name="l00678"></a>00678 }
<a name="l00679"></a>00679 <a class="code" href="group__ExprStream__Manip.html#ga2a0348c6d3f94f2f8febc6dd0a9c3218" title="Set the indentation to the current position.">push</a>();
<a name="l00680"></a>00680 d_bottomScope = d_core->getCM()->scopeLevel();
<a name="l00681"></a>00681 d_prioritySetBottomEntriesSizeStack.push_back(d_prioritySetBottomEntriesSize);
<a name="l00682"></a>00682 d_lastCheck = e;
<a name="l00683"></a>00683 e2 = !e;
<a name="l00684"></a>00684 }
<a name="l00685"></a>00685
<a name="l00686"></a>00686 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> thm;
<a name="l00687"></a>00687 <a class="code" href="classSAT_1_1CNF__Formula__Impl.html">CNF_Formula_Impl</a> cnf;
<a name="l00688"></a>00688 <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> qres;
<a name="l00689"></a>00689 d_cnfManager->setBottomScope(d_bottomScope);
<a name="l00690"></a>00690 d_dplltReady = <span class="keyword">false</span>;
<a name="l00691"></a>00691
<a name="l00692"></a>00692 newUserAssumptionInt(e2, cnf, <span class="keyword">true</span>);
<a name="l00693"></a>00693
<a name="l00694"></a>00694 d_inCheckSat = <span class="keyword">true</span>;
<a name="l00695"></a>00695
<a name="l00696"></a>00696 getNewClauses(cnf);
<a name="l00697"></a>00697
<a name="l00698"></a>00698 <span class="keywordflow">if</span> (!isRestart && d_core->inconsistent()) {
<a name="l00699"></a>00699 qres = <a class="code" href="xchaff__solver_8h.html#a259c70233f322b3e490149190b8bb87ba709691b4dfbbba6c6f992a7cd34dd0e9">UNSATISFIABLE</a>;
<a name="l00700"></a>00700 thm = d_rules->proofByContradiction(e, d_core->inconsistentThm());
<a name="l00701"></a>00701 <a class="code" href="group__ExprStream__Manip.html#gaddb050a787be87116afc51791293d3be" title="Restore the indentation.">pop</a>();
<a name="l00702"></a>00702 d_lastValid = thm;
<a name="l00703"></a>00703 d_cnfManager->setBottomScope(-1);
<a name="l00704"></a>00704 d_inCheckSat = <span class="keyword">false</span>;
<a name="l00705"></a>00705 result = d_lastValid;
<a name="l00706"></a>00706 <span class="keywordflow">return</span> qres;
<a name="l00707"></a>00707 }
<a name="l00708"></a>00708 <span class="keywordflow">else</span> {
<a name="l00709"></a>00709 <span class="comment">// Run DPLLT engine</span>
<a name="l00710"></a>00710 qres = isRestart ? d_dpllt->continueCheck(cnf) : d_dpllt->checkSat(cnf);
<a name="l00711"></a>00711 }
<a name="l00712"></a>00712
<a name="l00713"></a>00713 <span class="keywordflow">if</span> (qres == <a class="code" href="xchaff__solver_8h.html#a259c70233f322b3e490149190b8bb87ba709691b4dfbbba6c6f992a7cd34dd0e9">UNSATISFIABLE</a>) {
<a name="l00714"></a>00714 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(d_core->getCM()->scopeLevel() == d_bottomScope,
<a name="l00715"></a>00715 <span class="stringliteral">"Expected unchanged context after unsat"</span>);
<a name="l00716"></a>00716 e2 = d_lastCheck;
<a name="l00717"></a>00717 <a class="code" href="group__ExprStream__Manip.html#gaddb050a787be87116afc51791293d3be" title="Restore the indentation.">pop</a>();
<a name="l00718"></a>00718 <span class="keywordflow">if</span> (d_core->getTM()->withProof()) {
<a name="l00719"></a>00719 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf = d_dpllt->getSatProof(d_cnfManager, d_core);
<a name="l00720"></a>00720 <span class="comment">// std::cout<<"WITH PROOF:"<<pf<<std::endl;</span>
<a name="l00721"></a>00721 d_lastValid = d_rules->satProof(e2, pf);
<a name="l00722"></a>00722 }
<a name="l00723"></a>00723 <span class="keywordflow">else</span> {
<a name="l00724"></a>00724 d_lastValid = d_commonRules->assumpRule(d_lastCheck);
<a name="l00725"></a>00725 }
<a name="l00726"></a>00726 }
<a name="l00727"></a>00727 <span class="keywordflow">else</span> {
<a name="l00728"></a>00728 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(d_lemmasNext == d_lemmas.numClauses(),
<a name="l00729"></a>00729 <span class="stringliteral">"Expected no lemmas after satisfiable check"</span>);
<a name="l00730"></a>00730 d_dplltReady = <span class="keyword">true</span>;
<a name="l00731"></a>00731 d_lastValid = <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>();
<a name="l00732"></a>00732 <span class="keywordflow">if</span> (qres == <a class="code" href="xchaff__solver_8h.html#a259c70233f322b3e490149190b8bb87baa6a5c07f8c320f440ebc34fed65eb550">SATISFIABLE</a> && d_core->incomplete()) qres = <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">UNKNOWN</a>;
<a name="l00733"></a>00733
<a name="l00734"></a>00734 <span class="preprocessor">#ifdef _CVC3_DEBUG_MODE</span>
<a name="l00735"></a>00735 <span class="preprocessor"></span>
<a name="l00736"></a>00736 <span class="keywordflow">if</span>( CVC3::debugger.trace(<span class="stringliteral">"quant debug"</span>) ){
<a name="l00737"></a>00737 d_core->theoryOf(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7b7b6f6e2b88589bd4656a14bcb7eb94">FORALL</a>)->debug(1);
<a name="l00738"></a>00738 }
<a name="l00739"></a>00739
<a name="l00740"></a>00740
<a name="l00741"></a>00741 <span class="keywordflow">if</span>( CVC3::debugger.trace(<span class="stringliteral">"sat model unknown"</span>) ){
<a name="l00742"></a>00742 std::vector<SAT::Lit> cur_assigns = d_dpllt->getCurAssignments();
<a name="l00743"></a>00743 cout<<<span class="stringliteral">"Current assignments"</span><<<a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00744"></a>00744 {
<a name="l00745"></a>00745 <span class="keywordflow">for</span>(<span class="keywordtype">size_t</span> i = 0 ; i < cur_assigns.size(); i++){
<a name="l00746"></a>00746 <a class="code" href="classSAT_1_1Lit.html">Lit</a> l = cur_assigns[i];
<a name="l00747"></a>00747 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e = d_cnfManager->concreteLit(l);
<a name="l00748"></a>00748
<a name="l00749"></a>00749 <span class="keywordtype">string</span> val = <span class="stringliteral">" := "</span>;
<a name="l00750"></a>00750
<a name="l00751"></a>00751 <span class="keywordflow">if</span> (l.<a class="code" href="classSAT_1_1Lit.html#ada14f3ca2b88500b5c2500d60e7f554b">isPositive</a>()) val += <span class="stringliteral">"1"</span>; <span class="keywordflow">else</span> val += <span class="stringliteral">"0"</span>;
<a name="l00752"></a>00752 cout<<l.<a class="code" href="classSAT_1_1Lit.html#a57e2e6e37cad9595c3edbea88a41262f">getVar</a>()<<val<<<a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00753"></a>00753 <span class="comment">// cout<<e<<endl;</span>
<a name="l00754"></a>00754
<a name="l00755"></a>00755 }
<a name="l00756"></a>00756 }
<a name="l00757"></a>00757
<a name="l00758"></a>00758
<a name="l00759"></a>00759 std::vector< std::vector<SAT::Lit> > cur_clauses = d_dpllt->getCurClauses();
<a name="l00760"></a>00760 cout<<<span class="stringliteral">"Current Clauses"</span><<<a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00761"></a>00761 {
<a name="l00762"></a>00762 <span class="keywordflow">for</span>(<span class="keywordtype">size_t</span> i = 0 ; i < cur_clauses.size(); i++){
<a name="l00763"></a>00763 <span class="comment">// cout<<"clause "<<i<<"================="<<endl;</span>
<a name="l00764"></a>00764 <span class="keywordflow">for</span>(<span class="keywordtype">size_t</span> j = 0; j < cur_clauses[i].size(); j++){
<a name="l00765"></a>00765
<a name="l00766"></a>00766 <a class="code" href="classSAT_1_1Lit.html">Lit</a> l = cur_clauses[i][j];
<a name="l00767"></a>00767 <span class="keywordtype">string</span> val ;
<a name="l00768"></a>00768 <span class="keywordflow">if</span> (l.<a class="code" href="classSAT_1_1Lit.html#ada14f3ca2b88500b5c2500d60e7f554b">isPositive</a>()) val += <span class="stringliteral">"+"</span>; <span class="keywordflow">else</span> val += <span class="stringliteral">"-"</span>;
<a name="l00769"></a>00769 cout<<val<<l.<a class="code" href="classSAT_1_1Lit.html#a57e2e6e37cad9595c3edbea88a41262f">getVar</a>()<<<span class="stringliteral">" "</span>;
<a name="l00770"></a>00770 }
<a name="l00771"></a>00771 cout<<<a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00772"></a>00772 }
<a name="l00773"></a>00773 }
<a name="l00774"></a>00774 }
<a name="l00775"></a>00775
<a name="l00776"></a>00776 <span class="keywordflow">if</span>( CVC3::debugger.trace(<span class="stringliteral">"model unknown"</span>) ){
<a name="l00777"></a>00777 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a>& allterms = d_core->getTerms();
<a name="l00778"></a>00778 cout<<<span class="stringliteral">"===========terms begin=========="</span><<<a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00779"></a>00779
<a name="l00780"></a>00780 <span class="keywordflow">for</span> (<span class="keywordtype">size_t</span> i=0; i<allterms.<a class="code" href="classCVC3_1_1CDList.html#adf92d0f391d73e7ac70da57db135af27">size</a>(); i++){
<a name="l00781"></a>00781 <span class="comment">// cout<<"i="<<i<<" :"<<allterms[i].getFindLevel()<<":"<<d_core->simplifyExpr(allterms[i])<<"|"<<allterms[i]<<endl;</span>
<a name="l00782"></a>00782 cout<<<span class="stringliteral">"i="</span><<i<<<span class="stringliteral">" :"</span><<allterms[i].getFindLevel()<<<span class="stringliteral">":"</span><<d_core->simplifyExpr(allterms[i])<<<span class="stringliteral">"|"</span><<allterms[i]<<<a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00783"></a>00783
<a name="l00784"></a>00784 <span class="comment">//<<" and type is "<<allterms[i].getType() </span>
<a name="l00785"></a>00785 <span class="comment">// << " and kind is" << allterms[i].getEM()->getKindName(allterms[i].getKind())<<endl;</span>
<a name="l00786"></a>00786 }
<a name="l00787"></a>00787 cout<<<span class="stringliteral">"-----------term end ---------"</span><<<a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00788"></a>00788 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a>& allpreds = d_core->getPredicates();
<a name="l00789"></a>00789 cout<<<span class="stringliteral">"===========pred begin=========="</span><<<a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00790"></a>00790
<a name="l00791"></a>00791 <span class="keywordflow">for</span> (<span class="keywordtype">size_t</span> i=0; i<allpreds.<a class="code" href="classCVC3_1_1CDList.html#adf92d0f391d73e7ac70da57db135af27">size</a>(); i++){
<a name="l00792"></a>00792 <span class="keywordflow">if</span>(allpreds[i].hasFind()){
<a name="l00793"></a>00793 <span class="keywordflow">if</span>( (d_core->findExpr(allpreds[i])).isTrue()){
<a name="l00794"></a>00794 cout<<<span class="stringliteral">"ASSERT "</span><< allpreds[i] <<<span class="stringliteral">";"</span> <<<a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00795"></a>00795 }
<a name="l00796"></a>00796 <span class="keywordflow">else</span>{
<a name="l00797"></a>00797 cout<<<span class="stringliteral">"ASSERT NOT("</span><< allpreds[i] <<<span class="stringliteral">");"</span> <<<a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00798"></a>00798 }
<a name="l00799"></a>00799 <span class="comment">// cout<<"i="<<i<<" :";</span>
<a name="l00800"></a>00800 <span class="comment">// cout<<allpreds[i].getFindLevel();</span>
<a name="l00801"></a>00801 <span class="comment">// cout<<":"<<d_core->findExpr(allpreds[i])<<"|"<<allpreds[i]<<endl;</span>
<a name="l00802"></a>00802 }
<a name="l00803"></a>00803 <span class="comment">// else cout<<"U "<<endl;;</span>
<a name="l00804"></a>00804
<a name="l00805"></a>00805
<a name="l00806"></a>00806 <span class="comment">//" and type is "<<allpreds[i].getType() </span>
<a name="l00807"></a>00807 <span class="comment">// << " and kind is" << allpreds[i].getEM()->getKindName(allpreds[i].getKind())<<endl;</span>
<a name="l00808"></a>00808 }
<a name="l00809"></a>00809 cout<<<span class="stringliteral">"-----------end----------pred"</span><<<a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00810"></a>00810 }
<a name="l00811"></a>00811
<a name="l00812"></a>00812 <span class="keywordflow">if</span>( CVC3::debugger.trace(<span class="stringliteral">"model unknown quant"</span>) ){
<a name="l00813"></a>00813 cout<<<span class="stringliteral">"=========== quant pred begin=========="</span><<<a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00814"></a>00814 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a>& allpreds = d_core->getPredicates();
<a name="l00815"></a>00815 <span class="keywordflow">for</span> (<span class="keywordtype">size_t</span> i=0; i<allpreds.<a class="code" href="classCVC3_1_1CDList.html#adf92d0f391d73e7ac70da57db135af27">size</a>(); i++){
<a name="l00816"></a>00816
<a name="l00817"></a>00817 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> cur = allpreds[i];
<a name="l00818"></a>00818 <span class="keywordflow">if</span>(cur.<a class="code" href="group__ExprPkg.html#gaad6095e1d8b1551a006602d9421fb988">isForall</a>() || cur.<a class="code" href="group__ExprPkg.html#ga1c922163af59ed6bc101728d65e04d16">isExists</a>() || (cur.<a class="code" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a>() && (cur[0].<a class="code" href="group__ExprPkg.html#gaad6095e1d8b1551a006602d9421fb988">isForall</a>()||cur[0].<a class="code" href="group__ExprPkg.html#ga1c922163af59ed6bc101728d65e04d16">isExists</a>()))){
<a name="l00819"></a>00819 <span class="keywordflow">if</span>(allpreds[i].hasFind()) {
<a name="l00820"></a>00820 cout<<<span class="stringliteral">"i="</span><<i<<<span class="stringliteral">" :"</span>;
<a name="l00821"></a>00821 cout<<allpreds[i].getFindLevel();
<a name="l00822"></a>00822 cout<<<span class="stringliteral">":"</span><<d_core->findExpr(allpreds[i])<<<span class="stringliteral">"|"</span><<allpreds[i]<<<a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00823"></a>00823 }
<a name="l00824"></a>00824 }
<a name="l00825"></a>00825 }
<a name="l00826"></a>00826 cout<<<span class="stringliteral">"-----------end----------pred"</span><<<a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00827"></a>00827 }
<a name="l00828"></a>00828
<a name="l00829"></a>00829 <span class="keywordflow">if</span>( CVC3::debugger.trace(<span class="stringliteral">"model unknown nonquant"</span>) ){
<a name="l00830"></a>00830 cout<<<span class="stringliteral">"=========== quant pred begin=========="</span><<<a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00831"></a>00831 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a>& allpreds = d_core->getPredicates();
<a name="l00832"></a>00832 <span class="keywordflow">for</span> (<span class="keywordtype">size_t</span> i=0; i<allpreds.<a class="code" href="classCVC3_1_1CDList.html#adf92d0f391d73e7ac70da57db135af27">size</a>(); i++){
<a name="l00833"></a>00833
<a name="l00834"></a>00834 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> cur = allpreds[i];
<a name="l00835"></a>00835 <span class="keywordflow">if</span>(cur.<a class="code" href="group__ExprPkg.html#gaad6095e1d8b1551a006602d9421fb988">isForall</a>() || cur.<a class="code" href="group__ExprPkg.html#ga1c922163af59ed6bc101728d65e04d16">isExists</a>() ||
<a name="l00836"></a>00836 (cur.<a class="code" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a>() && (cur[0].<a class="code" href="group__ExprPkg.html#gaad6095e1d8b1551a006602d9421fb988">isForall</a>()||cur[0].<a class="code" href="group__ExprPkg.html#ga1c922163af59ed6bc101728d65e04d16">isExists</a>())) ||
<a name="l00837"></a>00837 cur.<a class="code" href="group__ExprPkg.html#gac4af2026c180da0f18d66ac616f61f3a">isEq</a>() ||
<a name="l00838"></a>00838 (cur.<a class="code" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a>() && cur[0].<a class="code" href="group__ExprPkg.html#gac4af2026c180da0f18d66ac616f61f3a">isEq</a>())){
<a name="l00839"></a>00839 }
<a name="l00840"></a>00840 <span class="keywordflow">else</span>{
<a name="l00841"></a>00841 <span class="keywordflow">if</span>(allpreds[i].hasFind()) {
<a name="l00842"></a>00842 cout<<<span class="stringliteral">"i="</span><<i<<<span class="stringliteral">" :"</span>;
<a name="l00843"></a>00843 cout<<allpreds[i].getFindLevel();
<a name="l00844"></a>00844 cout<<<span class="stringliteral">":"</span><<d_core->findExpr(allpreds[i])<<<span class="stringliteral">"|"</span><<allpreds[i]<<<a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00845"></a>00845 }
<a name="l00846"></a>00846 }
<a name="l00847"></a>00847 }
<a name="l00848"></a>00848 cout<<<span class="stringliteral">"-----------end----------pred"</span><<<a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00849"></a>00849 }
<a name="l00850"></a>00850
<a name="l00851"></a>00851 <span class="keywordflow">if</span>( CVC3::debugger.trace(<span class="stringliteral">"unknown state"</span>) ){
<a name="l00852"></a>00852 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a>& allpreds = d_core->getPredicates();
<a name="l00853"></a>00853 cout<<<span class="stringliteral">"===========pred begin=========="</span><<<a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00854"></a>00854
<a name="l00855"></a>00855 <span class="keywordflow">for</span> (<span class="keywordtype">size_t</span> i=0; i<allpreds.<a class="code" href="classCVC3_1_1CDList.html#adf92d0f391d73e7ac70da57db135af27">size</a>(); i++){
<a name="l00856"></a>00856 <span class="keywordflow">if</span>(allpreds[i].hasFind()){
<a name="l00857"></a>00857 <span class="comment">// Expr cur(allpreds[i]);</span>
<a name="l00858"></a>00858 <span class="comment">// if(cur.isForall() || cur.isExists() || </span>
<a name="l00859"></a>00859 <span class="comment">// (cur.isNot() && (cur[0].isForall()||cur[0].isExists()))</span>
<a name="l00860"></a>00860 <span class="comment">// ){</span>
<a name="l00861"></a>00861 <span class="comment">// continue;</span>
<a name="l00862"></a>00862 <span class="comment">// }</span>
<a name="l00863"></a>00863
<a name="l00864"></a>00864 <span class="keywordflow">if</span>( (d_core->findExpr(allpreds[i])).isTrue()){
<a name="l00865"></a>00865 cout<<<span class="stringliteral">":assumption "</span><< allpreds[i] <<<span class="stringliteral">""</span> <<<a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00866"></a>00866 }
<a name="l00867"></a>00867 <span class="keywordflow">else</span>{
<a name="l00868"></a>00868 cout<<<span class="stringliteral">":assumption(not "</span><< allpreds[i] <<<span class="stringliteral">")"</span> <<<a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00869"></a>00869 }
<a name="l00870"></a>00870 <span class="comment">// cout<<"i="<<i<<" :";</span>
<a name="l00871"></a>00871 <span class="comment">// cout<<allpreds[i].getFindLevel();</span>
<a name="l00872"></a>00872 <span class="comment">// cout<<":"<<d_core->findExpr(allpreds[i])<<"|"<<allpreds[i]<<endl;</span>
<a name="l00873"></a>00873 }
<a name="l00874"></a>00874 <span class="comment">// else cout<<"U "<<endl;;</span>
<a name="l00875"></a>00875
<a name="l00876"></a>00876
<a name="l00877"></a>00877 <span class="comment">//" and type is "<<allpreds[i].getType() </span>
<a name="l00878"></a>00878 <span class="comment">// << " and kind is" << allpreds[i].getEM()->getKindName(allpreds[i].getKind())<<endl;</span>
<a name="l00879"></a>00879 }
<a name="l00880"></a>00880 cout<<<span class="stringliteral">"-----------end----------pred"</span><<<a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00881"></a>00881 }
<a name="l00882"></a>00882
<a name="l00883"></a>00883 <span class="keywordflow">if</span>( CVC3::debugger.trace(<span class="stringliteral">"unknown state noforall"</span>) ){
<a name="l00884"></a>00884 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a>& allpreds = d_core->getPredicates();
<a name="l00885"></a>00885 cout<<<span class="stringliteral">"===========pred begin=========="</span><<<a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00886"></a>00886
<a name="l00887"></a>00887 <span class="keywordflow">for</span> (<span class="keywordtype">size_t</span> i=0; i<allpreds.<a class="code" href="classCVC3_1_1CDList.html#adf92d0f391d73e7ac70da57db135af27">size</a>(); i++){
<a name="l00888"></a>00888 <span class="keywordflow">if</span>(allpreds[i].hasFind()){
<a name="l00889"></a>00889 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> cur(allpreds[i]);
<a name="l00890"></a>00890 <span class="comment">// if(cur.isForall() || cur.isExists() || </span>
<a name="l00891"></a>00891 <span class="comment">// (cur.isNot() && (cur[0].isForall()||cur[0].isExists()))</span>
<a name="l00892"></a>00892 <span class="comment">// ){</span>
<a name="l00893"></a>00893 <span class="comment">// continue;</span>
<a name="l00894"></a>00894 <span class="comment">// }</span>
<a name="l00895"></a>00895
<a name="l00896"></a>00896 <span class="keywordflow">if</span>( (d_core->findExpr(allpreds[i])).isTrue()){
<a name="l00897"></a>00897 <span class="comment">// if(cur.isExists()){</span>
<a name="l00898"></a>00898 <span class="comment">// continue;</span>
<a name="l00899"></a>00899 <span class="comment">// }</span>
<a name="l00900"></a>00900 cout<<<span class="stringliteral">"ASSERT "</span><< allpreds[i] <<<span class="stringliteral">";"</span> <<<a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00901"></a>00901 <span class="comment">// cout<<":assumption "<< allpreds[i] <<"" <<endl;</span>
<a name="l00902"></a>00902 }
<a name="l00903"></a>00903 <span class="keywordflow">else</span> <span class="keywordflow">if</span> ( (d_core->findExpr(allpreds[i])).isFalse()){
<a name="l00904"></a>00904 <span class="comment">// if (cur.isForall()){</span>
<a name="l00905"></a>00905 <span class="comment">// continue;</span>
<a name="l00906"></a>00906 <span class="comment">// }</span>
<a name="l00907"></a>00907 cout<<<span class="stringliteral">"ASSERT (NOT "</span><< allpreds[i] <<<span class="stringliteral">");"</span> <<<a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00908"></a>00908 <span class="comment">// cout<<":assumption(not "<< allpreds[i] <<")" <<endl;</span>
<a name="l00909"></a>00909 }
<a name="l00910"></a>00910 <span class="keywordflow">else</span>{
<a name="l00911"></a>00911 cout<<<span class="stringliteral">"--ERROR"</span><<<a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00912"></a>00912 }
<a name="l00913"></a>00913 <span class="comment">// cout<<"i="<<i<<" :";</span>
<a name="l00914"></a>00914 <span class="comment">// cout<<allpreds[i].getFindLevel();</span>
<a name="l00915"></a>00915 <span class="comment">// cout<<":"<<d_core->findExpr(allpreds[i])<<"|"<<allpreds[i]<<endl;</span>
<a name="l00916"></a>00916 }
<a name="l00917"></a>00917 <span class="comment">// else cout<<"U "<<endl;;</span>
<a name="l00918"></a>00918
<a name="l00919"></a>00919
<a name="l00920"></a>00920 <span class="comment">//" and type is "<<allpreds[i].getType() </span>
<a name="l00921"></a>00921 <span class="comment">// << " and kind is" << allpreds[i].getEM()->getKindName(allpreds[i].getKind())<<endl;</span>
<a name="l00922"></a>00922 }
<a name="l00923"></a>00923 cout<<<span class="stringliteral">"-----------end----------pred"</span><<<a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00924"></a>00924 }
<a name="l00925"></a>00925
<a name="l00926"></a>00926
<a name="l00927"></a>00927 <span class="preprocessor">#endif</span>
<a name="l00928"></a>00928 <span class="preprocessor"></span> }
<a name="l00929"></a>00929 d_cnfManager->setBottomScope(-1);
<a name="l00930"></a>00930 d_inCheckSat = <span class="keyword">false</span>;
<a name="l00931"></a>00931 result = d_lastValid;
<a name="l00932"></a>00932 <span class="keywordflow">return</span> qres;
<a name="l00933"></a>00933 }
<a name="l00934"></a>00934
<a name="l00935"></a>00935
<a name="l00936"></a><a class="code" href="classCVC3_1_1SearchSat.html#a8298bda3d71fc4f613476d49c8270ecc">00936</a> SearchSat::SearchSat(<a class="code" href="classCVC3_1_1TheoryCore.html" title="This theory handles the built-in logical connectives plus equality. It also handles the registration ...">TheoryCore</a>* core, <span class="keyword">const</span> <span class="keywordtype">string</span>& name)
<a name="l00937"></a>00937 : <a class="code" href="classCVC3_1_1SearchEngine.html" title="API to to a generic proof search engine.">SearchEngine</a>(core),
<a name="l00938"></a>00938 d_name(name),
<a name="l00939"></a>00939 d_bottomScope(core->getCM()->getCurrentContext(), -1),
<a name="l00940"></a>00940 d_lastCheck(core->getCM()->getCurrentContext()),
<a name="l00941"></a>00941 d_lastValid(core->getCM()->getCurrentContext(),
<a name="l00942"></a>00942 d_commonRules->trueTheorem()),
<a name="l00943"></a>00943 d_userAssumptions(core->getCM()->getCurrentContext()),
<a name="l00944"></a>00944 d_intAssumptions(core->getCM()->getCurrentContext()),
<a name="l00945"></a>00945 d_idxUserAssump(core->getCM()->getCurrentContext(), 0),
<a name="l00946"></a>00946 d_decider(NULL),
<a name="l00947"></a>00947 d_theorems(core->getCM()->getCurrentContext()),
<a name="l00948"></a>00948 d_inCheckSat(false),
<a name="l00949"></a>00949 d_lemmas(core->getCM()->getCurrentContext()),
<a name="l00950"></a>00950 d_pendingLemmasSize(core->getCM()->getCurrentContext(), 0),
<a name="l00951"></a>00951 d_pendingLemmasNext(core->getCM()->getCurrentContext(), 0),
<a name="l00952"></a>00952 d_lemmasNext(core->getCM()->getCurrentContext(), 0),
<a name="l00953"></a>00953 d_varsUndoListSize(core->getCM()->getCurrentContext(), 0),
<a name="l00954"></a>00954 d_prioritySetStart(core->getCM()->getCurrentContext()),
<a name="l00955"></a>00955 d_prioritySetEntriesSize(core->getCM()->getCurrentContext(), 0),
<a name="l00956"></a>00956 d_prioritySetBottomEntriesSize(0),
<a name="l00957"></a>00957 d_lastRegisteredVar(core->getCM()->getCurrentContext(), 0),
<a name="l00958"></a>00958 d_dplltReady(core->getCM()->getCurrentContext(), true),
<a name="l00959"></a>00959 d_nextImpliedLiteral(core->getCM()->getCurrentContext(), 0),
<a name="l00960"></a>00960 d_restorer(core->getCM()->getCurrentContext(), this)
<a name="l00961"></a>00961 {
<a name="l00962"></a>00962 <a class="code" href="classCVC3_1_1SearchSat.html#a996335737d383fd882b6f1085f72b964" title="Manages CNF formula and its relationship to original Exprs and Theorems.">d_cnfManager</a> = <span class="keyword">new</span> <a class="code" href="classSAT_1_1CNF__Manager.html">CNF_Manager</a>(core-><a class="code" href="classCVC3_1_1TheoryCore.html#af3077cff0601b8ae28e420ef5ce2ea37">getTM</a>(), core-><a class="code" href="classCVC3_1_1TheoryCore.html#a7f119c4fa5313b72feca7dd441e045f0">getStatistics</a>(),
<a name="l00963"></a>00963 core-><a class="code" href="classCVC3_1_1TheoryCore.html#a46b2792a5c24f95ccfc3fbfc0456b09f">getFlags</a>());
<a name="l00964"></a>00964
<a name="l00965"></a>00965 <a class="code" href="classCVC3_1_1SearchSat.html#a158485ff14b490fc2c91936a4e72bf5b" title="Callback for CNF_Manager.">d_cnfCallback</a> = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1SearchSat.html#acfd18b3733ce33513e1e5ddaad615624">SearchSatCNFCallback</a>(<span class="keyword">this</span>);
<a name="l00966"></a>00966 <a class="code" href="classCVC3_1_1SearchSat.html#a996335737d383fd882b6f1085f72b964" title="Manages CNF formula and its relationship to original Exprs and Theorems.">d_cnfManager</a>-><a class="code" href="classSAT_1_1CNF__Manager.html#a0d2b7a6369e9e7ad4ae6aca1398e404d" title="Register CNF callback.">registerCNFCallback</a>(d_cnfCallback);
<a name="l00967"></a>00967 <a class="code" href="classCVC3_1_1SearchSat.html#aab55d9ceeb2a938841230c920762ba77">d_coreSatAPI</a> = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1SearchSat.html#a71c71132ecb225ad44dd66fc2c3505f3">SearchSatCoreSatAPI</a>(<span class="keyword">this</span>);
<a name="l00968"></a>00968 core-><a class="code" href="classCVC3_1_1TheoryCore.html#afb6629080bceb44023f1bb3a44f9136f" title="Register a SatAPI for TheoryCore.">registerCoreSatAPI</a>(<a class="code" href="classCVC3_1_1SearchSat.html#aab55d9ceeb2a938841230c920762ba77">d_coreSatAPI</a>);
<a name="l00969"></a>00969 <a class="code" href="classCVC3_1_1SearchSat.html#a8abc1b647affa60cc367e0eeaa52cdf4" title="Implementation of TheoryAPI for DPLLT.">d_theoryAPI</a> = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1SearchSat.html#a8cb09d5d17839a0377e369713fcbbedf">SearchSatTheoryAPI</a>(<span class="keyword">this</span>);
<a name="l00970"></a>00970 <span class="keywordflow">if</span> (core-><a class="code" href="classCVC3_1_1TheoryCore.html#a46b2792a5c24f95ccfc3fbfc0456b09f">getFlags</a>()[<span class="stringliteral">"de"</span>].getString() == <span class="stringliteral">"dfs"</span>) <a class="code" href="classCVC3_1_1SearchSat.html#aa4be1d02557a46fbbdc32deefc4f3a32" title="Implementation of Decider for DPLLT.">d_decider</a> = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1SearchSat.html#a447de240c99ed9d998d211b07609bc5d">SearchSatDecider</a>(<span class="keyword">this</span>);
<a name="l00971"></a>00971
<a name="l00972"></a>00972 <span class="keywordflow">if</span> (core-><a class="code" href="classCVC3_1_1TheoryCore.html#a46b2792a5c24f95ccfc3fbfc0456b09f">getFlags</a>()[<span class="stringliteral">"sat"</span>].getString() == <span class="stringliteral">"sat"</span>) {
<a name="l00973"></a>00973 <span class="preprocessor">#ifdef DPLL_BASIC</span>
<a name="l00974"></a>00974 <span class="preprocessor"></span> <a class="code" href="classCVC3_1_1SearchSat.html#a884c103ef1313d56a3a42d4e3e8468cb" title="Pointer to DPLLT implementation.">d_dpllt</a> = <span class="keyword">new</span> <a class="code" href="classSAT_1_1DPLLTBasic.html">DPLLTBasic</a>(<a class="code" href="classCVC3_1_1SearchSat.html#a8abc1b647affa60cc367e0eeaa52cdf4" title="Implementation of TheoryAPI for DPLLT.">d_theoryAPI</a>, <a class="code" href="classCVC3_1_1SearchSat.html#aa4be1d02557a46fbbdc32deefc4f3a32" title="Implementation of Decider for DPLLT.">d_decider</a>, core-><a class="code" href="classCVC3_1_1TheoryCore.html#a9377f423f4fd59fdac396794363733a6">getCM</a>(),
<a name="l00975"></a>00975 core-><a class="code" href="classCVC3_1_1TheoryCore.html#a46b2792a5c24f95ccfc3fbfc0456b09f">getFlags</a>()[<span class="stringliteral">"stats"</span>].getBool());
<a name="l00976"></a>00976 <span class="preprocessor">#else</span>
<a name="l00977"></a>00977 <span class="preprocessor"></span> <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1CLException.html">CLException</a>(<span class="stringliteral">"SAT solver 'sat' not supported in this build"</span>);
<a name="l00978"></a>00978 <span class="preprocessor">#endif</span>
<a name="l00979"></a>00979 <span class="preprocessor"></span> } <span class="keywordflow">else</span> <span class="keywordflow">if</span> (core-><a class="code" href="classCVC3_1_1TheoryCore.html#a46b2792a5c24f95ccfc3fbfc0456b09f">getFlags</a>()[<span class="stringliteral">"sat"</span>].getString() == <span class="stringliteral">"minisat"</span>) {
<a name="l00980"></a>00980 <a class="code" href="classCVC3_1_1SearchSat.html#a884c103ef1313d56a3a42d4e3e8468cb" title="Pointer to DPLLT implementation.">d_dpllt</a> = <span class="keyword">new</span> <a class="code" href="classSAT_1_1DPLLTMiniSat.html">DPLLTMiniSat</a>(<a class="code" href="classCVC3_1_1SearchSat.html#a8abc1b647affa60cc367e0eeaa52cdf4" title="Implementation of TheoryAPI for DPLLT.">d_theoryAPI</a>, <a class="code" href="classCVC3_1_1SearchSat.html#aa4be1d02557a46fbbdc32deefc4f3a32" title="Implementation of Decider for DPLLT.">d_decider</a>,
<a name="l00981"></a>00981 core-><a class="code" href="classCVC3_1_1TheoryCore.html#a46b2792a5c24f95ccfc3fbfc0456b09f">getFlags</a>()[<span class="stringliteral">"stats"</span>].getBool(),
<a name="l00982"></a>00982 core-><a class="code" href="classCVC3_1_1TheoryCore.html#af3077cff0601b8ae28e420ef5ce2ea37">getTM</a>()-><a class="code" href="classCVC3_1_1TheoremManager.html#a462f27eb0eca420b334354a9ddc7a257">withProof</a>());
<a name="l00983"></a>00983 } <span class="keywordflow">else</span> {
<a name="l00984"></a>00984 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1CLException.html">CLException</a>(<span class="stringliteral">"Unrecognized SAT solver name: "</span> + (core-><a class="code" href="classCVC3_1_1TheoryCore.html#a46b2792a5c24f95ccfc3fbfc0456b09f">getFlags</a>()[<span class="stringliteral">"sat"</span>].getString()));
<a name="l00985"></a>00985 }
<a name="l00986"></a>00986
<a name="l00987"></a>00987 <a class="code" href="classCVC3_1_1SearchSat.html#ad7b3c57fadbc655bddd204b9ea122a62" title="Current position in prioritySet.">d_prioritySetStart</a> = <a class="code" href="classCVC3_1_1SearchSat.html#ab4dbd42cf98469a2abb679024a402b77" title="Used to determine order to find splitters.">d_prioritySet</a>.end();
<a name="l00988"></a>00988 }
<a name="l00989"></a>00989
<a name="l00990"></a>00990
<a name="l00991"></a><a class="code" href="classCVC3_1_1SearchSat.html#ad2e00c54dd9d8d8f1e674065f255a28b">00991</a> <a class="code" href="classCVC3_1_1SearchSat.html#ad2e00c54dd9d8d8f1e674065f255a28b" title="Destructor.">SearchSat::~SearchSat</a>()
<a name="l00992"></a>00992 {
<a name="l00993"></a>00993 <span class="keyword">delete</span> <a class="code" href="classCVC3_1_1SearchSat.html#a884c103ef1313d56a3a42d4e3e8468cb" title="Pointer to DPLLT implementation.">d_dpllt</a>;
<a name="l00994"></a>00994 <span class="keyword">delete</span> <a class="code" href="classCVC3_1_1SearchSat.html#aa4be1d02557a46fbbdc32deefc4f3a32" title="Implementation of Decider for DPLLT.">d_decider</a>;
<a name="l00995"></a>00995 <span class="keyword">delete</span> <a class="code" href="classCVC3_1_1SearchSat.html#a8abc1b647affa60cc367e0eeaa52cdf4" title="Implementation of TheoryAPI for DPLLT.">d_theoryAPI</a>;
<a name="l00996"></a>00996 <span class="keyword">delete</span> <a class="code" href="classCVC3_1_1SearchSat.html#aab55d9ceeb2a938841230c920762ba77">d_coreSatAPI</a>;
<a name="l00997"></a>00997 <span class="keyword">delete</span> <a class="code" href="classCVC3_1_1SearchSat.html#a158485ff14b490fc2c91936a4e72bf5b" title="Callback for CNF_Manager.">d_cnfCallback</a>;
<a name="l00998"></a>00998 <span class="keyword">delete</span> <a class="code" href="classCVC3_1_1SearchSat.html#a996335737d383fd882b6f1085f72b964" title="Manages CNF formula and its relationship to original Exprs and Theorems.">d_cnfManager</a>;
<a name="l00999"></a>00999 }
<a name="l01000"></a>01000
<a name="l01001"></a>01001
<a name="l01002"></a><a class="code" href="classCVC3_1_1SearchSat.html#a2ca4a66d1bf7d0227e646edd3c9b9964">01002</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchSat.html#a2ca4a66d1bf7d0227e646edd3c9b9964" title="Register an atomic formula of interest.">SearchSat::registerAtom</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e)
<a name="l01003"></a>01003 {
<a name="l01004"></a>01004 e.<a class="code" href="group__ExprPkg.html#ga6f8db899f4680e53c4cf11c20dc10735" title="Set the UserRegisteredAtom flag for this Expr.">setUserRegisteredAtom</a>();
<a name="l01005"></a>01005 <span class="keywordflow">if</span> (!e.<a class="code" href="group__ExprPkg.html#ga8b55ff94d7f47d1166350cf308f2dd09">isRegisteredAtom</a>())
<a name="l01006"></a>01006 <a class="code" href="group__SE.html#ga3772c6af7eac91b9ed7fc278edf5ef90" title="Access to theory reasoning.">d_core</a>-><a class="code" href="classCVC3_1_1TheoryCore.html#ade1177fbf32e95b9433eb608c82857d7" title="Register an atomic formula of interest.">registerAtom</a>(e, <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>());
<a name="l01007"></a>01007 }
<a name="l01008"></a>01008
<a name="l01009"></a>01009
<a name="l01010"></a><a class="code" href="classCVC3_1_1SearchSat.html#a737cf8f3791197c405017db18163ce6b">01010</a> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1SearchSat.html#a737cf8f3791197c405017db18163ce6b" title="Return next literal implied by last assertion. Null Expr if none.">SearchSat::getImpliedLiteral</a>(<span class="keywordtype">void</span>)
<a name="l01011"></a>01011 {
<a name="l01012"></a>01012 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> imp;
<a name="l01013"></a>01013 <span class="keywordflow">while</span> (d_nextImpliedLiteral < d_core->numImpliedLiterals()) {
<a name="l01014"></a>01014 imp = <a class="code" href="group__SE.html#ga3772c6af7eac91b9ed7fc278edf5ef90" title="Access to theory reasoning.">d_core</a>-><a class="code" href="classCVC3_1_1TheoryCore.html#adb97ff20d5c0d9a93d322b347b306f69" title="Return an implied literal by index.">getImpliedLiteralByIndex</a>(<a class="code" href="classCVC3_1_1SearchSat.html#ae97f61c9a0ae9ed8186929e15892ad73">d_nextImpliedLiteral</a>);
<a name="l01015"></a>01015 <a class="code" href="classCVC3_1_1SearchSat.html#ae97f61c9a0ae9ed8186929e15892ad73">d_nextImpliedLiteral</a> = <a class="code" href="classCVC3_1_1SearchSat.html#ae97f61c9a0ae9ed8186929e15892ad73">d_nextImpliedLiteral</a> + 1;
<a name="l01016"></a>01016 <span class="keywordflow">if</span> (imp.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>().<a class="code" href="group__ExprPkg.html#ga39070a3fb12c398dc5bb7526d6aeb7f3" title="Remove leading NOT if any.">unnegate</a>().<a class="code" href="group__ExprPkg.html#ga8296386eb481a436937b6f0b140f8af0">isUserRegisteredAtom</a>()) <span class="keywordflow">return</span> imp;
<a name="l01017"></a>01017 }
<a name="l01018"></a>01018 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>();
<a name="l01019"></a>01019 }
<a name="l01020"></a>01020
<a name="l01021"></a>01021
<a name="l01022"></a><a class="code" href="classCVC3_1_1SearchSat.html#a43a09dbf7232bfdb6f10aee4df1add94">01022</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchSat.html#a43a09dbf7232bfdb6f10aee4df1add94" title="Returns to context immediately before last call to checkValid.">SearchSat::returnFromCheck</a>()
<a name="l01023"></a>01023 {
<a name="l01024"></a>01024 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1SearchSat.html#a8153b8d7b772217bafddf3d92be4759b" title="Bottom scope for current query.">d_bottomScope</a> < 0) {
<a name="l01025"></a>01025 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1Exception.html">Exception</a>
<a name="l01026"></a>01026 (<span class="stringliteral">"returnFromCheck called with no previous invalid call to checkValid"</span>);
<a name="l01027"></a>01027 }
<a name="l01028"></a>01028 <a class="code" href="classCVC3_1_1SearchSat.html#a5c3eeec4b2c970f9d503b2892c9eb770" title="Restore last checkpoint.">pop</a>();
<a name="l01029"></a>01029 }
<a name="l01030"></a>01030
<a name="l01031"></a>01031
<a name="l01032"></a><a class="code" href="search__sat_8cpp.html#ad519c4d1da4622f4bca7cfdc5b6fee7b">01032</a> <span class="keyword">static</span> <span class="keywordtype">void</span> <a class="code" href="search__sat_8cpp.html#ad519c4d1da4622f4bca7cfdc5b6fee7b">setRecursiveInUserAssumption</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> scope)
<a name="l01033"></a>01033 {
<a name="l01034"></a>01034 <span class="keywordflow">if</span> (e.<a class="code" href="group__ExprPkg.html#ga110d4a1734b738dbb999b7798e07c3d1">inUserAssumption</a>()) <span class="keywordflow">return</span>;
<a name="l01035"></a>01035 <span class="keywordflow">for</span> (<span class="keywordtype">int</span> i = 0; i < e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>(); ++i) {
<a name="l01036"></a>01036 <a class="code" href="search__sat_8cpp.html#ad519c4d1da4622f4bca7cfdc5b6fee7b">setRecursiveInUserAssumption</a>(e[i], scope);
<a name="l01037"></a>01037 }
<a name="l01038"></a>01038 e.<a class="code" href="group__ExprPkg.html#gacfaaa30a1743a0955e0568b3bcd7cc08">setInUserAssumption</a>(scope);
<a name="l01039"></a>01039 }
<a name="l01040"></a>01040
<a name="l01041"></a>01041
<a name="l01042"></a><a class="code" href="classCVC3_1_1SearchSat.html#a4bc91d2be335eabdcd6174cf634fe9e3">01042</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchSat.html#a4bc91d2be335eabdcd6174cf634fe9e3" title="Helper for newUserAssumptionInt.">SearchSat::newUserAssumptionIntHelper</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm, <a class="code" href="classSAT_1_1CNF__Formula__Impl.html">CNF_Formula_Impl</a>& cnf, <span class="keywordtype">bool</span> atBottomScope)
<a name="l01043"></a>01043 {
<a name="l01044"></a>01044 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e = thm.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>();
<a name="l01045"></a>01045 <span class="keywordflow">if</span> (e.<a class="code" href="group__ExprPkg.html#ga383260cf4f8919728e2712e6e11f21fa">isAnd</a>()) {
<a name="l01046"></a>01046 <span class="keywordflow">for</span> (<span class="keywordtype">int</span> i = 0; i < e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>(); ++i) {
<a name="l01047"></a>01047 <a class="code" href="classCVC3_1_1SearchSat.html#a4bc91d2be335eabdcd6174cf634fe9e3" title="Helper for newUserAssumptionInt.">newUserAssumptionIntHelper</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, i), cnf, atBottomScope);
<a name="l01048"></a>01048 }
<a name="l01049"></a>01049 }
<a name="l01050"></a>01050 <span class="keywordflow">else</span> {
<a name="l01051"></a>01051 <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#a46b2792a5c24f95ccfc3fbfc0456b09f">getFlags</a>()[<span class="stringliteral">"cnf-formula"</span>].getBool()) {
<a name="l01052"></a>01052 <span class="keywordflow">if</span> (!<a class="code" href="classCVC3_1_1SearchSat.html#a0f3b2311296e520c22aea55c68c4b477" title="Helper for addLemma and check.">recordNewRootLit</a>(<a class="code" href="classCVC3_1_1SearchSat.html#a996335737d383fd882b6f1085f72b964" title="Manages CNF formula and its relationship to original Exprs and Theorems.">d_cnfManager</a>-><a class="code" href="classSAT_1_1CNF__Manager.html#a5cf1943a3bc3773fd0d8f64c123478f7" title="Given thm of form A |- B, convert B to CNF and add it to cnf.">addAssumption</a>(thm, cnf), 0, atBottomScope)) {
<a name="l01053"></a>01053 cnf.<a class="code" href="classSAT_1_1CNF__Formula__Impl.html#accfd5e8d24cbb46cef5c4025a92c40eb">deleteLast</a>();
<a name="l01054"></a>01054 }
<a name="l01055"></a>01055 }
<a name="l01056"></a>01056 <span class="keywordflow">else</span>{
<a name="l01057"></a>01057 <a class="code" href="classCVC3_1_1SearchSat.html#a996335737d383fd882b6f1085f72b964" title="Manages CNF formula and its relationship to original Exprs and Theorems.">d_cnfManager</a>-><a class="code" href="classSAT_1_1CNF__Manager.html#a5cf1943a3bc3773fd0d8f64c123478f7" title="Given thm of form A |- B, convert B to CNF and add it to cnf.">addAssumption</a>(thm, cnf);
<a name="l01058"></a>01058 }
<a name="l01059"></a>01059 <span class="comment">// if cnf-formula is enabled, d_cnfManager->addAssumption returns a random literal, not a RootLit. A random lit can make recordNewRootLit return false, which in turn makes cnf.deleteLast() to delete the last clause, which is not correct. </span>
<a name="l01060"></a>01060 }
<a name="l01061"></a>01061 }
<a name="l01062"></a>01062
<a name="l01063"></a>01063
<a name="l01064"></a><a class="code" href="classCVC3_1_1SearchSat.html#ab9c866f4bb3ba8f3662a8ee99760f257">01064</a> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1SearchSat.html#ab9c866f4bb3ba8f3662a8ee99760f257" title="Helper for newUserAssumption.">SearchSat::newUserAssumptionInt</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="classSAT_1_1CNF__Formula__Impl.html">CNF_Formula_Impl</a>& cnf, <span class="keywordtype">bool</span> atBottomScope)
<a name="l01065"></a>01065 {
<a name="l01066"></a>01066 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!<a class="code" href="classCVC3_1_1SearchSat.html#a00573a594dd2b83cbb6f2997516862d3" title="Whether we are currently in a call to dpllt->checkSat.">d_inCheckSat</a>,
<a name="l01067"></a>01067 <span class="stringliteral">"User assumptions should be added before calling checkSat"</span>);
<a name="l01068"></a>01068 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> thm;
<a name="l01069"></a>01069 <span class="keywordtype">int</span> scope;
<a name="l01070"></a>01070 <span class="keywordflow">if</span> (atBottomScope) scope = <a class="code" href="classCVC3_1_1SearchSat.html#a8153b8d7b772217bafddf3d92be4759b" title="Bottom scope for current query.">d_bottomScope</a>;
<a name="l01071"></a>01071 <span class="keywordflow">else</span> scope = -1;
<a name="l01072"></a>01072 <a class="code" href="search__sat_8cpp.html#ad519c4d1da4622f4bca7cfdc5b6fee7b">setRecursiveInUserAssumption</a>(e, scope);
<a name="l01073"></a>01073 <span class="keywordflow">if</span> (!<a class="code" href="classCVC3_1_1SearchSat.html#a4ec713d6bbbd5d4bd6a9fcacc42a044e" title="Check if the formula has already been assumed previously.">isAssumption</a>(e)) {
<a name="l01074"></a>01074 e.<a class="code" href="group__ExprPkg.html#ga63eb3b8c124654cf056b2814794c4236">setUserAssumption</a>(scope);
<a name="l01075"></a>01075 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, scope);
<a name="l01076"></a>01076 <a class="code" href="classCVC3_1_1SearchSat.html#a3b9b2371a24908e62ec71b6f141afea8" title="List of all user assumptions.">d_userAssumptions</a>.<a class="code" href="classCVC3_1_1CDList.html#aa1e8d3591c596d1b9c585dec955b519b">push_back</a>(thm, scope);
<a name="l01077"></a>01077
<a name="l01078"></a>01078 <span class="keywordflow">if</span> (atBottomScope && <a class="code" href="classCVC3_1_1SearchSat.html#a8153b8d7b772217bafddf3d92be4759b" title="Bottom scope for current query.">d_bottomScope</a> != <a class="code" href="group__SE.html#ga3772c6af7eac91b9ed7fc278edf5ef90" title="Access to theory reasoning.">d_core</a>-><a class="code" href="classCVC3_1_1TheoryCore.html#a9377f423f4fd59fdac396794363733a6">getCM</a>()-><a class="code" href="classCVC3_1_1ContextManager.html#a194f7ddd794eaa876544a45006a3ff6f">scopeLevel</a>()) {
<a name="l01079"></a>01079 <span class="comment">//TODO: run preprocessor without using context-dependent information</span>
<a name="l01080"></a>01080 <span class="comment">//TODO: this will break if we have stuff like the BVDIV rewrite that needs to get enqueued during preprocessing</span>
<a name="l01081"></a>01081 <a class="code" href="classCVC3_1_1SearchSat.html#a4bc91d2be335eabdcd6174cf634fe9e3" title="Helper for newUserAssumptionInt.">newUserAssumptionIntHelper</a>(thm, cnf, <span class="keyword">true</span>);
<a name="l01082"></a>01082 }
<a name="l01083"></a>01083 <span class="keywordflow">else</span> {
<a name="l01084"></a>01084 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> thm2 = <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="l01085"></a>01085 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e2 = thm2.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>();
<a name="l01086"></a>01086 <span class="keywordflow">if</span> (e2.<a class="code" href="group__ExprPkg.html#ga6173f64b22cba76472cd0c814bbf6dae">isFalse</a>()) {
<a name="l01087"></a>01087 <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>(thm2);
<a name="l01088"></a>01088 <span class="keywordflow">return</span> thm;
<a name="l01089"></a>01089 }
<a name="l01090"></a>01090 <span class="keywordflow">else</span> <span class="keywordflow">if</span> (!e2.<a class="code" href="group__ExprPkg.html#gadf8596df73fa69ff8e6a22b9321f5c34">isTrue</a>()) {
<a name="l01091"></a>01091 <a class="code" href="classCVC3_1_1SearchSat.html#a4bc91d2be335eabdcd6174cf634fe9e3" title="Helper for newUserAssumptionInt.">newUserAssumptionIntHelper</a>(thm2, cnf, <span class="keyword">false</span>);
<a name="l01092"></a>01092 }
<a name="l01093"></a>01093 }
<a name="l01094"></a>01094 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1SearchSat.html#a996335737d383fd882b6f1085f72b964" title="Manages CNF formula and its relationship to original Exprs and Theorems.">d_cnfManager</a>-><a class="code" href="classSAT_1_1CNF__Manager.html#ad6052496e803e074e91efe7212360b23" title="Return the number of variables being managed.">numVars</a>() > <a class="code" href="classCVC3_1_1SearchSat.html#a455c295a13215ddc99b8df18f4598af4" title="Cached values of variables.">d_vars</a>.size()) {
<a name="l01095"></a>01095 <a class="code" href="classCVC3_1_1SearchSat.html#a455c295a13215ddc99b8df18f4598af4" title="Cached values of variables.">d_vars</a>.resize(<a class="code" href="classCVC3_1_1SearchSat.html#a996335737d383fd882b6f1085f72b964" title="Manages CNF formula and its relationship to original Exprs and Theorems.">d_cnfManager</a>-><a class="code" href="classSAT_1_1CNF__Manager.html#ad6052496e803e074e91efe7212360b23" title="Return the number of variables being managed.">numVars</a>(), <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498ba249f3dbc426c80d4a31cb5073bf07cfa">SAT::Var::UNKNOWN</a>);
<a name="l01096"></a>01096 }
<a name="l01097"></a>01097 }
<a name="l01098"></a>01098 <span class="keywordflow">return</span> thm;
<a name="l01099"></a>01099 }
<a name="l01100"></a>01100
<a name="l01101"></a>01101
<a name="l01102"></a><a class="code" href="classCVC3_1_1SearchSat.html#a859331cc6fc93adfdd09cb848cd6de0b">01102</a> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1SearchSat.html#a859331cc6fc93adfdd09cb848cd6de0b" title="Generate and add an assumption to the set of assumptions in the current context.">SearchSat::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="l01103"></a>01103 {
<a name="l01104"></a>01104 <a class="code" href="classSAT_1_1CNF__Formula__Impl.html">CNF_Formula_Impl</a> cnf;
<a name="l01105"></a>01105 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> thm = <a class="code" href="classCVC3_1_1SearchSat.html#ab9c866f4bb3ba8f3662a8ee99760f257" title="Helper for newUserAssumption.">newUserAssumptionInt</a>(e, cnf, <span class="keyword">false</span>);
<a name="l01106"></a>01106 <a class="code" href="classCVC3_1_1SearchSat.html#a884c103ef1313d56a3a42d4e3e8468cb" title="Pointer to DPLLT implementation.">d_dpllt</a>-><a class="code" href="classSAT_1_1DPLLT.html#aaaa6884de9ebd8b9596e85167e8f9273" title="Add new clauses to the SAT solver.">addAssertion</a>(cnf);
<a name="l01107"></a>01107 <span class="keywordflow">return</span> thm;
<a name="l01108"></a>01108 }
<a name="l01109"></a>01109
<a name="l01110"></a>01110
<a name="l01111"></a><a class="code" href="classCVC3_1_1SearchSat.html#a7344ad67225c0d6e30f8c2215bc7e0b0">01111</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchSat.html#a7344ad67225c0d6e30f8c2215bc7e0b0" title="Get all user assumptions made in this and all previous contexts.">SearchSat::getUserAssumptions</a>(vector<Expr>& assumptions)
<a name="l01112"></a>01112 {
<a name="l01113"></a>01113 <span class="keywordflow">for</span>(<a class="code" href="classCVC3_1_1CDList.html">CDList<Theorem>::const_iterator</a> i=<a class="code" href="classCVC3_1_1SearchSat.html#a3b9b2371a24908e62ec71b6f141afea8" title="List of all user assumptions.">d_userAssumptions</a>.<a class="code" href="classCVC3_1_1CDList.html#ae2cf006604b1ab88139332a5e2c08568">begin</a>(),
<a name="l01114"></a>01114 iend=<a class="code" href="classCVC3_1_1SearchSat.html#a3b9b2371a24908e62ec71b6f141afea8" title="List of all user assumptions.">d_userAssumptions</a>.<a class="code" href="classCVC3_1_1CDList.html#a96313ff2924c89a93d7fe6c618c837af">end</a>(); i!=iend; ++i)
<a name="l01115"></a>01115 assumptions.push_back((*i).getExpr());
<a name="l01116"></a>01116 }
<a name="l01117"></a>01117
<a name="l01118"></a>01118
<a name="l01119"></a><a class="code" href="classCVC3_1_1SearchSat.html#acee513ead4033fd5bfc16cbab7951dc7">01119</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchSat.html#acee513ead4033fd5bfc16cbab7951dc7" title="Get assumptions made internally in this and all previous contexts.">SearchSat::getInternalAssumptions</a>(vector<Expr>& assumptions)
<a name="l01120"></a>01120 {
<a name="l01121"></a>01121 <span class="keywordflow">for</span>(<a class="code" href="classCVC3_1_1CDList.html">CDList<Theorem>::const_iterator</a> i=<a class="code" href="classCVC3_1_1SearchSat.html#ad3b9879d655cf3fce1a70de7b1d6fedc" title="List of all internal assumptions.">d_intAssumptions</a>.<a class="code" href="classCVC3_1_1CDList.html#ae2cf006604b1ab88139332a5e2c08568">begin</a>(),
<a name="l01122"></a>01122 iend=<a class="code" href="classCVC3_1_1SearchSat.html#ad3b9879d655cf3fce1a70de7b1d6fedc" title="List of all internal assumptions.">d_intAssumptions</a>.<a class="code" href="classCVC3_1_1CDList.html#a96313ff2924c89a93d7fe6c618c837af">end</a>(); i!=iend; ++i)
<a name="l01123"></a>01123 assumptions.push_back((*i).getExpr());
<a name="l01124"></a>01124 }
<a name="l01125"></a>01125
<a name="l01126"></a>01126
<a name="l01127"></a>01127
<a name="l01128"></a><a class="code" href="classCVC3_1_1SearchSat.html#a63ffdace5647b9d783e4a4a0dd90fb0b">01128</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchSat.html#a63ffdace5647b9d783e4a4a0dd90fb0b" title="Get all assumptions made in this and all previous contexts.">SearchSat::getAssumptions</a>(vector<Expr>& assumptions)
<a name="l01129"></a>01129 {
<a name="l01130"></a>01130 <a class="code" href="classCVC3_1_1CDList.html">CDList<Theorem>::const_iterator</a> iU=<a class="code" href="classCVC3_1_1SearchSat.html#a3b9b2371a24908e62ec71b6f141afea8" title="List of all user assumptions.">d_userAssumptions</a>.<a class="code" href="classCVC3_1_1CDList.html#ae2cf006604b1ab88139332a5e2c08568">begin</a>(),
<a name="l01131"></a>01131 iUend=<a class="code" href="classCVC3_1_1SearchSat.html#a3b9b2371a24908e62ec71b6f141afea8" title="List of all user assumptions.">d_userAssumptions</a>.<a class="code" href="classCVC3_1_1CDList.html#a96313ff2924c89a93d7fe6c618c837af">end</a>(), iI = <a class="code" href="classCVC3_1_1SearchSat.html#ad3b9879d655cf3fce1a70de7b1d6fedc" title="List of all internal assumptions.">d_intAssumptions</a>.<a class="code" href="classCVC3_1_1CDList.html#ae2cf006604b1ab88139332a5e2c08568">begin</a>(),
<a name="l01132"></a>01132 iIend=<a class="code" href="classCVC3_1_1SearchSat.html#ad3b9879d655cf3fce1a70de7b1d6fedc" title="List of all internal assumptions.">d_intAssumptions</a>.<a class="code" href="classCVC3_1_1CDList.html#a96313ff2924c89a93d7fe6c618c837af">end</a>();
<a name="l01133"></a>01133 <span class="keywordflow">while</span> (<span class="keyword">true</span>) {
<a name="l01134"></a>01134 <span class="keywordflow">if</span> (iI == iIend) {
<a name="l01135"></a>01135 <span class="keywordflow">if</span> (iU == iUend) <span class="keywordflow">break</span>;
<a name="l01136"></a>01136 assumptions.push_back((*iU).getExpr());
<a name="l01137"></a>01137 ++iU;
<a name="l01138"></a>01138 }
<a name="l01139"></a>01139 <span class="keywordflow">else</span> <span class="keywordflow">if</span> (iU == iUend) {
<a name="l01140"></a>01140 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> intAssump = (*iI).getExpr();
<a name="l01141"></a>01141 <span class="keywordflow">if</span> (!intAssump.<a class="code" href="group__ExprPkg.html#gadeefef680b6323acc5d79a553644be8e">isUserAssumption</a>()) {
<a name="l01142"></a>01142 assumptions.push_back(intAssump);
<a name="l01143"></a>01143 }
<a name="l01144"></a>01144 ++iI;
<a name="l01145"></a>01145 }
<a name="l01146"></a>01146 <span class="keywordflow">else</span> {
<a name="l01147"></a>01147 <span class="keywordflow">if</span> ((*iI).getScope() <= (*iU).getScope()) {
<a name="l01148"></a>01148 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> intAssump = (*iI).getExpr();
<a name="l01149"></a>01149 <span class="keywordflow">if</span> (!intAssump.<a class="code" href="group__ExprPkg.html#gadeefef680b6323acc5d79a553644be8e">isUserAssumption</a>()) {
<a name="l01150"></a>01150 assumptions.push_back(intAssump);
<a name="l01151"></a>01151 }
<a name="l01152"></a>01152 ++iI;
<a name="l01153"></a>01153 }
<a name="l01154"></a>01154 <span class="keywordflow">else</span> {
<a name="l01155"></a>01155 assumptions.push_back((*iU).getExpr());
<a name="l01156"></a>01156 ++iU;
<a name="l01157"></a>01157 }
<a name="l01158"></a>01158 }
<a name="l01159"></a>01159 }
<a name="l01160"></a>01160 }
<a name="l01161"></a>01161
<a name="l01162"></a>01162
<a name="l01163"></a><a class="code" href="classCVC3_1_1SearchSat.html#a4ec713d6bbbd5d4bd6a9fcacc42a044e">01163</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1SearchSat.html#a4ec713d6bbbd5d4bd6a9fcacc42a044e" title="Check if the formula has already been assumed previously.">SearchSat::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="l01164"></a>01164 {
<a name="l01165"></a>01165 <span class="keywordflow">return</span> e.<a class="code" href="group__ExprPkg.html#gadeefef680b6323acc5d79a553644be8e">isUserAssumption</a>() || e.<a class="code" href="group__ExprPkg.html#gaf42121131fd56040faef7a64d9e67729">isIntAssumption</a>();
<a name="l01166"></a>01166 }
<a name="l01167"></a>01167
<a name="l01168"></a>01168
<a name="l01169"></a><a class="code" href="classCVC3_1_1SearchSat.html#af2296bfb7f363cb9b83ca2fa6042d496">01169</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchSat.html#af2296bfb7f363cb9b83ca2fa6042d496" title="Will return the set of assertions which make the queried formula false.">SearchSat::getCounterExample</a>(vector<Expr>& assumptions, <span class="keywordtype">bool</span> inOrder)
<a name="l01170"></a>01170 {
<a name="l01171"></a>01171 <span class="keywordflow">if</span> (!<a class="code" href="classCVC3_1_1SearchSat.html#ab41637f4522c5e3f318993392adf84bb" title="Theorem from the last successful checkValid call. It is used by getProof and getAssumptions.">d_lastValid</a>.<a class="code" href="classCVC3_1_1CDO.html#a818fcacc7b30b0f05347335ab125626c">get</a>().<a class="code" href="classCVC3_1_1Theorem.html#afc6fdb0507eb3669e28d9be5ed0bd333">isNull</a>()) {
<a name="l01172"></a>01172 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1Exception.html">Exception</a>(<span class="stringliteral">"Expected last query to be invalid"</span>);
<a name="l01173"></a>01173 }
<a name="l01174"></a>01174 <a class="code" href="classCVC3_1_1SearchSat.html#acee513ead4033fd5bfc16cbab7951dc7" title="Get assumptions made internally in this and all previous contexts.">getInternalAssumptions</a>(assumptions);
<a name="l01175"></a>01175 }
<a name="l01176"></a>01176
<a name="l01177"></a>01177
<a name="l01178"></a><a class="code" href="classCVC3_1_1SearchSat.html#aa8b7c9812f7f61fc567c502ef3240d85">01178</a> <a class="code" href="classCVC3_1_1Proof.html">Proof</a> <a class="code" href="classCVC3_1_1SearchSat.html#aa8b7c9812f7f61fc567c502ef3240d85" title="Returns the proof term for the last proven query.">SearchSat::getProof</a>()
<a name="l01179"></a>01179 {
<a name="l01180"></a>01180 <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="l01181"></a>01181 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1EvalException.html">EvalException</a>
<a name="l01182"></a>01182 (<span class="stringliteral">"getProof cannot be called without proofs activated"</span>);
<a name="l01183"></a>01183 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1SearchSat.html#ab41637f4522c5e3f318993392adf84bb" title="Theorem from the last successful checkValid call. It is used by getProof and getAssumptions.">d_lastValid</a>.<a class="code" href="classCVC3_1_1CDO.html#a818fcacc7b30b0f05347335ab125626c">get</a>().<a class="code" href="classCVC3_1_1Theorem.html#afc6fdb0507eb3669e28d9be5ed0bd333">isNull</a>())
<a name="l01184"></a>01184 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1EvalException.html">EvalException</a>
<a name="l01185"></a>01185 (<span class="stringliteral">"getProof must be called only after a successful check"</span>);
<a name="l01186"></a>01186 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1SearchSat.html#ab41637f4522c5e3f318993392adf84bb" title="Theorem from the last successful checkValid call. It is used by getProof and getAssumptions.">d_lastValid</a>.<a class="code" href="classCVC3_1_1CDO.html#a818fcacc7b30b0f05347335ab125626c">get</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="l01187"></a>01187 <span class="keywordflow">else</span> <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1SearchSat.html#ab41637f4522c5e3f318993392adf84bb" title="Theorem from the last successful checkValid call. It is used by getProof and getAssumptions.">d_lastValid</a>.<a class="code" href="classCVC3_1_1CDO.html#a818fcacc7b30b0f05347335ab125626c">get</a>().<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>();
<a name="l01188"></a>01188 }
</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>
