diff options
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 198f51024..cf9074129 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -1505,6 +1505,23 @@ enum CVC4_PUBLIC Kind : int32_t * arrays, the solver doesn't know what to do and aborts (Issue #1667). */ CONST_ARRAY, + /** + * Equality over arrays a and b over a given range [i,j], i.e., + * \forall k . i <= k <= j --> a[k] = b[k] + * + * Parameters: 4 + * -[1]: First array + * -[2]: Second array + * -[3]: Lower bound of range (inclusive) + * -[4]: Uppper bound of range (inclusive) + * Create with: + * mkTerm(Op op, const std::vector<Term>& children) + * + * Note: We currently support the creation of array equalities over index + * types bit-vector, floating-point, integer and real. Option --arrays-exp is + * required to support this operator. + */ + EQ_RANGE, #if 0 /* array table function (internal-only symbol) */ ARR_TABLE_FUN, |