From 463cf1b3ec4df9dff10026a2d306de2f41c9cef9 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 7 Mar 2014 15:42:29 -0500 Subject: [PATCH] Fix for (get-assignment), resolves bug 553. --- src/smt/options | 3 + src/smt/options_handlers.h | 13 ++++ src/smt/smt_engine.cpp | 103 ++++++++++++++++++++++-------- src/smt/smt_engine.h | 6 ++ test/regress/regress0/Makefile.am | 4 +- 5 files changed, 101 insertions(+), 28 deletions(-) diff --git a/src/smt/options b/src/smt/options index fffe559e7..873aec6d1 100644 --- a/src/smt/options +++ b/src/smt/options @@ -10,6 +10,9 @@ common-option - --dump=MODE argument :handler CVC4::smt::dumpMode :handler-inclu common-option - --dump-to=FILE argument :handler CVC4::smt::dumpToFile :handler-include "smt/options_handlers.h" all dumping goes to FILE (instead of stdout) +expert-option forceLogic force-logic --force-logic=LOGIC LogicInfo :include "theory/logic_info.h" :handler CVC4::smt::stringToLogicInfo :handler-include "smt/options_handlers.h" :default '""' + set the logic, and override all further user attempts to change it + option simplificationMode simplification-mode --simplification=MODE SimplificationMode :handler CVC4::smt::stringToSimplificationMode :default SIMPLIFICATION_MODE_BATCH :read-write :include "smt/simplification_mode.h" :handler-include "smt/options_handlers.h" choose simplification mode, see --simplification=help alias --no-simplification = --simplification=none diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h index c9c3d6345..49f2c7943 100644 --- a/src/smt/options_handlers.h +++ b/src/smt/options_handlers.h @@ -257,6 +257,19 @@ inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) { #endif /* CVC4_DUMPING */ } +inline LogicInfo stringToLogicInfo(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + try { + LogicInfo logic(optarg); + if(smt != NULL) { + smt->setLogic(logic); + } + return logic; + } catch(IllegalArgumentException& e) { + throw OptionException(std::string("invalid logic specification for --force-logic: `") + + optarg + "':\n" + e.what()); + } +} + inline SimplificationMode stringToSimplificationMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { if(optarg == "batch") { return SIMPLIFICATION_MODE_BATCH; 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")); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 8e400468c..51fa09864 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -283,6 +283,12 @@ class CVC4_PUBLIC SmtEngine { */ void finalOptionsAreSet(); + /** + * Apply heuristics settings and other defaults. Done once, at + * finishInit() time. + */ + void setDefaults(); + /** * Create theory engine, prop engine, decision engine. Called by * finalOptionsAreSet() diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index fe6b156f1..664958e5a 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -140,6 +140,7 @@ BUG_TESTS = \ bug421.smt2 \ bug421b.smt2 \ bug425.cvc \ + bug480.smt2 \ bug484.smt2 \ bug486.cvc \ bug507.smt2 \ @@ -173,8 +174,7 @@ endif EXTRA_DIST += \ subranges.cvc \ arrayinuf_error.smt2 \ - error.cvc \ - bug480.smt2 + error.cvc # synonyms for "check" in this directory .PHONY: regress regress0 test -- 2.30.2