From: Christopher L. Conway <christopherleeconway@gmail.com>
Date: Thu, 8 Jul 2010 19:12:41 +0000 (+0000)
Subject: Adding missing operators in SMT2 parser: UMINUS, DIVISION, GEQ, LEQ
X-Git-Tag: cvc5-1.0.0~8913
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8b84abb2a69ef595b4ccae8bde56414dd3fa295c;p=cvc5.git

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 c23ccca6b..89c37883a 100644
--- 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 e25b8217b..23879fda8 100644
--- 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);