LogicInfo locking implemented, and some initialization-order issues in SmtEngine resolved.

ALL_SUPPORTED and QF_ALL_SUPPORTED logics now supported by SMT-LIB parsers.  In SMT-LIBv2, if a (set-logic..) command is missing, ALL_SUPPORTED is assumed, and a warning is issued, as discussed on the cvc4-devel mailing list.

1 files changed, 60 insertions, 23 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8b3e6b742..ed28c23a3 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -242,7 +242,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   d_assertionList(NULL),
   d_assignments(NULL),
   d_logic(),
-  d_logicIsSet(false),
+  d_fullyInited(false),
   d_problemExtended(false),
   d_queryMade(false),
   d_needPostsolve(false),
@@ -328,6 +328,19 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   if(Options::current()->cumulativeMillisecondLimit != 0) {
     setTimeLimit(Options::current()->cumulativeMillisecondLimit, true);
   }
+}
+
+void SmtEngine::finalOptionsAreSet() {
+  if(d_fullyInited) {
+    return;
+  }
+
+  AlwaysAssert( d_propEngine->getAssertionLevel() == 0,
+                "The PropEngine has pushed but the SmtEngine "
+                "hasn't finished initializing!" );
+
+  d_fullyInited = true;
+  d_logic.lock();
 
   d_propEngine->assertFormula(NodeManager::currentNM()->mkConst<bool>(true));
   d_propEngine->assertFormula(NodeManager::currentNM()->mkConst<bool>(false).notNode());
@@ -401,15 +414,12 @@ SmtEngine::~SmtEngine() throw() {
 void SmtEngine::setLogic(const LogicInfo& logic) throw(ModalException) {
   NodeManagerScope nms(d_nodeManager);
 
-  if(d_logicIsSet) {
-    throw ModalException("logic already set");
-  }
-
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << SetBenchmarkLogicCommand(logic.getLogicString());
   }
 
-  setLogicInternal(logic);
+  d_logic = logic;
+  setLogicInternal();
 }
 
 void SmtEngine::setLogic(const std::string& s) throw(ModalException) {
@@ -418,57 +428,63 @@ void SmtEngine::setLogic(const std::string& s) throw(ModalException) {
   setLogic(LogicInfo(s));
 }
 
-void SmtEngine::setLogicInternal(const LogicInfo& logic) throw() {
-  d_logic = 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(AssertionException) {
+  Assert(!d_fullyInited, "setting logic in SmtEngine but the engine has already finished initializing for this run");
+
+  d_logic.lock();
 
   // by default, symmetry breaker is on only for QF_UF
   if(! Options::current()->ufSymmetryBreakerSetByUser) {
-    bool qf_uf = logic.isPure(theory::THEORY_UF) && !logic.isQuantified();
+    bool qf_uf = d_logic.isPure(theory::THEORY_UF) && !d_logic.isQuantified();
     Trace("smt") << "setting uf symmetry breaker to " << qf_uf << std::endl;
     NodeManager::currentNM()->getOptions()->ufSymmetryBreaker = qf_uf;
   }
   // by default, nonclausal simplification is off for QF_SAT
   if(! Options::current()->simplificationModeSetByUser) {
-    bool qf_sat = logic.isPure(theory::THEORY_BOOL) && !logic.isQuantified();
-    Trace("smt") << "setting simplification mode to <" << logic.getLogicString() << "> " << (!qf_sat) << std::endl;
+    bool qf_sat = d_logic.isPure(theory::THEORY_BOOL) && !d_logic.isQuantified();
+    Trace("smt") << "setting simplification mode to <" << d_logic.getLogicString() << "> " << (!qf_sat) << std::endl;
     NodeManager::currentNM()->getOptions()->simplificationMode = (qf_sat ? Options::SIMPLIFICATION_MODE_NONE : Options::SIMPLIFICATION_MODE_BATCH);
   }
 
   // If in arrays, set the UF handler to arrays
-  if(logic.isPure(theory::THEORY_ARRAY) && !logic.isQuantified()) {
+  if(d_logic.isPure(theory::THEORY_ARRAY) && !d_logic.isQuantified()) {
     theory::Theory::setUninterpretedSortOwner(theory::THEORY_ARRAY);
   } else {
     theory::Theory::setUninterpretedSortOwner(theory::THEORY_UF);
   }
   // Turn on ite simplification for QF_LIA and QF_AUFBV
   if(! Options::current()->doITESimpSetByUser) {
-    bool iteSimp = !logic.isQuantified() &&
-      ((logic.isPure(theory::THEORY_ARITH) && logic.isLinear() && !logic.isDifferenceLogic() &&  !logic.areRealsUsed()) ||
-       (logic.isTheoryEnabled(theory::THEORY_ARRAY) && logic.isTheoryEnabled(theory::THEORY_UF) && logic.isTheoryEnabled(theory::THEORY_BV)));
+    bool iteSimp = !d_logic.isQuantified() &&
+      ((d_logic.isPure(theory::THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() &&  !d_logic.areRealsUsed()) ||
+       (d_logic.isTheoryEnabled(theory::THEORY_ARRAY) && d_logic.isTheoryEnabled(theory::THEORY_UF) && d_logic.isTheoryEnabled(theory::THEORY_BV)));
     Trace("smt") << "setting ite simplification to " << iteSimp << std::endl;
     NodeManager::currentNM()->getOptions()->doITESimp = iteSimp;
   }
   // Turn on multiple-pass non-clausal simplification for QF_AUFBV
   if(! Options::current()->repeatSimpSetByUser) {
-    bool repeatSimp = !logic.isQuantified() &&
-      (logic.isTheoryEnabled(theory::THEORY_ARRAY) && logic.isTheoryEnabled(theory::THEORY_UF) && logic.isTheoryEnabled(theory::THEORY_BV));
+    bool repeatSimp = !d_logic.isQuantified() &&
+      (d_logic.isTheoryEnabled(theory::THEORY_ARRAY) && d_logic.isTheoryEnabled(theory::THEORY_UF) && d_logic.isTheoryEnabled(theory::THEORY_BV));
     Trace("smt") << "setting repeat simplification to " << repeatSimp << std::endl;
     NodeManager::currentNM()->getOptions()->repeatSimp = repeatSimp;
   }
   // Turn on unconstrained simplification for all but QF_SAT as long as we are not in incremental solving mode
   if(! Options::current()->unconstrainedSimpSetByUser || Options::current()->incrementalSolving) {
-    bool qf_sat = logic.isPure(theory::THEORY_BOOL) && !logic.isQuantified();
+    bool qf_sat = d_logic.isPure(theory::THEORY_BOOL) && !d_logic.isQuantified();
     bool uncSimp = false && !qf_sat && !Options::current()->incrementalSolving;
     Trace("smt") << "setting unconstrained simplification to " << uncSimp << std::endl;
     NodeManager::currentNM()->getOptions()->unconstrainedSimp = uncSimp;
   }
   // Turn on arith rewrite equalities only for pure arithmetic
   if(! Options::current()->arithRewriteEqSetByUser) {
-    bool arithRewriteEq = logic.isPure(theory::THEORY_ARITH) && !logic.isQuantified();
+    bool arithRewriteEq = d_logic.isPure(theory::THEORY_ARITH) && !d_logic.isQuantified();
     Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq << std::endl;
     NodeManager::currentNM()->getOptions()->arithRewriteEq = arithRewriteEq;
   }
-
 }
 
 void SmtEngine::setInfo(const std::string& key, const SExpr& value)
@@ -496,7 +512,8 @@ void SmtEngine::setInfo(const std::string& key, const SExpr& value)
           throw BadOptionException("argument to (set-info :cvc4-logic ..) must be a string");
         }
         NodeManagerScope nms(d_nodeManager);
-        setLogicInternal(value.getValue());
+        d_logic = value.getValue();
+        setLogicInternal();
         return;
       }
     }
@@ -592,7 +609,7 @@ void SmtEngine::setOption(const std::string& key, const SExpr& value)
   } else {
     // The following options can only be set at the beginning; we throw
     // a ModalException if someone tries.
-    if(d_logicIsSet) {
+    if(d_logic.isLocked()) {
       throw ModalException("logic already set; cannot set options");
     }
 
@@ -761,8 +778,9 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<TNode, Node, TNodeHas
   }
 }
 
-
 void SmtEnginePrivate::removeITEs() {
+  d_smt.finalOptionsAreSet();
+
   Trace("simplify") << "SmtEnginePrivate::removeITEs()" << endl;
 
   // Remove all of the ITE occurrences and normalize
@@ -774,6 +792,7 @@ void SmtEnginePrivate::removeITEs() {
 }
 
 void SmtEnginePrivate::staticLearning() {
+  d_smt.finalOptionsAreSet();
 
   TimerStat::CodeTimer staticLearningTimer(d_smt.d_staticLearningTime);
 
@@ -793,6 +812,7 @@ void SmtEnginePrivate::staticLearning() {
 }
 
 void SmtEnginePrivate::nonClausalSimplify() {
+  d_smt.finalOptionsAreSet();
 
   TimerStat::CodeTimer nonclausalTimer(d_smt.d_nonclausalSimplificationTime);
 
@@ -1072,6 +1092,8 @@ void SmtEnginePrivate::simplifyAssertions()
 }
 
 Result SmtEngine::check() {
+  Assert(d_fullyInited);
+
   Trace("smt") << "SmtEngine::check()" << endl;
 
   // Make sure the prop layer has all of the assertions
@@ -1124,11 +1146,13 @@ Result SmtEngine::check() {
 }
 
 Result SmtEngine::quickCheck() {
+  Assert(d_fullyInited);
   Trace("smt") << "SMT quickCheck()" << endl;
   return Result(Result::VALIDITY_UNKNOWN, Result::REQUIRES_FULL_CHECK);
 }
 
 void SmtEnginePrivate::processAssertions() {
+  Assert(d_smt.d_fullyInited);
 
   Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl;
 
@@ -1252,6 +1276,8 @@ Result SmtEngine::checkSat(const BoolExpr& e) {
 
   NodeManagerScope nms(d_nodeManager);
 
+  finalOptionsAreSet();
+
   Trace("smt") << "SmtEngine::checkSat(" << e << ")" << endl;
 
   if(d_queryMade && !Options::current()->incrementalSolving) {
@@ -1313,6 +1339,8 @@ Result SmtEngine::query(const BoolExpr& e) {
 
   NodeManagerScope nms(d_nodeManager);
 
+  finalOptionsAreSet();
+
   Trace("smt") << "SMT query(" << e << ")" << endl;
 
   if(d_queryMade && !Options::current()->incrementalSolving) {
@@ -1366,6 +1394,7 @@ Result SmtEngine::query(const BoolExpr& e) {
 Result SmtEngine::assertFormula(const BoolExpr& e) {
   Assert(e.getExprManager() == d_exprManager);
   NodeManagerScope nms(d_nodeManager);
+  finalOptionsAreSet();
   Trace("smt") << "SmtEngine::assertFormula(" << e << ")" << endl;
   ensureBoolean(e);
   if(d_assertionList != NULL) {
@@ -1378,6 +1407,7 @@ Result SmtEngine::assertFormula(const BoolExpr& e) {
 Expr SmtEngine::simplify(const Expr& e) {
   Assert(e.getExprManager() == d_exprManager);
   NodeManagerScope nms(d_nodeManager);
+  finalOptionsAreSet();
   if( Options::current()->typeChecking ) {
     e.getType(true);// ensure expr is type-checked at this point
   }
@@ -1435,6 +1465,7 @@ Expr SmtEngine::getValue(const Expr& e)
 
 bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
+  finalOptionsAreSet();
   Type type = e.getType(Options::current()->typeChecking);
   // must be Boolean
   CheckArgument( type.isBoolean(), e,
@@ -1463,6 +1494,7 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
 SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
   Trace("smt") << "SMT getAssignment()" << endl;
   NodeManagerScope nms(d_nodeManager);
+  finalOptionsAreSet();
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << GetAssignmentCommand();
   }
@@ -1519,6 +1551,7 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
 Proof* SmtEngine::getProof() throw(ModalException, AssertionException) {
   Trace("smt") << "SMT getProof()" << endl;
   NodeManagerScope nms(d_nodeManager);
+  finalOptionsAreSet();
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << GetProofCommand();
   }
@@ -1566,6 +1599,7 @@ size_t SmtEngine::getStackLevel() const {
 
 void SmtEngine::push() {
   NodeManagerScope nms(d_nodeManager);
+  finalOptionsAreSet();
   Trace("smt") << "SMT push()" << endl;
   d_private->processAssertions();
   if(Dump.isOn("benchmark")) {
@@ -1589,6 +1623,7 @@ void SmtEngine::push() {
 
 void SmtEngine::pop() {
   NodeManagerScope nms(d_nodeManager);
+  finalOptionsAreSet();
   Trace("smt") << "SMT pop()" << endl;
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << PopCommand();
@@ -1624,6 +1659,7 @@ void SmtEngine::pop() {
 }
 
 void SmtEngine::internalPush() {
+  Assert(d_fullyInited);
   Trace("smt") << "SmtEngine::internalPush()" << endl;
   if(Options::current()->incrementalSolving) {
     d_private->processAssertions();
@@ -1634,6 +1670,7 @@ void SmtEngine::internalPush() {
 }
 
 void SmtEngine::internalPop() {
+  Assert(d_fullyInited);
   Trace("smt") << "SmtEngine::internalPop()" << endl;
   if(Options::current()->incrementalSolving) {
     d_propEngine->pop();