The SmtEngine now ensures that setLogicInternal() is called even if there is no explicit setLogic(). This is important for the CVC language, where the parser doesn't ensure that setLogic() is called, and for API uses. setLogicInternal() should be called in order to properly set up heuristics, even if the logic is just ALL_SUPPORTED.

This means that the CVC language can now take advantage of statistics.

Also added the ability to set the logic from CVC presentation language via (e.g.)
  OPTION "logic" "QF_UFLIA";

Disabled the justification decision heuristic for ALL_SUPPORTED, as it interferes with incrementality.  Kshitij may have a fix (I warned him about this commit).

6 files changed, 128 insertions, 41 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 1a85f45c3..05fed15ea 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -610,7 +610,12 @@ mainCommand[CVC4::Command*& cmd]
   | OPTION_TOK
     ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
     symbolicExpr[sexpr]
-    { cmd = new SetOptionCommand(s, sexpr); }
+    { if(s == "logic") {
+        cmd = new SetBenchmarkLogicCommand(sexpr.getValue());
+      } else {
+        cmd = new SetOptionCommand(s, sexpr);
+      }
+    }
 
     /* push / pop */
   | PUSH_TOK ( k=numeral { cmd = REPEAT_COMMAND(k, PushCommand()); }
diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h
index b82d3a01c..1d550cd7e 100644
--- a/src/parser/smt/smt.h
+++ b/src/parser/smt/smt.h
@@ -122,4 +122,4 @@ private:
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__PARSER__SMT_INPUT_H */
+#endif /* __CVC4__PARSER__SMT_H */
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index c55a5e430..9bd85d7bc 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -96,4 +96,4 @@ private:
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__PARSER__SMT2_INPUT_H */
+#endif /* __CVC4__PARSER__SMT2_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 90b9ac774..32e72f40a 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -351,6 +351,11 @@ void SmtEngine::finalOptionsAreSet() {
     return;
   }
 
+  if(! d_logic.isLocked()) {
+    // ensure that our heuristics are properly set up
+    setLogicInternal();
+  }
+
   // finish initalization, creat the prop engine, etc.
   finishInit();
 
@@ -359,7 +364,7 @@ void SmtEngine::finalOptionsAreSet() {
                 "hasn't finished initializing!" );
 
   d_fullyInited = true;
-  d_logic.lock();
+  Assert(d_logic.isLocked());
 
   d_propEngine->assertFormula(NodeManager::currentNM()->mkConst<bool>(true));
   d_propEngine->assertFormula(NodeManager::currentNM()->mkConst<bool>(false).notNode());
@@ -557,47 +562,55 @@ void SmtEngine::setLogicInternal() throw(AssertionException) {
   }
   // Turn on justification heuristic of the decision engine for QF_BV and QF_AUFBV
   // and also use it in stop-only mode for QF_AUFLIA, QF_LRA and Quantifiers
+  // BUT use neither in ALL_SUPPORTED mode (since it doesn't yet work well
+  // with incrementality)
   if(!options::decisionMode.wasSetByUser()) {
     decision::DecisionMode decMode =
-      //QF_BV
-      (not d_logic.isQuantified() &&
-        d_logic.isPure(THEORY_BV)
-        ) ||
-      //QF_AUFBV
-      (not d_logic.isQuantified() &&
-       d_logic.isTheoryEnabled(THEORY_ARRAY) &&
-       d_logic.isTheoryEnabled(THEORY_UF) &&
-       d_logic.isTheoryEnabled(THEORY_BV)
-       ) ||
-      //QF_AUFLIA (and may be ends up enabling QF_AUFLRA?)
-      (not d_logic.isQuantified() &&
-       d_logic.isTheoryEnabled(THEORY_ARRAY) &&
-       d_logic.isTheoryEnabled(THEORY_UF) &&
-       d_logic.isTheoryEnabled(THEORY_ARITH)
-       ) ||
-      // QF_LRA
-      (not d_logic.isQuantified() &&
-       d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() &&  !d_logic.areIntegersUsed()
-       ) ||
-      // Quantifiers
-      d_logic.isQuantified()
-      ? decision::DECISION_STRATEGY_JUSTIFICATION
-      : decision::DECISION_STRATEGY_INTERNAL;
+      // ALL_SUPPORTED
+      d_logic.hasEverything() ? decision::DECISION_STRATEGY_INTERNAL :
+      ( // QF_BV
+        (not d_logic.isQuantified() &&
+          d_logic.isPure(THEORY_BV)
+          ) ||
+        // QF_AUFBV
+        (not d_logic.isQuantified() &&
+         d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+         d_logic.isTheoryEnabled(THEORY_UF) &&
+         d_logic.isTheoryEnabled(THEORY_BV)
+         ) ||
+        // QF_AUFLIA (and may be ends up enabling QF_AUFLRA?)
+        (not d_logic.isQuantified() &&
+         d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+         d_logic.isTheoryEnabled(THEORY_UF) &&
+         d_logic.isTheoryEnabled(THEORY_ARITH)
+         ) ||
+        // QF_LRA
+        (not d_logic.isQuantified() &&
+         d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() &&  !d_logic.areIntegersUsed()
+         ) ||
+        // Quantifiers
+        d_logic.isQuantified()
+        ? decision::DECISION_STRATEGY_JUSTIFICATION
+        : decision::DECISION_STRATEGY_INTERNAL
+      );
 
     bool stoponly =
-      // QF_AUFLIA
-      (not d_logic.isQuantified() &&
-       d_logic.isTheoryEnabled(THEORY_ARRAY) &&
-       d_logic.isTheoryEnabled(THEORY_UF) &&
-       d_logic.isTheoryEnabled(THEORY_ARITH)
-       ) ||
-      // QF_LRA
-      (not d_logic.isQuantified() &&
-       d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() &&  !d_logic.areIntegersUsed()
-       ) ||
-      // Quantifiers
-      d_logic.isQuantified()
-      ? true : false;
+      // ALL_SUPPORTED
+      d_logic.hasEverything() ? false :
+      ( // QF_AUFLIA
+        (not d_logic.isQuantified() &&
+         d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+         d_logic.isTheoryEnabled(THEORY_UF) &&
+         d_logic.isTheoryEnabled(THEORY_ARITH)
+         ) ||
+        // QF_LRA
+        (not d_logic.isQuantified() &&
+         d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() &&  !d_logic.areIntegersUsed()
+         ) ||
+        // Quantifiers
+        d_logic.isQuantified()
+        ? true : false
+      );
 
     Trace("smt") << "setting decision mode to " << decMode << std::endl;
     options::decisionMode.set(decMode);
diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h
index 7fa6e157f..36b71e931 100644
--- a/src/theory/logic_info.h
+++ b/src/theory/logic_info.h
@@ -108,6 +108,7 @@ public:
     Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
     return d_sharingTheories > 1;
   }
+
   /** Is the given theory module active in this logic? */
   bool isTheoryEnabled(theory::TheoryId theory) const {
     Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
@@ -120,6 +121,22 @@ public:
     return isTheoryEnabled(theory::THEORY_QUANTIFIERS) || isTheoryEnabled(theory::THEORY_REWRITERULES);
   }
 
+  /** Is this the all-inclusive logic? */
+  bool hasEverything() const {
+    Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+    LogicInfo everything;
+    everything.lock();
+    return *this == everything;
+  }
+
+  /** Is this the all-exclusive logic?  (Here, that means propositional logic) */
+  bool hasNothing() const {
+    Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+    LogicInfo nothing("");
+    nothing.lock();
+    return *this == nothing;
+  }
+
   /**
    * Is this a pure logic (only one "true" background theory).  Quantifiers
    * can exist in such logics though; to test for quantifier-free purity,
diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h
index 069f99d0b..a2f61f5d2 100644
--- a/test/unit/theory/logic_info_white.h
+++ b/test/unit/theory/logic_info_white.h
@@ -36,6 +36,8 @@ public:
     TS_ASSERT( !info.isSharingEnabled() );
     TS_ASSERT( info.isPure( THEORY_BOOL ) );
     TS_ASSERT( !info.isQuantified() );
+    TS_ASSERT( !info.hasEverything() );
+    TS_ASSERT( info.hasNothing() );
 
     info = LogicInfo("AUFLIA");
     TS_ASSERT( !info.isPure( THEORY_BOOL ) );
@@ -51,6 +53,8 @@ public:
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( !info.areRealsUsed() );
+    TS_ASSERT( !info.hasEverything() );
+    TS_ASSERT( !info.hasNothing() );
 
     info = LogicInfo("AUFLIRA");
     TS_ASSERT( !info.isPure( THEORY_BOOL ) );
@@ -66,6 +70,8 @@ public:
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areRealsUsed() );
+    TS_ASSERT( !info.hasEverything() );
+    TS_ASSERT( !info.hasNothing() );
 
     info = LogicInfo("AUFNIRA");
     TS_ASSERT( !info.isPure( THEORY_BOOL ) );
@@ -81,6 +87,8 @@ public:
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areRealsUsed() );
+    TS_ASSERT( !info.hasEverything() );
+    TS_ASSERT( !info.hasNothing() );
 
     info = LogicInfo("LRA");
     TS_ASSERT( !info.isPure( THEORY_BOOL ) );
@@ -97,6 +105,8 @@ public:
     TS_ASSERT( !info.areIntegersUsed() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areRealsUsed() );
+    TS_ASSERT( !info.hasEverything() );
+    TS_ASSERT( !info.hasNothing() );
 
     info = LogicInfo("QF_ABV");
     TS_ASSERT( !info.isPure( THEORY_BOOL ) );
@@ -109,6 +119,8 @@ public:
     TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+    TS_ASSERT( !info.hasEverything() );
+    TS_ASSERT( !info.hasNothing() );
 
     info = LogicInfo("QF_AUFBV");
     TS_ASSERT( !info.isQuantified() );
@@ -120,6 +132,8 @@ public:
     TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+    TS_ASSERT( !info.hasEverything() );
+    TS_ASSERT( !info.hasNothing() );
 
     info = LogicInfo("QF_AUFLIA");
     TS_ASSERT( !info.isQuantified() );
@@ -135,6 +149,8 @@ public:
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( !info.areRealsUsed() );
+    TS_ASSERT( !info.hasEverything() );
+    TS_ASSERT( !info.hasNothing() );
 
     info = LogicInfo("QF_AX");
     TS_ASSERT( !info.isQuantified() );
@@ -146,6 +162,8 @@ public:
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+    TS_ASSERT( !info.hasEverything() );
+    TS_ASSERT( !info.hasNothing() );
 
     info = LogicInfo("QF_BV");
     TS_ASSERT( !info.isQuantified() );
@@ -157,6 +175,8 @@ public:
     TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+    TS_ASSERT( !info.hasEverything() );
+    TS_ASSERT( !info.hasNothing() );
 
     info = LogicInfo("QF_IDL");
     TS_ASSERT( !info.isQuantified() );
@@ -172,6 +192,8 @@ public:
     TS_ASSERT( info.isDifferenceLogic() );
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.areRealsUsed() );
+    TS_ASSERT( !info.hasEverything() );
+    TS_ASSERT( !info.hasNothing() );
 
     info = LogicInfo("QF_LIA");
     TS_ASSERT( !info.isQuantified() );
@@ -187,6 +209,8 @@ public:
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.areRealsUsed() );
+    TS_ASSERT( !info.hasEverything() );
+    TS_ASSERT( !info.hasNothing() );
 
     info = LogicInfo("QF_LRA");
     TS_ASSERT( !info.isQuantified() );
@@ -202,6 +226,8 @@ public:
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( !info.areIntegersUsed() );
     TS_ASSERT( info.areRealsUsed() );
+    TS_ASSERT( !info.hasEverything() );
+    TS_ASSERT( !info.hasNothing() );
 
     info = LogicInfo("QF_NIA");
     TS_ASSERT( !info.isQuantified() );
@@ -217,6 +243,8 @@ public:
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.areRealsUsed() );
+    TS_ASSERT( !info.hasEverything() );
+    TS_ASSERT( !info.hasNothing() );
 
     info = LogicInfo("QF_NRA");
     TS_ASSERT( !info.isQuantified() );
@@ -232,6 +260,8 @@ public:
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( !info.areIntegersUsed() );
     TS_ASSERT( info.areRealsUsed() );
+    TS_ASSERT( !info.hasEverything() );
+    TS_ASSERT( !info.hasNothing() );
 
     info = LogicInfo("QF_RDL");
     TS_ASSERT( !info.isQuantified() );
@@ -247,6 +277,8 @@ public:
     TS_ASSERT( info.isDifferenceLogic() );
     TS_ASSERT( !info.areIntegersUsed() );
     TS_ASSERT( info.areRealsUsed() );
+    TS_ASSERT( !info.hasEverything() );
+    TS_ASSERT( !info.hasNothing() );
 
     info = LogicInfo("QF_UF");
     TS_ASSERT( !info.isPure( THEORY_BOOL ) );
@@ -259,6 +291,8 @@ public:
     TS_ASSERT( info.isPure( THEORY_UF ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+    TS_ASSERT( !info.hasEverything() );
+    TS_ASSERT( !info.hasNothing() );
 
     info = LogicInfo("QF_UFBV");
     TS_ASSERT( !info.isQuantified() );
@@ -271,6 +305,8 @@ public:
     TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+    TS_ASSERT( !info.hasEverything() );
+    TS_ASSERT( !info.hasNothing() );
 
     info = LogicInfo("QF_UFIDL");
     TS_ASSERT( !info.isQuantified() );
@@ -286,6 +322,8 @@ public:
     TS_ASSERT( info.isDifferenceLogic() );
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.areRealsUsed() );
+    TS_ASSERT( !info.hasEverything() );
+    TS_ASSERT( !info.hasNothing() );
 
     info = LogicInfo("QF_UFLIA");
     TS_ASSERT( !info.isQuantified() );
@@ -301,6 +339,8 @@ public:
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.areRealsUsed() );
+    TS_ASSERT( !info.hasEverything() );
+    TS_ASSERT( !info.hasNothing() );
 
     info = LogicInfo("QF_UFLRA");
     TS_ASSERT( !info.isQuantified() );
@@ -315,6 +355,8 @@ public:
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( !info.areIntegersUsed() );
     TS_ASSERT( info.areRealsUsed() );
+    TS_ASSERT( !info.hasEverything() );
+    TS_ASSERT( !info.hasNothing() );
 
     info = LogicInfo("QF_UFNRA");
     TS_ASSERT( !info.isQuantified() );
@@ -330,6 +372,8 @@ public:
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( !info.areIntegersUsed() );
     TS_ASSERT( info.areRealsUsed() );
+    TS_ASSERT( !info.hasEverything() );
+    TS_ASSERT( !info.hasNothing() );
 
     info = LogicInfo("UFLRA");
     TS_ASSERT( info.isQuantified() );
@@ -345,6 +389,8 @@ public:
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( !info.areIntegersUsed() );
     TS_ASSERT( info.areRealsUsed() );
+    TS_ASSERT( !info.hasEverything() );
+    TS_ASSERT( !info.hasNothing() );
 
     info = LogicInfo("UFNIA");
     TS_ASSERT( info.isQuantified() );
@@ -360,6 +406,8 @@ public:
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.areRealsUsed() );
+    TS_ASSERT( !info.hasEverything() );
+    TS_ASSERT( !info.hasNothing() );
 
     info = LogicInfo("QF_ALL_SUPPORTED");
     TS_ASSERT( info.isLocked() );
@@ -376,6 +424,8 @@ public:
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areRealsUsed() );
+    TS_ASSERT( !info.hasEverything() );
+    TS_ASSERT( !info.hasNothing() );
 
     info = LogicInfo("ALL_SUPPORTED");
     TS_ASSERT( info.isLocked() );
@@ -392,6 +442,8 @@ public:
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areRealsUsed() );
+    TS_ASSERT( info.hasEverything() );
+    TS_ASSERT( !info.hasNothing() );
   }
 
   void testDefaultLogic() {