From a2fc412f22552ae0e8f9c36650d1de2d362638dd Mon Sep 17 00:00:00 2001 From: makaimann Date: Thu, 4 Jun 2020 18:21:37 -0700 Subject: [PATCH] Add a method for retrieving base of a constant array through API (#4494) --- src/api/cvc4cpp.cpp | 13 +++++++++++-- src/api/cvc4cpp.h | 7 +++++++ src/api/cvc4cppkind.h | 2 +- src/api/python/cvc4.pxd | 1 + src/api/python/cvc4.pxi | 5 +++++ src/parser/smt2/Smt2.g | 2 +- src/parser/smt2/smt2.cpp | 4 ++-- test/unit/api/term_black.h | 17 +++++++++++++++++ 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 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 /* 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().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 @@ -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 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& 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&); +} -- 2.30.2