diff options
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 51 |
1 files changed, 23 insertions, 28 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 6dc29b8fe..c7e70495e 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -123,23 +123,18 @@ void Smt2::addBitvectorOperators() { addOperator(kind::BITVECTOR_TO_NAT, "bv2nat"); addIndexedOperator( - kind::BITVECTOR_EXTRACT, api::BITVECTOR_EXTRACT_OP, "extract"); + kind::BITVECTOR_EXTRACT, api::BITVECTOR_EXTRACT, "extract"); + addIndexedOperator(kind::BITVECTOR_REPEAT, api::BITVECTOR_REPEAT, "repeat"); addIndexedOperator( - kind::BITVECTOR_REPEAT, api::BITVECTOR_REPEAT_OP, "repeat"); - addIndexedOperator(kind::BITVECTOR_ZERO_EXTEND, - api::BITVECTOR_ZERO_EXTEND_OP, - "zero_extend"); - addIndexedOperator(kind::BITVECTOR_SIGN_EXTEND, - api::BITVECTOR_SIGN_EXTEND_OP, - "sign_extend"); - addIndexedOperator(kind::BITVECTOR_ROTATE_LEFT, - api::BITVECTOR_ROTATE_LEFT_OP, - "rotate_left"); + kind::BITVECTOR_ZERO_EXTEND, api::BITVECTOR_ZERO_EXTEND, "zero_extend"); + addIndexedOperator( + kind::BITVECTOR_SIGN_EXTEND, api::BITVECTOR_SIGN_EXTEND, "sign_extend"); + addIndexedOperator( + kind::BITVECTOR_ROTATE_LEFT, api::BITVECTOR_ROTATE_LEFT, "rotate_left"); addIndexedOperator(kind::BITVECTOR_ROTATE_RIGHT, - api::BITVECTOR_ROTATE_RIGHT_OP, + api::BITVECTOR_ROTATE_RIGHT, "rotate_right"); - addIndexedOperator( - kind::INT_TO_BITVECTOR, api::INT_TO_BITVECTOR_OP, "int2bv"); + addIndexedOperator(kind::INT_TO_BITVECTOR, api::INT_TO_BITVECTOR, "int2bv"); } void Smt2::addDatatypesOperators() @@ -234,29 +229,29 @@ void Smt2::addFloatingPointOperators() { addOperator(kind::FLOATINGPOINT_TO_REAL, "fp.to_real"); addIndexedOperator(kind::FLOATINGPOINT_TO_FP_GENERIC, - api::FLOATINGPOINT_TO_FP_GENERIC_OP, + api::FLOATINGPOINT_TO_FP_GENERIC, "to_fp"); addIndexedOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, - api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP, + api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, "to_fp_unsigned"); addIndexedOperator( - kind::FLOATINGPOINT_TO_UBV, api::FLOATINGPOINT_TO_UBV_OP, "fp.to_ubv"); + kind::FLOATINGPOINT_TO_UBV, api::FLOATINGPOINT_TO_UBV, "fp.to_ubv"); addIndexedOperator( - kind::FLOATINGPOINT_TO_SBV, api::FLOATINGPOINT_TO_SBV_OP, "fp.to_sbv"); + kind::FLOATINGPOINT_TO_SBV, api::FLOATINGPOINT_TO_SBV, "fp.to_sbv"); if (!strictModeEnabled()) { addIndexedOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, - api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP, + api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, "to_fp_bv"); addIndexedOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT, - api::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP, + api::FLOATINGPOINT_TO_FP_FLOATINGPOINT, "to_fp_fp"); addIndexedOperator(kind::FLOATINGPOINT_TO_FP_REAL, - api::FLOATINGPOINT_TO_FP_REAL_OP, + api::FLOATINGPOINT_TO_FP_REAL, "to_fp_real"); addIndexedOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, - api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP, + api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, "to_fp_signed"); } } @@ -311,7 +306,7 @@ void Smt2::addTheory(Theory theory) { addOperator(kind::INTS_DIVISION, "div"); addOperator(kind::INTS_MODULUS, "mod"); addOperator(kind::ABS, "abs"); - addIndexedOperator(kind::DIVISIBLE, api::DIVISIBLE_OP, "divisible"); + addIndexedOperator(kind::DIVISIBLE, api::DIVISIBLE, "divisible"); break; case THEORY_REALS: @@ -549,8 +544,8 @@ api::Term Smt2::mkIndexedConstant(const std::string& name, return api::Term(); } -api::OpTerm Smt2::mkIndexedOp(const std::string& name, - const std::vector<uint64_t>& numerals) +api::Op Smt2::mkIndexedOp(const std::string& name, + const std::vector<uint64_t>& numerals) { const auto& kIt = d_indexedOpKindMap.find(name); if (kIt != d_indexedOpKindMap.end()) @@ -558,16 +553,16 @@ api::OpTerm Smt2::mkIndexedOp(const std::string& name, api::Kind k = (*kIt).second; if (numerals.size() == 1) { - return d_solver->mkOpTerm(k, numerals[0]); + return d_solver->mkOp(k, numerals[0]); } else if (numerals.size() == 2) { - return d_solver->mkOpTerm(k, numerals[0], numerals[1]); + return d_solver->mkOp(k, numerals[0], numerals[1]); } } parseError(std::string("Unknown indexed function `") + name + "'"); - return api::OpTerm(); + return api::Op(); } Expr Smt2::mkDefineFunRec( |