diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 61 |
1 files changed, 37 insertions, 24 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d450319b1..832779944 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -60,6 +60,8 @@ #include "theory/booleans/circuit_propagator.h" #include "util/ite_removal.h" #include "theory/model.h" +#include "printer/printer.h" +#include "prop/options.h" using namespace std; using namespace CVC4; @@ -488,7 +490,9 @@ void SmtEngine::setLogicInternal() throw(AssertionException) { bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified(); bool quantifiers = d_logic.isQuantified(); Trace("smt") << "setting simplification mode to <" << d_logic.getLogicString() << "> " << (!qf_sat && !quantifiers) << std::endl; - options::simplificationMode.set(qf_sat || quantifiers ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH); + //simplifaction=none works better for SMT LIB benchmarks with quantifiers, not others + //options::simplificationMode.set(qf_sat || quantifiers ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH); + options::simplificationMode.set(qf_sat ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH); } // If in arrays, set the UF handler to arrays @@ -617,6 +621,21 @@ void SmtEngine::setLogicInternal() throw(AssertionException) { options::decisionMode.set(decMode); options::decisionStopOnly.set(stoponly); } + + //for finite model finding + if( ! options::instWhenMode.wasSetByUser()){ + if( options::fmfInstEngine() ){ + Trace("smt") << "setting inst when mode to LAST_CALL" << std::endl; + options::instWhenMode.set( INST_WHEN_LAST_CALL ); + } + } + + //until bug 371 is fixed + if( ! options::minisatUseElim.wasSetByUser()){ + if( d_logic.isQuantified() ){ + options::minisatUseElim.set( false ); + } + } } void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) @@ -1727,11 +1746,10 @@ Expr SmtEngine::getValue(const Expr& e) throw ModalException(msg); } - // Apply what was learned from preprocessing - Node n = d_private->applySubstitutions(e.getNode()); + // do not need to apply preprocessing substitutions (should be recorded in model already) // Normalize for the theories - n = Rewriter::rewrite(n); + Node n = Rewriter::rewrite( e.getNode() ); Trace("smt") << "--- getting value of " << n << endl; theory::TheoryModel* m = d_theoryEngine->getModel(); @@ -1835,34 +1853,19 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) } -void SmtEngine::addToModelType( Type& t ){ - Trace("smt") << "SMT addToModelType(" << t << ")" << endl; - SmtScope smts(this); - finalOptionsAreSet(); - if( options::produceModels() ) { - d_theoryEngine->getModel()->addDefineType( TypeNode::fromType( t ) ); - } -} - -void SmtEngine::addToModelFunction( Expr& e ){ - Trace("smt") << "SMT addToModelFunction(" << e << ")" << endl; +void SmtEngine::addToModelCommand( Command* c, int c_type ){ + Trace("smt") << "SMT addToModelCommand(" << c << ", " << c_type << ")" << endl; SmtScope smts(this); finalOptionsAreSet(); if( options::produceModels() ) { - d_theoryEngine->getModel()->addDefineFunction( e.getNode() ); + d_theoryEngine->getModel()->addCommand( c, c_type ); } } - Model* SmtEngine::getModel() throw(ModalException, AssertionException){ Trace("smt") << "SMT getModel()" << endl; SmtScope smts(this); - if(!options::produceModels()) { - const char* msg = - "Cannot get model when produce-models options is off."; - throw ModalException(msg); - } if(d_status.isNull() || d_status.asSatisfiabilityResult() == Result::UNSAT || d_problemExtended) { @@ -1871,7 +1874,11 @@ Model* SmtEngine::getModel() throw(ModalException, AssertionException){ "preceded by SAT/INVALID or UNKNOWN response."; throw ModalException(msg); } - + if(!options::produceModels()) { + const char* msg = + "Cannot get model when produce-models options is off."; + throw ModalException(msg); + } return d_theoryEngine->getModel(); } @@ -2066,7 +2073,13 @@ StatisticsRegistry* SmtEngine::getStatisticsRegistry() const { void SmtEngine::printModel( std::ostream& out, Model* m ){ SmtScope smts(this); - m->toStream(out); + Printer::getPrinter(options::outputLanguage())->toStream( out, m ); + //m->toStream(out); +} + +void SmtEngine::setUserAttribute( std::string& attr, Expr expr ){ + SmtScope smts(this); + d_theoryEngine->setUserAttribute( attr, expr.getNode() ); } }/* CVC4 namespace */ |