diff options
Diffstat (limited to 'src/api/cvc4cpp.h')
| -rw-r--r-- | src/api/cvc4cpp.h | 9 |
1 files changed, 9 insertions, 0 deletions
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 |