diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 31 |
1 files changed, 19 insertions, 12 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 1f83bb547..ec37eaf26 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -46,8 +46,10 @@ #include "theory/theory_engine.h" #include "theory/bv/theory_bv_rewriter.h" #include "proof/proof_manager.h" +#include "main/options.h" #include "util/proof.h" #include "proof/proof.h" +#include "proof/proof_manager.h" #include "util/boolean_simplification.h" #include "util/node_visitor.h" #include "util/configuration.h" @@ -157,6 +159,8 @@ struct SmtEngineStatistics { IntStat d_numAssertionsPost; /** time spent in checkModel() */ TimerStat d_checkModelTime; + /** time spent in checkProof() */ + TimerStat d_checkProofTime; /** time spent in PropEngine::checkSat() */ TimerStat d_solveTime; /** time spent in pushing/popping */ @@ -183,11 +187,11 @@ struct SmtEngineStatistics { d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0), d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0), d_checkModelTime("smt::SmtEngine::checkModelTime"), + d_checkProofTime("smt::SmtEngine::checkProofTime"), d_solveTime("smt::SmtEngine::solveTime"), d_pushPopTime("smt::SmtEngine::pushPopTime"), d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"), d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0) - { StatisticsRegistry::registerStat(&d_definitionExpansionTime); @@ -667,6 +671,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_decisionEngine(NULL), d_theoryEngine(NULL), d_propEngine(NULL), + d_proofManager(NULL), d_definedFunctions(NULL), d_assertionList(NULL), d_assignments(NULL), @@ -696,6 +701,8 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_statisticsRegistry = new StatisticsRegistry(); d_stats = new SmtEngineStatistics(); + PROOF( d_proofManager = new ProofManager(); ); + // We have mutual dependency here, so we add the prop engine to the theory // engine later (it is non-essential there) d_theoryEngine = new TheoryEngine(d_context, d_userContext, d_private->d_iteRemover, const_cast<const LogicInfo&>(d_logic)); @@ -763,6 +770,7 @@ void SmtEngine::finishInit() { if(options::cumulativeMillisecondLimit() != 0) { setTimeLimit(options::cumulativeMillisecondLimit(), true); } + PROOF( ProofManager::currentPM()->setLogic(d_logic.getLogicString()); ); } @@ -777,16 +785,11 @@ void SmtEngine::finalOptionsAreSet() { } if(options::checkModels()) { - if(! options::produceModels()) { - Notice() << "SmtEngine: turning on produce-models to support check-model" << endl; - setOption("produce-models", SExpr("true")); - } if(! options::interactive()) { - Notice() << "SmtEngine: turning on interactive-mode to support check-model" << endl; + Notice() << "SmtEngine: turning on interactive-mode to support check-models" << endl; setOption("interactive-mode", SExpr("true")); } } - if(options::produceAssignments() && !options::produceModels()) { Notice() << "SmtEngine: turning on produce-models to support produce-assignments" << endl; setOption("produce-models", SExpr("true")); @@ -3291,9 +3294,6 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc finalOptionsAreSet(); doPendingPops(); - - PROOF( ProofManager::currentPM()->addAssertion(ex); ); - Trace("smt") << "SmtEngine::checkSat(" << ex << ")" << endl; if(d_queryMade && !options::incrementalSolving()) { @@ -3308,6 +3308,8 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); // Ensure expr is type-checked at this point. ensureBoolean(e); + // Give it to proof manager + PROOF( ProofManager::currentPM()->addAssertion(e); ); } // check to see if a postsolve() is pending @@ -3361,6 +3363,7 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc // Check that UNSAT results generate a proof correctly. if(options::checkProofs()) { if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) { + TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime); checkProof(); } } @@ -3384,9 +3387,10 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept // Substitute out any abstract values in ex Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); - // Ensure that the expression is type-checked at this point, and Boolean ensureBoolean(e); + // Give it to proof manager + PROOF( ProofManager::currentPM()->addAssertion(e.notExpr()); ); // check to see if a postsolve() is pending if(d_needPostsolve) { @@ -3437,6 +3441,7 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept // Check that UNSAT results generate a proof correctly. if(options::checkProofs()) { if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) { + TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime); checkProof(); } } @@ -3449,7 +3454,9 @@ Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, Log SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); - PROOF( ProofManager::currentPM()->addAssertion(ex);); + + PROOF( ProofManager::currentPM()->addAssertion(ex); ); + Trace("smt") << "SmtEngine::assertFormula(" << ex << ")" << endl; // Substitute out any abstract values in ex |