diff options
author | makaimann <makaim@stanford.edu> | 2019-09-18 19:34:22 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-09-18 19:34:22 -0700 |
commit | cfe4f59c0a10d49a35b9f59bb2fd6ab7d224e53d (patch) | |
tree | f6bdaca320b09f11b2ac92acac86b2a1b60486c2 /src | |
parent | a9c40f60e4b36494e10520dcc3a3985b4700342f (diff) |
Add support for creating constant arrays to the new C++ API (#3296)
* Add support for constant arrays to new C++ API
* Fix macro usage in unit test
* Add not null check
* Add test for null term
* Formatting
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 |