Merge branch '1.2.x'

7 files changed, 51 insertions, 132 deletions

diff --git a/NEWS b/NEWS
index eb991f74c..0532716a9 100644
--- a/NEWS
+++ b/NEWS
@@ -6,7 +6,7 @@ Changes since 1.2
 * We no longer permit model or proof generation if there's been an
   intervening push/pop.
 * Increased compliance to SMT-LIBv2, numerous bugs and usability issues
-  resolved
+  resolved.
 
 Changes since 1.1
 =================
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 36336a959..423bf3234 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -1118,7 +1118,8 @@ void SetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
     smtEngine->setInfo(d_flag, d_sexpr);
     d_commandStatus = CommandSuccess::instance();
   } catch(UnrecognizedOptionException&) {
-    d_commandStatus = new CommandUnsupported();
+    // As per SMT-LIB spec, silently accept unknown set-info keys
+    d_commandStatus = CommandSuccess::instance();
   } catch(exception& e) {
     d_commandStatus = new CommandFailure(e.what());
   }
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index a7f7796cd..c042c3992 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -36,7 +36,6 @@ void Smt2::addArithmeticOperators() {
   addOperator(kind::MINUS);
   addOperator(kind::UMINUS);
   addOperator(kind::MULT);
-  addOperator(kind::DIVISION);
   addOperator(kind::LT);
   addOperator(kind::LEQ);
   addOperator(kind::GT);
@@ -106,16 +105,20 @@ void Smt2::addTheory(Theory theory) {
 
   case THEORY_REALS_INTS:
     defineType("Real", getExprManager()->realType());
-    // falling-through on purpose, to add Ints part of RealsInts
+    addOperator(kind::DIVISION);
+    // falling through on purpose, to add Ints part of Reals_Ints
 
   case THEORY_INTS:
     defineType("Int", getExprManager()->integerType());
     addArithmeticOperators();
+    addOperator(kind::INTS_DIVISION);
+    addOperator(kind::INTS_MODULUS);
     break;
 
   case THEORY_REALS:
     defineType("Real", getExprManager()->realType());
     addArithmeticOperators();
+    addOperator(kind::DIVISION);
     break;
 
   case THEORY_BITVECTORS:
@@ -138,135 +141,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() */
 
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 5762ff5f9..7a464c773 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -21,6 +21,7 @@
 
 #include "parser/parser.h"
 #include "parser/smt1/smt1.h"
+#include "theory/logic_info.h"
 #include "util/abstract_value.h"
 
 #include <sstream>
@@ -47,7 +48,7 @@ public:
 
 private:
   bool d_logicSet;
-  Smt1::Logic d_logic;
+  LogicInfo d_logic;
 
 protected:
   Smt2(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false);
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index a2fe96271..fc2574036 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -241,11 +241,16 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::MULT:
   case kind::MINUS:
   case kind::UMINUS:
-  case kind::DIVISION:
   case kind::LT:
   case kind::LEQ:
   case kind::GT:
-  case kind::GEQ: out << smtKindString(k) << " "; break;
+  case kind::GEQ:
+  case kind::DIVISION:
+  case kind::DIVISION_TOTAL:
+  case kind::INTS_DIVISION:
+  case kind::INTS_DIVISION_TOTAL:
+  case kind::INTS_MODULUS:
+  case kind::INTS_MODULUS_TOTAL: out << smtKindString(k) << " "; break;
 
     // arrays theory
   case kind::SELECT:
@@ -421,11 +426,16 @@ static string smtKindString(Kind k) throw() {
   case kind::MULT: return "*";
   case kind::MINUS: return "-";
   case kind::UMINUS: return "-";
-  case kind::DIVISION: return "/";
   case kind::LT: return "<";
   case kind::LEQ: return "<=";
   case kind::GT: return ">";
   case kind::GEQ: return ">=";
+  case kind::DIVISION:
+  case kind::DIVISION_TOTAL: return "/";
+  case kind::INTS_DIVISION:
+  case kind::INTS_DIVISION_TOTAL: return "div";
+  case kind::INTS_MODULUS:
+  case kind::INTS_MODULUS_TOTAL: return "mod";
 
     // arrays theory
   case kind::SELECT: return "select";
diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h
index c7b5c58f9..2448898c0 100644
--- a/src/theory/logic_info.h
+++ b/src/theory/logic_info.h
@@ -155,21 +155,25 @@ public:
   /** Are integers in this logic? */
   bool areIntegersUsed() const {
     CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
+    CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether integers are used");
     return d_integers;
   }
   /** Are reals in this logic? */
   bool areRealsUsed() const {
     CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
+    CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether reals are used");
     return d_reals;
   }
   /** Does this logic only linear arithmetic? */
   bool isLinear() const {
     CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
+    CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether it's linear");
     return d_linear || d_differenceLogic;
   }
   /** Does this logic only permit difference reasoning? (implies linear) */
   bool isDifferenceLogic() const {
     CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
+    CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether it's difference logic");
     return d_differenceLogic;
   }
 
diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h
index a0d415296..39d8aadb1 100644
--- a/test/unit/theory/logic_info_white.h
+++ b/test/unit/theory/logic_info_white.h
@@ -555,10 +555,10 @@ public:
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
-    TS_ASSERT( !info.isLinear() );
-    TS_ASSERT( !info.areIntegersUsed() );
-    TS_ASSERT( !info.isDifferenceLogic() );
-    TS_ASSERT( !info.areRealsUsed() );
+    TS_ASSERT_THROWS( info.isLinear(), IllegalArgumentException );
+    TS_ASSERT_THROWS( info.areIntegersUsed(), IllegalArgumentException );
+    TS_ASSERT_THROWS( info.isDifferenceLogic(), IllegalArgumentException );
+    TS_ASSERT_THROWS( info.areRealsUsed(), IllegalArgumentException );
 
     // check copy is unchanged
     info = info.getUnlockedCopy();
@@ -574,10 +574,10 @@ public:
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
-    TS_ASSERT( !info.isLinear() );
-    TS_ASSERT( !info.areIntegersUsed() );
-    TS_ASSERT( !info.isDifferenceLogic() );
-    TS_ASSERT( !info.areRealsUsed() );
+    TS_ASSERT_THROWS( info.isLinear(), IllegalArgumentException );
+    TS_ASSERT_THROWS( info.areIntegersUsed(), IllegalArgumentException );
+    TS_ASSERT_THROWS( info.isDifferenceLogic(), IllegalArgumentException );
+    TS_ASSERT_THROWS( info.areRealsUsed(), IllegalArgumentException );
 
     // check all-included logic
     info = info.getUnlockedCopy();