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

1 files changed, 17 insertions, 0 deletions

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,