diff options
Diffstat (limited to 'src/prop/prop_engine.cpp')
-rw-r--r-- | src/prop/prop_engine.cpp | 33 |
1 files changed, 17 insertions, 16 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 738b4dc9c..473449179 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -32,6 +32,7 @@ #include "proof/proof_manager.h" #include "prop/cnf_stream.h" #include "prop/minisat/minisat.h" +#include "prop/prop_proof_manager.h" #include "prop/sat_solver.h" #include "prop/sat_solver_factory.h" #include "prop/theory_proxy.h" @@ -83,7 +84,7 @@ PropEngine::PropEngine(TheoryEngine* te, d_resourceManager(rm), d_outMgr(outMgr) { - Debug("prop") << "Constructing the PropEngine" << endl; + Debug("prop") << "Constructing the PropEngine" << std::endl; d_decisionEngine.reset(new DecisionEngine(satContext, userContext, rm)); d_decisionEngine->init(); // enable appropriate strategies @@ -146,7 +147,7 @@ void PropEngine::finishInit() } PropEngine::~PropEngine() { - Debug("prop") << "Destructing the PropEngine" << endl; + Debug("prop") << "Destructing the PropEngine" << std::endl; d_decisionEngine->shutdown(); d_decisionEngine.reset(nullptr); delete d_cnfStream; @@ -179,7 +180,7 @@ void PropEngine::notifyPreprocessedAssertions( void PropEngine::assertFormula(TNode node) { Assert(!d_inCheckSat) << "Sat solver in solve()!"; - Debug("prop") << "assertFormula(" << node << ")" << endl; + Debug("prop") << "assertFormula(" << node << ")" << std::endl; d_decisionEngine->addAssertion(node); assertInternal(node, false, false, true); } @@ -187,7 +188,7 @@ void PropEngine::assertFormula(TNode node) { void PropEngine::assertSkolemDefinition(TNode node, TNode skolem) { Assert(!d_inCheckSat) << "Sat solver in solve()!"; - Debug("prop") << "assertFormula(" << node << ")" << endl; + Debug("prop") << "assertFormula(" << node << ")" << std::endl; d_decisionEngine->addSkolemDefinition(node, skolem); assertInternal(node, false, false, true); } @@ -235,7 +236,7 @@ void PropEngine::assertTrustedLemmaInternal(theory::TrustNode trn, bool removable) { Node node = trn.getNode(); - Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl; + Debug("prop::lemmas") << "assertLemma(" << node << ")" << std::endl; bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT; Assert(!isProofEnabled() || trn.getGenerator() != nullptr); assertInternal(trn.getNode(), negated, removable, false, trn.getGenerator()); @@ -292,7 +293,7 @@ void PropEngine::assertLemmasInternal( } void PropEngine::requirePhase(TNode n, bool phase) { - Debug("prop") << "requirePhase(" << n << ", " << phase << ")" << endl; + Debug("prop") << "requirePhase(" << n << ", " << phase << ")" << std::endl; Assert(n.getType().isBoolean()); SatLiteral lit = d_cnfStream->getLiteral(n); @@ -307,26 +308,26 @@ bool PropEngine::isDecision(Node lit) const { void PropEngine::printSatisfyingAssignment(){ const CnfStream::NodeToLiteralMap& transCache = d_cnfStream->getTranslationCache(); - Debug("prop-value") << "Literal | Value | Expr" << endl + Debug("prop-value") << "Literal | Value | Expr" << std::endl << "----------------------------------------" - << "-----------------" << endl; + << "-----------------" << std::endl; for(CnfStream::NodeToLiteralMap::const_iterator i = transCache.begin(), end = transCache.end(); i != end; ++i) { - pair<Node, SatLiteral> curr = *i; + std::pair<Node, SatLiteral> curr = *i; SatLiteral l = curr.second; if(!l.isNegated()) { Node n = curr.first; SatValue value = d_satSolver->modelValue(l); - Debug("prop-value") << "'" << l << "' " << value << " " << n << endl; + Debug("prop-value") << "'" << l << "' " << value << " " << n << std::endl; } } } Result PropEngine::checkSat() { Assert(!d_inCheckSat) << "Sat solver in solve()!"; - Debug("prop") << "PropEngine::checkSat()" << endl; + Debug("prop") << "PropEngine::checkSat()" << std::endl; // Mark that we are in the checkSat ScopedBool scopedBool(d_inCheckSat); @@ -360,7 +361,7 @@ Result PropEngine::checkSat() { printSatisfyingAssignment(); } - Debug("prop") << "PropEngine::checkSat() => " << result << endl; + Debug("prop") << "PropEngine::checkSat() => " << result << std::endl; if(result == SAT_VALUE_TRUE && d_theoryEngine->isIncomplete()) { return Result(Result::SAT_UNKNOWN, Result::INCOMPLETE); } @@ -491,20 +492,20 @@ void PropEngine::push() { Assert(!d_inCheckSat) << "Sat solver in solve()!"; d_satSolver->push(); - Debug("prop") << "push()" << endl; + Debug("prop") << "push()" << std::endl; } void PropEngine::pop() { Assert(!d_inCheckSat) << "Sat solver in solve()!"; d_satSolver->pop(); - Debug("prop") << "pop()" << endl; + Debug("prop") << "pop()" << std::endl; } void PropEngine::resetTrail() { d_satSolver->resetTrail(); - Debug("prop") << "resetTrail()" << endl; + Debug("prop") << "resetTrail()" << std::endl; } unsigned PropEngine::getAssertionLevel() const @@ -522,7 +523,7 @@ void PropEngine::interrupt() d_interrupted = true; d_satSolver->interrupt(); - Debug("prop") << "interrupt()" << endl; + Debug("prop") << "interrupt()" << std::endl; } void PropEngine::spendResource(ResourceManager::Resource r) |