diff options
Diffstat (limited to 'src/api')
| -rw-r--r-- | src/api/cpp/cvc5.cpp | 96 | ||||
| -rw-r--r-- | src/api/cpp/cvc5.h | 2 | ||||
| -rw-r--r-- | src/api/cpp/cvc5_kind.h | 125 | ||||
| -rw-r--r-- | src/api/parsekinds.py | 2 |
4 files changed, 116 insertions, 109 deletions
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index f587bbfc0..9684c29c5 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -273,26 +273,27 @@ const static std::unordered_map<Kind, cvc5::Kind> s_kinds{ {SEP_STAR, cvc5::Kind::SEP_STAR}, {SEP_WAND, cvc5::Kind::SEP_WAND}, /* Sets ---------------------------------------------------------------- */ - {EMPTYSET, cvc5::Kind::EMPTYSET}, - {UNION, cvc5::Kind::UNION}, - {INTERSECTION, cvc5::Kind::INTERSECTION}, - {SETMINUS, cvc5::Kind::SETMINUS}, - {SUBSET, cvc5::Kind::SUBSET}, - {MEMBER, cvc5::Kind::MEMBER}, - {SINGLETON, cvc5::Kind::SINGLETON}, - {INSERT, cvc5::Kind::INSERT}, - {CARD, cvc5::Kind::CARD}, - {COMPLEMENT, cvc5::Kind::COMPLEMENT}, - {UNIVERSE_SET, cvc5::Kind::UNIVERSE_SET}, - {JOIN, cvc5::Kind::JOIN}, - {PRODUCT, cvc5::Kind::PRODUCT}, - {TRANSPOSE, cvc5::Kind::TRANSPOSE}, - {TCLOSURE, cvc5::Kind::TCLOSURE}, - {JOIN_IMAGE, cvc5::Kind::JOIN_IMAGE}, - {IDEN, cvc5::Kind::IDEN}, - {COMPREHENSION, cvc5::Kind::COMPREHENSION}, - {CHOOSE, cvc5::Kind::CHOOSE}, - {IS_SINGLETON, cvc5::Kind::IS_SINGLETON}, + {SET_EMPTY, cvc5::Kind::SET_EMPTY}, + {SET_UNION, cvc5::Kind::SET_UNION}, + {SET_INTERSECTION, cvc5::Kind::SET_INTERSECTION}, + {SET_MINUS, cvc5::Kind::SET_MINUS}, + {SET_SUBSET, cvc5::Kind::SET_SUBSET}, + {SET_MEMBER, cvc5::Kind::SET_MEMBER}, + {SET_SINGLETON, cvc5::Kind::SET_SINGLETON}, + {SET_INSERT, cvc5::Kind::SET_INSERT}, + {SET_CARD, cvc5::Kind::SET_CARD}, + {SET_COMPLEMENT, cvc5::Kind::SET_COMPLEMENT}, + {SET_UNIVERSE, cvc5::Kind::SET_UNIVERSE}, + {SET_COMPREHENSION, cvc5::Kind::SET_COMPREHENSION}, + {SET_CHOOSE, cvc5::Kind::SET_CHOOSE}, + {SET_IS_SINGLETON, cvc5::Kind::SET_IS_SINGLETON}, + /* Relations ----------------------------------------------------------- */ + {RELATION_JOIN, cvc5::Kind::RELATION_JOIN}, + {RELATION_PRODUCT, cvc5::Kind::RELATION_PRODUCT}, + {RELATION_TRANSPOSE, cvc5::Kind::RELATION_TRANSPOSE}, + {RELATION_TCLOSURE, cvc5::Kind::RELATION_TCLOSURE}, + {RELATION_JOIN_IMAGE, cvc5::Kind::RELATION_JOIN_IMAGE}, + {RELATION_IDEN, cvc5::Kind::RELATION_IDEN}, /* Bags ---------------------------------------------------------------- */ {UNION_MAX, cvc5::Kind::UNION_MAX}, {UNION_DISJOINT, cvc5::Kind::UNION_DISJOINT}, @@ -582,26 +583,27 @@ const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction> {cvc5::Kind::SEP_STAR, SEP_STAR}, {cvc5::Kind::SEP_WAND, SEP_WAND}, /* Sets ------------------------------------------------------------ */ - {cvc5::Kind::EMPTYSET, EMPTYSET}, - {cvc5::Kind::UNION, UNION}, - {cvc5::Kind::INTERSECTION, INTERSECTION}, - {cvc5::Kind::SETMINUS, SETMINUS}, - {cvc5::Kind::SUBSET, SUBSET}, - {cvc5::Kind::MEMBER, MEMBER}, - {cvc5::Kind::SINGLETON, SINGLETON}, - {cvc5::Kind::INSERT, INSERT}, - {cvc5::Kind::CARD, CARD}, - {cvc5::Kind::COMPLEMENT, COMPLEMENT}, - {cvc5::Kind::UNIVERSE_SET, UNIVERSE_SET}, - {cvc5::Kind::JOIN, JOIN}, - {cvc5::Kind::PRODUCT, PRODUCT}, - {cvc5::Kind::TRANSPOSE, TRANSPOSE}, - {cvc5::Kind::TCLOSURE, TCLOSURE}, - {cvc5::Kind::JOIN_IMAGE, JOIN_IMAGE}, - {cvc5::Kind::IDEN, IDEN}, - {cvc5::Kind::COMPREHENSION, COMPREHENSION}, - {cvc5::Kind::CHOOSE, CHOOSE}, - {cvc5::Kind::IS_SINGLETON, IS_SINGLETON}, + {cvc5::Kind::SET_EMPTY, SET_EMPTY}, + {cvc5::Kind::SET_UNION, SET_UNION}, + {cvc5::Kind::SET_INTERSECTION, SET_INTERSECTION}, + {cvc5::Kind::SET_MINUS, SET_MINUS}, + {cvc5::Kind::SET_SUBSET, SET_SUBSET}, + {cvc5::Kind::SET_MEMBER, SET_MEMBER}, + {cvc5::Kind::SET_SINGLETON, SET_SINGLETON}, + {cvc5::Kind::SET_INSERT, SET_INSERT}, + {cvc5::Kind::SET_CARD, SET_CARD}, + {cvc5::Kind::SET_COMPLEMENT, SET_COMPLEMENT}, + {cvc5::Kind::SET_UNIVERSE, SET_UNIVERSE}, + {cvc5::Kind::SET_COMPREHENSION, SET_COMPREHENSION}, + {cvc5::Kind::SET_CHOOSE, SET_CHOOSE}, + {cvc5::Kind::SET_IS_SINGLETON, SET_IS_SINGLETON}, + /* Relations ------------------------------------------------------- */ + {cvc5::Kind::RELATION_JOIN, RELATION_JOIN}, + {cvc5::Kind::RELATION_PRODUCT, RELATION_PRODUCT}, + {cvc5::Kind::RELATION_TRANSPOSE, RELATION_TRANSPOSE}, + {cvc5::Kind::RELATION_TCLOSURE, RELATION_TCLOSURE}, + {cvc5::Kind::RELATION_JOIN_IMAGE, RELATION_JOIN_IMAGE}, + {cvc5::Kind::RELATION_IDEN, RELATION_IDEN}, /* Bags ------------------------------------------------------------ */ {cvc5::Kind::UNION_MAX, UNION_MAX}, {cvc5::Kind::UNION_DISJOINT, UNION_DISJOINT}, @@ -618,7 +620,7 @@ const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction> {cvc5::Kind::BAG_IS_SINGLETON, BAG_IS_SINGLETON}, {cvc5::Kind::BAG_FROM_SET, BAG_FROM_SET}, {cvc5::Kind::BAG_TO_SET, BAG_TO_SET}, - {cvc5::Kind::BAG_MAP,BAG_MAP}, + {cvc5::Kind::BAG_MAP, BAG_MAP}, /* Strings --------------------------------------------------------- */ {cvc5::Kind::STRING_CONCAT, STRING_CONCAT}, {cvc5::Kind::STRING_IN_REGEXP, STRING_IN_REGEXP}, @@ -3266,12 +3268,12 @@ void Term::collectSet(std::set<Term>& set, const Solver* slv) { // We asserted that node has a set type, and node.isConst() - // Thus, node only contains of EMPTYSET, UNION and SINGLETON. + // Thus, node only contains of SET_EMPTY, SET_UNION and SET_SINGLETON. switch (node.getKind()) { - case cvc5::Kind::EMPTYSET: break; - case cvc5::Kind::SINGLETON: set.emplace(Term(slv, node[0])); break; - case cvc5::Kind::UNION: + case cvc5::Kind::SET_EMPTY: break; + case cvc5::Kind::SET_SINGLETON: set.emplace(Term(slv, node[0])); break; + case cvc5::Kind::SET_UNION: { for (const auto& sub : node) { @@ -5176,7 +5178,7 @@ Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const { // default case, same as above checkMkTerm(kind, children.size()); - if (kind == api::SINGLETON) + if (kind == api::SET_SINGLETON) { // the type of the term is the same as the type of the internal node // see Term::getSort() @@ -5906,7 +5908,7 @@ Term Solver::mkUniverseSet(const Sort& sort) const //////// all checks before this line Node res = getNodeManager()->mkNullaryOperator(*sort.d_type, - cvc5::kind::UNIVERSE_SET); + cvc5::kind::SET_UNIVERSE); // TODO(#2771): Reenable? // (void)res->getType(true); /* kick off type checking */ return Term(this, res); diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index b73c1ce27..1ecf8715b 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -1484,7 +1484,7 @@ class CVC5_EXPORT Term * where `c1 ... cn` are values ordered by id such that `c1 > ... > cn` (see * also @ref Term::operator>(const Term&) const). * - * Note that a universe set term (kind UNIVERSE_SET) is not considered to be + * Note that a universe set term (kind SET_UNIVERSE) is not considered to be * a set value. */ bool isSetValue() const; diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index bece49098..57941aa5f 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -2117,7 +2117,7 @@ enum Kind : int32_t * Create with: * - `Solver::mkEmptySet(const Sort& sort) const` */ - EMPTYSET, + SET_EMPTY, /** * Set union. * @@ -2128,7 +2128,7 @@ enum Kind : int32_t * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ - UNION, + SET_UNION, /** * Set intersection. * @@ -2139,7 +2139,7 @@ enum Kind : int32_t * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ - INTERSECTION, + SET_INTERSECTION, /** * Set subtraction. * @@ -2150,7 +2150,7 @@ enum Kind : int32_t * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ - SETMINUS, + SET_MINUS, /** * Subset predicate. * @@ -2161,7 +2161,7 @@ enum Kind : int32_t * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ - SUBSET, + SET_SUBSET, /** * Set membership predicate. * @@ -2172,7 +2172,7 @@ enum Kind : int32_t * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ - MEMBER, + SET_MEMBER, /** * Construct a singleton set from an element given as a parameter. * The returned set has same type of the element. @@ -2183,7 +2183,7 @@ enum Kind : int32_t * Create with: * - `Solver::mkTerm(Kind kind, const Term& child) const` */ - SINGLETON, + SET_SINGLETON, /** * The set obtained by inserting elements; * @@ -2197,7 +2197,7 @@ enum Kind : int32_t * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ - INSERT, + SET_INSERT, /** * Set cardinality. * @@ -2207,7 +2207,7 @@ enum Kind : int32_t * Create with: * - `Solver::mkTerm(Kind kind, const Term& child) const` */ - CARD, + SET_CARD, /** * Set complement with respect to finite universe. * @@ -2217,63 +2217,83 @@ enum Kind : int32_t * Create with: * - `Solver::mkTerm(Kind kind, const Term& child) const` */ - COMPLEMENT, + SET_COMPLEMENT, /** * Finite universe set. * All set variables must be interpreted as subsets of it. * - * Note that UNIVERSE_SET is considered a special symbol of the theory of + * Note that SET_UNIVERSE is considered a special symbol of the theory of * sets and is not considered as a set value, * i.e., `Term::isSetValue() const` will return false. * * Create with: * - `Solver::mkUniverseSet(const Sort& sort) const` */ - UNIVERSE_SET, + SET_UNIVERSE, /** - * Set join. + * Set comprehension + * A set comprehension is specified by a bound variable list x1 ... xn, + * a predicate P[x1...xn], and a term t[x1...xn]. A comprehension C with the + * above form has members given by the following semantics: + * @f[ + * \forall y. ( \exists x_1...x_n. P[x_1...x_n] \hat{} t[x_1...x_n] = y ) + * \Leftrightarrow (member y C) + * @f] + * where y ranges over the element type of the (set) type of the + * comprehension. If @f$ t[x_1..x_n] @f$ is not provided, it is equivalent to + * y in the above formula. * * Parameters: - * - 1..2: Terms of set sort + * - 1: Term BOUND_VAR_LIST + * - 2: Term denoting the predicate of the comprehension + * - 3: (optional) a Term denoting the generator for the comprehension * * Create with: * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ - JOIN, + SET_COMPREHENSION, /** - * Set cartesian product. + * Returns an element from a given set. + * If a set A = {x}, then the term (choose A) is equivalent to the term x. + * If the set is empty, then (choose A) is an arbitrary value. + * If the set has cardinality > 1, then (choose A) will deterministically + * return an element in A. * * Parameters: - * - 1..2: Terms of set sort + * - 1: Term of set sort * * Create with: - * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` - * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ - PRODUCT, + SET_CHOOSE, /** - * Set transpose. + * Set is_singleton predicate. * * Parameters: - * - 1: Term of set sort + * - 1: Term of set sort, is [1] a singleton set? * * Create with: * - `Solver::mkTerm(Kind kind, const Term& child) const` */ - TRANSPOSE, + SET_IS_SINGLETON, + + /* Relations ------------------------------------------------------------- */ + /** - * Set transitive closure. + * Set join. * * Parameters: - * - 1: Term of set sort + * - 1..2: Terms of set sort * * Create with: - * - `Solver::mkTerm(Kind kind, const Term& child) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ - TCLOSURE, + RELATION_JOIN, /** - * Set join image. + * Set cartesian product. * * Parameters: * - 1..2: Terms of set sort @@ -2282,9 +2302,9 @@ enum Kind : int32_t * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ - JOIN_IMAGE, + RELATION_PRODUCT, /** - * Set identity. + * Set transpose. * * Parameters: * - 1: Term of set sort @@ -2292,56 +2312,41 @@ enum Kind : int32_t * Create with: * - `Solver::mkTerm(Kind kind, const Term& child) const` */ - IDEN, + RELATION_TRANSPOSE, /** - * Set comprehension - * A set comprehension is specified by a bound variable list x1 ... xn, - * a predicate P[x1...xn], and a term t[x1...xn]. A comprehension C with the - * above form has members given by the following semantics: - * @f[ - * \forall y. ( \exists x_1...x_n. P[x_1...x_n] \hat{} t[x_1...x_n] = y ) - * \Leftrightarrow (member y C) - * @f] - * where y ranges over the element type of the (set) type of the - * comprehension. If @f$ t[x_1..x_n] @f$ is not provided, it is equivalent to - * y in the above formula. + * Set transitive closure. * * Parameters: - * - 1: Term BOUND_VAR_LIST - * - 2: Term denoting the predicate of the comprehension - * - 3: (optional) a Term denoting the generator for the comprehension + * - 1: Term of set sort * * Create with: - * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` - * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` - * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` + * - `Solver::mkTerm(Kind kind, const Term& child) const` */ - COMPREHENSION, + RELATION_TCLOSURE, /** - * Returns an element from a given set. - * If a set A = {x}, then the term (choose A) is equivalent to the term x. - * If the set is empty, then (choose A) is an arbitrary value. - * If the set has cardinality > 1, then (choose A) will deterministically - * return an element in A. + * Set join image. * * Parameters: - * - 1: Term of set sort + * - 1..2: Terms of set sort * * Create with: - * - `Solver::mkTerm(Kind kind, const Term& child) const` + * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` + * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ - CHOOSE, + RELATION_JOIN_IMAGE, /** - * Set is_singleton predicate. + * Set identity. * * Parameters: - * - 1: Term of set sort, is [1] a singleton set? + * - 1: Term of set sort * * Create with: * - `Solver::mkTerm(Kind kind, const Term& child) const` */ - IS_SINGLETON, + RELATION_IDEN, + /* Bags ------------------------------------------------------------------ */ + /** * Empty bag constant. * diff --git a/src/api/parsekinds.py b/src/api/parsekinds.py index 0dcc7be68..14762c24c 100644 --- a/src/api/parsekinds.py +++ b/src/api/parsekinds.py @@ -105,7 +105,7 @@ class KindsParser: BITVECTOR_ADD --> BVAdd APPLY_SELECTOR --> ApplySelector FLOATINGPOINT_ISNAN --> FPIsNan - SETMINUS --> Setminus + SET_MINUS --> Setminus See the generated .pxi file for an explicit mapping ''' |