5b71e5ec581eca4a05f572d902880426a1711f2f
1 /********************* */
2 /*! \file prop_engine.cpp
4 ** Original author: mdeters
5 ** Major contributors: dejan
6 ** Minor contributors (to current version): barrett, taking, cconway, kshitij
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief Implementation of the propositional engine of CVC4
16 ** Implementation of the propositional engine of CVC4.
19 #include "prop/cnf_stream.h"
20 #include "prop/prop_engine.h"
21 #include "prop/theory_proxy.h"
22 #include "prop/sat_solver.h"
23 #include "prop/sat_solver_factory.h"
25 #include "decision/decision_engine.h"
26 #include "theory/theory_engine.h"
27 #include "theory/theory_registrar.h"
28 #include "util/Assert.h"
29 #include "util/options.h"
30 #include "util/output.h"
31 #include "util/result.h"
32 #include "expr/expr.h"
33 #include "expr/command.h"
40 using namespace CVC4::context
;
45 /** Keeps a boolean flag scoped */
55 ScopedBool(bool& reference
) :
56 d_reference(reference
) {
57 d_original
= reference
;
61 d_reference
= d_original
;
65 PropEngine::PropEngine(TheoryEngine
* te
, DecisionEngine
*de
, Context
* context
) :
73 d_interrupted(false) {
75 Debug("prop") << "Constructing the PropEngine" << endl
;
77 d_satSolver
= SatSolverFactory::createDPLLMinisat();
79 theory::TheoryRegistrar
* registrar
= new theory::TheoryRegistrar(d_theoryEngine
);
80 d_cnfStream
= new CVC4::prop::TseitinCnfStream(d_satSolver
, registrar
, Options::current()->threads
> 1);
82 d_satSolver
->initialize(d_context
, new TheoryProxy(this, d_theoryEngine
, d_decisionEngine
, d_context
, d_cnfStream
));
84 d_decisionEngine
->setSatSolver(d_satSolver
);
85 d_decisionEngine
->setCnfStream(d_cnfStream
);
88 PropEngine::~PropEngine() {
89 Debug("prop") << "Destructing the PropEngine" << endl
;
94 void PropEngine::assertFormula(TNode node
) {
95 Assert(!d_inCheckSat
, "Sat solver in solve()!");
96 Debug("prop") << "assertFormula(" << node
<< ")" << endl
;
97 // Assert as non-removable
98 d_cnfStream
->convertAndAssert(node
, false, false);
101 void PropEngine::assertLemma(TNode node
, bool negated
, bool removable
) {
102 //Assert(d_inCheckSat, "Sat solver should be in solve()!");
103 Debug("prop::lemmas") << "assertLemma(" << node
<< ")" << endl
;
105 if(!d_inCheckSat
&& Dump
.isOn("learned")) {
106 Dump("learned") << AssertCommand(BoolExpr(node
.toExpr()));
107 } else if(Dump
.isOn("lemmas")) {
108 Dump("lemmas") << AssertCommand(BoolExpr(node
.toExpr()));
111 /* Tell decision engine */
113 // NodeBuilder<> nb(kind::NOT);
115 // d_decisionEngine->addAssertion(nb.constructNode());
117 // d_decisionEngine->addAssertion(node);
120 //TODO This comment is now false
121 // Assert as removable
122 d_cnfStream
->convertAndAssert(node
, removable
, negated
);
125 void PropEngine::printSatisfyingAssignment(){
126 const CnfStream::TranslationCache
& transCache
=
127 d_cnfStream
->getTranslationCache();
128 Debug("prop-value") << "Literal | Value | Expr" << endl
129 << "----------------------------------------"
130 << "-----------------" << endl
;
131 for(CnfStream::TranslationCache::const_iterator i
= transCache
.begin(),
132 end
= transCache
.end();
135 pair
<Node
, CnfStream::TranslationInfo
> curr
= *i
;
136 SatLiteral l
= curr
.second
.literal
;
139 SatValue value
= d_satSolver
->modelValue(l
);
140 Debug("prop-value") << "'" << l
<< "' " << value
<< " " << n
<< endl
;
145 Result
PropEngine::checkSat(unsigned long& millis
, unsigned long& resource
) {
146 Assert(!d_inCheckSat
, "Sat solver in solve()!");
147 Debug("prop") << "PropEngine::checkSat()" << endl
;
149 // Mark that we are in the checkSat
150 ScopedBool
scopedBool(d_inCheckSat
);
153 // TODO This currently ignores conflicts (a dangerous practice).
154 d_theoryEngine
->presolve();
156 if(Options::current()->preprocessOnly
) {
157 millis
= resource
= 0;
158 return Result(Result::SAT_UNKNOWN
, Result::REQUIRES_FULL_CHECK
);
162 d_satTimer
.set(millis
);
164 // Reset the interrupted flag
165 d_interrupted
= false;
168 SatValue result
= d_satSolver
->solve(resource
);
170 millis
= d_satTimer
.elapsed();
172 if( result
== SAT_VALUE_UNKNOWN
) {
173 Result::UnknownExplanation why
=
174 d_satTimer
.expired() ? Result::TIMEOUT
:
175 (d_interrupted
? Result::INTERRUPTED
: Result::RESOURCEOUT
);
176 return Result(Result::SAT_UNKNOWN
, why
);
179 if( result
== SAT_VALUE_TRUE
&& Debug
.isOn("prop") ) {
180 printSatisfyingAssignment();
183 Debug("prop") << "PropEngine::checkSat() => " << result
<< endl
;
184 if(result
== SAT_VALUE_TRUE
&& d_theoryEngine
->isIncomplete()) {
185 return Result(Result::SAT_UNKNOWN
, Result::INCOMPLETE
);
187 return Result(result
== SAT_VALUE_TRUE
? Result::SAT
: Result::UNSAT
);
190 Node
PropEngine::getValue(TNode node
) const {
191 Assert(node
.getType().isBoolean());
192 Assert(d_cnfStream
->hasLiteral(node
));
194 SatLiteral lit
= d_cnfStream
->getLiteral(node
);
196 SatValue v
= d_satSolver
->value(lit
);
197 if(v
== SAT_VALUE_TRUE
) {
198 return NodeManager::currentNM()->mkConst(true);
199 } else if(v
== SAT_VALUE_FALSE
) {
200 return NodeManager::currentNM()->mkConst(false);
202 Assert(v
== SAT_VALUE_UNKNOWN
);
207 bool PropEngine::isSatLiteral(TNode node
) const {
208 return d_cnfStream
->hasLiteral(node
);
211 bool PropEngine::isTranslatedSatLiteral(TNode node
) const {
212 return d_cnfStream
->isTranslated(node
);
215 bool PropEngine::hasValue(TNode node
, bool& value
) const {
216 Assert(node
.getType().isBoolean());
217 Assert(d_cnfStream
->hasLiteral(node
));
219 SatLiteral lit
= d_cnfStream
->getLiteral(node
);
221 SatValue v
= d_satSolver
->value(lit
);
222 if(v
== SAT_VALUE_TRUE
) {
225 } else if(v
== SAT_VALUE_FALSE
) {
229 Assert(v
== SAT_VALUE_UNKNOWN
);
234 void PropEngine::ensureLiteral(TNode n
) {
235 d_cnfStream
->ensureLiteral(n
);
238 void PropEngine::push() {
239 Assert(!d_inCheckSat
, "Sat solver in solve()!");
241 Debug("prop") << "push()" << endl
;
244 void PropEngine::pop() {
245 Assert(!d_inCheckSat
, "Sat solver in solve()!");
247 Debug("prop") << "pop()" << endl
;
250 bool PropEngine::isRunning() const {
254 void PropEngine::interrupt() throw(ModalException
) {
256 throw ModalException("SAT solver is not currently solving anything; "
257 "cannot interrupt it");
260 d_interrupted
= true;
261 d_satSolver
->interrupt();
262 Debug("prop") << "interrupt()" << endl
;
265 void PropEngine::spendResource() throw() {
269 bool PropEngine::properExplanation(TNode node
, TNode expl
) const {
270 if(! d_cnfStream
->hasLiteral(node
)) {
271 Trace("properExplanation") << "properExplanation(): Failing because node "
272 << "being explained doesn't have a SAT literal ?!" << std::endl
273 << "properExplanation(): The node is: " << node
<< std::endl
;
277 SatLiteral nodeLit
= d_cnfStream
->getLiteral(node
);
279 for(TNode::kinded_iterator i
= expl
.begin(kind::AND
),
280 i_end
= expl
.end(kind::AND
);
283 if(! d_cnfStream
->hasLiteral(*i
)) {
284 Trace("properExplanation") << "properExplanation(): Failing because one of explanation "
285 << "nodes doesn't have a SAT literal" << std::endl
286 << "properExplanation(): The explanation node is: " << *i
<< std::endl
;
290 SatLiteral iLit
= d_cnfStream
->getLiteral(*i
);
292 if(iLit
== nodeLit
) {
293 Trace("properExplanation") << "properExplanation(): Failing because the node" << std::endl
294 << "properExplanation(): " << node
<< std::endl
295 << "properExplanation(): cannot be made to explain itself!" << std::endl
;
299 if(! d_satSolver
->properExplanation(nodeLit
, iLit
)) {
300 Trace("properExplanation") << "properExplanation(): SAT solver told us that node" << std::endl
301 << "properExplanation(): " << *i
<< std::endl
302 << "properExplanation(): is not part of a proper explanation node for" << std::endl
303 << "properExplanation(): " << node
<< std::endl
304 << "properExplanation(): Perhaps it one of the two isn't assigned or the explanation" << std::endl
305 << "properExplanation(): node wasn't propagated before the node being explained" << std::endl
;
313 }/* CVC4::prop namespace */
314 }/* CVC4 namespace */