Add a method for retrieving base of a constant array through API (#4494)

8 files changed, 45 insertions, 6 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 734fcddae..164df0631 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -213,7 +213,7 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{
     /* Arrays -------------------------------------------------------------- */
     {SELECT, CVC4::Kind::SELECT},
     {STORE, CVC4::Kind::STORE},
-    {STORE_ALL, CVC4::Kind::STORE_ALL},
+    {CONST_ARRAY, CVC4::Kind::STORE_ALL},
     /* Datatypes ----------------------------------------------------------- */
     {APPLY_SELECTOR, CVC4::Kind::APPLY_SELECTOR},
     {APPLY_CONSTRUCTOR, CVC4::Kind::APPLY_CONSTRUCTOR},
@@ -479,7 +479,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
         /* Arrays ---------------------------------------------------------- */
         {CVC4::Kind::SELECT, SELECT},
         {CVC4::Kind::STORE, STORE},
-        {CVC4::Kind::STORE_ALL, STORE_ALL},
+        {CVC4::Kind::STORE_ALL, CONST_ARRAY},
         /* Datatypes ------------------------------------------------------- */
         {CVC4::Kind::APPLY_SELECTOR, APPLY_SELECTOR},
         {CVC4::Kind::APPLY_CONSTRUCTOR, APPLY_CONSTRUCTOR},
@@ -1492,6 +1492,15 @@ bool Term::isConst() const
   return d_expr->isConst();
 }
 
+Term Term::getConstArrayBase() const
+{
+  CVC4_API_CHECK_NOT_NULL;
+  // CONST_ARRAY kind maps to STORE_ALL internal kind
+  CVC4_API_CHECK(d_expr->getKind() == CVC4::Kind::STORE_ALL)
+      << "Expecting a CONST_ARRAY Term when calling getConstArrayBase()";
+  return Term(d_solver, d_expr->getConst<ArrayStoreAll>().getExpr());
+}
+
 Term Term::notTerm() const
 {
   CVC4_API_CHECK_NOT_NULL;
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 855ba4400..73e3ed856 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -900,6 +900,13 @@ class CVC4_PUBLIC Term
   bool isConst() const;
 
   /**
+   *  Return the base (element stored at all indices) of a constant array
+   *  throws an exception if the kind is not CONST_ARRAY
+   *  @return the base value
+   */
+  Term getConstArrayBase() const;
+
+  /**
    * Boolean negation.
    * @return the Boolean negation of this term
    */
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index e084daf1e..02f13310a 100644
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -1504,7 +1504,7 @@ enum CVC4_PUBLIC Kind : int32_t
    * conditions when there is a chain of equalities connecting two constant
    * arrays, the solver doesn't know what to do and aborts (Issue #1667).
    */
-  STORE_ALL,
+  CONST_ARRAY,
 #if 0
   /* array table function (internal-only symbol) */
   ARR_TABLE_FUN,
diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index 1e0b9893b..cc998306d 100644
--- a/src/api/python/cvc4.pxd
+++ b/src/api/python/cvc4.pxd
@@ -250,6 +250,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         bint hasOp() except +
         Op getOp() except +
         bint isNull() except +
+        Term getConstArrayBase() except +
         Term notTerm() except +
         Term andTerm(const Term& t) except +
         Term orTerm(const Term& t) except +
diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi
index 827c53ef4..9dd9c1cde 100644
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc4.pxi
@@ -1096,6 +1096,11 @@ cdef class Term:
     def isNull(self):
         return self.cterm.isNull()
 
+    def getConstArrayBase(self):
+        cdef Term term = Term()
+        term.cterm = self.cterm.getConstArrayBase()
+        return term
+
     def notTerm(self):
         cdef Term term = Term()
         term.cterm = self.cterm.notTerm()
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 62bf7e974..ec3e874df 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1990,7 +1990,7 @@ qualIdentifier[CVC4::ParseOp& p]
   | LPAREN_TOK AS_TOK
     ( CONST_TOK sortSymbol[type, CHECK_DECLARED]
       {
-        p.d_kind = api::STORE_ALL;
+        p.d_kind = api::CONST_ARRAY;
         PARSER_STATE->parseOpApplyTypeAscription(p, type);
       }
     | identifier[p]
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 608e47a6b..3f25e3776 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1535,7 +1535,7 @@ void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type)
   Debug("parser") << "parseOpApplyTypeAscription : " << p << " " << type
                   << std::endl;
   // (as const (Array T1 T2))
-  if (p.d_kind == api::STORE_ALL)
+  if (p.d_kind == api::CONST_ARRAY)
   {
     if (!type.isArray())
     {
@@ -1701,7 +1701,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
   // Second phase: apply the arguments to the parse op
   const Options& opts = d_solver->getExprManager()->getOptions();
   // handle special cases
-  if (p.d_kind == api::STORE_ALL && !p.d_type.isNull())
+  if (p.d_kind == api::CONST_ARRAY && !p.d_type.isNull())
   {
     if (args.size() != 1)
     {
diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h
index a3cbd028f..56d13fc63 100644
--- a/test/unit/api/term_black.h
+++ b/test/unit/api/term_black.h
@@ -43,6 +43,7 @@ class TermBlack : public CxxTest::TestSuite
   void testTermChildren();
   void testSubstitute();
   void testIsConst();
+  void testConstArray();
 
  private:
   Solver d_solver;
@@ -752,3 +753,19 @@ void TermBlack::testIsConst()
   Term tnull;
   TS_ASSERT_THROWS(tnull.isConst(), CVC4ApiException&);
 }
+
+void TermBlack::testConstArray()
+{
+  Sort intsort = d_solver.getIntegerSort();
+  Sort arrsort = d_solver.mkArraySort(intsort, intsort);
+  Term a = d_solver.mkConst(arrsort, "a");
+  Term one = d_solver.mkReal(1);
+  Term constarr = d_solver.mkConstArray(arrsort, one);
+
+  TS_ASSERT(!a.isConst());
+  TS_ASSERT(constarr.isConst());
+
+  TS_ASSERT_EQUALS(constarr.getKind(), CONST_ARRAY);
+  TS_ASSERT_EQUALS(constarr.getConstArrayBase(), one);
+  TS_ASSERT_THROWS(a.getConstArrayBase(), CVC4ApiException&);
+}