From 3c37d6aeb7028923ea1827a75de54bd6947b955b Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 17 Mar 2022 14:36:48 -0700 Subject: [PATCH] [Parser] Simplify `Smt2::addIndexedOperator()` (#8333) It seems that Smt2::addIndexedOperator() has not been updated after we fully switched the parser over to using API kinds. This commit simplifies Smt2::addIndexedOperator() accordingly. --- src/parser/smt2/smt2.cpp | 65 ++++++++++++++-------------------------- src/parser/smt2/smt2.h | 6 +--- 2 files changed, 23 insertions(+), 48 deletions(-) diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 24b055eef..74e045b4c 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -115,16 +115,12 @@ void Smt2::addBitvectorOperators() { addOperator(api::BITVECTOR_REDOR, "bvredor"); addOperator(api::BITVECTOR_REDAND, "bvredand"); - addIndexedOperator(api::BITVECTOR_EXTRACT, api::BITVECTOR_EXTRACT, "extract"); - addIndexedOperator(api::BITVECTOR_REPEAT, api::BITVECTOR_REPEAT, "repeat"); - addIndexedOperator( - api::BITVECTOR_ZERO_EXTEND, api::BITVECTOR_ZERO_EXTEND, "zero_extend"); - addIndexedOperator( - api::BITVECTOR_SIGN_EXTEND, api::BITVECTOR_SIGN_EXTEND, "sign_extend"); - addIndexedOperator( - api::BITVECTOR_ROTATE_LEFT, api::BITVECTOR_ROTATE_LEFT, "rotate_left"); - addIndexedOperator( - api::BITVECTOR_ROTATE_RIGHT, api::BITVECTOR_ROTATE_RIGHT, "rotate_right"); + addIndexedOperator(api::BITVECTOR_EXTRACT, "extract"); + addIndexedOperator(api::BITVECTOR_REPEAT, "repeat"); + addIndexedOperator(api::BITVECTOR_ZERO_EXTEND, "zero_extend"); + addIndexedOperator(api::BITVECTOR_SIGN_EXTEND, "sign_extend"); + addIndexedOperator(api::BITVECTOR_ROTATE_LEFT, "rotate_left"); + addIndexedOperator(api::BITVECTOR_ROTATE_RIGHT, "rotate_right"); } void Smt2::addDatatypesOperators() @@ -140,9 +136,8 @@ void Smt2::addDatatypesOperators() // Notice that tuple operators, we use the generic APPLY_SELECTOR and // APPLY_UPDATER kinds. These are processed based on the context // in which they are parsed, e.g. when parsing identifiers. - addIndexedOperator( - api::APPLY_SELECTOR, api::APPLY_SELECTOR, "tuple_select"); - addIndexedOperator(api::APPLY_UPDATER, api::APPLY_UPDATER, "tuple_update"); + addIndexedOperator(api::APPLY_SELECTOR, "tuple_select"); + addIndexedOperator(api::APPLY_UPDATER, "tuple_update"); } } @@ -197,8 +192,8 @@ void Smt2::addStringOperators() { addOperator(api::REGEXP_STAR, "re.*"); addOperator(api::REGEXP_PLUS, "re.+"); addOperator(api::REGEXP_OPT, "re.opt"); - addIndexedOperator(api::REGEXP_REPEAT, api::REGEXP_REPEAT, "re.^"); - addIndexedOperator(api::REGEXP_LOOP, api::REGEXP_LOOP, "re.loop"); + addIndexedOperator(api::REGEXP_REPEAT, "re.^"); + addIndexedOperator(api::REGEXP_LOOP, "re.loop"); addOperator(api::REGEXP_RANGE, "re.range"); addOperator(api::REGEXP_COMPLEMENT, "re.comp"); addOperator(api::REGEXP_DIFF, "re.diff"); @@ -234,31 +229,17 @@ void Smt2::addFloatingPointOperators() { addOperator(api::FLOATINGPOINT_IS_POS, "fp.isPositive"); addOperator(api::FLOATINGPOINT_TO_REAL, "fp.to_real"); - addIndexedOperator(api::FLOATINGPOINT_TO_FP_GENERIC, - api::FLOATINGPOINT_TO_FP_GENERIC, - "to_fp"); - addIndexedOperator(api::FLOATINGPOINT_TO_FP_FROM_UBV, - api::FLOATINGPOINT_TO_FP_FROM_UBV, - "to_fp_unsigned"); - addIndexedOperator( - api::FLOATINGPOINT_TO_UBV, api::FLOATINGPOINT_TO_UBV, "fp.to_ubv"); - addIndexedOperator( - api::FLOATINGPOINT_TO_SBV, api::FLOATINGPOINT_TO_SBV, "fp.to_sbv"); + addIndexedOperator(api::FLOATINGPOINT_TO_FP_GENERIC, "to_fp"); + addIndexedOperator(api::FLOATINGPOINT_TO_FP_FROM_UBV, "to_fp_unsigned"); + addIndexedOperator(api::FLOATINGPOINT_TO_UBV, "fp.to_ubv"); + addIndexedOperator(api::FLOATINGPOINT_TO_SBV, "fp.to_sbv"); if (!strictModeEnabled()) { - addIndexedOperator(api::FLOATINGPOINT_TO_FP_FROM_IEEE_BV, - api::FLOATINGPOINT_TO_FP_FROM_IEEE_BV, - "to_fp_bv"); - addIndexedOperator(api::FLOATINGPOINT_TO_FP_FROM_FP, - api::FLOATINGPOINT_TO_FP_FROM_FP, - "to_fp_fp"); - addIndexedOperator(api::FLOATINGPOINT_TO_FP_FROM_REAL, - api::FLOATINGPOINT_TO_FP_FROM_REAL, - "to_fp_real"); - addIndexedOperator(api::FLOATINGPOINT_TO_FP_FROM_SBV, - api::FLOATINGPOINT_TO_FP_FROM_SBV, - "to_fp_signed"); + addIndexedOperator(api::FLOATINGPOINT_TO_FP_FROM_IEEE_BV, "to_fp_bv"); + addIndexedOperator(api::FLOATINGPOINT_TO_FP_FROM_FP, "to_fp_fp"); + addIndexedOperator(api::FLOATINGPOINT_TO_FP_FROM_REAL, "to_fp_real"); + addIndexedOperator(api::FLOATINGPOINT_TO_FP_FROM_SBV, "to_fp_signed"); } } @@ -299,11 +280,10 @@ void Smt2::addOperator(api::Kind kind, const std::string& name) } void Smt2::addIndexedOperator(api::Kind tKind, - api::Kind opKind, const std::string& name) { Parser::addOperator(tKind); - d_indexedOpKindMap[name] = opKind; + d_indexedOpKindMap[name] = tKind; } api::Kind Smt2::getOperatorKind(const std::string& name) const @@ -521,7 +501,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) addOperator(api::INTS_MODULUS, "mod"); addOperator(api::ABS, "abs"); } - addIndexedOperator(api::DIVISIBLE, api::DIVISIBLE, "divisible"); + addIndexedOperator(api::DIVISIBLE, "divisible"); } if (d_logic.areRealsUsed()) @@ -550,7 +530,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) if (!strictModeEnabled()) { // integer version of AND - addIndexedOperator(api::IAND, api::IAND, "iand"); + addIndexedOperator(api::IAND, "iand"); // pow2 addOperator(api::POW2, "int.pow2"); } @@ -570,8 +550,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) { // Conversions between bit-vectors and integers addOperator(api::BITVECTOR_TO_NAT, "bv2nat"); - addIndexedOperator( - api::INT_TO_BITVECTOR, api::INT_TO_BITVECTOR, "int2bv"); + addIndexedOperator(api::INT_TO_BITVECTOR, "int2bv"); } } diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index cee795648..e53dc2048 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -83,14 +83,10 @@ class Smt2 : public Parser * Registers an indexed function symbol. * * @param tKind The kind of the term that uses the operator kind (e.g. - * BITVECTOR_EXTRACT). NOTE: this is an internal kind for now - * because that is what we use to create expressions. Eventually - * it will be an api::Kind. - * @param opKind The kind of the operator term (e.g. BITVECTOR_EXTRACT) + * BITVECTOR_EXTRACT). * @param name The name of the symbol (e.g. "extract") */ void addIndexedOperator(api::Kind tKind, - api::Kind opKind, const std::string& name); api::Kind getOperatorKind(const std::string& name) const; -- 2.30.2