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/api/cvc4cppkind.h | |
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/api/cvc4cppkind.h')
-rw-r--r-- | src/api/cvc4cppkind.h | 371 |
1 files changed, 165 insertions, 206 deletions
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index 1f2a36676..bb2700706 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -143,26 +143,24 @@ enum CVC4_PUBLIC Kind : int32_t */ CHOICE, /** - * Chained operation. + * Chained operator. + * Parameters: 1 + * -[1]: Kind of the binary operation + * Create with: + * mkOp(Kind opkind, Kind kind) + + * Apply chained operation. * Parameters: n > 1 - * -[1]: Term of kind CHAIN_OP (represents a binary op) + * -[1]: Op of kind CHAIN (represents a binary op) * -[2]..[n]: Arguments to that operator * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * mkTerm(Op op, Term child1, Term child2) + * mkTerm(Op op, Term child1, Term child2, Term child3) + * mkTerm(Op op, const std::vector<Term>& children) * Turned into a conjunction of binary applications of the operator on * adjoining parameters. */ CHAIN, - /** - * Chained operator. - * Parameters: 1 - * -[1]: Kind of the binary operation - * Create with: - * mkOpTerm(Kind opkind, Kind kind) - */ - CHAIN_OP, /* Boolean --------------------------------------------------------------- */ @@ -382,16 +380,6 @@ enum CVC4_PUBLIC Kind : int32_t */ ABS, /** - * Divisibility-by-k predicate. - * Parameters: 2 - * -[1]: DIVISIBLE_OP Term - * -[2]: Integer Term - * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) - */ - DIVISIBLE, - /** * Arithmetic power. * Parameters: 2 * -[1]..[2]: Terms of sort Integer, Real @@ -517,9 +505,17 @@ enum CVC4_PUBLIC Kind : int32_t * Parameter: 1 * -[1]: The k to divide by (sort Integer) * Create with: - * mkOpTerm(Kind kind, uint32_t param) + * mkOp(Kind kind, uint32_t param) + * + * Apply divisibility-by-k predicate. + * Parameters: 2 + * -[1]: Op of kind DIVISIBLE + * -[2]: Integer Term + * Create with: + * mkTerm(Op op, Term child1, Term child2) + * mkTerm(Op op, const std::vector<Term>& children) */ - DIVISIBLE_OP, + DIVISIBLE, /** * Multiple-precision rational constant. * Parameters: @@ -973,9 +969,6 @@ enum CVC4_PUBLIC Kind : int32_t /* term to be treated as a variable. used for eager bit-blasting Ackermann * expansion of bvurem (internal-only symbol) */ BITVECTOR_ACKERMANIZE_UREM, - /* operator for the bit-vector boolean bit extract. - * One parameter, parameter is the index of the bit to extract */ - BITVECTOR_BITOF_OP, #endif /** * Operator for bit-vector extract (from index 'high' to 'low'). @@ -983,125 +976,115 @@ enum CVC4_PUBLIC Kind : int32_t * -[1]: The 'high' index * -[2]: The 'low' index * Create with: - * mkOpTerm(Kind kind, uint32_t param, uint32_t param) + * mkOp(Kind kind, uint32_t param, uint32_t param) + * + * Apply bit-vector extract. + * Parameters: 2 + * -[1]: Op of kind BITVECTOR_EXTRACT + * -[2]: Term of bit-vector sort + * Create with: + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ - BITVECTOR_EXTRACT_OP, + BITVECTOR_EXTRACT, /** * Operator for bit-vector repeat. * Parameter 1: * -[1]: Number of times to repeat a given bit-vector * Create with: - * mkOpTerm(Kind kind, uint32_t param). + * mkOp(Kind kind, uint32_t param). + * + * Apply bit-vector repeat. + * Parameters: 2 + * -[1]: Op of kind BITVECTOR_REPEAT + * -[2]: Term of bit-vector sort + * Create with: + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ - BITVECTOR_REPEAT_OP, + BITVECTOR_REPEAT, /** * Operator for bit-vector zero-extend. * Parameter 1: * -[1]: Number of bits by which a given bit-vector is to be extended * Create with: - * mkOpTerm(Kind kind, uint32_t param). + * mkOp(Kind kind, uint32_t param). + * + * Apply bit-vector zero-extend. + * Parameters: 2 + * -[1]: Op of kind BITVECTOR_ZERO_EXTEND + * -[2]: Term of bit-vector sort + * Create with: + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ - BITVECTOR_ZERO_EXTEND_OP, + BITVECTOR_ZERO_EXTEND, /** * Operator for bit-vector sign-extend. * Parameter 1: * -[1]: Number of bits by which a given bit-vector is to be extended * Create with: - * mkOpTerm(Kind kind, uint32_t param). - */ - BITVECTOR_SIGN_EXTEND_OP, - /** - * Operator for bit-vector rotate left. - * Parameter 1: - * -[1]: Number of bits by which a given bit-vector is to be rotated + * mkOp(Kind kind, uint32_t param). + * + * Apply bit-vector sign-extend. + * Parameters: 2 + * -[1]: Op of kind BITVECTOR_SIGN_EXTEND + * -[2]: Term of bit-vector sort * Create with: - * mkOpTerm(Kind kind, uint32_t param). + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ - BITVECTOR_ROTATE_LEFT_OP, + BITVECTOR_SIGN_EXTEND, /** - * Operator for bit-vector rotate right. + * Operator for bit-vector rotate left. * Parameter 1: * -[1]: Number of bits by which a given bit-vector is to be rotated * Create with: - * mkOpTerm(Kind kind, uint32_t param). - */ - BITVECTOR_ROTATE_RIGHT_OP, -#if 0 - /* bit-vector boolean bit extract. - * first parameter is a BITVECTOR_BITOF_OP, second is a bit-vector term */ - BITVECTOR_BITOF, -#endif - /* Bit-vector extract. - * Parameters: 2 - * -[1]: BITVECTOR_EXTRACT_OP Term - * -[2]: Term of bit-vector sort - * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) - */ - BITVECTOR_EXTRACT, - /* Bit-vector repeat. - * Parameters: 2 - * -[1]: BITVECTOR_REPEAT_OP Term - * -[2]: Term of bit-vector sort - * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) - */ - BITVECTOR_REPEAT, - /* Bit-vector zero-extend. - * Parameters: 2 - * -[1]: BITVECTOR_ZERO_EXTEND_OP Term - * -[2]: Term of bit-vector sort - * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) - */ - BITVECTOR_ZERO_EXTEND, - /* Bit-vector sign-extend. - * Parameters: 2 - * -[1]: BITVECTOR_SIGN_EXTEND_OP Term - * -[2]: Term of bit-vector sort - * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) - */ - BITVECTOR_SIGN_EXTEND, - /* Bit-vector rotate left. + * mkOp(Kind kind, uint32_t param). + * + * Apply bit-vector rotate left. * Parameters: 2 - * -[1]: BITVECTOR_ROTATE_LEFT_OP Term + * -[1]: Op of kind BITVECTOR_ROTATE_LEFT * -[2]: Term of bit-vector sort * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ BITVECTOR_ROTATE_LEFT, /** - * Bit-vector rotate right. + * Operator for bit-vector rotate right. + * Parameter 1: + * -[1]: Number of bits by which a given bit-vector is to be rotated + * Create with: + * mkOp(Kind kind, uint32_t param). + * + * Apply bit-vector rotate right. * Parameters: 2 - * -[1]: BITVECTOR_ROTATE_RIGHT_OP Term + * -[1]: Op of kind BITVECTOR_ROTATE_RIGHT * -[2]: Term of bit-vector sort * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ BITVECTOR_ROTATE_RIGHT, +#if 0 + /* bit-vector boolean bit extract. */ + BITVECTOR_BITOF, +#endif /** * Operator for the conversion from Integer to bit-vector. * Parameter: 1 * -[1]: Size of the bit-vector to convert to * Create with: - * mkOpTerm(Kind kind, uint32_t param). - */ - INT_TO_BITVECTOR_OP, - /** - * Integer conversion to bit-vector. + * mkOp(Kind kind, uint32_t param). + * + * Apply integer conversion to bit-vector. * Parameters: 2 - * -[1]: INT_TO_BITVECTOR_OP Term + * -[1]: Op of kind INT_TO_BITVECTOR * -[2]: Integer term * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ INT_TO_BITVECTOR, /** @@ -1371,17 +1354,15 @@ enum CVC4_PUBLIC Kind : int32_t * -[1]: Exponent size * -[2]: Significand size * Create with: - * mkOpTerm(Kind kind, uint32_t param1, uint32_t param2) - */ - FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP, - /** + * mkOp(Kind kind, uint32_t param1, uint32_t param2) + * * Conversion from an IEEE-754 bit vector to floating-point. * Parameters: 2 - * -[1]: FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP Term + * -[1]: Op of kind FLOATINGPOINT_TO_FP_IEEE_BITVECTOR * -[2]: Term of sort FloatingPoint * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, /** @@ -1390,17 +1371,15 @@ enum CVC4_PUBLIC Kind : int32_t * -[1]: Exponent size * -[2]: Significand size * Create with: - * mkOpTerm(Kind kind, uint32_t param1, uint32_t param2) - */ - FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP, - /** + * mkOp(Kind kind, uint32_t param1, uint32_t param2) + * * Conversion between floating-point sorts. * Parameters: 2 - * -[1]: FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP Term + * -[1]: Op of kind FLOATINGPOINT_TO_FP_FLOATINGPOINT * -[2]: Term of sort FloatingPoint * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ FLOATINGPOINT_TO_FP_FLOATINGPOINT, /** @@ -1409,17 +1388,15 @@ enum CVC4_PUBLIC Kind : int32_t * -[1]: Exponent size * -[2]: Significand size * Create with: - * mkOpTerm(Kind kind, uint32_t param1, uint32_t param2) - */ - FLOATINGPOINT_TO_FP_REAL_OP, - /** + * mkOp(Kind kind, uint32_t param1, uint32_t param2) + * * Conversion from a real to floating-point. * Parameters: 2 - * -[1]: FLOATINGPOINT_TO_FP_REAL_OP Term + * -[1]: Op of kind FLOATINGPOINT_TO_FP_REAL * -[2]: Term of sort FloatingPoint * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ FLOATINGPOINT_TO_FP_REAL, /* @@ -1428,17 +1405,15 @@ enum CVC4_PUBLIC Kind : int32_t * -[1]: Exponent size * -[2]: Significand size * Create with: - * mkOpTerm(Kind kind, uint32_t param1, uint32_t param2) - */ - FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP, - /** + * mkOp(Kind kind, uint32_t param1, uint32_t param2) + * * Conversion from a signed bit vector to floating-point. * Parameters: 2 - * -[1]: FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP Term + * -[1]: Op of kind FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR * -[2]: Term of sort FloatingPoint * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, /** @@ -1447,17 +1422,15 @@ enum CVC4_PUBLIC Kind : int32_t * -[1]: Exponent size * -[2]: Significand size * Create with: - * mkOpTerm(Kind kind, uint32_t param1, uint32_t param2) - */ - FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP, - /** - * Operator for converting an unsigned bit vector to floating-point. + * mkOp(Kind kind, uint32_t param1, uint32_t param2) + * + * Converting an unsigned bit vector to floating-point. * Parameters: 2 - * -[1]: FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP Term + * -[1]: Op of kind FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR * -[2]: Term of sort FloatingPoint * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, /** @@ -1466,17 +1439,15 @@ enum CVC4_PUBLIC Kind : int32_t * -[1]: exponent size * -[2]: Significand size * Create with: - * mkOpTerm(Kind kind, uint32_t param1, uint32_t param2) - */ - FLOATINGPOINT_TO_FP_GENERIC_OP, - /** + * mkOp(Kind kind, uint32_t param1, uint32_t param2) + * * Generic conversion to floating-point, used in parsing only. * Parameters: 2 - * -[1]: FLOATINGPOINT_TO_FP_GENERIC_OP Term + * -[1]: Op of kind FLOATINGPOINT_TO_FP_GENERIC * -[2]: Term of sort FloatingPoint * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ FLOATINGPOINT_TO_FP_GENERIC, /** @@ -1484,17 +1455,15 @@ enum CVC4_PUBLIC Kind : int32_t * Parameters: 1 * -[1]: Size of the bit-vector to convert to * Create with: - * mkOpTerm(Kind kind, uint32_t param) - */ - FLOATINGPOINT_TO_UBV_OP, - /** + * mkOp(Kind kind, uint32_t param) + * * Conversion from a floating-point value to an unsigned bit vector. * Parameters: 2 - * -[1]: FLOATINGPOINT_TO_FP_TO_UBV_OP Term + * -[1]: Op of kind FLOATINGPOINT_TO_FP_TO_UBV * -[2]: Term of sort FloatingPoint * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ FLOATINGPOINT_TO_UBV, /** @@ -1502,18 +1471,16 @@ enum CVC4_PUBLIC Kind : int32_t * Parameters: 1 * -[1]: Size of the bit-vector to convert to * Create with: - * mkOpTerm(Kind kind, uint32_t param) - */ - FLOATINGPOINT_TO_UBV_TOTAL_OP, - /** + * mkOp(Kind kind, uint32_t param) + * * Conversion from a floating-point value to an unsigned bit vector * (defined for all inputs). * Parameters: 2 - * -[1]: FLOATINGPOINT_TO_FP_TO_UBV_TOTAL_OP Term + * -[1]: Op of kind FLOATINGPOINT_TO_FP_TO_UBV_TOTAL * -[2]: Term of sort FloatingPoint * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ FLOATINGPOINT_TO_UBV_TOTAL, /** @@ -1521,17 +1488,15 @@ enum CVC4_PUBLIC Kind : int32_t * Parameters: 1 * -[1]: Size of the bit-vector to convert to * Create with: - * mkOpTerm(Kind kind, uint32_t param) - */ - FLOATINGPOINT_TO_SBV_OP, - /** + * mkOp(Kind kind, uint32_t param) + * * Conversion from a floating-point value to a signed bit vector. * Parameters: 2 - * -[1]: FLOATINGPOINT_TO_FP_TO_SBV_OP Term + * -[1]: Op of kind FLOATINGPOINT_TO_FP_TO_SBV * -[2]: Term of sort FloatingPoint * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ FLOATINGPOINT_TO_SBV, /** @@ -1539,18 +1504,16 @@ enum CVC4_PUBLIC Kind : int32_t * Parameters: 1 * -[1]: Size of the bit-vector to convert to * Create with: - * mkOpTerm(Kind kind, uint32_t param) - */ - FLOATINGPOINT_TO_SBV_TOTAL_OP, - /** + * mkOp(Kind kind, uint32_t param) + * * Conversion from a floating-point value to a signed bit vector * (defined for all inputs). * Parameters: 2 - * -[1]: FLOATINGPOINT_TO_FP_TO_SBV_TOTAL_OP Term + * -[1]: Op of kind FLOATINGPOINT_TO_FP_TO_SBV_TOTAL * -[2]: Term of sort FloatingPoint * Create with: - * mkTerm(Term opTerm, Term child) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child) + * mkTerm(Op op, const std::vector<Term>& children) */ FLOATINGPOINT_TO_SBV_TOTAL, /** @@ -1578,8 +1541,8 @@ enum CVC4_PUBLIC Kind : int32_t * -[1]: Term of array sort * -[2]: Selection index * Create with: - * mkTerm(Term opTerm, Term child1, Term child2) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child1, Term child2) + * mkTerm(Op op, const std::vector<Term>& children) */ SELECT, /** @@ -1589,8 +1552,8 @@ enum CVC4_PUBLIC Kind : int32_t * -[2]: Store index * -[3]: Term to store at the index * Create with: - * mkTerm(Term opTerm, Term child1, Term child2, Term child3) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child1, Term child2, Term child3) + * mkTerm(Op op, const std::vector<Term>& children) */ STORE, /** @@ -1599,8 +1562,8 @@ enum CVC4_PUBLIC Kind : int32_t * -[1]: Array sort * -[2]: Term representing a constant * Create with: - * mkTerm(Term opTerm, Term child1, Term child2) - * mkTerm(Term opTerm, const std::vector<Term>& children) + * mkTerm(Op op, Term child1, Term child2) + * mkTerm(Op op, const std::vector<Term>& children) * * Note: We currently support the creation of constant arrays, but under some * conditions when there is a chain of equalities connecting two constant @@ -1623,32 +1586,32 @@ enum CVC4_PUBLIC Kind : int32_t /** * Constructor application. * Paramters: n > 0 - * -[1]: Constructor (operator term) + * -[1]: Constructor (operator) * -[2]..[n]: Parameters to the constructor * Create with: - * mkTerm(Kind kind, OpTerm opTerm) - * mkTerm(Kind kind, OpTerm opTerm, Term child) - * mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2) - * mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, OpTerm opTerm, const std::vector<Term>& children) + * mkTerm(Kind kind, Op op) + * mkTerm(Kind kind, Op op, Term child) + * mkTerm(Kind kind, Op op, Term child1, Term child2) + * mkTerm(Kind kind, Op op, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, Op op, const std::vector<Term>& children) */ APPLY_CONSTRUCTOR, /** * Datatype selector application. * Parameters: 1 - * -[1]: Selector (operator term) + * -[1]: Selector (operator) * -[2]: Datatype term (undefined if mis-applied) * Create with: - * mkTerm(Kind kind, OpTerm opTerm, Term child) + * mkTerm(Kind kind, Op op, Term child) */ APPLY_SELECTOR, /** * Datatype selector application. * Parameters: 1 - * -[1]: Selector (operator term) + * -[1]: Selector (operator) * -[2]: Datatype term (defined rigidly if mis-applied) * Create with: - * mkTerm(Kind kind, OpTerm opTerm, Term child) + * mkTerm(Kind kind, Op op, Term child) */ APPLY_SELECTOR_TOTAL, /** @@ -1674,18 +1637,16 @@ enum CVC4_PUBLIC Kind : int32_t * Parameters: 1 * -[1]: Index of the tuple to be updated * Create with: - * mkOpTerm(Kind kind, uint32_t param) - */ - TUPLE_UPDATE_OP, - /** - * Tuple update. + * mkOp(Kind kind, uint32_t param) + * + * Apply tuple update. * Parameters: 3 - * -[1]: TUPLE_UPDATE_OP (which references an index) + * -[1]: Op of kind TUPLE_UPDATE (which references an index) * -[2]: Tuple * -[3]: Element to store in the tuple at the given index * Create with: - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector<Term>& children) + * mkTerm(Op op, Term child1, Term child2) + * mkTerm(Op op, const std::vector<Term>& children) */ TUPLE_UPDATE, /** @@ -1693,18 +1654,16 @@ enum CVC4_PUBLIC Kind : int32_t * Parameters: 1 * -[1]: Name of the field to be updated * Create with: - * mkOpTerm(Kind kind, const std::string& param) - */ - RECORD_UPDATE_OP, - /** + * mkOp(Kind kind, const std::string& param) + * * Record update. * Parameters: 3 - * -[1]: RECORD_UPDATE_OP Term (which references a field) + * -[1]: Op of kind RECORD_UPDATE (which references a field) * -[2]: Record term to update * -[3]: Element to store in the record in the given field * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector<Term>& children) + * mkTerm(Op op, Term child1, Term child2) + * mkTerm(Op op,, const std::vector<Term>& children) */ RECORD_UPDATE, #if 0 |