From: makaimann <makaim@stanford.edu>
Date: Thu, 19 Sep 2019 02:34:22 +0000 (-0700)
Subject: Add support for creating constant arrays to the new C++ API (#3296)
X-Git-Tag: cvc5-1.0.0~3939
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cfe4f59c0a10d49a35b9f59bb2fd6ab7d224e53d;p=cvc5.git

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