diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 13 | ||||
| -rw-r--r-- | src/api/cvc4cpp.h | 9 |
2 files changed, 22 insertions, 0 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 904da0f10..6a6088007 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -2555,6 +2555,19 @@ Term Solver::mkBitVector(uint32_t size, std::string& s, uint32_t base) const CVC4_API_SOLVER_TRY_CATCH_END; } +Term Solver::mkConstArray(Sort sort, Term val) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_NOT_NULL(val); + CVC4_API_CHECK(sort.isArray()) << "Not an array sort."; + CVC4_API_CHECK(sort.getArrayElementSort() == val.getSort()) + << "Value does not match element sort."; + Term res = mkValHelper<CVC4::ArrayStoreAll>( + CVC4::ArrayStoreAll(*sort.d_type, *val.d_expr)); + return res; + CVC4_API_SOLVER_TRY_CATCH_END; +} + Term Solver::mkPosInf(uint32_t exp, uint32_t sig) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 67e8bb6e7..7fee35afd 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -2097,6 +2097,15 @@ class CVC4_PUBLIC Solver Term mkBitVector(uint32_t size, std::string& s, uint32_t base) const; /** + * Create a constant array with the provided constant value stored at every + * index + * @param sort the sort of the constant array (must be an array sort) + * @param val the constant value to store (must match the sort's element sort) + * @return the constant array term + */ + Term mkConstArray(Sort sort, Term val) const; + + /** * Create a positive infinity floating-point constant. Requires CVC4 to be * compiled with SymFPU support. * @param exp Number of bits in the exponent |