diff options
author | Guy <katz911@gmail.com> | 2016-06-20 14:20:15 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-06-20 14:20:15 -0700 |
commit | a592e0137504c5788084cb8e150f46f109f566d7 (patch) | |
tree | 0816b285c639e0121a1d0a63033ad29bf25b5e35 /src/smt | |
parent | 4b8972fec229012812bb7edc9e315c2e54f7c059 (diff) |
Addressed a bug that occurs when proof production is triggered via text flags in the input.
Separated some initialization into two phases:
1. Those that can be done when the proof compiliation flag is set
2. Those that can be done only when the --proof option is set.
For #2, deferred their execution until the text flags in the input have been processed
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 69a150cc9..08495c936 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1083,7 +1083,9 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : 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)); ); +#ifdef CVC4_PROOF + ProofManager::currentPM()->getTheoryProofEngine()->registerTheory(d_theoryEngine->theoryOf(id)); +#endif } d_private->addUseTheoryListListener(d_theoryEngine); @@ -1152,6 +1154,13 @@ void SmtEngine::finishInit() { d_dumpCommands.clear(); PROOF( ProofManager::currentPM()->setLogic(d_logic); ); + PROOF({ + for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) { + ProofManager::currentPM()->getTheoryProofEngine()-> + finishRegisterTheory(d_theoryEngine->theoryOf(id)); + } + }); + Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl; } @@ -1846,7 +1855,7 @@ void SmtEngine::setDefaults() { } //counterexample-guided instantiation for non-sygus // enable if any possible quantifiers with arithmetic, datatypes or bitvectors - if( ( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) || d_logic.isTheoryEnabled(THEORY_BV) ) ) || + if( ( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) || d_logic.isTheoryEnabled(THEORY_BV) ) ) || options::cbqiAll() ){ if( !options::cbqi.wasSetByUser() ){ options::cbqi.set( true ); |