Adding missing operators in SMT2 parser: UMINUS, DIVISION, GEQ, LEQ

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index c23ccca6b2046332c791c55dd476489eaa85c67a..89c37883a8610fc66d6e85631890ce0ff894ed60 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -212,10 +212,12 @@ term[CVC4::Expr& expr]
         /* Unary AND/OR can be replaced with the argument.
               It just so happens expr should already by the only argument. */
         Assert( expr == args[0] );
-        } else if( CVC4::kind::isAssociative(kind) && 
+      } else if( CVC4::kind::isAssociative(kind) && 
                  args.size() > EXPR_MANAGER->maxArity(kind) ) {
        /* Special treatment for associative operators with lots of children */
         expr = EXPR_MANAGER->mkAssociative(kind,args);
+      } else if( kind == CVC4::kind::MINUS && args.size() == 1 ) {
+        expr = MK_EXPR(CVC4::kind::UMINUS, args[0]);
       } else {
         PARSER_STATE->checkOperator(kind, args.size());
         expr = MK_EXPR(kind, args);
@@ -304,15 +306,16 @@ builtinOp[CVC4::Kind& kind]
   | ITE_TOK      { $kind = CVC4::kind::ITE; }
   | GREATER_THAN_TOK
                  { $kind = CVC4::kind::GT; }
-  | GREATER_THAN_TOK EQUAL_TOK
+  | GREATER_THAN_EQUAL_TOK
                  { $kind = CVC4::kind::GEQ; }
-  | LESS_THAN_TOK EQUAL_TOK
+  | LESS_THAN_EQUAL_TOK
                  { $kind = CVC4::kind::LEQ; }
   | LESS_THAN_TOK
                  { $kind = CVC4::kind::LT; }
   | PLUS_TOK     { $kind = CVC4::kind::PLUS; }
-  | STAR_TOK     { $kind = CVC4::kind::MULT; }
   | MINUS_TOK    { $kind = CVC4::kind::MINUS; }
+  | STAR_TOK     { $kind = CVC4::kind::MULT; }
+  | DIV_TOK      { $kind = CVC4::kind::DIVISION; }
   | SELECT_TOK   { $kind = CVC4::kind::SELECT; }
   | STORE_TOK    { $kind = CVC4::kind::STORE; }
   // NOTE: Theory operators go here
@@ -427,8 +430,10 @@ EQUAL_TOK         : '=';
 EXISTS_TOK        : 'exists';
 FORALL_TOK        : 'forall';
 GREATER_THAN_TOK  : '>';
+GREATER_THAN_EQUAL_TOK  : '>=';
 IMPLIES_TOK       : '=>';
 LESS_THAN_TOK     : '<';
+LESS_THAN_EQUAL_TOK     : '<=';
 MINUS_TOK         : '-';
 NOT_TOK           : 'not';
 OR_TOK            : 'or';

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index e25b8217ba8eea6c0a8a2037fd8335582babc450..23879fda883217f7d7fc9ce0e5a73b0af4f4cfbe 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -36,6 +36,7 @@ void Smt2::addArithmeticOperators() {
   addOperator(kind::MINUS);
   addOperator(kind::UMINUS);
   addOperator(kind::MULT);
+  addOperator(kind::DIVISION);
   addOperator(kind::LT);
   addOperator(kind::LEQ);
   addOperator(kind::GT);