fp builtinop parser changes

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 87dd1838162bd28ca3618959b04dd3a7eb5a77b6..190b43d513522e5ebb0920789810ca657fac6d8e 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2074,32 +2074,6 @@ builtinOp[CVC4::Kind& kind]
   
   | INST_CLOSURE_TOK { $kind = CVC4::kind::INST_CLOSURE; }
   
-  | FP_TOK        { $kind = CVC4::kind::FLOATINGPOINT_FP; }
-  | FP_EQ_TOK     { $kind = CVC4::kind::FLOATINGPOINT_EQ; }
-  | FP_ABS_TOK    { $kind = CVC4::kind::FLOATINGPOINT_ABS; }
-  | FP_NEG_TOK    { $kind = CVC4::kind::FLOATINGPOINT_NEG; }
-  | FP_PLUS_TOK   { $kind = CVC4::kind::FLOATINGPOINT_PLUS; }
-  | FP_SUB_TOK    { $kind = CVC4::kind::FLOATINGPOINT_SUB; }
-  | FP_MUL_TOK    { $kind = CVC4::kind::FLOATINGPOINT_MULT; }
-  | FP_DIV_TOK    { $kind = CVC4::kind::FLOATINGPOINT_DIV; }
-  | FP_FMA_TOK    { $kind = CVC4::kind::FLOATINGPOINT_FMA; }
-  | FP_SQRT_TOK   { $kind = CVC4::kind::FLOATINGPOINT_SQRT; }
-  | FP_REM_TOK    { $kind = CVC4::kind::FLOATINGPOINT_REM; }
-  | FP_RTI_TOK    { $kind = CVC4::kind::FLOATINGPOINT_RTI; }
-  | FP_MIN_TOK    { $kind = CVC4::kind::FLOATINGPOINT_MIN; }
-  | FP_MAX_TOK    { $kind = CVC4::kind::FLOATINGPOINT_MAX; }
-  | FP_LEQ_TOK    { $kind = CVC4::kind::FLOATINGPOINT_LEQ; }
-  | FP_LT_TOK     { $kind = CVC4::kind::FLOATINGPOINT_LT; }
-  | FP_GEQ_TOK    { $kind = CVC4::kind::FLOATINGPOINT_GEQ; }
-  | FP_GT_TOK     { $kind = CVC4::kind::FLOATINGPOINT_GT; }
-  | FP_ISN_TOK    { $kind = CVC4::kind::FLOATINGPOINT_ISN; }
-  | FP_ISSN_TOK   { $kind = CVC4::kind::FLOATINGPOINT_ISSN; }
-  | FP_ISZ_TOK    { $kind = CVC4::kind::FLOATINGPOINT_ISZ; }
-  | FP_ISINF_TOK  { $kind = CVC4::kind::FLOATINGPOINT_ISINF; }
-  | FP_ISNAN_TOK  { $kind = CVC4::kind::FLOATINGPOINT_ISNAN; }
-  | FP_ISNEG_TOK  { $kind = CVC4::kind::FLOATINGPOINT_ISNEG; }
-  | FP_ISPOS_TOK  { $kind = CVC4::kind::FLOATINGPOINT_ISPOS; }
-  | FP_TO_REAL_TOK {$kind = CVC4::kind::FLOATINGPOINT_TO_REAL; }
   // NOTE: Theory operators go here
   ;
 
@@ -2549,33 +2523,6 @@ FP_PZERO_TOK : '+zero';
 FP_NZERO_TOK : '-zero';
 FP_NAN_TOK : 'NaN';
 
-FP_TOK : 'fp';
-FP_EQ_TOK : 'fp.eq';
-FP_ABS_TOK : 'fp.abs';
-FP_NEG_TOK : 'fp.neg';
-FP_PLUS_TOK : 'fp.add';
-FP_SUB_TOK : 'fp.sub';
-FP_MUL_TOK : 'fp.mul';
-FP_DIV_TOK : 'fp.div';
-FP_FMA_TOK : 'fp.fma';
-FP_SQRT_TOK : 'fp.sqrt';
-FP_REM_TOK : 'fp.rem';
-FP_RTI_TOK : 'fp.roundToIntegral';
-FP_MIN_TOK : 'fp.min';
-FP_MAX_TOK : 'fp.max';
-FP_LEQ_TOK : 'fp.leq';
-FP_LT_TOK : 'fp.lt';
-FP_GEQ_TOK : 'fp.geq';
-FP_GT_TOK : 'fp.gt';
-FP_ISN_TOK : 'fp.isNormal';
-FP_ISSN_TOK : 'fp.isSubnormal';
-FP_ISZ_TOK : 'fp.isZero';
-FP_ISINF_TOK : 'fp.isInfinite';
-FP_ISNAN_TOK : 'fp.isNaN';
-FP_ISNEG_TOK : 'fp.isNegative';
-FP_ISPOS_TOK : 'fp.isPositive';
-FP_TO_REAL_TOK : 'fp.to_real';
-
 FP_TO_FP_TOK : 'to_fp';
 FP_TO_FPBV_TOK : 'to_fp_bv';
 FP_TO_FPFP_TOK : 'to_fp_fp';

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 85f2d1ec5a66abf09a1d5b5d24681eb0caec2be9..8f0b143285993740ee3aabef3ffb3a0bfc53751e 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -98,29 +98,33 @@ void Smt2::addStringOperators() {
 }
 
 void Smt2::addFloatingPointOperators() {
-  Parser::addOperator(kind::FLOATINGPOINT_FP);
-  Parser::addOperator(kind::FLOATINGPOINT_EQ);
-  Parser::addOperator(kind::FLOATINGPOINT_ABS);
-  Parser::addOperator(kind::FLOATINGPOINT_NEG);
-  Parser::addOperator(kind::FLOATINGPOINT_PLUS);
-  Parser::addOperator(kind::FLOATINGPOINT_SUB);
-  Parser::addOperator(kind::FLOATINGPOINT_MULT);
-  Parser::addOperator(kind::FLOATINGPOINT_DIV);
-  Parser::addOperator(kind::FLOATINGPOINT_FMA);
-  Parser::addOperator(kind::FLOATINGPOINT_SQRT);
-  Parser::addOperator(kind::FLOATINGPOINT_REM);
-  Parser::addOperator(kind::FLOATINGPOINT_RTI);
-  Parser::addOperator(kind::FLOATINGPOINT_MIN);
-  Parser::addOperator(kind::FLOATINGPOINT_MAX);
-  Parser::addOperator(kind::FLOATINGPOINT_LEQ);
-  Parser::addOperator(kind::FLOATINGPOINT_LT);
-  Parser::addOperator(kind::FLOATINGPOINT_GEQ);
-  Parser::addOperator(kind::FLOATINGPOINT_GT);
-  Parser::addOperator(kind::FLOATINGPOINT_ISN);
-  Parser::addOperator(kind::FLOATINGPOINT_ISSN);
-  Parser::addOperator(kind::FLOATINGPOINT_ISZ);
-  Parser::addOperator(kind::FLOATINGPOINT_ISINF);
-  Parser::addOperator(kind::FLOATINGPOINT_ISNAN);
+  addOperator(kind::FLOATINGPOINT_FP, "fp");
+  addOperator(kind::FLOATINGPOINT_EQ, "fp.eq");
+  addOperator(kind::FLOATINGPOINT_ABS, "fp.abs");
+  addOperator(kind::FLOATINGPOINT_NEG, "fp.neg");
+  addOperator(kind::FLOATINGPOINT_PLUS, "fp.add");
+  addOperator(kind::FLOATINGPOINT_SUB, "fp.sub");
+  addOperator(kind::FLOATINGPOINT_MULT, "fp.mul");
+  addOperator(kind::FLOATINGPOINT_DIV, "fp.div");
+  addOperator(kind::FLOATINGPOINT_FMA, "fp.fma");
+  addOperator(kind::FLOATINGPOINT_SQRT, "fp.sqrt");
+  addOperator(kind::FLOATINGPOINT_REM, "fp.rem");
+  addOperator(kind::FLOATINGPOINT_RTI, "fp.roundToIntegral");
+  addOperator(kind::FLOATINGPOINT_MIN, "fp.min");
+  addOperator(kind::FLOATINGPOINT_MAX, "fp.max");
+  addOperator(kind::FLOATINGPOINT_LEQ, "fp.leq");
+  addOperator(kind::FLOATINGPOINT_LT, "fp.lt");
+  addOperator(kind::FLOATINGPOINT_GEQ, "fp.geq");
+  addOperator(kind::FLOATINGPOINT_GT, "fp.gt");
+  addOperator(kind::FLOATINGPOINT_ISN, "fp.isNormal");
+  addOperator(kind::FLOATINGPOINT_ISSN, "fp.isSubnormal");
+  addOperator(kind::FLOATINGPOINT_ISZ, "fp.isZero");
+  addOperator(kind::FLOATINGPOINT_ISINF, "fp.isInfinite");
+  addOperator(kind::FLOATINGPOINT_ISNAN, "fp.isNaN");
+  addOperator(kind::FLOATINGPOINT_ISNEG, "fp.isNegative");
+  addOperator(kind::FLOATINGPOINT_ISPOS, "fp.isPositive");
+  addOperator(kind::FLOATINGPOINT_TO_REAL, "fp.to_real");
+
   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR);
   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT);
   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_REAL);
@@ -128,7 +132,6 @@ void Smt2::addFloatingPointOperators() {
   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR);
   Parser::addOperator(kind::FLOATINGPOINT_TO_UBV);
   Parser::addOperator(kind::FLOATINGPOINT_TO_SBV);
-  Parser::addOperator(kind::FLOATINGPOINT_TO_REAL);
 }