diff options
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 53 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 51 |
2 files changed, 27 insertions, 77 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 87dd18381..190b43d51 100644 --- 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 85f2d1ec5..8f0b14328 100644 --- 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); } |