From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 4 Jun 2014 22:34:24 +0000 (-0400)
Subject: Add operator support (resolves bug #563).
X-Git-Tag: cvc5-1.0.0~6858
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=90e3d3127d41348d9d3c7d7877d2d9d7e2828124;p=cvc5.git

Add operator support (resolves bug #563).
---

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index f9055f5db..aa24ce9c4 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -150,6 +150,8 @@ tokens {
   MOD_TOK = 'MOD';
   INTDIV_TOK = 'DIV';
   FLOOR_TOK = 'FLOOR';
+  ABS_TOK = 'ABS';
+  DIVISIBLE_TOK = 'DIVISIBLE';
   DISTINCT_TOK = 'DISTINCT';
 
   // Bitvectors
@@ -180,7 +182,7 @@ tokens {
   //BVTOINT_TOK = 'BVTOINT';
   //INTTOBV_TOK = 'INTTOBV';
   //BOOLEXTRACT_TOK = 'BOOLEXTRACT';
-  //IS_INTEGER_TOK = 'IS_INTEGER';
+  IS_INTEGER_TOK = 'IS_INTEGER';
   BVLT_TOK = 'BVLT';
   BVGT_TOK = 'BVGT';
   BVLE_TOK = 'BVLE';
@@ -237,7 +239,7 @@ int getOperatorPrecedence(int type) {
   case LBRACE: return 2;
   case LBRACKET: return 3;
   case ARROW_TOK: return 4;
-  //case IS_INTEGER_TOK: return 5;
+  case IS_INTEGER_TOK: return 5;
   case BVSLT_TOK:
   case BVSLE_TOK:
   case BVSGT_TOK:
@@ -567,7 +569,7 @@ using namespace CVC4::parser;
   } else if (k < size) {                                       \
     f = MK_EXPR(MK_CONST(BitVectorExtract(k - 1, 0)), f);      \
   }                                                            \
-}                                            
+}
 
 }/* @parser::postinclude */
 
@@ -1679,6 +1681,12 @@ postfixTerm[CVC4::Expr& f]
     )*
     | FLOOR_TOK LPAREN formula[f] RPAREN
       { f = MK_EXPR(CVC4::kind::TO_INTEGER, f); }
+    | IS_INTEGER_TOK LPAREN formula[f] RPAREN
+      { f = MK_EXPR(CVC4::kind::IS_INTEGER, f); }
+    | ABS_TOK LPAREN formula[f] RPAREN
+      { f = MK_EXPR(CVC4::kind::ABS, f); }
+    | DIVISIBLE_TOK LPAREN formula[f] COMMA n=numeral RPAREN
+      { f = MK_EXPR(CVC4::kind::DIVISIBLE, MK_CONST(CVC4::Divisible(n)), f); }
     | DISTINCT_TOK LPAREN
       formula[f] { args.push_back(f); }
       ( COMMA formula[f] { args.push_back(f); } )* RPAREN
@@ -1724,11 +1732,11 @@ bvTerm[CVC4::Expr& f]
     { f = MK_EXPR(CVC4::kind::BITVECTOR_NEG, f); }
     /* BV addition */
   | BVPLUS_TOK LPAREN k=numeral COMMA formula[f] { args.push_back(f); }
-    ( COMMA formula[f2] { args.push_back(f2); } )+ RPAREN 
+    ( COMMA formula[f2] { args.push_back(f2); } )+ RPAREN
     {
       if (k <= 0) {
         PARSER_STATE->parseError("BVPLUS(k,_,_) must have k > 0");
-      }      
+      }
       for (unsigned i = 0; i < args.size(); ++ i) {
         ENSURE_BV_SIZE(k, args[i]);
       }
@@ -1736,17 +1744,17 @@ bvTerm[CVC4::Expr& f]
     }
     /* BV subtraction */
   | BVSUB_TOK LPAREN k=numeral COMMA formula[f] COMMA formula[f2] RPAREN
-    {       
+    {
       if (k <= 0) {
         PARSER_STATE->parseError("BVSUB(k,_,_) must have k > 0");
-      }      
+      }
       ENSURE_BV_SIZE(k, f);
       ENSURE_BV_SIZE(k, f2);
       f = MK_EXPR(CVC4::kind::BITVECTOR_SUB, f, f2);
     }
     /* BV multiplication */
   | BVMULT_TOK LPAREN k=numeral COMMA formula[f] COMMA formula[f2] RPAREN
-    { 
+    {
       if (k <= 0) {
         PARSER_STATE->parseError("BVMULT(k,_,_) must have k > 0");
       }
@@ -1822,11 +1830,6 @@ bvTerm[CVC4::Expr& f]
   | BVSGE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
     { f = MK_EXPR(CVC4::kind::BITVECTOR_SGE, f, f2); }
 
-  /*
-  | IS_INTEGER_TOK LPAREN formula[f] RPAREN
-    { f = MK_EXPR(CVC4::kind::BITVECTOR_IS_INTEGER, f); }
-  */
-
   | stringTerm[f]
   ;
 
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 63529c2a5..77d8f14de 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -483,6 +483,27 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       op << '^';
       opType = INFIX;
       break;
+    case kind::ABS:
+      op << "ABS";
+      opType = PREFIX;
+      break;
+    case kind::IS_INTEGER:
+      op << "IS_INTEGER";
+      opType = PREFIX;
+      break;
+    case kind::TO_INTEGER:
+      op << "FLOOR";
+      opType = PREFIX;
+      break;
+    case kind::TO_REAL:
+      // ignore, there is no to-real in CVC language
+      toStream(out, n[0], depth, types, false);
+      return;
+    case kind::DIVISIBLE:
+      out << "DIVISIBLE(";
+      toStream(out, n[0], depth, types, false);
+      out << ", " << n.getOperator().getConst<Divisible>().k << ")";
+      return;
 
     // BITVECTORS
     case kind::BITVECTOR_XOR:
@@ -573,7 +594,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       opType = INFIX;
       break;
     case kind::BITVECTOR_PLUS: {
-      //This interprets a BITVECTOR_PLUS as a bvadd in SMT-LIB
+      // This interprets a BITVECTOR_PLUS as a bvadd in SMT-LIB
       Assert(n.getType().isBitVector());
       unsigned numc = n.getNumChildren()-2;
       unsigned child = 0;
@@ -590,7 +611,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       out << ',';
       toStream(out, n[child], depth, types, false);
       out << ',';
-      toStream(out, n[child+1], depth, types, false);
+      toStream(out, n[child + 1], depth, types, false);
       while (child > 0) {
         out << ')';
         --child;
@@ -627,7 +648,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       out << ',';
       toStream(out, n[child], depth, types, false);
       out << ',';
-      toStream(out, n[child+1], depth, types, false);
+      toStream(out, n[child + 1], depth, types, false);
       while (child > 0) {
         out << ')';
         --child;