diff options
Diffstat (limited to 'src/api/cpp')
-rw-r--r-- | src/api/cpp/cvc5.cpp | 116 | ||||
-rw-r--r-- | src/api/cpp/cvc5.h | 29 | ||||
-rw-r--r-- | src/api/cpp/cvc5_kind.h | 56 |
3 files changed, 109 insertions, 92 deletions
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 6ee1409d6..18db5d5ab 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -243,8 +243,7 @@ const static std::unordered_map<Kind, cvc5::Kind> s_kinds{ {APPLY_SELECTOR, cvc5::Kind::APPLY_SELECTOR}, {APPLY_CONSTRUCTOR, cvc5::Kind::APPLY_CONSTRUCTOR}, {APPLY_TESTER, cvc5::Kind::APPLY_TESTER}, - {TUPLE_UPDATE, cvc5::Kind::TUPLE_UPDATE}, - {RECORD_UPDATE, cvc5::Kind::RECORD_UPDATE}, + {APPLY_UPDATER, cvc5::Kind::APPLY_UPDATER}, {DT_SIZE, cvc5::Kind::DT_SIZE}, {TUPLE_PROJECT, cvc5::Kind::TUPLE_PROJECT}, /* Separation Logic ---------------------------------------------------- */ @@ -550,10 +549,7 @@ const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction> {cvc5::Kind::APPLY_CONSTRUCTOR, APPLY_CONSTRUCTOR}, {cvc5::Kind::APPLY_SELECTOR_TOTAL, INTERNAL_KIND}, {cvc5::Kind::APPLY_TESTER, APPLY_TESTER}, - {cvc5::Kind::TUPLE_UPDATE_OP, TUPLE_UPDATE}, - {cvc5::Kind::TUPLE_UPDATE, TUPLE_UPDATE}, - {cvc5::Kind::RECORD_UPDATE_OP, RECORD_UPDATE}, - {cvc5::Kind::RECORD_UPDATE, RECORD_UPDATE}, + {cvc5::Kind::APPLY_UPDATER, APPLY_UPDATER}, {cvc5::Kind::DT_SIZE, DT_SIZE}, {cvc5::Kind::TUPLE_PROJECT, TUPLE_PROJECT}, /* Separation Logic ------------------------------------------------ */ @@ -661,8 +657,7 @@ const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction> /* Set of kinds for indexed operators */ const static std::unordered_set<Kind> s_indexed_kinds( - {RECORD_UPDATE, - DIVISIBLE, + {DIVISIBLE, IAND, BITVECTOR_REPEAT, BITVECTOR_ZERO_EXTEND, @@ -672,7 +667,6 @@ const static std::unordered_set<Kind> s_indexed_kinds( INT_TO_BITVECTOR, FLOATINGPOINT_TO_UBV, FLOATINGPOINT_TO_SBV, - TUPLE_UPDATE, BITVECTOR_EXTRACT, FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, FLOATINGPOINT_TO_FP_FLOATINGPOINT, @@ -718,7 +712,8 @@ bool isDefinedKind(Kind k) { return k > UNDEFINED_KIND && k < LAST_KIND; } bool isApplyKind(cvc5::Kind k) { return (k == cvc5::Kind::APPLY_UF || k == cvc5::Kind::APPLY_CONSTRUCTOR - || k == cvc5::Kind::APPLY_SELECTOR || k == cvc5::Kind::APPLY_TESTER); + || k == cvc5::Kind::APPLY_SELECTOR || k == cvc5::Kind::APPLY_TESTER + || k == cvc5::Kind::APPLY_UPDATER); } #ifdef CVC5_ASSERTIONS @@ -1194,6 +1189,15 @@ bool Sort::isTester() const CVC5_API_TRY_CATCH_END; } +bool Sort::isUpdater() const +{ + CVC5_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return d_type->isUpdater(); + //////// + CVC5_API_TRY_CATCH_END; +} + bool Sort::isFunction() const { CVC5_API_TRY_CATCH_BEGIN; @@ -1852,7 +1856,6 @@ size_t Op::getNumIndices() const switch (k) { case DIVISIBLE: size = 1; break; - case RECORD_UPDATE: size = 1; break; case BITVECTOR_REPEAT: size = 1; break; case BITVECTOR_ZERO_EXTEND: size = 1; break; case BITVECTOR_SIGN_EXTEND: size = 1; break; @@ -1862,7 +1865,6 @@ size_t Op::getNumIndices() const case IAND: size = 1; break; case FLOATINGPOINT_TO_UBV: size = 1; break; case FLOATINGPOINT_TO_SBV: size = 1; break; - case TUPLE_UPDATE: size = 1; break; case REGEXP_REPEAT: size = 1; break; case BITVECTOR_EXTRACT: size = 2; break; case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: size = 2; break; @@ -1892,12 +1894,10 @@ std::string Op::getIndices() const CVC5_API_CHECK(!d_node->isNull()) << "Expecting a non-null internal expression. This Op is not indexed."; Kind k = intToExtKind(d_node->getKind()); - CVC5_API_CHECK(k == DIVISIBLE || k == RECORD_UPDATE) - << "Can't get string index from" - << " kind " << kindToString(k); + CVC5_API_CHECK(k == DIVISIBLE) << "Can't get string index from" + << " kind " << kindToString(k); //////// all checks before this line - return k == DIVISIBLE ? d_node->getConst<Divisible>().k.toString() - : d_node->getConst<RecordUpdate>().getField(); + return d_node->getConst<Divisible>().k.toString(); //////// CVC5_API_TRY_CATCH_END; } @@ -1938,7 +1938,6 @@ uint32_t Op::getIndices() const case FLOATINGPOINT_TO_SBV: i = d_node->getConst<FloatingPointToSBV>().d_bv_size.d_size; break; - case TUPLE_UPDATE: i = d_node->getConst<TupleUpdate>().getIndex(); break; case REGEXP_REPEAT: i = d_node->getConst<RegExpRepeat>().d_repeatAmount; break; @@ -3062,6 +3061,15 @@ Term DatatypeSelector::getSelectorTerm() const //////// CVC5_API_TRY_CATCH_END; } +Term DatatypeSelector::getUpdaterTerm() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + return Term(d_solver, d_stor->getUpdater()); + //////// + CVC5_API_TRY_CATCH_END; +} Sort DatatypeSelector::getRangeSort() const { @@ -3424,7 +3432,17 @@ Term Datatype::getConstructorTerm(const std::string& name) const CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; //////// all checks before this line - return getConstructor(name).getConstructorTerm(); + return getConstructorForName(name).getConstructorTerm(); + //////// + CVC5_API_TRY_CATCH_END; +} + +DatatypeSelector Datatype::getSelector(const std::string& name) const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + return getSelectorForName(name); //////// CVC5_API_TRY_CATCH_END; } @@ -3579,6 +3597,30 @@ DatatypeConstructor Datatype::getConstructorForName( return DatatypeConstructor(d_solver, (*d_dtype)[index]); } +DatatypeSelector Datatype::getSelectorForName(const std::string& name) const +{ + bool foundSel = false; + size_t index = 0; + size_t sindex = 0; + for (size_t i = 0, ncons = getNumConstructors(); i < ncons; i++) + { + int si = (*d_dtype)[i].getSelectorIndexForName(name); + if (si >= 0) + { + sindex = static_cast<size_t>(si); + index = i; + foundSel = true; + break; + } + } + if (!foundSel) + { + CVC5_API_CHECK(foundSel) + << "No select " << name << " for datatype " << getName() << " exists"; + } + return DatatypeSelector(d_solver, (*d_dtype)[index][sindex]); +} + Datatype::const_iterator::const_iterator(const Solver* slv, const cvc5::DType& dtype, bool begin) @@ -5806,29 +5848,18 @@ Op Solver::mkOp(Kind kind, const std::string& arg) const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_KIND_CHECK(kind); - CVC5_API_KIND_CHECK_EXPECTED((kind == RECORD_UPDATE) || (kind == DIVISIBLE), - kind) - << "RECORD_UPDATE or DIVISIBLE"; + CVC5_API_KIND_CHECK_EXPECTED((kind == DIVISIBLE), kind) << "DIVISIBLE"; //////// all checks before this line Op res; - if (kind == RECORD_UPDATE) - { - res = Op(this, - kind, - *mkValHelper<cvc5::RecordUpdate>(cvc5::RecordUpdate(arg)).d_node); - } - else - { - /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP - * throws an std::invalid_argument exception. For consistency, we treat it - * as invalid. */ - CVC5_API_ARG_CHECK_EXPECTED(arg != ".", arg) - << "a string representing an integer, real or rational value."; - res = Op(this, - kind, - *mkValHelper<cvc5::Divisible>(cvc5::Divisible(cvc5::Integer(arg))) - .d_node); - } + /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP + * throws an std::invalid_argument exception. For consistency, we treat it + * as invalid. */ + CVC5_API_ARG_CHECK_EXPECTED(arg != ".", arg) + << "a string representing an integer, real or rational value."; + res = Op(this, + kind, + *mkValHelper<cvc5::Divisible>(cvc5::Divisible(cvc5::Integer(arg))) + .d_node); return res; //////// CVC5_API_TRY_CATCH_END; @@ -5905,11 +5936,6 @@ Op Solver::mkOp(Kind kind, uint32_t arg) const *mkValHelper<cvc5::FloatingPointToSBV>(cvc5::FloatingPointToSBV(arg)) .d_node); break; - case TUPLE_UPDATE: - res = Op(this, - kind, - *mkValHelper<cvc5::TupleUpdate>(cvc5::TupleUpdate(arg)).d_node); - break; case REGEXP_REPEAT: res = Op(this, diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 1e857085b..16f58ee80 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -399,6 +399,11 @@ class CVC5_EXPORT Sort */ bool isTester() const; /** + * Is this a datatype updater sort? + * @return true if the sort is a datatype updater sort + */ + bool isUpdater() const; + /** * Is this a function sort? * @return true if the sort is a function sort */ @@ -1575,6 +1580,7 @@ class CVC5_EXPORT DatatypeDecl */ class CVC5_EXPORT DatatypeSelector { + friend class Datatype; friend class DatatypeConstructor; friend class Solver; @@ -1598,6 +1604,12 @@ class CVC5_EXPORT DatatypeSelector */ Term getSelectorTerm() const; + /** + * Get the upater operator of this datatype selector. + * @return the updater term + */ + Term getUpdaterTerm() const; + /** @return the range sort of this argument. */ Sort getRangeSort() const; @@ -1908,6 +1920,15 @@ class CVC5_EXPORT Datatype */ Term getConstructorTerm(const std::string& name) const; + /** + * Get the datatype constructor with the given name. + * This is a linear search through the constructors and their selectors, so + * in case of multiple, similarly-named selectors, the first is returned. + * @param name the name of the datatype selector + * @return the datatype selector with the given name + */ + DatatypeSelector getSelector(const std::string& name) const; + /** @return the name of this Datatype. */ std::string getName() const; @@ -2070,6 +2091,13 @@ class CVC5_EXPORT Datatype DatatypeConstructor getConstructorForName(const std::string& name) const; /** + * Return selector for name. + * @param name The name of selector to find + * @return the selector object for the name + */ + DatatypeSelector getSelectorForName(const std::string& name) const; + + /** * Helper for isNull checks. This prevents calling an API function with * CVC5_API_CHECK_NOT_NULL */ @@ -2890,7 +2918,6 @@ class CVC5_EXPORT Solver /** * Create operator of kind: - * - RECORD_UPDATE * - DIVISIBLE (to support arbitrary precision integers) * See enum Kind for a description of the parameters. * @param kind the kind of the operator diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index f7658412c..0375b5e60 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -1918,11 +1918,11 @@ enum CVC5_EXPORT Kind : int32_t */ APPLY_CONSTRUCTOR, /** - * Datatype selector application. + * Datatype selector application, which is undefined if misapplied. * * Parameters: * - 1: Selector (operator) - * - 2: Datatype term (undefined if mis-applied) + * - 2: Datatype term * * Create with: * - `Solver::mkTerm(const Op& op, const Term& child) const` @@ -1940,56 +1940,20 @@ enum CVC5_EXPORT Kind : int32_t * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ APPLY_TESTER, -#if 0 - /* Parametric datatype term. */ - PARAMETRIC_DATATYPE, - /* type ascription, for datatype constructor applications; - * first parameter is an ASCRIPTION_TYPE, second is the datatype constructor - * application being ascribed */ - APPLY_TYPE_ASCRIPTION, -#endif - /** - * Operator for a tuple update. - * - * Parameters: - * - 1: Index of the tuple to be updated - * - * Create with: - * - `Solver::mkOp(Kind kind, uint32_t param) const` - * - * Apply tuple update. - * - * Parameters: - * - 1: Op of kind TUPLE_UPDATE (which references an index) - * - 2: Tuple - * - 3: Element to store in the tuple at the given index - * - * Create with: - * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const` - * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` - */ - TUPLE_UPDATE, /** - * Operator for a record update. + * Datatype update application, which does not change the argument if + * misapplied. * * Parameters: - * - 1: Name of the field to be updated - * - * Create with: - * - `Solver::mkOp(Kind kind, const std::string& param) const` - * - * Record update. - * - * Parameters: - * - 1: Op of kind RECORD_UPDATE (which references a field) - * - 2: Record term to update - * - 3: Element to store in the record in the given field + * - 1: Updater (operator) + * - 2: Datatype term + * - 3: Value to update a field of the datatype term with * * Create with: - * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const` - * - `Solver::mkTerm(const Op& op,, const std::vector<Term>& children) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ - RECORD_UPDATE, + APPLY_UPDATER, /** * Match expressions. * For example, the smt2 syntax match term |