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

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 734fcddaeac33caab7fd5d8d1fc18696361a5e47..164df06314aa16e40a77ce7f6bec34f9e4f50508 100644 (file)
--- 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 855ba440000c2ed062a3a1f5682d4e30562f24de..73e3ed856792a156137688d609970bbd58f594da 100644 (file)
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -899,6 +899,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 e084daf1e26a9d8a09da7478209128b98652e417..02f13310aa3af78d7e9e9b3cc3e6c96a257ae0cb 100644 (file)
--- 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 1e0b9893b6b625c3a0cd3a6fe41663b8f203efeb..cc998306d7fbfdfb782972e3be95d6d9fc45355b 100644 (file)
--- 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 827c53ef41b3ba933c51381b162be77698b2c51d..9dd9c1cde26cff4a22aed63abb1ff1fce91ded42 100644 (file)
--- 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 62bf7e974e255c3547232b8aeb39ffbd4f87e2d6..ec3e874df1f448660f38ac08af667c63cb2d27ad 100644 (file)
--- 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 608e47a6b4901ef521c92d18c0ce947fb642d20e..3f25e3776eb4613a9a5128febe34920263f1061e 100644 (file)
--- 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 a3cbd028f14c9e4f2e8ac0c378659db7f0f8d632..56d13fc63b1f4dc63f6e530cb3f986283467564c 100644 (file)
--- 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&);
+}