From 93f084750d8a76d63fc74d242944bce0635c2194 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 3 Jan 2014 12:13:13 -0600 Subject: Added support for proof production in Equality Engine. Cleaned up existing proof signatures and added proof signature for theory of arrays. Added new MBQI technique based on interval abstraction. Cleaned up option names. Improved symmetry breaking for uf strong solver. Other minor cleanup. --- src/smt/smt_engine.cpp | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) (limited to 'src/smt') diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f26456cae..539622877 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -771,7 +771,7 @@ void SmtEngine::finishInit() { setTimeLimit(options::cumulativeMillisecondLimit(), true); } - PROOF( ProofManager::currentPM()->setLogic(d_logic.getLogicString()); ); + PROOF( ProofManager::currentPM()->setLogic(d_logic.getLogicString()); ); } void SmtEngine::finalOptionsAreSet() { @@ -1144,13 +1144,17 @@ void SmtEngine::setLogicInternal() throw() { } if ( ! options::fmfInstGen.wasSetByUser()) { //if full model checking is on, disable inst-gen techniques - if( options::fmfFullModelCheck() ){ + if( options::mbqiMode()==quantifiers::MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_INTERVAL ){ options::fmfInstGen.set( false ); + }else{ + options::fmfInstGen.set( true ); } } if ( options::fmfBoundInt() ){ - //if bounded integers are set, must use full model check for MBQI - options::fmfFullModelCheck.set( true ); + if( options::mbqiMode()!=quantifiers::MBQI_NONE ){ + //if bounded integers are set, must use full model check for MBQI + options::mbqiMode.set( quantifiers::MBQI_FMC ); + } } if( options::ufssSymBreak() ){ options::sortInference.set( true ); @@ -3309,7 +3313,7 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc // Ensure expr is type-checked at this point. ensureBoolean(e); // Give it to proof manager - PROOF( ProofManager::currentPM()->addAssertion(e); ); + PROOF( ProofManager::currentPM()->addAssertion(e); ); } // check to see if a postsolve() is pending @@ -3390,7 +3394,7 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept // 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()); ); + PROOF( ProofManager::currentPM()->addAssertion(e.notExpr()); ); // check to see if a postsolve() is pending if(d_needPostsolve) { @@ -3455,7 +3459,7 @@ Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, Log finalOptionsAreSet(); doPendingPops(); - PROOF( ProofManager::currentPM()->addAssertion(ex); ); + PROOF( ProofManager::currentPM()->addAssertion(ex); ); Trace("smt") << "SmtEngine::assertFormula(" << ex << ")" << endl; -- cgit v1.2.3