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

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 904da0f105181ff1b63ceebd0183712ccdc9ec7b..6a6088007158ab66f0b3d7f184c204212109e827 100644 (file)
--- 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 67e8bb6e7ccd955331fb7a1da6a64429b225369e..7fee35afd57d4adf4cce6ca96c62e1a6c96f4a14 100644 (file)
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -2096,6 +2096,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.

diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 835ecd88007ebe812e40b31bdcc9202180b6fca8..9dd913ea26cf9f26436dfa23830f3099e6b0c887 100644 (file)
--- 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");