Standardize SMT-LIBv2 set of logics to use LogicInfo.

Previously, SMT-LIB logics were treated specially, as in SMT-LIB v1.2.
This led to inconsistencies---such as nonstandard logics like "QF_LIRA"
being accepted in set-logic but not providing the "Real" sort.  Now,
the LogicInfo is used and queried, so nonstandard logics should work
fine and declare the correct symbols.  SMT-LIB v1.2, unfortunately,
can't take advantage of this fully since symbols like "Array" have
substantially different meanings in different logics.

1 files changed, 16 insertions, 116 deletions

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index a7f7796cd..a4623bdfc 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -138,135 +138,35 @@ bool Smt2::logicIsSet() {
 
 void Smt2::setLogic(const std::string& name) {
   d_logicSet = true;
-  d_logic = Smt1::toLogic(name);
+  d_logic = name;
 
   // Core theory belongs to every logic
   addTheory(THEORY_CORE);
 
-  switch(d_logic) {
-  case Smt1::QF_SAT:
-    /* No extra symbols necessary */
-    break;
-
-  case Smt1::QF_AX:
-    addTheory(THEORY_ARRAYS);
-    break;
-
-  case Smt1::QF_IDL:
-  case Smt1::QF_LIA:
-  case Smt1::QF_NIA:
-    addTheory(THEORY_INTS);
-    break;
-
-  case Smt1::QF_RDL:
-  case Smt1::QF_LRA:
-  case Smt1::QF_NRA:
-    addTheory(THEORY_REALS);
-    break;
-
-  case Smt1::QF_UF:
-    addOperator(kind::APPLY_UF);
-    break;
-
-  case Smt1::QF_UFIDL:
-  case Smt1::QF_UFLIA:
-  case Smt1::QF_UFNIA:// nonstandard logic
-    addTheory(THEORY_INTS);
-    addOperator(kind::APPLY_UF);
-    break;
-
-  case Smt1::QF_UFLRA:
-  case Smt1::QF_UFNRA:
-    addTheory(THEORY_REALS);
-    addOperator(kind::APPLY_UF);
-    break;
-
-  case Smt1::QF_UFLIRA:// nonstandard logic
-  case Smt1::QF_UFNIRA:// nonstandard logic
-    addOperator(kind::APPLY_UF);
-    addTheory(THEORY_INTS);
-    addTheory(THEORY_REALS);
-    break;
-
-  case Smt1::QF_BV:
-    addTheory(THEORY_BITVECTORS);
-    break;
-
-  case Smt1::QF_ABV:
-    addTheory(THEORY_ARRAYS);
-    addTheory(THEORY_BITVECTORS);
-    break;
-
-  case Smt1::QF_UFBV:
-    addOperator(kind::APPLY_UF);
-    addTheory(THEORY_BITVECTORS);
-    break;
-
-  case Smt1::QF_AUFBV:
+  if(d_logic.isTheoryEnabled(theory::THEORY_UF)) {
     addOperator(kind::APPLY_UF);
-    addTheory(THEORY_ARRAYS);
-    addTheory(THEORY_BITVECTORS);
-    break;
-
-  case Smt1::QF_AUFBVLIA:
-    addOperator(kind::APPLY_UF);
-    addTheory(THEORY_ARRAYS);
-    addTheory(THEORY_BITVECTORS);
-    addTheory(THEORY_INTS);
-    break;
+  }
 
-  case Smt1::QF_AUFBVLRA:
-    addOperator(kind::APPLY_UF);
-    addTheory(THEORY_ARRAYS);
-    addTheory(THEORY_BITVECTORS);
-    addTheory(THEORY_REALS);
-    break;
+  if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) {
+    if(d_logic.areIntegersUsed()) {
+      addTheory(THEORY_INTS);
+    }
 
-  case Smt1::QF_AUFLIA:
-    addTheory(THEORY_ARRAYS);
-    addOperator(kind::APPLY_UF);
-    addTheory(THEORY_INTS);
-    break;
+    if(d_logic.areRealsUsed()) {
+      addTheory(THEORY_REALS);
+    }
+  }
 
-  case Smt1::QF_AUFLIRA:
+  if(d_logic.isTheoryEnabled(theory::THEORY_ARRAY)) {
     addTheory(THEORY_ARRAYS);
-    addOperator(kind::APPLY_UF);
-    addTheory(THEORY_INTS);
-    addTheory(THEORY_REALS);
-    break;
+  }
 
-  case Smt1::ALL_SUPPORTED:
-    addTheory(THEORY_QUANTIFIERS);
-    /* fall through */
-  case Smt1::QF_ALL_SUPPORTED:
-    addTheory(THEORY_ARRAYS);
-    addOperator(kind::APPLY_UF);
-    addTheory(THEORY_INTS);
-    addTheory(THEORY_REALS);
+  if(d_logic.isTheoryEnabled(theory::THEORY_BV)) {
     addTheory(THEORY_BITVECTORS);
-    break;
+  }
 
-  case Smt1::AUFLIA:
-  case Smt1::AUFLIRA:
-  case Smt1::AUFNIRA:
-  case Smt1::LRA:
-  case Smt1::UFNIA:
-  case Smt1::UFNIRA:
-  case Smt1::UFLRA:
-    if(d_logic != Smt1::AUFLIA && d_logic != Smt1::UFNIA) {
-      addTheory(THEORY_REALS);
-    }
-    if(d_logic != Smt1::LRA) {
-      addOperator(kind::APPLY_UF);
-      if(d_logic != Smt1::UFLRA) {
-        addTheory(THEORY_INTS);
-        if(d_logic != Smt1::UFNIA && d_logic != Smt1::UFNIRA) {
-          addTheory(THEORY_ARRAYS);
-        }
-      }
-    }
+  if(d_logic.isQuantified()) {
     addTheory(THEORY_QUANTIFIERS);
-    break;
   }
 }/* Smt2::setLogic() */