The SmtEngine now ensures that setLogicInternal() is called even if there is no expli...

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).

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 1a85f45c33ed98972a359edb6f960208d824e49d..05fed15ea20ed2dae1941e6f8541b4f2fad12c3b 100644 (file)
--- 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 b82d3a01c82a4a168ee5f2bb17cf6ff8270c7f64..1d550cd7ef917f3984da057dd8e8f628913e2e7a 100644 (file)
--- 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 c55a5e4309dbc5593f2e55c91e6018e0c7eca039..9bd85d7bc3dc2a22b8f792b8c9b2dc5aadcf63f5 100644 (file)
--- 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 90b9ac7748d5a92535978ba602519a346f851845..32e72f40a7ca5d79315cf3b7cf96e09b6cb3ea43 100644 (file)
--- 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 7fa6e157fc77686b2df6df942d5fa78a1dd194ee..36b71e931864cfa6681097fb6fdf191cbfbad0f6 100644 (file)
--- 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 069f99d0bbf9baba86f1a11581ccf317a5691dad..a2f61f5d2460aa67bf58ad7853a3eb4c4086c267 100644 (file)
--- 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() {