diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-10 15:51:25 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-10 13:51:25 -0700 |
| commit | 7e9b3dfa40f0297bdb005f6c802443ebb3b8cad1 (patch) | |
| tree | be4db1f4485a4722a7c816edee708c57d676b5ba /src/api/cvc4cppkind.h | |
| parent | 1dbc8aa695772daf2c83d10a7adb8123f97fa16f (diff) | |
Front end support for integer AND (#4717)
Diffstat (limited to 'src/api/cvc4cppkind.h')
| -rw-r--r-- | src/api/cvc4cppkind.h | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index b3e88c98c..1f23d0e8d 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -319,6 +319,23 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, const std::vector<Term>& children) */ MULT, + /** + * Operator for Integer AND + * Parameter: 1 + * -[1]: Size of the bit-vector that determines the semantics of the IAND + * Create with: + * mkOp(Kind kind, uint32_t param). + * + * Apply integer conversion to bit-vector. + * Parameters: 2 + * -[1]: Op of kind IAND + * -[2]: Integer term + * -[3]: Integer term + * Create with: + * mkTerm(Op op, Term child1, Term child2) + * mkTerm(Op op, const std::vector<Term>& children) + */ + IAND, #if 0 /* Synonym for MULT. */ NONLINEAR_MULT, |