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.

2 files changed, 37 insertions, 17 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c95b9d197..4b3410cf7 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -57,6 +57,7 @@
 #include "theory/bv/theory_bv.h"
 #include "theory/datatypes/theory_datatypes.h"
 #include "theory/theory_traits.h"
+#include "theory/logic_info.h"
 #include "util/ite_removal.h"
 
 using namespace std;
@@ -230,7 +231,8 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   d_definedFunctions(NULL),
   d_assertionList(NULL),
   d_assignments(NULL),
-  d_logic(""),
+  d_logic(),
+  d_logicIsSet(false),
   d_problemExtended(false),
   d_queryMade(false),
   d_needPostsolve(false),
@@ -256,7 +258,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
 
   // We have mutual dependency here, so we add the prop engine to the theory
   // engine later (it is non-essential there)
-  d_theoryEngine = new TheoryEngine(d_context, d_userContext);
+  d_theoryEngine = new TheoryEngine(d_context, d_userContext, const_cast<const LogicInfo&>(d_logic));
 
   // Add the theories
 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
@@ -356,36 +358,44 @@ SmtEngine::~SmtEngine() throw() {
   }
 }
 
-void SmtEngine::setLogic(const std::string& s) throw(ModalException) {
+void SmtEngine::setLogic(const LogicInfo& logic) throw(ModalException) {
   NodeManagerScope nms(d_nodeManager);
 
-  if(d_logic != "") {
+  if(d_logicIsSet) {
     throw ModalException("logic already set");
   }
 
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << SetBenchmarkLogicCommand(s);
+    Dump("benchmark") << SetBenchmarkLogicCommand(logic.getLogicString());
   }
 
-  setLogicInternal(s);
+  setLogicInternal(logic);
+}
+
+void SmtEngine::setLogic(const std::string& s) throw(ModalException) {
+  NodeManagerScope nms(d_nodeManager);
+
+  setLogic(LogicInfo(s));
 }
 
-void SmtEngine::setLogicInternal(const std::string& s) throw() {
-  d_logic = s;
+void SmtEngine::setLogicInternal(const LogicInfo& logic) throw() {
+  d_logic = logic;
 
   // by default, symmetry breaker is on only for QF_UF
   if(! Options::current()->ufSymmetryBreakerSetByUser) {
-    Trace("smt") << "setting uf symmetry breaker to " << (s == "QF_UF") << std::endl;
-    NodeManager::currentNM()->getOptions()->ufSymmetryBreaker = (s == "QF_UF");
+    bool qf_uf = logic.isPure(theory::THEORY_UF) && !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) {
-    Trace("smt") << "setting simplification mode to <" << s << "> " << (s != "QF_SAT") << std::endl;
-    NodeManager::currentNM()->getOptions()->simplificationMode = (s == "QF_SAT" ? Options::SIMPLIFICATION_MODE_NONE : Options::SIMPLIFICATION_MODE_BATCH);
+    bool qf_sat = logic.isPure(theory::THEORY_BOOL) && !logic.isQuantified();
+    Trace("smt") << "setting simplification mode to <" << 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(s == "QF_AX") {
+  if(logic.isPure(theory::THEORY_ARRAY) && !logic.isQuantified()) {
     theory::Theory::setUninterpretedSortOwner(theory::THEORY_ARRAY);
   } else {
     theory::Theory::setUninterpretedSortOwner(theory::THEORY_UF);
@@ -513,7 +523,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_logic != "") {
+    if(d_logicIsSet) {
       throw ModalException("logic already set; cannot set options");
     }
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 7feaa7e61..43d3e1125 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -37,6 +37,7 @@
 #include "util/result.h"
 #include "util/sexpr.h"
 #include "util/stats.h"
+#include "theory/logic_info.h"
 
 // In terms of abstraction, this is below (and provides services to)
 // ValidityChecker and above (and requires the services of)
@@ -131,7 +132,12 @@ class CVC4_PUBLIC SmtEngine {
   /**
    * The logic we're in.
    */
-  std::string d_logic;
+  LogicInfo d_logic;
+
+  /**
+   * Whether the logic has been set yet.
+   */
+  bool d_logicIsSet;
 
   /**
    * Whether or not we have added any assertions/declarations/definitions
@@ -212,7 +218,7 @@ class CVC4_PUBLIC SmtEngine {
   /**
    * Internally handle the setting of a logic.
    */
-  void setLogicInternal(const std::string& logic) throw();
+  void setLogicInternal(const LogicInfo& logic) throw();
 
   friend class ::CVC4::smt::SmtEnginePrivate;
 
@@ -226,7 +232,6 @@ class CVC4_PUBLIC SmtEngine {
   /** how the SMT engine got the answer -- SAT solver or DE */
   BackedStat<std::string> d_statResultSource;
 
-
 public:
 
   /**
@@ -245,6 +250,11 @@ public:
   void setLogic(const std::string& logic) throw(ModalException);
 
   /**
+   * Set the logic of the script.
+   */
+  void setLogic(const LogicInfo& logic) throw(ModalException);
+
+  /**
    * Set information about the script executing.
    */
   void setInfo(const std::string& key, const SExpr& value)