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

1 files changed, 15 insertions, 0 deletions

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");