diff options
Diffstat (limited to 'src/api')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 1 | ||||
| -rw-r--r-- | src/api/cvc4cppkind.h | 17 |
2 files changed, 18 insertions, 0 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 2fd5cb444..cebba9b5e 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -214,6 +214,7 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ {SELECT, CVC4::Kind::SELECT}, {STORE, CVC4::Kind::STORE}, {CONST_ARRAY, CVC4::Kind::STORE_ALL}, + {EQ_RANGE, CVC4::Kind::EQ_RANGE}, /* Datatypes ----------------------------------------------------------- */ {APPLY_SELECTOR, CVC4::Kind::APPLY_SELECTOR}, {APPLY_CONSTRUCTOR, CVC4::Kind::APPLY_CONSTRUCTOR}, 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, |