Parsing support for SMT divisions: LRA, QF_UFLIA, QF_UFLRA, QF_UFNRA, UFNIA

4 files changed, 51 insertions, 20 deletions

diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index 53c58e2e6..bbec3299f 100644
--- a/src/parser/smt/smt.cpp
+++ b/src/parser/smt/smt.cpp
@@ -121,6 +121,11 @@ bool Smt::logicIsSet() {
   return d_logicSet;
 }
 
+inline void Smt::addUf() {
+  addTheory(Smt::THEORY_EMPTY);
+  addOperator(kind::APPLY_UF);
+}
+
 /**
  * Sets the logic for the current benchmark. Declares any logic and theory symbols.
  *
@@ -152,17 +157,26 @@ void Smt::setLogic(const std::string& name) {
     break;
 
   case QF_UFIDL:
+  case QF_UFLIA:
     addTheory(THEORY_INTS);
-    // falling-through on purpose, to add UF part of UFIDL
+    addUf();
+    break;
+
+  case QF_UFLRA:
+  case QF_UFNRA:
+    addTheory(THEORY_REALS);
+    addUf();
+    break;
 
   case QF_UF:
-    addTheory(THEORY_EMPTY);
-    addOperator(kind::APPLY_UF);
+    addUf();
     break;
 
   case AUFLIA:
   case AUFLIRA:
   case AUFNIRA:
+  case LRA:
+  case UFNIA:
   case QF_AUFBV:
   case QF_AUFLIA:
   case QF_BV:
diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h
index c6a15b335..d08e25ba9 100644
--- a/src/parser/smt/smt.h
+++ b/src/parser/smt/smt.h
@@ -36,9 +36,10 @@ class Smt : public Parser {
 
 public:
   enum Logic {
-    AUFLIA,
+    AUFLIA, // +p and -p?
     AUFLIRA,
     AUFNIRA,
+    LRA,
     QF_AUFBV,
     QF_AUFLIA,
     QF_AX,
@@ -50,7 +51,11 @@ public:
     QF_RDL,
     QF_SAT,
     QF_UF,
-    QF_UFIDL
+    QF_UFIDL,
+    QF_UFLIA,
+    QF_UFLRA,
+    QF_UFNRA,
+    UFNIA
   };
 
   enum Theory {
@@ -102,6 +107,7 @@ public:
 private:
 
   void addArithmeticOperators();
+  void addUf();
   static std::hash_map<const std::string, Logic, CVC4::StringHashFunction> newLogicMap();
 };
 }/* CVC4::parser namespace */
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 69b2eba76..56457d006 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -230,16 +230,16 @@ term[CVC4::Expr& expr]
     // TODO: check arity
     { expr = MK_EXPR(CVC4::kind::APPLY_UF,args); }
 
-  | /* An ite expression */
-    LPAREN_TOK ITE_TOK 
-    term[expr]
-    { args.push_back(expr); } 
-    term[expr]
-    { args.push_back(expr); } 
-    term[expr]
-    { args.push_back(expr); } 
-    RPAREN_TOK
-    { expr = MK_EXPR(CVC4::kind::ITE, args); }
+  // | /* An ite expression */
+  //   LPAREN_TOK ITE_TOK 
+  //   term[expr]
+  //   { args.push_back(expr); } 
+  //   term[expr]
+  //   { args.push_back(expr); } 
+  //   term[expr]
+  //   { args.push_back(expr); } 
+  //   RPAREN_TOK
+  //   { expr = MK_EXPR(CVC4::kind::ITE, args); }
 
   | /* a let binding */
     LPAREN_TOK LET_TOK LPAREN_TOK 
@@ -256,17 +256,18 @@ term[CVC4::Expr& expr]
     { expr = PARSER_STATE->getVariable(name); }
 
     /* constants */
-//  | TRUE_TOK          { expr = MK_CONST(true); }
-//  | FALSE_TOK         { expr = MK_CONST(false); }
   | INTEGER_LITERAL
     { expr = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); }
+
   | DECIMAL_LITERAL
     { // FIXME: This doesn't work because an SMT rational is not a valid GMP rational string
       expr = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); }
+
   | HEX_LITERAL
     { Assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 );
       std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL,2);
       expr = MK_CONST( BitVector(hexString, 16) ); }
+
   | BINARY_LITERAL
     { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 );
       std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL,2);
@@ -300,6 +301,7 @@ builtinOp[CVC4::Kind& kind]
   | XOR_TOK      { $kind = CVC4::kind::XOR;     }
   | EQUAL_TOK    { $kind = CVC4::kind::EQUAL;   }
   | DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; }
+  | ITE_TOK      { $kind = CVC4::kind::ITE; }
   | GREATER_THAN_TOK
                  { $kind = CVC4::kind::GT; }
   | GREATER_THAN_TOK EQUAL_TOK
@@ -310,7 +312,6 @@ builtinOp[CVC4::Kind& kind]
                  { $kind = CVC4::kind::LT; }
   | PLUS_TOK     { $kind = CVC4::kind::PLUS; }
   | STAR_TOK     { $kind = CVC4::kind::MULT; }
-  | TILDE_TOK    { $kind = CVC4::kind::UMINUS; }
   | MINUS_TOK    { $kind = CVC4::kind::MINUS; }
   | SELECT_TOK   { $kind = CVC4::kind::SELECT; }
   | STORE_TOK    { $kind = CVC4::kind::STORE; }
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 34245669e..79d5ccb3a 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -128,17 +128,27 @@ void Smt2::setLogic(const std::string& name) {
     addTheory(THEORY_REALS);
     break;
 
+  case Smt::QF_UF:
+    addOperator(kind::APPLY_UF);
+    break;
+
   case Smt::QF_UFIDL:
     addTheory(THEORY_INTS);
-    // falling-through on purpose, to add UF part of UFIDL
+    addOperator(kind::APPLY_UF);
+    break;
 
-  case Smt::QF_UF:
+  case Smt::QF_UFLIA:
+  case Smt::QF_UFLRA:
+  case Smt::QF_UFNRA:
+    addTheory(THEORY_REALS);
     addOperator(kind::APPLY_UF);
     break;
 
   case Smt::AUFLIA:
   case Smt::AUFLIRA:
   case Smt::AUFNIRA:
+  case Smt::LRA:
+  case Smt::UFNIA:
   case Smt::QF_AUFBV:
   case Smt::QF_AUFLIA:
   case Smt::QF_BV: