<!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: dpllt_minisat.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">dpllt_minisat.cpp</div> </div>
</div>
<div class="contents">
<a href="dpllt__minisat_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 dpllt_minisat.cpp</span>
<a name="l00004"></a>00004 <span class="comment"> *\brief Implementation of dpllt module using MiniSat</span>
<a name="l00005"></a>00005 <span class="comment"> *</span>
<a name="l00006"></a>00006 <span class="comment"> * Author: Alexander Fuchs</span>
<a name="l00007"></a>00007 <span class="comment"> *</span>
<a name="l00008"></a>00008 <span class="comment"> * Created: Fri Sep 08 11:04:00 2006</span>
<a name="l00009"></a>00009 <span class="comment"> *</span>
<a name="l00010"></a>00010 <span class="comment"> * <hr></span>
<a name="l00011"></a>00011 <span class="comment"> *</span>
<a name="l00012"></a>00012 <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span>
<a name="l00013"></a>00013 <span class="comment"> * and its documentation for any purpose is hereby granted without</span>
<a name="l00014"></a>00014 <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span>
<a name="l00015"></a>00015 <span class="comment"> * LICENSE file provided with this distribution.</span>
<a name="l00016"></a>00016 <span class="comment"> * </span>
<a name="l00017"></a>00017 <span class="comment"> * <hr></span>
<a name="l00018"></a>00018 <span class="comment"> */</span>
<a name="l00019"></a>00019 <span class="comment">/*****************************************************************************/</span>
<a name="l00020"></a>00020 <span class="comment">//we need this to use newPf</span>
<a name="l00021"></a><a class="code" href="dpllt__minisat_8cpp.html#a8663c36bbf15bb5a0dcb01b97897fa95">00021</a> <span class="preprocessor">#define _CVC3_TRUSTED_ </span>
<a name="l00022"></a>00022 <span class="preprocessor"></span>
<a name="l00023"></a>00023 <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="l00024"></a>00024 <span class="preprocessor">#include "<a class="code" href="minisat__solver_8h.html" title="Adaptation of MiniSat to DPLL(T)">minisat_solver.h</a>"</span>
<a name="l00025"></a>00025 <span class="preprocessor">#include "<a class="code" href="sat__proof_8h.html" title="Sat solver proof representation.">sat_proof.h</a>"</span>
<a name="l00026"></a>00026 <span class="preprocessor">#include "<a class="code" href="theorem__producer_8h.html">theorem_producer.h</a>"</span>
<a name="l00027"></a>00027 <span class="preprocessor">#include "<a class="code" href="exception_8h.html">exception.h</a>"</span>
<a name="l00028"></a>00028
<a name="l00029"></a>00029 <span class="keyword">using namespace </span>std;
<a name="l00030"></a>00030 <span class="keyword">using namespace </span>CVC3;
<a name="l00031"></a>00031 <span class="keyword">using namespace </span>SAT;
<a name="l00032"></a>00032
<a name="l00033"></a>00033
<a name="l00034"></a><a class="code" href="classSAT_1_1DPLLTMiniSat.html#a8845ef99231d4f4096f0254423aca649">00034</a> DPLLTMiniSat::DPLLTMiniSat(<a class="code" href="classSAT_1_1DPLLT_1_1TheoryAPI.html">TheoryAPI</a>* theoryAPI, <a class="code" href="classSAT_1_1DPLLT_1_1Decider.html">Decider</a>* decider,
<a name="l00035"></a>00035 <span class="keywordtype">bool</span> printStats, <span class="keywordtype">bool</span> createProof)
<a name="l00036"></a>00036 : <a class="code" href="classSAT_1_1DPLLT.html">DPLLT</a>(theoryAPI, decider), d_printStats(printStats),
<a name="l00037"></a>00037 d_createProof(createProof), d_proof(NULL) {
<a name="l00038"></a>00038 <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a2ee2582067c44520f4554de44ebec16a">pushSolver</a>();
<a name="l00039"></a>00039 }
<a name="l00040"></a>00040
<a name="l00041"></a><a class="code" href="classSAT_1_1DPLLTMiniSat.html#ad95c622192084c6fb35d4a944b02a41f">00041</a> <a class="code" href="classSAT_1_1DPLLTMiniSat.html#ad95c622192084c6fb35d4a944b02a41f">DPLLTMiniSat::~DPLLTMiniSat</a>() {
<a name="l00042"></a>00042 <span class="keywordflow">while</span> (!<a class="code" href="classSAT_1_1DPLLTMiniSat.html#a36d133e42dbd9557434a166d1e97d050">d_solvers</a>.empty()) {
<a name="l00043"></a>00043 <span class="comment">// don't pop theories, this is not allowed when cvc shuts down.</span>
<a name="l00044"></a>00044 <span class="keyword">delete</span> (<a class="code" href="classSAT_1_1DPLLTMiniSat.html#a36d133e42dbd9557434a166d1e97d050">d_solvers</a>.top());
<a name="l00045"></a>00045 <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a36d133e42dbd9557434a166d1e97d050">d_solvers</a>.pop();
<a name="l00046"></a>00046 }
<a name="l00047"></a>00047 <span class="keyword">delete</span> <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a9eb24ce4c4b1a9f1dae868b18017f905">d_proof</a>;
<a name="l00048"></a>00048 }
<a name="l00049"></a>00049
<a name="l00050"></a><a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">00050</a> <a class="code" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a>* <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">DPLLTMiniSat::getActiveSolver</a>() {
<a name="l00051"></a>00051 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!<a class="code" href="classSAT_1_1DPLLTMiniSat.html#a36d133e42dbd9557434a166d1e97d050">d_solvers</a>.empty(), <span class="stringliteral">"DPLLTMiniSat::getActiveSolver: no solver"</span>);
<a name="l00052"></a>00052 <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a36d133e42dbd9557434a166d1e97d050">d_solvers</a>.top();
<a name="l00053"></a>00053 }
<a name="l00054"></a>00054
<a name="l00055"></a>00055
<a name="l00056"></a><a class="code" href="classSAT_1_1DPLLTMiniSat.html#a2ee2582067c44520f4554de44ebec16a">00056</a> <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a2ee2582067c44520f4554de44ebec16a">DPLLTMiniSat::pushSolver</a>() {
<a name="l00057"></a>00057 <span class="keywordflow">if</span> (<a class="code" href="classSAT_1_1DPLLTMiniSat.html#a36d133e42dbd9557434a166d1e97d050">d_solvers</a>.empty()) {
<a name="l00058"></a>00058 <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a36d133e42dbd9557434a166d1e97d050">d_solvers</a>.push(<span class="keyword">new</span> <a class="code" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a>(<a class="code" href="classSAT_1_1DPLLT.html#aafa21967afbd30f8c18ebc9f6c37bfa9">d_theoryAPI</a>, <a class="code" href="classSAT_1_1DPLLT.html#aebea99801d1e6b690feb9610403f1162">d_decider</a>, <a class="code" href="classSAT_1_1DPLLTMiniSat.html#ac6230604f45056b39c0869f05fe0ae7e">d_createProof</a>));
<a name="l00059"></a>00059 }
<a name="l00060"></a>00060 <span class="keywordflow">else</span> {
<a name="l00061"></a>00061 <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a36d133e42dbd9557434a166d1e97d050">d_solvers</a>.push(<a class="code" href="classMiniSat_1_1Solver.html#a7fce9c6a705405959f91d559a6e06ee4">MiniSat::Solver::createFrom</a>(<a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>()));
<a name="l00062"></a>00062 }
<a name="l00063"></a>00063 }
<a name="l00064"></a>00064
<a name="l00065"></a><a class="code" href="classSAT_1_1DPLLTMiniSat.html#a30d61595534052f920440688f5cec73b">00065</a> <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a30d61595534052f920440688f5cec73b">DPLLTMiniSat::search</a>()
<a name="l00066"></a>00066 {
<a name="l00067"></a>00067 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classSAT_1_1DPLLTMiniSat.html#a36d133e42dbd9557434a166d1e97d050">d_solvers</a>.size() > 0, <span class="stringliteral">"DPLLTMiniSat::search: no solver"</span>);
<a name="l00068"></a>00068 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>()->inPush(), <span class="stringliteral">"DPLLTMiniSat::search: solver not pushed"</span>);
<a name="l00069"></a>00069
<a name="l00070"></a>00070 <span class="comment">// search</span>
<a name="l00071"></a>00071 <a class="code" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a>* solver = <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>();
<a name="l00072"></a>00072 <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> result = solver-><a class="code" href="classMiniSat_1_1Solver.html#af43d31ac67426e7b3b699491b02d62c1" title="search">search</a>();
<a name="l00073"></a>00073
<a name="l00074"></a>00074 <span class="comment">// print statistics</span>
<a name="l00075"></a>00075 <span class="keywordflow">if</span> (<a class="code" href="classSAT_1_1DPLLTMiniSat.html#afa6ba4582477c902c7eb4d498c42882e">d_printStats</a>) {
<a name="l00076"></a>00076 <span class="keywordflow">switch</span> (result) {
<a name="l00077"></a>00077 <span class="keywordflow">case</span> <a class="code" href="xchaff__solver_8h.html#a259c70233f322b3e490149190b8bb87baa6a5c07f8c320f440ebc34fed65eb550">SATISFIABLE</a>:
<a name="l00078"></a>00078 <span class="keywordflow">break</span>;
<a name="l00079"></a>00079 <span class="keywordflow">case</span> <a class="code" href="xchaff__solver_8h.html#a259c70233f322b3e490149190b8bb87ba709691b4dfbbba6c6f992a7cd34dd0e9">UNSATISFIABLE</a>:
<a name="l00080"></a>00080 cout << <span class="stringliteral">"Instance unsatisfiable"</span> << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00081"></a>00081 <span class="keywordflow">break</span>;
<a name="l00082"></a>00082 <span class="keywordflow">case</span> <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498ba33046505033fa14ebb412efb4474ff56">ABORT</a>:
<a name="l00083"></a>00083 cout << <span class="stringliteral">"aborted, unable to determine the satisfiablility of the instance"</span> << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00084"></a>00084 <span class="keywordflow">break</span>;
<a name="l00085"></a>00085 <span class="keywordflow">case</span> <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">UNKNOWN</a>:
<a name="l00086"></a>00086 cout << <span class="stringliteral">"unknown, unable to determing the satisfiablility of the instance"</span> << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00087"></a>00087 <span class="keywordflow">break</span>;
<a name="l00088"></a>00088 <span class="keywordflow">default</span>:
<a name="l00089"></a>00089 <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">"DPLTBasic::handle_result: Unknown outcome"</span>);
<a name="l00090"></a>00090 }
<a name="l00091"></a>00091
<a name="l00092"></a>00092 cout << <span class="stringliteral">"Number of Decisions\t\t\t"</span> << solver-><a class="code" href="classMiniSat_1_1Solver.html#ac386ec8bbd27857254bae149db775412" title="Statistics.">getStats</a>().decisions << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00093"></a>00093 cout << <span class="stringliteral">"Number of Propagations\t\t\t"</span> << solver-><a class="code" href="classMiniSat_1_1Solver.html#ac386ec8bbd27857254bae149db775412" title="Statistics.">getStats</a>().propagations << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00094"></a>00094 cout << <span class="stringliteral">"Number of Propositional Conflicts\t"</span>
<a name="l00095"></a>00095 << (solver-><a class="code" href="classMiniSat_1_1Solver.html#ac386ec8bbd27857254bae149db775412" title="Statistics.">getStats</a>().conflicts - solver-><a class="code" href="classMiniSat_1_1Solver.html#ac386ec8bbd27857254bae149db775412" title="Statistics.">getStats</a>().theory_conflicts) << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00096"></a>00096 cout << <span class="stringliteral">"Number of Theory Conflicts\t\t"</span> << solver-><a class="code" href="classMiniSat_1_1Solver.html#ac386ec8bbd27857254bae149db775412" title="Statistics.">getStats</a>().theory_conflicts << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00097"></a>00097 cout << <span class="stringliteral">"Number of Variables\t\t\t"</span> << solver-><a class="code" href="classMiniSat_1_1Solver.html#a679fa13af0d75beca98981dc40f3f2a2">nVars</a>() << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00098"></a>00098 cout << <span class="stringliteral">"Number of Literals\t\t\t"</span>
<a name="l00099"></a>00099 << (solver-><a class="code" href="classMiniSat_1_1Solver.html#ac386ec8bbd27857254bae149db775412" title="Statistics.">getStats</a>().clauses_literals + solver-><a class="code" href="classMiniSat_1_1Solver.html#ac386ec8bbd27857254bae149db775412" title="Statistics.">getStats</a>().learnts_literals) << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00100"></a>00100 cout << <span class="stringliteral">"Max. Number of Literals\t\t\t"</span> << solver-><a class="code" href="classMiniSat_1_1Solver.html#ac386ec8bbd27857254bae149db775412" title="Statistics.">getStats</a>().max_literals << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00101"></a>00101 cout << <span class="stringliteral">"Number of Clauses\t\t\t"</span> << solver-><a class="code" href="classMiniSat_1_1Solver.html#a70a7ffd14675ce9d3f1d445a79505278">getClauses</a>().size() << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00102"></a>00102 cout << <span class="stringliteral">"Number of Lemmas\t\t\t"</span> << solver-><a class="code" href="classMiniSat_1_1Solver.html#aadbf5bfce16879745ac1fc7e5226957c">getLemmas</a>().size() << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00103"></a>00103 cout << <span class="stringliteral">"Max. Decision Level\t\t\t"</span> << solver-><a class="code" href="classMiniSat_1_1Solver.html#ac386ec8bbd27857254bae149db775412" title="Statistics.">getStats</a>().max_level << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00104"></a>00104 cout << <span class="stringliteral">"Number of Deleted Clauses\t\t"</span> << solver-><a class="code" href="classMiniSat_1_1Solver.html#ac386ec8bbd27857254bae149db775412" title="Statistics.">getStats</a>().del_clauses << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00105"></a>00105 cout << <span class="stringliteral">"Number of Deleted Lemmas\t\t"</span> << solver-><a class="code" href="classMiniSat_1_1Solver.html#ac386ec8bbd27857254bae149db775412" title="Statistics.">getStats</a>().del_lemmas << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00106"></a>00106 cout << <span class="stringliteral">"Number of Database Simplifications\t"</span> << solver-><a class="code" href="classMiniSat_1_1Solver.html#ac386ec8bbd27857254bae149db775412" title="Statistics.">getStats</a>().db_simpl << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00107"></a>00107 cout << <span class="stringliteral">"Number of Lemma Cleanups\t\t"</span> << solver-><a class="code" href="classMiniSat_1_1Solver.html#ac386ec8bbd27857254bae149db775412" title="Statistics.">getStats</a>().lm_simpl << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00108"></a>00108
<a name="l00109"></a>00109 cout << <span class="stringliteral">"Debug\t\t\t\t\t"</span> << solver-><a class="code" href="classMiniSat_1_1Solver.html#ac386ec8bbd27857254bae149db775412" title="Statistics.">getStats</a>().debug << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00110"></a>00110 }
<a name="l00111"></a>00111
<a name="l00112"></a>00112 <span class="comment">// the dpllt interface requires that for an unsat result</span>
<a name="l00113"></a>00113 <span class="comment">// all theory pops are undone right away.</span>
<a name="l00114"></a>00114 <span class="keywordflow">if</span> (result == <a class="code" href="xchaff__solver_8h.html#a259c70233f322b3e490149190b8bb87ba709691b4dfbbba6c6f992a7cd34dd0e9">UNSATISFIABLE</a>) {
<a name="l00115"></a>00115 <span class="comment">// cout << "unsat" <<endl;</span>
<a name="l00116"></a>00116 <span class="comment">// return result;</span>
<a name="l00117"></a>00117 <span class="keywordflow">if</span> (<a class="code" href="classSAT_1_1DPLLTMiniSat.html#ac6230604f45056b39c0869f05fe0ae7e">d_createProof</a> ) {
<a name="l00118"></a>00118 <span class="keyword">delete</span> <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a9eb24ce4c4b1a9f1dae868b18017f905">d_proof</a>;
<a name="l00119"></a>00119 <span class="comment">// cout<<"creating proof" << endl;</span>
<a name="l00120"></a>00120 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classSAT_1_1DPLLTMiniSat.html#a36d133e42dbd9557434a166d1e97d050">d_solvers</a>.top()->getDerivation() != NULL, <span class="stringliteral">"DplltMiniSat::search: no proof"</span>);
<a name="l00121"></a>00121 <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a9eb24ce4c4b1a9f1dae868b18017f905">d_proof</a> = <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a36d133e42dbd9557434a166d1e97d050">d_solvers</a>.top()->getDerivation()->createProof();
<a name="l00122"></a>00122 }
<a name="l00123"></a>00123 <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a36d133e42dbd9557434a166d1e97d050">d_solvers</a>.top()->popTheories();
<a name="l00124"></a>00124 <a class="code" href="classSAT_1_1DPLLT.html#aafa21967afbd30f8c18ebc9f6c37bfa9">d_theoryAPI</a>-><a class="code" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a51a08aab04c2185513676a316aee14b4" title="Restore most recent checkpoint.">pop</a>();
<a name="l00125"></a>00125 }
<a name="l00126"></a>00126
<a name="l00127"></a>00127 <span class="keywordflow">return</span> result;
<a name="l00128"></a>00128 }
<a name="l00129"></a>00129
<a name="l00130"></a>00130
<a name="l00131"></a><a class="code" href="classSAT_1_1DPLLTMiniSat.html#a51a36acb7b2ed49d97fa8d5524604604">00131</a> <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a51a36acb7b2ed49d97fa8d5524604604" title="Check the satisfiability of a set of clauses in the current context.">DPLLTMiniSat::checkSat</a>(<span class="keyword">const</span> <a class="code" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a>& cnf)
<a name="l00132"></a>00132 {
<a name="l00133"></a>00133 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classSAT_1_1DPLLTMiniSat.html#a36d133e42dbd9557434a166d1e97d050">d_solvers</a>.size() > 0, <span class="stringliteral">"DPLLTMiniSat::checkSat: no solver"</span>);
<a name="l00134"></a>00134
<a name="l00135"></a>00135 <span class="comment">// perform any requested solver pops</span>
<a name="l00136"></a>00136 <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>()-><a class="code" href="classMiniSat_1_1Solver.html#a8cc5207e3580ab0f09c6e9c225eaebff">doPops</a>();
<a name="l00137"></a>00137
<a name="l00138"></a>00138 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!<a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>()->inSearch(), <span class="stringliteral">"DPLLTMiniSat::checkSat: solver already in search"</span>);
<a name="l00139"></a>00139
<a name="l00140"></a>00140 <span class="comment">// required by dpllt interface: theory push before search</span>
<a name="l00141"></a>00141 <a class="code" href="classSAT_1_1DPLLT.html#aafa21967afbd30f8c18ebc9f6c37bfa9">d_theoryAPI</a>-><a class="code" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a771e84ea6308cb7d3f7d02e7858b37db" title="Set a checkpoint for backtracking.">push</a>();
<a name="l00142"></a>00142
<a name="l00143"></a>00143 <span class="comment">// solver already in use, so create a new solver</span>
<a name="l00144"></a>00144 <span class="keywordflow">if</span> (<a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>()->inSearch()) {
<a name="l00145"></a>00145 <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a2ee2582067c44520f4554de44ebec16a">pushSolver</a>();
<a name="l00146"></a>00146 }
<a name="l00147"></a>00147
<a name="l00148"></a>00148 <span class="comment">// add new formula and search</span>
<a name="l00149"></a>00149 <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>()-><a class="code" href="classMiniSat_1_1Solver.html#ab7ceeed839df517256ce77c126f28e00">addFormula</a>(cnf, <span class="keyword">false</span>);
<a name="l00150"></a>00150 <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a30d61595534052f920440688f5cec73b">search</a>();
<a name="l00151"></a>00151 }
<a name="l00152"></a>00152
<a name="l00153"></a>00153
<a name="l00154"></a><a class="code" href="classSAT_1_1DPLLTMiniSat.html#aae7502914c5ca0708d0bd11ebc766d0a">00154</a> <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="code" href="classSAT_1_1DPLLTMiniSat.html#aae7502914c5ca0708d0bd11ebc766d0a" title="Continue checking the last check with additional constraints.">DPLLTMiniSat::continueCheck</a>(<span class="keyword">const</span> <a class="code" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a>& cnf)
<a name="l00155"></a>00155 {
<a name="l00156"></a>00156 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classSAT_1_1DPLLTMiniSat.html#a36d133e42dbd9557434a166d1e97d050">d_solvers</a>.size() > 0, <span class="stringliteral">"DPLLTMiniSat::continueCheck: no solver"</span>);
<a name="l00157"></a>00157
<a name="l00158"></a>00158 <span class="comment">// if the current solver has no push, all its pushes have already been undone,</span>
<a name="l00159"></a>00159 <span class="comment">// so remove it</span>
<a name="l00160"></a>00160 <span class="keywordflow">if</span> (!<a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>()-><a class="code" href="classMiniSat_1_1Solver.html#a1bcf27269a8286f82b3235d982e4724e">inPush</a>()) {
<a name="l00161"></a>00161 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!<a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>()->inSearch(), <span class="stringliteral">"DPLLTMiniSat::continueCheck: solver without push in search"</span>);
<a name="l00162"></a>00162 <span class="keyword">delete</span> <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>();
<a name="l00163"></a>00163 <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a36d133e42dbd9557434a166d1e97d050">d_solvers</a>.pop();
<a name="l00164"></a>00164 }
<a name="l00165"></a>00165
<a name="l00166"></a>00166 <span class="comment">// perform any requested solver pops</span>
<a name="l00167"></a>00167 <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>()-><a class="code" href="classMiniSat_1_1Solver.html#a8cc5207e3580ab0f09c6e9c225eaebff">doPops</a>();
<a name="l00168"></a>00168
<a name="l00169"></a>00169 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classSAT_1_1DPLLTMiniSat.html#a36d133e42dbd9557434a166d1e97d050">d_solvers</a>.size() > 0, <span class="stringliteral">"DPLLTMiniSat::continueCheck: no solver (2)"</span>);
<a name="l00170"></a>00170 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>()->inPush(), <span class="stringliteral">"DPLLTMiniSat::continueCheck: solver not in push"</span>);
<a name="l00171"></a>00171 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>()->inSearch(), <span class="stringliteral">"DPLLTMiniSat::continueCheck: solver not in search"</span>);
<a name="l00172"></a>00172
<a name="l00173"></a>00173 <span class="comment">// add new formula and search</span>
<a name="l00174"></a>00174 <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>()-><a class="code" href="classMiniSat_1_1Solver.html#ab7ceeed839df517256ce77c126f28e00">addFormula</a>(cnf, <span class="keyword">false</span>);
<a name="l00175"></a>00175 <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a30d61595534052f920440688f5cec73b">search</a>();
<a name="l00176"></a>00176 }
<a name="l00177"></a>00177
<a name="l00178"></a>00178
<a name="l00179"></a><a class="code" href="classSAT_1_1DPLLTMiniSat.html#a169decc11aac46183d6213a2c6f12633">00179</a> <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a169decc11aac46183d6213a2c6f12633" title="Set a checkpoint for backtracking.">DPLLTMiniSat::push</a>() {
<a name="l00180"></a>00180 <span class="comment">// perform any requested solver pops</span>
<a name="l00181"></a>00181 <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>()-><a class="code" href="classMiniSat_1_1Solver.html#a8cc5207e3580ab0f09c6e9c225eaebff">doPops</a>();
<a name="l00182"></a>00182
<a name="l00183"></a>00183 <span class="comment">// if the current solver is already in a search, then create a new one</span>
<a name="l00184"></a>00184 <span class="keywordflow">if</span> (<a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>()->inSearch()) {
<a name="l00185"></a>00185 <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a2ee2582067c44520f4554de44ebec16a">pushSolver</a>();
<a name="l00186"></a>00186 }
<a name="l00187"></a>00187
<a name="l00188"></a>00188 <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>()-><a class="code" href="classMiniSat_1_1Solver.html#aec12c38c0c17d7067e12da239353ebc8" title="Push / Pop.">push</a>();
<a name="l00189"></a>00189 <a class="code" href="classSAT_1_1DPLLT.html#aafa21967afbd30f8c18ebc9f6c37bfa9">d_theoryAPI</a>-><a class="code" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a771e84ea6308cb7d3f7d02e7858b37db" title="Set a checkpoint for backtracking.">push</a>();
<a name="l00190"></a>00190 }
<a name="l00191"></a>00191
<a name="l00192"></a><a class="code" href="classSAT_1_1DPLLTMiniSat.html#a6cf0c23d330fc8609323cb3dd8282377">00192</a> <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a6cf0c23d330fc8609323cb3dd8282377" title="Restore checkpoint.">DPLLTMiniSat::pop</a>() {
<a name="l00193"></a>00193 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classSAT_1_1DPLLTMiniSat.html#a36d133e42dbd9557434a166d1e97d050">d_solvers</a>.size() > 0, <span class="stringliteral">"DPLLTMiniSat::pop: no solver"</span>);
<a name="l00194"></a>00194
<a name="l00195"></a>00195 <span class="comment">// if the current solver has no push, all its pushes have already been undone,</span>
<a name="l00196"></a>00196 <span class="comment">// so remove it</span>
<a name="l00197"></a>00197 <span class="keywordflow">if</span> (!<a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>()-><a class="code" href="classMiniSat_1_1Solver.html#a1bcf27269a8286f82b3235d982e4724e">inPush</a>()) {
<a name="l00198"></a>00198 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!<a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>()->inSearch(), <span class="stringliteral">"DPLLTMiniSat::pop: solver without push in search"</span>);
<a name="l00199"></a>00199 <span class="keyword">delete</span> <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>();
<a name="l00200"></a>00200 <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a36d133e42dbd9557434a166d1e97d050">d_solvers</a>.pop();
<a name="l00201"></a>00201 }
<a name="l00202"></a>00202
<a name="l00203"></a>00203 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classSAT_1_1DPLLTMiniSat.html#a36d133e42dbd9557434a166d1e97d050">d_solvers</a>.size() > 0, <span class="stringliteral">"DPLLTMiniSat::pop: no solver 2"</span>);
<a name="l00204"></a>00204 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>()->inPush(), <span class="stringliteral">"DPLLTMiniSat::pop: solver not in push"</span>);
<a name="l00205"></a>00205
<a name="l00206"></a>00206 <span class="comment">// undo checkSat theory push for an invalid query.</span>
<a name="l00207"></a>00207 <span class="comment">// for a valid query this is done in search right away.</span>
<a name="l00208"></a>00208 <span class="keywordflow">if</span> (<a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>()->inSearch() && <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>()->isConsistent()) {
<a name="l00209"></a>00209 <a class="code" href="classSAT_1_1DPLLT.html#aafa21967afbd30f8c18ebc9f6c37bfa9">d_theoryAPI</a>-><a class="code" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a51a08aab04c2185513676a316aee14b4" title="Restore most recent checkpoint.">pop</a>();
<a name="l00210"></a>00210 }
<a name="l00211"></a>00211 <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>()-><a class="code" href="classMiniSat_1_1Solver.html#a8be8edbecd5a07bd39990ee7ba0918e3">requestPop</a>();
<a name="l00212"></a>00212 <a class="code" href="classSAT_1_1DPLLT.html#aafa21967afbd30f8c18ebc9f6c37bfa9">d_theoryAPI</a>-><a class="code" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a51a08aab04c2185513676a316aee14b4" title="Restore most recent checkpoint.">pop</a>();
<a name="l00213"></a>00213 }
<a name="l00214"></a>00214
<a name="l00215"></a><a class="code" href="classSAT_1_1DPLLTMiniSat.html#aae30c40897ec35d1a0485899865b723e">00215</a> std::vector<SAT::Lit> <a class="code" href="classSAT_1_1DPLLTMiniSat.html#aae30c40897ec35d1a0485899865b723e">DPLLTMiniSat::getCurAssignments</a>(){
<a name="l00216"></a>00216 <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>()-><a class="code" href="classMiniSat_1_1Solver.html#aac50fbefa27ff761747fe0873722f927">curAssigns</a>();
<a name="l00217"></a>00217 }
<a name="l00218"></a>00218
<a name="l00219"></a><a class="code" href="classSAT_1_1DPLLTMiniSat.html#a1a19b6494dbc9bdd404e5917ee9eea24">00219</a> std::vector<std::vector<SAT::Lit> > <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a1a19b6494dbc9bdd404e5917ee9eea24">DPLLTMiniSat::getCurClauses</a>(){
<a name="l00220"></a>00220 <span class="keywordflow">return</span> <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>()-><a class="code" href="classMiniSat_1_1Solver.html#afb1410338334a3220d95ec28e5a68f71">curClauses</a>();
<a name="l00221"></a>00221 }
<a name="l00222"></a>00222
<a name="l00223"></a><a class="code" href="classSAT_1_1DPLLTMiniSat.html#afdf7f3a5aa5eccf6c04ba4326567f0b9">00223</a> <span class="keywordtype">void</span> <a class="code" href="classSAT_1_1DPLLTMiniSat.html#afdf7f3a5aa5eccf6c04ba4326567f0b9" title="Add new clauses to the SAT solver.">DPLLTMiniSat::addAssertion</a>(<span class="keyword">const</span> <a class="code" href="classSAT_1_1CNF__Formula.html">CNF_Formula</a>& cnf) {
<a name="l00224"></a>00224 <span class="comment">// perform any requested solver pops</span>
<a name="l00225"></a>00225 <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>()-><a class="code" href="classMiniSat_1_1Solver.html#a8cc5207e3580ab0f09c6e9c225eaebff">doPops</a>();
<a name="l00226"></a>00226
<a name="l00227"></a>00227 <span class="comment">// if the current solver is already performing a search create a new solver</span>
<a name="l00228"></a>00228 <span class="keywordflow">if</span> (<a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>()->inSearch()) {
<a name="l00229"></a>00229 <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a2ee2582067c44520f4554de44ebec16a">pushSolver</a>();
<a name="l00230"></a>00230 }
<a name="l00231"></a>00231
<a name="l00232"></a>00232 <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>()-><a class="code" href="classMiniSat_1_1Solver.html#ab7ceeed839df517256ce77c126f28e00">addFormula</a>(cnf, <span class="keyword">false</span>);
<a name="l00233"></a>00233
<a name="l00234"></a>00234 <span class="comment">// Immediately assert unit clauses -</span>
<a name="l00235"></a>00235 <span class="comment">// the intention is to make these immediately available for interactive use</span>
<a name="l00236"></a>00236 <span class="keywordflow">for</span> (<a class="code" href="classSAT_1_1CNF__Formula.html#ac247d01a4cc1e5aab84294cb4c00ddbf">CNF_Formula::const_iterator</a> i = cnf.<a class="code" href="classSAT_1_1CNF__Formula.html#a69dfc94796b23b6913c44a4d6d60f0d8">begin</a>(); i != cnf.<a class="code" href="classSAT_1_1CNF__Formula.html#a6631cf3c5a6938f655360f7f63522b79">end</a>(); ++i) {
<a name="l00237"></a>00237 <span class="keywordflow">if</span> ((*i).isUnit() && <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>()-><a class="code" href="classMiniSat_1_1Solver.html#a7eb95fc222427a795a3b5ae48e94518e">isConsistent</a>()) {
<a name="l00238"></a>00238 <a class="code" href="classSAT_1_1DPLLT.html#aafa21967afbd30f8c18ebc9f6c37bfa9">d_theoryAPI</a>-><a class="code" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a3b3ef70567e0298cd3e971fd57d26fa6" title="Notify theory when a literal is set to true.">assertLit</a>(*(*i).begin());
<a name="l00239"></a>00239 }
<a name="l00240"></a>00240 }
<a name="l00241"></a>00241 }
<a name="l00242"></a>00242
<a name="l00243"></a>00243
<a name="l00244"></a><a class="code" href="classSAT_1_1DPLLTMiniSat.html#a06fd86d63383adc68d1ace6deb466175">00244</a> <a class="code" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">Var::Val</a> <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a06fd86d63383adc68d1ace6deb466175" title="Get value of variable: unassigned, false, or true.">DPLLTMiniSat::getValue</a>(<a class="code" href="classSAT_1_1Var.html">Var</a> var) {
<a name="l00245"></a>00245 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classSAT_1_1DPLLTMiniSat.html#a36d133e42dbd9557434a166d1e97d050">d_solvers</a>.size() > 0,
<a name="l00246"></a>00246 <span class="stringliteral">"DPLLTMiniSat::getValue: should be called after a previous satisfiable result"</span>);
<a name="l00247"></a>00247
<a name="l00248"></a>00248 <a class="code" href="classMiniSat_1_1lbool.html">MiniSat::lbool</a> value = <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a19b4d9e00382a6b386ac51461f156785">getActiveSolver</a>()-><a class="code" href="classMiniSat_1_1Solver.html#adc9d01899ff6c1eefea8749a1a97309b" title="clauses / assignment">getValue</a>(<a class="code" href="namespaceMiniSat.html#a6d37e2f7d3903e1a85baf8f1e83eff78">MiniSat::cvcToMiniSat</a>(var));
<a name="l00249"></a>00249 <span class="keywordflow">if</span> (value == <a class="code" href="namespaceMiniSat.html#ad0b6e52186f3374f569c4de9db621be1">MiniSat::l_True</a>)
<a name="l00250"></a>00250 <span class="keywordflow">return</span> <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfafbdc0d362f5bc36703903ef24ebbd30b">Var::TRUE_VAL</a>;
<a name="l00251"></a>00251 <span class="keywordflow">else</span> <span class="keywordflow">if</span> (value == <a class="code" href="namespaceMiniSat.html#a810166165364a8a8262d24b13d7b1da9">MiniSat::l_False</a>)
<a name="l00252"></a>00252 <span class="keywordflow">return</span> <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfa047662472190c5c32f81cb409b2139bc">Var::FALSE_VAL</a>;
<a name="l00253"></a>00253 <span class="keywordflow">else</span>
<a name="l00254"></a>00254 <span class="keywordflow">return</span> <a class="code" href="xchaff__base_8h.html#a915d220aba4527d1e33010bdfcbc6855a6ce26a62afab55d7606ad4e92428b30c">Var::UNKNOWN</a>;
<a name="l00255"></a>00255 }
<a name="l00256"></a>00256
<a name="l00257"></a>00257
<a name="l00258"></a><a class="code" href="dpllt__minisat_8cpp.html#a3fffe610feac92e588d04cb0a81c497d">00258</a> <a class="code" href="classCVC3_1_1Proof.html">CVC3::Proof</a> <a class="code" href="dpllt__minisat_8cpp.html#a3fffe610feac92e588d04cb0a81c497d">generateSatProof</a>(<a class="code" href="classSAT_1_1SatProofNode.html">SAT::SatProofNode</a>* node, <a class="code" href="classSAT_1_1CNF__Manager.html">CNF_Manager</a>* cnfManager, <a class="code" href="classCVC3_1_1TheoremProducer.html">TheoremProducer</a>* thmProducer){
<a name="l00259"></a>00259 <span class="keywordflow">if</span>(node-><a class="code" href="classSAT_1_1SatProofNode.html#a174ea8ebc16d85209afefd5048579991">hasNodeProof</a>()) {
<a name="l00260"></a>00260 <span class="keywordflow">return</span> node-><a class="code" href="classSAT_1_1SatProofNode.html#a728ac3f95a5bd503ed952d6dc9052aff">getNodeProof</a>();
<a name="l00261"></a>00261 }
<a name="l00262"></a>00262 <span class="keywordflow">if</span> (node-><a class="code" href="classSAT_1_1SatProofNode.html#a3ebf0d7ca635f0028e20b06fc5c0603a">isLeaf</a>()){
<a name="l00263"></a>00263
<a name="l00264"></a>00264 <span class="comment">/*</span>
<a name="l00265"></a>00265 <span class="comment">//<<<<<<< dpllt_minisat.cpp</span>
<a name="l00266"></a>00266 <span class="comment"></span>
<a name="l00267"></a>00267 <span class="comment"> SAT::Clause curClause = *(node->getLeaf());</span>
<a name="l00268"></a>00268 <span class="comment"></span>
<a name="l00269"></a>00269 <span class="comment"> DebugAssert(!curClause.isNull(), "Null clause found in generateSatProof");</span>
<a name="l00270"></a>00270 <span class="comment"></span>
<a name="l00271"></a>00271 <span class="comment"> cout << "get leaf clause " << curClause.getId() << endl; </span>
<a name="l00272"></a>00272 <span class="comment"></span>
<a name="l00273"></a>00273 <span class="comment"> const CVC3::Theorem clauseThm = curClause.getClauseTheorem();</span>
<a name="l00274"></a>00274 <span class="comment">//=======</span>
<a name="l00275"></a>00275 <span class="comment"> */</span>
<a name="l00276"></a>00276
<a name="l00277"></a>00277 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> clauseThm = node-><a class="code" href="classSAT_1_1SatProofNode.html#a7a26868e17f2fe9fef1d3b8f934de4a5">getLeaf</a>();
<a name="l00278"></a>00278
<a name="l00279"></a>00279 <span class="comment">/*</span>
<a name="l00280"></a>00280 <span class="comment">//>>>>>>> 1.14</span>
<a name="l00281"></a>00281 <span class="comment"> */</span>
<a name="l00282"></a>00282
<a name="l00283"></a>00283 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!clauseThm.<a class="code" href="classCVC3_1_1Theorem.html#afc6fdb0507eb3669e28d9be5ed0bd333">isNull</a>(), <span class="stringliteral">"Null thm found in generateSatProof"</span>);
<a name="l00284"></a>00284 node-><a class="code" href="classSAT_1_1SatProofNode.html#ae1bb4eb633b82329667ade6192f0d9cb">setNodeProof</a>(clauseThm.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00285"></a>00285 <span class="comment">// cout<<"set proof " << clauseThm.getProof() << endl;</span>
<a name="l00286"></a>00286 <span class="comment">// cout<<"set proof for theorem " << clauseThm << endl;</span>
<a name="l00287"></a>00287 <span class="keywordflow">return</span> clauseThm.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>();
<a name="l00288"></a>00288 }
<a name="l00289"></a>00289 <span class="keywordflow">else</span>{
<a name="l00290"></a>00290 <a class="code" href="classCVC3_1_1Proof.html">CVC3::Proof</a> leftProof = <a class="code" href="dpllt__minisat_8cpp.html#a3fffe610feac92e588d04cb0a81c497d">generateSatProof</a>(node-><a class="code" href="classSAT_1_1SatProofNode.html#a5e8c4112ac870c8d843e54a393bea892">getLeftParent</a>(), cnfManager, thmProducer);
<a name="l00291"></a>00291 <a class="code" href="classCVC3_1_1Proof.html">CVC3::Proof</a> rightProof = <a class="code" href="dpllt__minisat_8cpp.html#a3fffe610feac92e588d04cb0a81c497d">generateSatProof</a>(node-><a class="code" href="classSAT_1_1SatProofNode.html#a611593dffb824df842f88492bf160e80">getRightParent</a>(), cnfManager, thmProducer);
<a name="l00292"></a>00292
<a name="l00293"></a>00293 <span class="keywordflow">if</span>(node-><a class="code" href="classSAT_1_1SatProofNode.html#a5e8c4112ac870c8d843e54a393bea892">getLeftParent</a>() == node-><a class="code" href="classSAT_1_1SatProofNode.html#a611593dffb824df842f88492bf160e80">getRightParent</a>() ) 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="l00294"></a>00294 vector<Proof> pfs;
<a name="l00295"></a>00295 pfs.push_back(leftProof);
<a name="l00296"></a>00296 pfs.push_back(rightProof);
<a name="l00297"></a>00297 <span class="comment">// if(leftProof == rightProof) cout<<"***********"<<endl;</span>
<a name="l00298"></a>00298
<a name="l00299"></a>00299 <a class="code" href="classSAT_1_1Lit.html">Lit</a> lit = node-><a class="code" href="classSAT_1_1SatProofNode.html#a08af371d991d7e9b9e3a1a32b2ab0ec4">getLit</a>();
<a name="l00300"></a>00300 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e = cnfManager-><a class="code" href="classSAT_1_1CNF__Manager.html#a42c3cbd432324757f09ffd622ab1f057" title="Convert a CNF literal to an Expr literal.">concreteLit</a>(lit);
<a name="l00301"></a>00301 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e_trans = cnfManager-><a class="code" href="classSAT_1_1CNF__Manager.html#a42c3cbd432324757f09ffd622ab1f057" title="Convert a CNF literal to an Expr literal.">concreteLit</a>(lit,<span class="keyword">false</span>);
<a name="l00302"></a>00302 <span class="comment">// cout<<"set lit "<<lit.getVar()<<endl << e_trans <<endl << e << endl;</span>
<a name="l00303"></a>00303 <span class="comment">// cout<<"set lit "<<lit.getVar()<<endl << e_trans.getIndex() <<endl ;</span>
<a name="l00304"></a>00304 <span class="keywordflow">if</span>(e != e_trans){
<a name="l00305"></a>00305 <span class="comment">// cout<<"-diff e "<<e<<endl<<flush;</span>
<a name="l00306"></a>00306 <span class="comment">// cout<<"-diff e_trans " <<e_trans <<endl <<flush; </span>
<a name="l00307"></a>00307 }
<a name="l00308"></a>00308 <span class="comment">// {</span>
<a name="l00309"></a>00309 <span class="comment">// cout<<"Lit "<<lit.getID() << " " ;</span>
<a name="l00310"></a>00310 <span class="comment">// if (lit.isNull()) cout << "NULL";</span>
<a name="l00311"></a>00311 <span class="comment">// else if (lit.isFalse()) cout << "F";</span>
<a name="l00312"></a>00312 <span class="comment">// else if (lit.isTrue()) cout << "T";</span>
<a name="l00313"></a>00313 <span class="comment">// else {</span>
<a name="l00314"></a>00314 <span class="comment">// if (!lit.isPositive()) cout << "-";</span>
<a name="l00315"></a>00315 <span class="comment">// cout << lit.getVar();</span>
<a name="l00316"></a>00316 <span class="comment">// }</span>
<a name="l00317"></a>00317 <span class="comment">// cout<<endl;</span>
<a name="l00318"></a>00318 <span class="comment">// }</span>
<a name="l00319"></a>00319
<a name="l00320"></a>00320 <span class="comment">// cout<<"e "<<e<<endl<<flush;</span>
<a name="l00321"></a>00321 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00322"></a>00322 pf = thmProducer-><a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(<span class="stringliteral">"bool_resolution"</span>, e_trans, pfs);
<a name="l00323"></a>00323 node-><a class="code" href="classSAT_1_1SatProofNode.html#ae1bb4eb633b82329667ade6192f0d9cb">setNodeProof</a>(pf);
<a name="l00324"></a>00324 <span class="keywordflow">return</span> pf;
<a name="l00325"></a>00325
<a name="l00326"></a>00326 }
<a name="l00327"></a>00327
<a name="l00328"></a>00328 }
<a name="l00329"></a>00329
<a name="l00330"></a><a class="code" href="dpllt__minisat_8cpp.html#ad267e4a889b4d5222cd489bc3b8139ce">00330</a> <span class="keywordtype">void</span> <a class="code" href="dpllt__minisat_8cpp.html#ad267e4a889b4d5222cd489bc3b8139ce">printSatProof</a>(<a class="code" href="classSAT_1_1SatProofNode.html">SAT::SatProofNode</a>* node){
<a name="l00331"></a>00331 <span class="keywordflow">if</span> (node-><a class="code" href="classSAT_1_1SatProofNode.html#a3ebf0d7ca635f0028e20b06fc5c0603a">isLeaf</a>()){
<a name="l00332"></a>00332 <a class="code" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> theorem = node-><a class="code" href="classSAT_1_1SatProofNode.html#a7a26868e17f2fe9fef1d3b8f934de4a5">getLeaf</a>();
<a name="l00333"></a>00333
<a name="l00334"></a>00334 <span class="keywordflow">if</span>(theorem.<a class="code" href="classCVC3_1_1Theorem.html#afc6fdb0507eb3669e28d9be5ed0bd333">isNull</a>()){
<a name="l00335"></a>00335 cout<<<span class="stringliteral">"theorem null"</span><<<a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00336"></a>00336 }
<a name="l00337"></a>00337 <span class="keywordflow">else</span>{
<a name="l00338"></a>00338 cout<<<span class="stringliteral">"===================="</span> << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00339"></a>00339 <span class="comment">/*</span>
<a name="l00340"></a>00340 <span class="comment">//<<<<<<< dpllt_minisat.cpp</span>
<a name="l00341"></a>00341 <span class="comment"> clause.print();</span>
<a name="l00342"></a>00342 <span class="comment"> cout<<"--------------------" << endl;</span>
<a name="l00343"></a>00343 <span class="comment"> */</span>
<a name="l00344"></a>00344 <span class="comment">/* </span>
<a name="l00345"></a>00345 <span class="comment"> const CVC3::Theorem clauseThm = clause.getClauseTheorem();</span>
<a name="l00346"></a>00346 <span class="comment"> cout<<"====================" << endl;</span>
<a name="l00347"></a>00347 <span class="comment"> clause.print();</span>
<a name="l00348"></a>00348 <span class="comment">//=======</span>
<a name="l00349"></a>00349 <span class="comment"> theorem.print();</span>
<a name="l00350"></a>00350 <span class="comment">//>>>>>>> 1.14</span>
<a name="l00351"></a>00351 <span class="comment"> cout<<"--------------------" << endl;</span>
<a name="l00352"></a>00352 <span class="comment">//<<<<<<< dpllt_minisat.cpp</span>
<a name="l00353"></a>00353 <span class="comment"> if(clauseThm.isNull()){</span>
<a name="l00354"></a>00354 <span class="comment"> cout<<"leaf id " << clause.getId() << " # " << "NULL" << endl;</span>
<a name="l00355"></a>00355 <span class="comment"> }</span>
<a name="l00356"></a>00356 <span class="comment"> else{</span>
<a name="l00357"></a>00357 <span class="comment"> cout<<"leaf id " << clause.getId() << " # " << clauseThm << endl;</span>
<a name="l00358"></a>00358 <span class="comment"> }</span>
<a name="l00359"></a>00359 <span class="comment"> */</span>
<a name="l00360"></a>00360 <span class="comment">/*</span>
<a name="l00361"></a>00361 <span class="comment">//=======</span>
<a name="l00362"></a>00362 <span class="comment">//>>>>>>> 1.14</span>
<a name="l00363"></a>00363 <span class="comment"> */</span>
<a name="l00364"></a>00364 }
<a name="l00365"></a>00365 }
<a name="l00366"></a>00366 <span class="keywordflow">else</span>{
<a name="l00367"></a>00367 <a class="code" href="classSAT_1_1SatProofNode.html">SAT::SatProofNode</a> * leftNode = node-><a class="code" href="classSAT_1_1SatProofNode.html#a5e8c4112ac870c8d843e54a393bea892">getLeftParent</a>();
<a name="l00368"></a>00368 <a class="code" href="classSAT_1_1SatProofNode.html">SAT::SatProofNode</a> * rightNode = node-><a class="code" href="classSAT_1_1SatProofNode.html#a611593dffb824df842f88492bf160e80">getRightParent</a>();
<a name="l00369"></a>00369
<a name="l00370"></a>00370 <a class="code" href="dpllt__minisat_8cpp.html#ad267e4a889b4d5222cd489bc3b8139ce">printSatProof</a>(leftNode);
<a name="l00371"></a>00371 <a class="code" href="dpllt__minisat_8cpp.html#ad267e4a889b4d5222cd489bc3b8139ce">printSatProof</a>(rightNode);
<a name="l00372"></a>00372 }
<a name="l00373"></a>00373
<a name="l00374"></a>00374 }
<a name="l00375"></a>00375
<a name="l00376"></a>00376
<a name="l00377"></a>00377
<a name="l00378"></a><a class="code" href="classSAT_1_1DPLLTMiniSat.html#ae465fc059c93948333a16b2c21a8828b">00378</a> <a class="code" href="classCVC3_1_1Proof.html">CVC3::Proof</a> <a class="code" href="classSAT_1_1DPLLTMiniSat.html#ae465fc059c93948333a16b2c21a8828b" title="Get the proof from SAT engine.">DPLLTMiniSat::getSatProof</a>(<a class="code" href="classSAT_1_1CNF__Manager.html">CNF_Manager</a>* cnfManager, <a class="code" href="classCVC3_1_1TheoryCore.html" title="This theory handles the built-in logical connectives plus equality. It also handles the registration ...">CVC3::TheoryCore</a>* core){
<a name="l00379"></a>00379 <a class="code" href="classSAT_1_1SatProof.html">SAT::SatProof</a>* proof = <a class="code" href="classSAT_1_1DPLLTMiniSat.html#a679c7d58efef6a952128669e7fb7e493">getProof</a>();
<a name="l00380"></a>00380 <a class="code" href="classSAT_1_1SatProofNode.html">SAT::SatProofNode</a> * rootNode = proof-><a class="code" href="classSAT_1_1SatProof.html#af60143aa39c6a582d71c9d61bb816bfb">getRoot</a>();
<a name="l00381"></a>00381
<a name="l00382"></a>00382 <span class="comment">// printSatProof(rootNode);</span>
<a name="l00383"></a>00383
<a name="l00384"></a>00384 <a class="code" href="classCVC3_1_1TheoremProducer.html">CVC3::TheoremProducer</a>* thmProducer = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1TheoremProducer.html">TheoremProducer</a>(core-><a class="code" href="classCVC3_1_1TheoryCore.html#af3077cff0601b8ae28e420ef5ce2ea37">getTM</a>());
<a name="l00385"></a>00385
<a name="l00386"></a>00386 <span class="keywordflow">return</span> <a class="code" href="dpllt__minisat_8cpp.html#a3fffe610feac92e588d04cb0a81c497d">generateSatProof</a>(rootNode, cnfManager, thmProducer);
<a name="l00387"></a>00387 }
<a name="l00388"></a>00388
</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>
