Fix for (get-assignment), resolves bug 553.

diff --git a/src/smt/options b/src/smt/options
index fffe559e7dcbe880da68f642dd392e9519c0d6da..873aec6d1f5c9ffa61ab7018558e1cc98490c82e 100644 (file)
--- 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 c9c3d6345a87cfe2cea33109c25e77ca4afe058d..49f2c79432f1ee3458b4345721dcdc20589d8f6e 100644 (file)
--- 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 8c8b5f8401376e5eda2c5f94f48a2da4ac9d2dbc..911a16eed8b1c85a659ec54c74d23c5c304a2545 100644 (file)
--- 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 8e400468c94a637511cb77eddfa13935378917d3..51fa098646ce2a516450d65eb3d4fdf1b60ee356 100644 (file)
--- 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 fe6b156f1cbbe3a6ddfc0421df11a296fd2b3e0a..664958e5a23e43a93c0653353714f01234654791 100644 (file)
--- 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