diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 103 |
1 files changed, 77 insertions, 26 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8c8b5f840..911a16eed 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -733,6 +733,9 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : } void SmtEngine::finishInit() { + // ensure that our heuristics are properly set up + setDefaults(); + d_decisionEngine = new DecisionEngine(d_context, d_userContext); d_decisionEngine->init(); // enable appropriate strategies @@ -790,24 +793,7 @@ void SmtEngine::finalOptionsAreSet() { return; } - if(options::bitvectorEagerBitblast()) { - // Eager solver should use the internal decision strategy - options::decisionMode.set(DECISION_STRATEGY_INTERNAL); - } - - if(options::checkModels()) { - if(! options::interactive()) { - 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")); - } - if(! d_logic.isLocked()) { - // ensure that our heuristics are properly set up setLogicInternal(); } @@ -922,15 +908,68 @@ LogicInfo SmtEngine::getLogicInfo() const { return d_logic; } -// This function is called when d_logic has just been changed. -// The LogicInfo isn't passed in explicitly, because that might -// tempt people in the code to use the (potentially unlocked) -// version that's passed in, leading to assert-fails in certain -// uses of the CVC4 library. void SmtEngine::setLogicInternal() throw() { Assert(!d_fullyInited, "setting logic in SmtEngine but the engine has already finished initializing for this run"); - d_logic.lock(); +} + +void SmtEngine::setDefaults() { + if(options::forceLogic.wasSetByUser()) { + d_logic = options::forceLogic(); + } + + // set strings-exp + if(!d_logic.hasEverything() && d_logic.isTheoryEnabled(THEORY_STRINGS) ) { + if(! options::stringExp.wasSetByUser()) { + options::stringExp.set( true ); + Trace("smt") << "turning on strings-exp, for the theory of strings" << std::endl; + } + } + // for strings + if(options::stringExp()) { + if( !d_logic.isQuantified() ) { + d_logic = d_logic.getUnlockedCopy(); + d_logic.enableQuantifiers(); + d_logic.lock(); + Trace("smt") << "turning on quantifier logic, for strings-exp" << std::endl; + } + if(! options::finiteModelFind.wasSetByUser()) { + options::finiteModelFind.set( true ); + Trace("smt") << "turning on finite-model-find, for strings-exp" << std::endl; + } + if(! options::fmfBoundInt.wasSetByUser()) { + options::fmfBoundInt.set( true ); + Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl; + } + /* + if(! options::rewriteDivk.wasSetByUser()) { + options::rewriteDivk.set( true ); + Trace("smt") << "turning on rewrite-divk, for strings-exp" << std::endl; + }*/ + /* + if(! options::stringFMF.wasSetByUser()) { + options::stringFMF.set( true ); + Trace("smt") << "turning on strings-fmf, for strings-exp" << std::endl; + } + */ + } + + if(options::bitvectorEagerBitblast()) { + // Eager solver should use the internal decision strategy + options::decisionMode.set(DECISION_STRATEGY_INTERNAL); + } + + if(options::checkModels()) { + if(! options::interactive()) { + 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")); + } // Set the options for the theoryOf if(!options::theoryOfMode.wasSetByUser()) { @@ -1065,7 +1104,7 @@ void SmtEngine::setLogicInternal() throw() { if(! options::unconstrainedSimp.wasSetByUser() || options::incrementalSolving()) { // bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified(); // bool uncSimp = false && !qf_sat && !options::incrementalSolving(); - bool uncSimp = !options::incrementalSolving() && !d_logic.isQuantified() && !options::produceModels() && !options::checkModels() && + bool uncSimp = !options::incrementalSolving() && !d_logic.isQuantified() && !options::produceModels() && !options::produceAssignments() && !options::checkModels() && (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_BV)); Trace("smt") << "setting unconstrained simplification to " << uncSimp << endl; options::unconstrainedSimp.set(uncSimp); @@ -1076,6 +1115,10 @@ void SmtEngine::setLogicInternal() throw() { Notice() << "SmtEngine: turning off produce-models to support unconstrainedSimp" << endl; setOption("produce-models", SExpr("false")); } + if (options::produceAssignments()) { + Notice() << "SmtEngine: turning off produce-assignments to support unconstrainedSimp" << endl; + setOption("produce-assignments", SExpr("false")); + } if (options::checkModels()) { Notice() << "SmtEngine: turning off check-models to support unconstrainedSimp" << endl; setOption("check-models", SExpr("false")); @@ -1211,7 +1254,7 @@ void SmtEngine::setLogicInternal() throw() { //until bugs 371,431 are fixed if( ! options::minisatUseElim.wasSetByUser()){ - if( d_logic.isQuantified() || options::produceModels() || options::checkModels() ){ + if( d_logic.isQuantified() || options::produceModels() || options::produceAssignments() || options::checkModels() ){ options::minisatUseElim.set( false ); } } @@ -1220,6 +1263,10 @@ void SmtEngine::setLogicInternal() throw() { Notice() << "SmtEngine: turning off produce-models to support minisatUseElim" << endl; setOption("produce-models", SExpr("false")); } + if (options::produceAssignments()) { + Notice() << "SmtEngine: turning off produce-assignments to support minisatUseElim" << endl; + setOption("produce-assignments", SExpr("false")); + } if (options::checkModels()) { Notice() << "SmtEngine: turning off check-models to support minisatUseElim" << endl; setOption("check-models", SExpr("false")); @@ -1227,7 +1274,7 @@ void SmtEngine::setLogicInternal() throw() { } // For now, these array theory optimizations do not support model-building - if (options::produceModels() || options::checkModels()) { + if (options::produceModels() || options::produceAssignments() || options::checkModels()) { options::arraysOptimizeLinear.set(false); options::arraysLazyRIntro1.set(false); } @@ -1239,6 +1286,10 @@ void SmtEngine::setLogicInternal() throw() { Warning() << "SmtEngine: turning off produce-models because unsupported for nonlinear arith" << endl; setOption("produce-models", SExpr("false")); } + if (options::produceAssignments()) { + Warning() << "SmtEngine: turning off produce-assignments because unsupported for nonlinear arith" << endl; + setOption("produce-assignments", SExpr("false")); + } if (options::checkModels()) { Warning() << "SmtEngine: turning off check-models because unsupported for nonlinear arith" << endl; setOption("check-models", SExpr("false")); |