diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 27 |
1 files changed, 21 insertions, 6 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 1962c6433..c66031265 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -788,6 +788,13 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_stats = new SmtEngineStatistics(); d_stats->d_resourceUnitsUsed.setData( d_private->getResourceManager()->getResourceUsage()); + + // The ProofManager is constructed before any other proof objects such as + // SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are + // initialized in TheoryEngine and PropEngine respectively. + Assert(d_proofManager == NULL); + 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, @@ -798,6 +805,8 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : // Add the theories for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) { TheoryConstructor::addTheory(d_theoryEngine, id); + //register with proof engine if applicable + THEORY_PROOF(ProofManager::currentPM()->getTheoryProofEngine()->registerTheory(d_theoryEngine->theoryOf(id)); ); } // global push/pop around everything, to ensure proper destruction @@ -817,9 +826,6 @@ void SmtEngine::finishInit() { // ensure that our heuristics are properly set up setDefaults(); - Assert(d_proofManager == NULL); - PROOF( d_proofManager = new ProofManager(); ); - d_decisionEngine = new DecisionEngine(d_context, d_userContext); d_decisionEngine->init(); // enable appropriate strategies @@ -857,7 +863,7 @@ void SmtEngine::finishInit() { } d_dumpCommands.clear(); - PROOF( ProofManager::currentPM()->setLogic(d_logic.getLogicString()); ); + PROOF( ProofManager::currentPM()->setLogic(d_logic); ); } void SmtEngine::finalOptionsAreSet() { @@ -3515,6 +3521,14 @@ void SmtEnginePrivate::processAssertions() { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-definition-expansion" << endl; dumpAssertions("post-definition-expansion", d_assertions); + // save the assertions now + THEORY_PROOF + ( + for (unsigned i = 0; i < d_assertions.size(); ++i) { + ProofManager::currentPM()->addAssertion(d_assertions[i].toExpr()); + } + ); + Debug("smt") << " d_assertions : " << d_assertions.size() << endl; if( options::ceGuidedInst() ){ @@ -3936,7 +3950,8 @@ void SmtEnginePrivate::addFormula(TNode n, bool inUnsatCore, bool inInput) PROOF( if( inInput ){ // n is an input assertion - ProofManager::currentPM()->addAssertion(n.toExpr(), inUnsatCore); + if (inUnsatCore || options::dumpUnsatCores() || options::checkUnsatCores()) + ProofManager::currentPM()->addCoreAssertion(n.toExpr()); }else{ // n is the result of an unknown preprocessing step, add it to dependency map to null ProofManager::currentPM()->addDependence(n, Node::null()); @@ -4724,7 +4739,7 @@ UnsatCore SmtEngine::getUnsatCore() throw(ModalException, UnsafeInterruptExcepti throw ModalException("Cannot get an unsat core unless immediately preceded by UNSAT/VALID response."); } - d_proofManager->getProof(this);// just to trigger core creation + d_proofManager->traceUnsatCore();// just to trigger core creation return UnsatCore(this, d_proofManager->begin_unsat_core(), d_proofManager->end_unsat_core()); #else /* IS_PROOFS_BUILD */ throw ModalException("This build of CVC4 doesn't have proof support (required for unsat cores)."); |