1 files changed, 24 insertions, 14 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");
     }