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

3 files changed, 37 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
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 835ecd880..9dd913ea2 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -53,6 +53,7 @@ class SolverBlack : public CxxTest::TestSuite
   void testMkBitVector();
   void testMkBoolean();
   void testMkConst();
+  void testMkConstArray();
   void testMkEmptySet();
   void testMkFalse();
   void testMkFloatingPoint();
@@ -755,6 +756,20 @@ void SolverBlack::testMkConst()
   TS_ASSERT_THROWS(d_solver->mkConst(Sort(), "a"), CVC4ApiException&);
 }
 
+void SolverBlack::testMkConstArray()
+{
+  Sort intSort = d_solver->getIntegerSort();
+  Sort arrSort = d_solver->mkArraySort(intSort, intSort);
+  Term zero = d_solver->mkReal(0);
+  Term constArr = d_solver->mkConstArray(arrSort, zero);
+
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkConstArray(arrSort, zero));
+  TS_ASSERT_THROWS(d_solver->mkConstArray(arrSort, Term()), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkConstArray(arrSort, d_solver->mkBitVector(1, 1)),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkConstArray(intSort, zero), CVC4ApiException&);
+}
+
 void SolverBlack::testDeclareDatatype()
 {
   DatatypeConstructorDecl cons("cons");