From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 5 Sep 2013 19:43:47 +0000 (-0400)
Subject: Fix FLOOR and DISTINCT in CVC language parser.
X-Git-Tag: cvc5-1.0.0~7287^2~27
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3544cac0bd08e3cf8b12c742fd7a6f6ab19de068;p=cvc5.git

Fix FLOOR and DISTINCT in CVC language parser.
---

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 9131c220f..51ea87e39 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -150,6 +150,7 @@ tokens {
   MOD_TOK = 'MOD';
   INTDIV_TOK = 'DIV';
   FLOOR_TOK = 'FLOOR';
+  DISTINCT_TOK = 'DISTINCT';
 
   // Bitvectors
 
@@ -270,8 +271,7 @@ int getOperatorPrecedence(int type) {
   case LEQ_TOK:
   case LT_TOK:
   case GEQ_TOK:
-  case GT_TOK:
-  case FLOOR_TOK: return 25;
+  case GT_TOK: return 25;
   case EQUAL_TOK:
   case DISEQUAL_TOK: return 26;
   case NOT_TOK: return 27;
@@ -1583,7 +1583,7 @@ postfixTerm[CVC4::Expr& f]
   std::string id;
   Type t;
 }
-  : bvTerm[f]
+  : ( bvTerm[f]
     ( /* array select / bitvector extract */
       LBRACKET
         ( formula[f2] { extract = false; }
@@ -1664,6 +1664,13 @@ postfixTerm[CVC4::Expr& f]
         }
       )
     )*
+    | FLOOR_TOK LPAREN formula[f] RPAREN
+      { f = MK_EXPR(CVC4::kind::TO_INTEGER, f); }
+    | DISTINCT_TOK LPAREN
+      formula[f] { args.push_back(f); }
+      ( COMMA formula[f] { args.push_back(f); } )* RPAREN
+      { f = (args.size() == 1) ? MK_CONST(bool(true)) : MK_EXPR(CVC4::kind::DISTINCT, args); }
+    )
     ( typeAscription[f, t]
       { if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && t.isDatatype()) {
           std::vector<CVC4::Expr> v;