diff options
author | makaimann <makaim@stanford.edu> | 2019-12-02 13:36:19 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-12-02 13:36:19 -0800 |
commit | 207de293b26cf7771814d3cf421e64fc6116434e (patch) | |
tree | 3b8af6d5d4504c182bd80df06330829dbcab2516 /src/parser | |
parent | dc99f1c45f616a93ee84b2a6ba877518206bdbaf (diff) |
OpTerm Refactor: Allow retrieving OpTerm used to create Term in public C++ API (#3355)
* Treat uninterpreted functions as a child in Term iteration
* Remove unnecessary const_iterator constructor
* Add parameter comments to const_iterator constructor
* Use operator[] instead of storing a vector of Expr children
* Switch pos member variable from int to uint32_t
* Add comment about how UFs are treated in iteration
* Allow OpTerm to contain a single Kind, update OpTerm construction
* Update mkTerm to use only an OpTerm (and not also a Kind)
* Remove unnecessary function checkMkOpTerm
* Update mkOpTerm comments to not use _OP Kinds
* Update examples to use new mkTerm
* First pass on fixing unit test
* Override kind for Constructor and Selector Terms
* More fixes to unit tests
* Updates to parser
* Remove old assert (for Kind, OpTerm pattern which was removed)
* Remove *_OP kinds from public API
* Add hasOpTerm and getOpTerm methods to Term
* Add test for UF iteration
* Add unit test for getOpTerm
* Move OpTerm implementation above Term implemenation to match header file
Moved in header because Term::getOpTerm() returns an OpTerm and the compiler complains
if OpTerm is not defined earlier. Simply moving the declaration is easier/cleaner than
forward declaring within the same file that it's declared.
* Fix mkTerm in datatypes-new.cpp example
* Use helper function for creating term from Kind to avoid nested API calls
* Rename: OpTerm->Op in API
* Update OpTerm->Op in examples/tests/parser
* Add case for APPLY_TESTER
* operator term -> operator
* Update src/api/cvc4cpp.h
Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>
* Comment comment suggestion
Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>
* Add not-null checks and implement Op from a single Kind constructor
* Undo sed mistake for OpTerm replacement
* Add 'd_' prefix to member vars
* Fix comment and remove old commented-out code
* Formatting
* Revert "Formatting"
This reverts commit d1d5fc1fb71496daeba668e97cad84c213200ba9.
* More fixes for sed mistakes
* Minor formatting
* Undo changes in CVC parser
* Add isIndexed and prefix with d_
* Create helper function for isIndexed to avoid calling API functions in other API functions
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/smt2.cpp | 51 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 10 |
2 files changed, 28 insertions, 33 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( diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index ec7e2071a..215f565cd 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -75,7 +75,7 @@ class Smt2 : public Parser std::unordered_map<std::string, Kind> operatorKindMap; /** * Maps indexed symbols to the kind of the operator (e.g. "extract" to - * BITVECTOR_EXTRACT_OP). + * BITVECTOR_EXTRACT). */ std::unordered_map<std::string, api::Kind> d_indexedOpKindMap; std::pair<Expr, std::string> d_lastNamedTerm; @@ -106,7 +106,7 @@ class Smt2 : public Parser * 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_OP) + * @param opKind The kind of the operator term (e.g. BITVECTOR_EXTRACT) * @param name The name of the symbol (e.g. "extract") */ void addIndexedOperator(Kind tKind, @@ -141,8 +141,8 @@ class Smt2 : public Parser * @return The operator term corresponding to the indexed operator or a parse * error if the name is not valid. */ - api::OpTerm mkIndexedOp(const std::string& name, - const std::vector<uint64_t>& numerals); + api::Op mkIndexedOp(const std::string& name, + const std::vector<uint64_t>& numerals); /** * Returns the expression that name should be interpreted as. @@ -214,7 +214,7 @@ class Smt2 : public Parser const std::vector<Expr>& guards, const std::vector<Expr>& heads, Expr body); - + /** * Class for creating instances of `SynthFunCommand`s. Creating an instance * of this class pushes the scope, destroying it pops the scope. |