New LogicInfo functionality.

src/theory/logic_info.{h,cpp} contains the CVC4::LogicInfo class, which keeps
track of which theories are active (which should remain constant throughout
the life of an SmtEngine) and other details (like integers, reals,
linear/nonlinear, etc.).

This class has a default constructor which is the most all-inclusive logic.
Alternatively, this class can be constructed from an SMT-LIB logic string
(the empty string gives the same as "QF_SAT").  Once constructed, theories
can be enabled or disabled, quantifiers flipped on and off, integers flipped
on and off, etc.  At any point an SMT-LIB-like logic string can be extracted.  

The SmtEngine keeps a LogicInfo for itself and shares with the TheoryEngine
(and, in turn, the theories) only a const reference to it.  This ensures that
the logic info doesn't mutate over the course of the run.

As part of this commit, the TheoryEngine's old notion of "active theories"
has been completely removed.  As a result, SMT benchmarks that are incorrectly
tagged with a logic will assert-fail or worse.  (We should probably fail
more gracefully in this case.)  One such example was bug303.smt2,
which used UF reasoning but was tagged QF_LIA.  This has been fixed.

1 files changed, 12 insertions, 12 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 46a9f5855..d5616221d 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -38,11 +38,12 @@ using namespace CVC4;
 using namespace CVC4::theory;
 
 TheoryEngine::TheoryEngine(context::Context* context,
-                           context::UserContext* userContext)
+                           context::UserContext* userContext,
+                           const LogicInfo& logicInfo)
 : d_propEngine(NULL),
   d_context(context),
   d_userContext(userContext),
-  d_activeTheories(context, 0),
+  d_logicInfo(logicInfo),
   d_notify(*this),
   d_sharedTerms(d_notify, context),
   d_ppCache(),
@@ -110,7 +111,7 @@ void TheoryEngine::check(Theory::Effort effort) {
 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 #endif
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
-    if (theory::TheoryTraits<THEORY>::hasCheck && isActive(THEORY)) { \
+    if (theory::TheoryTraits<THEORY>::hasCheck && d_logicInfo.isTheoryEnabled(THEORY)) { \
        reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->check(effort); \
        if (d_inConflict) { \
          break; \
@@ -135,9 +136,9 @@ void TheoryEngine::check(Theory::Effort effort) {
       Debug("theory") << "TheoryEngine::check(" << effort << "): running check" << std::endl;
 
       if (Debug.isOn("theory::assertions")) {
-        for (unsigned theoryId = 0; theoryId < THEORY_LAST; ++ theoryId) {
+        for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
           Theory* theory = d_theoryTable[theoryId];
-          if (theory && Theory::setContains((TheoryId)theoryId, d_activeTheories)) {
+          if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
             Debug("theory::assertions") << "--------------------------------------------" << std::endl;
             Debug("theory::assertions") << "Assertions of " << theory->getId() << ": " << std::endl;
             context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
@@ -248,7 +249,7 @@ void TheoryEngine::combineTheories() {
 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 #endif
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
-  if (theory::TheoryTraits<THEORY>::isParametric && isActive(THEORY)) { \
+  if (theory::TheoryTraits<THEORY>::isParametric && d_logicInfo.isTheoryEnabled(THEORY)) { \
      reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->getCareGraph(careGraph); \
   }
 
@@ -309,7 +310,7 @@ void TheoryEngine::propagate(Theory::Effort effort) {
 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 #endif
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
-  if (theory::TheoryTraits<THEORY>::hasPropagate && isActive(THEORY)) { \
+  if (theory::TheoryTraits<THEORY>::hasPropagate && d_logicInfo.isTheoryEnabled(THEORY)) { \
     reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->propagate(effort); \
   }
 
@@ -447,7 +448,7 @@ void TheoryEngine::notifyRestart() {
 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 #endif
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
-  if (theory::TheoryTraits<THEORY>::hasNotifyRestart && isActive(THEORY)) { \
+  if (theory::TheoryTraits<THEORY>::hasNotifyRestart && d_logicInfo.isTheoryEnabled(THEORY)) { \
     reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->notifyRestart(); \
   }
 
@@ -482,7 +483,7 @@ void TheoryEngine::shutdown() {
   d_hasShutDown = true;
 
   // Shutdown all the theories
-  for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) {
+  for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) {
     if(d_theoryTable[theoryId]) {
       theoryOf(static_cast<TheoryId>(theoryId))->shutdown();
     }
@@ -642,7 +643,6 @@ void TheoryEngine::assertFact(TNode node)
           }
         }
         d_sharedTerms.markNotified(term, theories);
-        markActive(theories);
       }
     }
 
@@ -665,7 +665,7 @@ void TheoryEngine::assertFact(TNode node)
       // TODO: have processSharedLiteral propagate disequalities?
       if (node.getKind() == kind::EQUAL) {
         // Don't have to assert it - this will be taken care of by processSharedLiteral
-        Assert(isActive(theory->getId()));
+        Assert(d_logicInfo.isTheoryEnabled(theory->getId()));
         return;
       }
     }
@@ -678,7 +678,7 @@ void TheoryEngine::assertFact(TNode node)
 
   // Assert the fact to the appropriate theory and mark it active
   theory->assertFact(node, true);
-  markActive(Theory::setInsert(theory->getId()));
+  Assert(d_logicInfo.isTheoryEnabled(theory->getId()));
 }
 
 void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {