Initializing Smt1::d_logic in all cases. This was resolved by extending the Logic enum with an UNSET value. (#1329)

2 files changed, 214 insertions, 217 deletions

diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp
index 9a6d880e9..c3365eb13 100644
--- a/src/parser/smt1/smt1.cpp
+++ b/src/parser/smt1/smt1.cpp
@@ -69,10 +69,9 @@ Smt1::Logic Smt1::toLogic(const std::string& name) {
   return logicMap[name];
 }
 
-Smt1::Smt1(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
-  Parser(exprManager,input,strictMode,parseOnly),
-  d_logicSet(false) {
-
+Smt1::Smt1(ExprManager* exprManager, Input* input, bool strictMode,
+           bool parseOnly)
+    : Parser(exprManager, input, strictMode, parseOnly), d_logic(UNSET) {
   // Boolean symbols are always defined
   addOperator(kind::AND);
   addOperator(kind::EQUAL);
@@ -170,167 +169,165 @@ void Smt1::addTheory(Theory theory) {
   }
 }
 
-bool Smt1::logicIsSet() {
-  return d_logicSet;
-}
+bool Smt1::logicIsSet() { return d_logic != UNSET; }
 
 void Smt1::setLogic(const std::string& name) {
-  d_logicSet = true;
-  if(logicIsForced()) {
-    d_logic = toLogic(getForcedLogic());
-  } else {
-    d_logic = toLogic(name);
-  }
+  d_logic = toLogic(logicIsForced() ? getForcedLogic() : name);
 
   switch(d_logic) {
-  case QF_S:
-    throw ParserException("Strings theory unsupported in SMT-LIBv1 front-end; try SMT-LIBv2.");
-    break;
-
-  case QF_AX:
-    addTheory(THEORY_ARRAYS_EX);
-    break;
-
-  case QF_IDL:
-  case QF_LIA:
-  case QF_NIA:
-    addTheory(THEORY_INTS);
-    break;
-
-  case QF_RDL:
-  case QF_LRA:
-  case QF_NRA:
-    addTheory(THEORY_REALS);
-    break;
-
-  case QF_SAT:
-    /* no extra symbols needed */
-    break;
-  case SAT:
-    addTheory(THEORY_QUANTIFIERS);
-    break;
-
-  case QF_UFIDL:
-  case QF_UFLIA:
-  case QF_UFNIA:// nonstandard logic
-    addTheory(THEORY_INTS);
-    addOperator(kind::APPLY_UF);
-    break;
-
-  case QF_UFLRA:
-  case QF_UFNRA:
-    addTheory(THEORY_REALS);
-    addOperator(kind::APPLY_UF);
-    break;
-
-  case QF_UFLIRA:// nonstandard logic
-  case QF_UFNIRA:// nonstandard logic
-    addTheory(THEORY_INTS);
-    addTheory(THEORY_REALS);
-    addOperator(kind::APPLY_UF);
-    break;
-
-  case QF_UF:
-    addTheory(THEORY_EMPTY);
-    addOperator(kind::APPLY_UF);
-    break;
-
-  case QF_BV:
-    addTheory(THEORY_BITVECTORS);
-    break;
-
-  case QF_ABV:// nonstandard logic
-    addTheory(THEORY_BITVECTOR_ARRAYS_EX);
-    addTheory(THEORY_BITVECTORS);
-    break;
-
-  case QF_UFBV:
-    addOperator(kind::APPLY_UF);
-    addTheory(THEORY_BITVECTORS);
-    break;
-
-  case QF_AUFBV:
-    addOperator(kind::APPLY_UF);
-    addTheory(THEORY_BITVECTOR_ARRAYS_EX);
-    addTheory(THEORY_BITVECTORS);
-    break;
-
-  case QF_AUFBVLIA:// nonstandard logic
-    addOperator(kind::APPLY_UF);
-    addTheory(THEORY_ARRAYS_EX);
-    addTheory(THEORY_BITVECTORS);
-    addTheory(THEORY_INTS);
-    break;
-
-  case QF_AUFBVLRA:// nonstandard logic
-    addOperator(kind::APPLY_UF);
-    addTheory(THEORY_ARRAYS_EX);
-    addTheory(THEORY_BITVECTORS);
-    addTheory(THEORY_REALS);
-    break;
-
-  case QF_AUFLIA:
-    addTheory(THEORY_INT_ARRAYS_EX);// nonstandard logic
-    addOperator(kind::APPLY_UF);
-    addTheory(THEORY_INTS);
-    break;
-
-  case QF_AUFLIRA:// nonstandard logic
-    addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX);
-    addOperator(kind::APPLY_UF);
-    addTheory(THEORY_INTS);
-    addTheory(THEORY_REALS);
-    break;
-
-  case ALL_SUPPORTED:// nonstandard logic
-    addTheory(THEORY_QUANTIFIERS);
-    /* fall through */
-  case QF_ALL_SUPPORTED:// nonstandard logic
-    addTheory(THEORY_ARRAYS_EX);
-    addOperator(kind::APPLY_UF);
-    addTheory(THEORY_INTS);
-    addTheory(THEORY_REALS);
-    addTheory(THEORY_BITVECTORS);
-    break;
-
-  case AUFLIA:
-    addOperator(kind::APPLY_UF);
-    addTheory(THEORY_INTS);
-    addTheory(THEORY_INT_ARRAYS_EX);
-    addTheory(THEORY_QUANTIFIERS);
-    break;
-
-  case AUFLIRA:
-  case AUFNIRA:
-    addOperator(kind::APPLY_UF);
-    addTheory(THEORY_INTS);
-    addTheory(THEORY_REALS);
-    addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX);
-    addTheory(THEORY_QUANTIFIERS);
-    break;
-
-  case LRA:
-    addTheory(THEORY_REALS);
-    addTheory(THEORY_QUANTIFIERS);
-    break;
-
-  case UFNIA:
-    addOperator(kind::APPLY_UF);
-    addTheory(THEORY_INTS);
-    addTheory(THEORY_QUANTIFIERS);
-    break;
-  case UFNIRA:
-    addOperator(kind::APPLY_UF);
-    addTheory(THEORY_INTS);
-    addTheory(THEORY_REALS);
-    addTheory(THEORY_QUANTIFIERS);
-    break;
-
-  case UFLRA:
-    addOperator(kind::APPLY_UF);
-    addTheory(THEORY_REALS);
-    addTheory(THEORY_QUANTIFIERS);
-    break;
+  case UNSET:
+      throw ParserException("Logic cannot remain UNSET after being set.");
+      break;
+
+    case QF_S:
+      throw ParserException(
+          "Strings theory unsupported in SMT-LIBv1 front-end; try SMT-LIBv2.");
+      break;
+
+    case QF_AX:
+      addTheory(THEORY_ARRAYS_EX);
+      break;
+
+    case QF_IDL:
+    case QF_LIA:
+    case QF_NIA:
+      addTheory(THEORY_INTS);
+      break;
+
+    case QF_RDL:
+    case QF_LRA:
+    case QF_NRA:
+      addTheory(THEORY_REALS);
+      break;
+
+    case QF_SAT:
+      /* no extra symbols needed */
+      break;
+    case SAT:
+      addTheory(THEORY_QUANTIFIERS);
+      break;
+
+    case QF_UFIDL:
+    case QF_UFLIA:
+    case QF_UFNIA:  // nonstandard logic
+      addTheory(THEORY_INTS);
+      addOperator(kind::APPLY_UF);
+      break;
+
+    case QF_UFLRA:
+    case QF_UFNRA:
+      addTheory(THEORY_REALS);
+      addOperator(kind::APPLY_UF);
+      break;
+
+    case QF_UFLIRA:  // nonstandard logic
+    case QF_UFNIRA:  // nonstandard logic
+      addTheory(THEORY_INTS);
+      addTheory(THEORY_REALS);
+      addOperator(kind::APPLY_UF);
+      break;
+
+    case QF_UF:
+      addTheory(THEORY_EMPTY);
+      addOperator(kind::APPLY_UF);
+      break;
+
+    case QF_BV:
+      addTheory(THEORY_BITVECTORS);
+      break;
+
+    case QF_ABV:  // nonstandard logic
+      addTheory(THEORY_BITVECTOR_ARRAYS_EX);
+      addTheory(THEORY_BITVECTORS);
+      break;
+
+    case QF_UFBV:
+      addOperator(kind::APPLY_UF);
+      addTheory(THEORY_BITVECTORS);
+      break;
+
+    case QF_AUFBV:
+      addOperator(kind::APPLY_UF);
+      addTheory(THEORY_BITVECTOR_ARRAYS_EX);
+      addTheory(THEORY_BITVECTORS);
+      break;
+
+    case QF_AUFBVLIA:  // nonstandard logic
+      addOperator(kind::APPLY_UF);
+      addTheory(THEORY_ARRAYS_EX);
+      addTheory(THEORY_BITVECTORS);
+      addTheory(THEORY_INTS);
+      break;
+
+    case QF_AUFBVLRA:  // nonstandard logic
+      addOperator(kind::APPLY_UF);
+      addTheory(THEORY_ARRAYS_EX);
+      addTheory(THEORY_BITVECTORS);
+      addTheory(THEORY_REALS);
+      break;
+
+    case QF_AUFLIA:
+      addTheory(THEORY_INT_ARRAYS_EX);  // nonstandard logic
+      addOperator(kind::APPLY_UF);
+      addTheory(THEORY_INTS);
+      break;
+
+    case QF_AUFLIRA:  // nonstandard logic
+      addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX);
+      addOperator(kind::APPLY_UF);
+      addTheory(THEORY_INTS);
+      addTheory(THEORY_REALS);
+      break;
+
+    case ALL_SUPPORTED:  // nonstandard logic
+      addTheory(THEORY_QUANTIFIERS);
+      /* fall through */
+    case QF_ALL_SUPPORTED:  // nonstandard logic
+      addTheory(THEORY_ARRAYS_EX);
+      addOperator(kind::APPLY_UF);
+      addTheory(THEORY_INTS);
+      addTheory(THEORY_REALS);
+      addTheory(THEORY_BITVECTORS);
+      break;
+
+    case AUFLIA:
+      addOperator(kind::APPLY_UF);
+      addTheory(THEORY_INTS);
+      addTheory(THEORY_INT_ARRAYS_EX);
+      addTheory(THEORY_QUANTIFIERS);
+      break;
+
+    case AUFLIRA:
+    case AUFNIRA:
+      addOperator(kind::APPLY_UF);
+      addTheory(THEORY_INTS);
+      addTheory(THEORY_REALS);
+      addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX);
+      addTheory(THEORY_QUANTIFIERS);
+      break;
+
+    case LRA:
+      addTheory(THEORY_REALS);
+      addTheory(THEORY_QUANTIFIERS);
+      break;
+
+    case UFNIA:
+      addOperator(kind::APPLY_UF);
+      addTheory(THEORY_INTS);
+      addTheory(THEORY_QUANTIFIERS);
+      break;
+    case UFNIRA:
+      addOperator(kind::APPLY_UF);
+      addTheory(THEORY_INTS);
+      addTheory(THEORY_REALS);
+      addTheory(THEORY_QUANTIFIERS);
+      break;
+
+    case UFLRA:
+      addOperator(kind::APPLY_UF);
+      addTheory(THEORY_REALS);
+      addTheory(THEORY_QUANTIFIERS);
+      break;
   }
 }/* Smt1::setLogic() */
 
diff --git a/src/parser/smt1/smt1.h b/src/parser/smt1/smt1.h
index 036453675..49a4b8000 100644
--- a/src/parser/smt1/smt1.h
+++ b/src/parser/smt1/smt1.h
@@ -32,64 +32,64 @@ class Smt1 : public Parser {
   friend class ParserBuilder;
 
 public:
-  enum Logic {
-    AUFLIA, // +p and -p?
-    AUFLIRA,
-    AUFNIRA,
-    LRA,
-    QF_ABV,
-    QF_AUFBV,
-    QF_AUFBVLIA,
-    QF_AUFBVLRA,
-    QF_AUFLIA,
-    QF_AUFLIRA,
-    QF_AX,
-    QF_BV,
-    QF_IDL,
-    QF_LIA,
-    QF_LRA,
-    QF_NIA,
-    QF_NRA,
-    QF_RDL,
-    QF_S, // nonstandard (for string theory)
-    QF_SAT,
-    QF_UF,
-    QF_UFIDL,
-    QF_UFBV,
-    QF_UFLIA,
-    QF_UFNIA, // nonstandard
-    QF_UFLRA,
-    QF_UFLIRA, // nonstandard
-    QF_UFNIRA, // nonstandard
-    QF_UFNRA,
-    SAT,
-    UFLRA,
-    UFNIRA, // nonstandard
-    UFNIA,
-    QF_ALL_SUPPORTED, // nonstandard
-    ALL_SUPPORTED // nonstandard
-  };
-
-  enum Theory {
-    THEORY_ARRAYS,
-    THEORY_ARRAYS_EX,
-    THEORY_BITVECTORS,
-    THEORY_BITVECTORS_32,
-    THEORY_BITVECTOR_ARRAYS_EX,
-    THEORY_EMPTY,
-    THEORY_INTS,
-    THEORY_INT_ARRAYS,
-    THEORY_INT_ARRAYS_EX,
-    THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX,
-    THEORY_REALS,
-    THEORY_REALS_INTS,
-    THEORY_STRINGS,
-    THEORY_QUANTIFIERS,
-    THEORY_CARDINALITY_CONSTRAINT
-  };
+ enum Logic {
+   UNSET = 0,  // This indicates that the logic has not been set.
+   AUFLIA,     // +p and -p?
+   AUFLIRA,
+   AUFNIRA,
+   LRA,
+   QF_ABV,
+   QF_AUFBV,
+   QF_AUFBVLIA,
+   QF_AUFBVLRA,
+   QF_AUFLIA,
+   QF_AUFLIRA,
+   QF_AX,
+   QF_BV,
+   QF_IDL,
+   QF_LIA,
+   QF_LRA,
+   QF_NIA,
+   QF_NRA,
+   QF_RDL,
+   QF_S,  // nonstandard (for string theory)
+   QF_SAT,
+   QF_UF,
+   QF_UFIDL,
+   QF_UFBV,
+   QF_UFLIA,
+   QF_UFNIA,  // nonstandard
+   QF_UFLRA,
+   QF_UFLIRA,  // nonstandard
+   QF_UFNIRA,  // nonstandard
+   QF_UFNRA,
+   SAT,
+   UFLRA,
+   UFNIRA,  // nonstandard
+   UFNIA,
+   QF_ALL_SUPPORTED,  // nonstandard
+   ALL_SUPPORTED      // nonstandard
+ };
+
+ enum Theory {
+   THEORY_ARRAYS,
+   THEORY_ARRAYS_EX,
+   THEORY_BITVECTORS,
+   THEORY_BITVECTORS_32,
+   THEORY_BITVECTOR_ARRAYS_EX,
+   THEORY_EMPTY,
+   THEORY_INTS,
+   THEORY_INT_ARRAYS,
+   THEORY_INT_ARRAYS_EX,
+   THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX,
+   THEORY_REALS,
+   THEORY_REALS_INTS,
+   THEORY_STRINGS,
+   THEORY_QUANTIFIERS,
+   THEORY_CARDINALITY_CONSTRAINT
+ };
 
 private:
-  bool d_logicSet;
   Logic d_logic;
 
 protected: