diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2019-01-29 11:47:04 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-01-29 11:47:04 -0800 |
commit | d4870775e67c7878c32c17f10b1217c14dc5869b (patch) | |
tree | 8e2bcd1a731eab54041724bb9310e1c7aaaf3e4c /src/api/cvc4cppkind.h | |
parent | 1eaf6cf987fa1452528dc0598ca7235be735ba3b (diff) |
New C++ API: Fix checks for mkTerm. (#2820)
This required fixing the OpTerm handling for mkTerm functions in the API.
Diffstat (limited to 'src/api/cvc4cppkind.h')
-rw-r--r-- | src/api/cvc4cppkind.h | 26 |
1 files changed, 14 insertions, 12 deletions
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index a7f6926bb..4e69ddfe1 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -1649,30 +1649,32 @@ enum CVC4_PUBLIC Kind : int32_t /** * Constructor application. * Paramters: n > 0 - * -[1]: Constructor + * -[1]: Constructor (operator term) * -[2]..[n]: Parameters to the constructor * Create with: - * mkTerm(Kind kind) - * mkTerm(Kind kind, Term child) - * 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(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) */ - APPLY_SELECTOR, + APPLY_CONSTRUCTOR, /** * Datatype selector application. * Parameters: 1 - * -[1]: Datatype term (undefined if mis-applied) + * -[1]: Selector (operator term) + * -[2]: Datatype term (undefined if mis-applied) * Create with: - * mkTerm(Kind kind, Term child) + * mkTerm(Kind kind, OpTerm opTerm, Term child) */ - APPLY_CONSTRUCTOR, + APPLY_SELECTOR, /** * Datatype selector application. * Parameters: 1 - * -[1]: Datatype term (defined rigidly if mis-applied) + * -[1]: Selector (operator term) + * -[2]: Datatype term (defined rigidly if mis-applied) * Create with: - * mkTerm(Kind kind, Term child) + * mkTerm(Kind kind, OpTerm opTerm, Term child) */ APPLY_SELECTOR_TOTAL, /** |