From: mudathirmahgoub Date: Tue, 28 Jun 2022 17:50:41 +0000 (-0500) Subject: Add rel.group operator to sets (#8876) X-Git-Tag: cvc5-1.0.1~29 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=61026f8e494a460906fd6d37dc0766608cce7aee;p=cvc5.git Add rel.group operator to sets (#8876) This PR is dependent on #8819 and #8867. --- diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 52c2045b0..1c45d2d4d 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -309,6 +309,7 @@ const static std::unordered_map> KIND_ENUM(RELATION_TCLOSURE, internal::Kind::RELATION_TCLOSURE), KIND_ENUM(RELATION_JOIN_IMAGE, internal::Kind::RELATION_JOIN_IMAGE), KIND_ENUM(RELATION_IDEN, internal::Kind::RELATION_IDEN), + KIND_ENUM(RELATION_GROUP, internal::Kind::RELATION_GROUP), /* Bags ------------------------------------------------------------- */ KIND_ENUM(BAG_UNION_MAX, internal::Kind::BAG_UNION_MAX), KIND_ENUM(BAG_UNION_DISJOINT, internal::Kind::BAG_UNION_DISJOINT), @@ -633,6 +634,7 @@ const static std::unordered_map s_op_kinds{ {REGEXP_REPEAT, internal::Kind::REGEXP_REPEAT_OP}, {REGEXP_LOOP, internal::Kind::REGEXP_LOOP_OP}, {TUPLE_PROJECT, internal::Kind::TUPLE_PROJECT_OP}, + {RELATION_GROUP, internal::Kind::RELATION_GROUP_OP}, {TABLE_PROJECT, internal::Kind::TABLE_PROJECT_OP}, {TABLE_AGGREGATE, internal::Kind::TABLE_AGGREGATE_OP}, {TABLE_JOIN, internal::Kind::TABLE_JOIN_OP}, @@ -1950,6 +1953,7 @@ size_t Op::getNumIndicesHelper() const case FLOATINGPOINT_TO_FP_FROM_UBV: size = 2; break; case REGEXP_LOOP: size = 2; break; case TUPLE_PROJECT: + case RELATION_GROUP: case TABLE_AGGREGATE: case TABLE_GROUP: case TABLE_JOIN: @@ -2110,6 +2114,7 @@ Term Op::getIndexHelper(size_t index) const break; } case TUPLE_PROJECT: + case RELATION_GROUP: case TABLE_AGGREGATE: case TABLE_GROUP: case TABLE_JOIN: @@ -6151,6 +6156,7 @@ Op Solver::mkOp(Kind kind, const std::vector& args) const res = mkOpHelper(kind, internal::RegExpLoop(args[0], args[1])); break; case TUPLE_PROJECT: + case RELATION_GROUP: case TABLE_AGGREGATE: case TABLE_GROUP: case TABLE_JOIN: diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 9aa4824d7..f71d6a447 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -3330,6 +3330,37 @@ enum Kind : int32_t * \endrst */ RELATION_IDEN, + /** + * Relation group + * + * \rst + * :math:`((\_ \; rel.group \; n_1 \; \dots \; n_k) \; A)` partitions tuples + * of relation :math:`A` such that tuples that have the same projection + * with indices :math:`n_1 \; \dots \; n_k` are in the same part. + * It returns a set of relations of type :math:`(Set \; T)` where + * :math:`T` is the type of :math:`A`. + * + * - Arity: ``1`` + * + * - ``1:`` Term of relation sort + * + * - Indices: ``n`` + * + * - ``1..n:`` Indices of the projection + * + * \endrst + * + * - Create Term of this Kind with: + * + * - Solver::mkTerm(Kind, const std::vector&) const + * - Solver::mkTerm(const Op&, const std::vector&) const + * + * \rst + * .. warning:: This kind is experimental and may be changed or removed in + * future versions. + * \endrst + */ + RELATION_GROUP, /* Bags ------------------------------------------------------------------ */ diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp index 6b8e32f55..644202805 100644 --- a/src/expr/skolem_manager.cpp +++ b/src/expr/skolem_manager.cpp @@ -98,6 +98,9 @@ const char* toString(SkolemFunId id) case SkolemFunId::TABLES_GROUP_PART: return "TABLES_GROUP_PART"; case SkolemFunId::TABLES_GROUP_PART_ELEMENT: return "TABLES_GROUP_PART_ELEMENT"; + case SkolemFunId::RELATIONS_GROUP_PART: return "RELATIONS_GROUP_PART"; + case SkolemFunId::RELATIONS_GROUP_PART_ELEMENT: + return "RELATIONS_GROUP_PART_ELEMENT"; case SkolemFunId::SETS_CHOOSE: return "SETS_CHOOSE"; case SkolemFunId::SETS_DEQ_DIFF: return "SETS_DEQ_DIFF"; case SkolemFunId::SETS_FOLD_CARD: return "SETS_FOLD_CARD"; diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h index da729e4a1..5b398280d 100644 --- a/src/expr/skolem_manager.h +++ b/src/expr/skolem_manager.h @@ -180,6 +180,17 @@ enum class SkolemFunId * that is a member of B if B is not empty. */ TABLES_GROUP_PART_ELEMENT, + /** Given a group term ((_ rel.group n1 ... nk) A) of type (Set (Relation T)) + * this uninterpreted function maps elements of A to their parts in the + * resulting partition. It has type (-> T (Relation T)) + */ + RELATIONS_GROUP_PART, + /** + * Given a group term ((_ rel.group n1 ... nk) A) of type (Set (Relation T)) + * and a part B of type (Relation T), this function returns a skolem element + * that is a member of B if B is not empty. + */ + RELATIONS_GROUP_PART_ELEMENT, /** An interpreted function for bag.choose operator: * (choose A) is expanded as * (witness ((x elementType)) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index bc5ee3147..875e41ee4 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1429,6 +1429,12 @@ termNonVariable[cvc5::Term& expr, cvc5::Term& expr2] cvc5::Op op = SOLVER->mkOp(cvc5::TABLE_GROUP, indices); expr = SOLVER->mkTerm(op, {expr}); } + | LPAREN_TOK RELATION_GROUP_TOK term[expr,expr2] RPAREN_TOK + { + std::vector indices; + cvc5::Op op = SOLVER->mkOp(cvc5::RELATION_GROUP, indices); + expr = SOLVER->mkTerm(op, {expr}); + } | /* an atomic term (a term with no subterms) */ termAtomic[atomTerm] { expr = atomTerm; } ; @@ -1598,6 +1604,13 @@ identifier[cvc5::ParseOp& p] p.d_kind = cvc5::TABLE_GROUP; p.d_op = SOLVER->mkOp(cvc5::TABLE_GROUP, numerals); } + | RELATION_GROUP_TOK nonemptyNumeralList[numerals] + { + // we adopt a special syntax (_ rel.group i_1 ... i_n) where + // i_1, ..., j_n are numerals + p.d_kind = cvc5::RELATION_GROUP; + p.d_op = SOLVER->mkOp(cvc5::RELATION_GROUP, numerals); + } | functionName[opName, CHECK_NONE] nonemptyNumeralList[numerals] { cvc5::Kind k = PARSER_STATE->getIndexedOpKind(opName); @@ -2210,6 +2223,7 @@ TABLE_PROJECT_TOK: { PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_BAGS TABLE_AGGREGATE_TOK: { PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_BAGS) }? 'table.aggr'; TABLE_JOIN_TOK: { PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_BAGS) }? 'table.join'; TABLE_GROUP_TOK: { PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_BAGS) }? 'table.group'; +RELATION_GROUP_TOK: { PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_SETS) }? 'rel.group'; FMF_CARD_TOK: { !PARSER_STATE->strictModeEnabled() && PARSER_STATE->hasCardinalityConstraints() }? 'fmf.card'; HO_ARROW_TOK : { PARSER_STATE->isHoEnabled() }? '->'; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 8c5be875a..900ff1016 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1130,7 +1130,7 @@ cvc5::Term Smt2::applyParseOp(ParseOp& p, std::vector& args) } else if (p.d_kind == cvc5::TUPLE_PROJECT || p.d_kind == cvc5::TABLE_PROJECT || p.d_kind == cvc5::TABLE_AGGREGATE || p.d_kind == cvc5::TABLE_JOIN - || p.d_kind == cvc5::TABLE_GROUP) + || p.d_kind == cvc5::TABLE_GROUP || p.d_kind == cvc5::RELATION_GROUP) { cvc5::Term ret = d_solver->mkTerm(p.d_op, args); Trace("parser") << "applyParseOp: return projection " << ret << std::endl; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 58cdd7739..5dc9252a9 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -820,6 +820,21 @@ void Smt2Printer::toStream(std::ostream& out, } return; } + case kind::RELATION_GROUP: + { + ProjectOp op = n.getOperator().getConst(); + if (op.getIndices().empty()) + { + // e.g. (rel.group A) + out << "rel.group " << n[0] << ")"; + } + else + { + // e.g. ((_ rel.group 0 1 2 3) A) + out << "(_ rel.group" << op << ") " << n[0] << ")"; + } + return; + } case kind::CONSTRUCTOR_TYPE: { out << n[n.getNumChildren()-1]; @@ -1159,6 +1174,7 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v) case kind::RELATION_TCLOSURE: return "rel.tclosure"; case kind::RELATION_IDEN: return "rel.iden"; case kind::RELATION_JOIN_IMAGE: return "rel.join_image"; + case kind::RELATION_GROUP: return "rel.group"; // bag theory case kind::BAG_TYPE: return "Bag"; diff --git a/src/theory/bags/bags_utils.cpp b/src/theory/bags/bags_utils.cpp index 17f1cf5d3..63112bee6 100644 --- a/src/theory/bags/bags_utils.cpp +++ b/src/theory/bags/bags_utils.cpp @@ -146,7 +146,7 @@ Node BagsUtils::evaluate(Rewriter* rewriter, TNode n) case BAG_FOLD: return evaluateBagFold(n); case TABLE_PRODUCT: return evaluateProduct(n); case TABLE_JOIN: return evaluateJoin(rewriter, n); - case TABLE_GROUP: return evaluateGroup(rewriter, n); + case TABLE_GROUP: return evaluateGroup(n); case TABLE_PROJECT: return evaluateTableProject(n); default: break; } @@ -975,7 +975,7 @@ Node BagsUtils::evaluateJoin(Rewriter* rewriter, TNode n) return ret; } -Node BagsUtils::evaluateGroup(Rewriter* rewriter, TNode n) +Node BagsUtils::evaluateGroup(TNode n) { Assert(n.getKind() == TABLE_GROUP); @@ -1049,7 +1049,7 @@ Node BagsUtils::evaluateGroup(Rewriter* rewriter, TNode n) parts[emptyPart] = Rational(1); } Node ret = constructConstantBagFromElements(partitionType, parts); - Trace("bags-partition") << "ret: " << ret << std::endl; + Trace("bags-group") << "ret: " << ret << std::endl; return ret; } diff --git a/src/theory/bags/bags_utils.h b/src/theory/bags/bags_utils.h index 4da592d5a..8267a0c66 100644 --- a/src/theory/bags/bags_utils.h +++ b/src/theory/bags/bags_utils.h @@ -138,7 +138,7 @@ class BagsUtils * @return a partition of A such that each part contains tuples with the same * projection with indices n_1 ... n_k */ - static Node evaluateGroup(Rewriter* rewriter, TNode n); + static Node evaluateGroup(TNode n); /** * @param n of the form ((_ table.project i_1 ... i_n) A) where A is a diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index ad3dfbeef..d828d6e5d 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -334,6 +334,7 @@ const char* toString(InferenceId i) case InferenceId::SEP_DISTINCT_REF: return "SEP_DISTINCT_REF"; case InferenceId::SEP_REF_BOUND: return "SEP_REF_BOUND"; + case InferenceId::SETS_SKOLEM: return "SETS_SKOLEM"; case InferenceId::SETS_CG_SPLIT: return "SETS_CG_SPLIT"; case InferenceId::SETS_COMPREHENSION: return "SETS_COMPREHENSION"; case InferenceId::SETS_DEQ: return "SETS_DEQ"; @@ -390,6 +391,15 @@ const char* toString(InferenceId i) case InferenceId::SETS_RELS_TRANSPOSE_REV: return "SETS_RELS_TRANSPOSE_REV"; case InferenceId::SETS_RELS_TUPLE_REDUCTION: return "SETS_RELS_TUPLE_REDUCTION"; + case InferenceId::SETS_RELS_GROUP_UP1: return "SETS_RELS_GROUP_UP1"; + case InferenceId::SETS_RELS_GROUP_UP2: return "SETS_RELS_GROUP_UP2"; + case InferenceId::SETS_RELS_GROUP_DOWN: return "SETS_RELS_GROUP_DOWN"; + case InferenceId::SETS_RELS_GROUP_PART_MEMBER: + return "SETS_RELS_GROUP_PART_MEMBER"; + case InferenceId::SETS_RELS_GROUP_SAME_PROJECTION: + return "SETS_RELS_GROUP_SAME_PROJECTION"; + case InferenceId::SETS_RELS_GROUP_SAME_PART: + return "SETS_RELS_GROUP_SAME_PART"; case InferenceId::STRINGS_I_NORM_S: return "STRINGS_I_NORM_S"; case InferenceId::STRINGS_I_CONST_MERGE: return "STRINGS_I_CONST_MERGE"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index 4f5e3d156..ee3cb6004 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -485,6 +485,7 @@ enum class InferenceId // ---------------------------------- sets theory //-------------------- sets core solver // split when computing care graph + SETS_SKOLEM, SETS_CG_SPLIT, SETS_COMPREHENSION, SETS_DEQ, @@ -545,6 +546,13 @@ enum class InferenceId SETS_RELS_TRANSPOSE_EQ, SETS_RELS_TRANSPOSE_REV, SETS_RELS_TUPLE_REDUCTION, + SETS_RELS_GROUP_NOT_EMPTY, + SETS_RELS_GROUP_UP1, + SETS_RELS_GROUP_UP2, + SETS_RELS_GROUP_DOWN, + SETS_RELS_GROUP_PART_MEMBER, + SETS_RELS_GROUP_SAME_PROJECTION, + SETS_RELS_GROUP_SAME_PART, //-------------------------------------- end sets theory //-------------------------------------- strings theory diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index e3e5e06b6..0c0e17dc1 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -89,6 +89,16 @@ operator SET_FILTER 2 "set filter operator" # A: a bag of type (Set T1) operator SET_FOLD 3 "set fold operator" +# rel.group operator +constant RELATION_GROUP_OP \ + class \ + ProjectOp+ \ + ::cvc5::internal::ProjectOpHashFunction \ + "theory/datatypes/project_op.h" \ + "operator for RELATION_GROUP; payload is an instance of the cvc5::internal::RelationGroupOp class" + +parameterized RELATION_GROUP RELATION_GROUP_OP 1 "relation group" + operator RELATION_JOIN 2 "relation join" operator RELATION_PRODUCT 2 "relation cartesian product" operator RELATION_TRANSPOSE 1 "relation transpose" @@ -120,6 +130,8 @@ typerule RELATION_TRANSPOSE ::cvc5::internal::theory::sets::RelTransposeTypeRu typerule RELATION_TCLOSURE ::cvc5::internal::theory::sets::RelTransClosureTypeRule typerule RELATION_JOIN_IMAGE ::cvc5::internal::theory::sets::JoinImageTypeRule typerule RELATION_IDEN ::cvc5::internal::theory::sets::RelIdenTypeRule +typerule RELATION_GROUP_OP "SimpleTypeRule" +typerule RELATION_GROUP ::cvc5::internal::theory::sets::RelationGroupTypeRule construle SET_UNION ::cvc5::internal::theory::sets::SetsBinaryOperatorTypeRule construle SET_SINGLETON ::cvc5::internal::theory::sets::SingletonTypeRule diff --git a/src/theory/sets/rels_utils.cpp b/src/theory/sets/rels_utils.cpp index 3b8e9ad32..08d4feb36 100644 --- a/src/theory/sets/rels_utils.cpp +++ b/src/theory/sets/rels_utils.cpp @@ -17,9 +17,13 @@ #include "expr/dtype.h" #include "expr/dtype_cons.h" +#include "theory/datatypes/project_op.h" #include "theory/datatypes/tuple_utils.h" +#include "theory/sets/normal_form.h" +using namespace cvc5::internal::kind; using namespace cvc5::internal::theory::datatypes; +using namespace cvc5::internal::theory::sets; namespace cvc5::internal { namespace theory { @@ -73,7 +77,78 @@ Node RelsUtils::constructPair(Node rel, Node a, Node b) { const DType& dt = rel.getType().getSetElementType().getDType(); return NodeManager::currentNM()->mkNode( - kind::APPLY_CONSTRUCTOR, dt[0].getConstructor(), a, b); + APPLY_CONSTRUCTOR, dt[0].getConstructor(), a, b); +} + +Node RelsUtils::evaluateGroup(TNode n) +{ + Assert(n.getKind() == RELATION_GROUP); + + NodeManager* nm = NodeManager::currentNM(); + + Node A = n[0]; + TypeNode setType = A.getType(); + TypeNode partitionType = n.getType(); + + if (A.getKind() == SET_EMPTY) + { + // return a nonempty partition + return nm->mkNode(SET_SINGLETON, A); + } + + std::vector indices = + n.getOperator().getConst().getIndices(); + + std::set elements = NormalForm::getElementsFromNormalConstant(A); + Trace("sets-group") << "elements: " << elements << std::endl; + // a simple map from elements to equivalent classes with this invariant: + // each key element must appear exactly once in one of the values. + std::map> sets; + std::set emptyClass; + for (const Node& element : elements) + { + // initially each singleton element is an equivalence class + sets[element] = {element}; + } + for (std::set::iterator i = elements.begin(); i != elements.end(); ++i) + { + Node iElement = *i; + if (sets[iElement].empty()) + { + // skip this element since its equivalent class has already been processed + continue; + } + std::set::iterator j = i; + ++j; + while (j != elements.end()) + { + Node jElement = *j; + if (TupleUtils::sameProjection(indices, iElement, jElement)) + { + // add element j to the equivalent class + sets[iElement].insert(jElement); + // mark the equivalent class of j as processed + sets[jElement] = emptyClass; + } + ++j; + } + } + + // construct the partition parts + std::set parts; + for (std::pair> pair : sets) + { + const std::set& eqc = pair.second; + if (eqc.empty()) + { + continue; + } + Node part = NormalForm::elementsToSet(eqc, setType); + parts.insert(part); + } + Node ret = NormalForm::elementsToSet(parts, partitionType); + Trace("sets-group") << "ret: " << ret << std::endl; + return ret; } } // namespace sets diff --git a/src/theory/sets/rels_utils.h b/src/theory/sets/rels_utils.h index 61d301074..559ef5281 100644 --- a/src/theory/sets/rels_utils.h +++ b/src/theory/sets/rels_utils.h @@ -64,6 +64,14 @@ class RelsUtils * @return a tuple (tuple a b) */ static Node constructPair(Node rel, Node a, Node b); + + /** + * @param n of the form ((_ rel.group (n_1 ... n_k) ) A) where A is a + * constant relation + * @return a partition of A such that each part contains tuples with the same + * projection with indices n_1 ... n_k + */ + static Node evaluateGroup(TNode n); }; } // namespace sets } // namespace theory diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp index cb02f4b06..11b16a0bb 100644 --- a/src/theory/sets/solver_state.cpp +++ b/src/theory/sets/solver_state.cpp @@ -30,8 +30,10 @@ SolverState::SolverState(Env& env, Valuation val, SkolemCache& skc) : TheoryState(env, val), d_skCache(skc), d_mapTerms(env.getUserContext()), + d_groupTerms(env.getUserContext()), d_mapSkolemElements(env.getUserContext()), - d_members(env.getContext()) + d_members(env.getContext()), + d_partElementSkolems(env.getUserContext()) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -154,6 +156,13 @@ void SolverState::registerTerm(Node r, TypeNode tnn, Node n) d_mapSkolemElements[n] = set; } } + else if (nk == RELATION_GROUP) + { + d_groupTerms.insert(n); + std::shared_ptr> set = + std::make_shared>(d_env.getUserContext()); + d_partElementSkolems[n] = set; + } else if (nk == SET_COMPREHENSION) { d_compSets[r].push_back(n); @@ -481,6 +490,11 @@ const std::vector& SolverState::getFilterTerms() const { return d_filterTe const context::CDHashSet& SolverState::getMapTerms() const { return d_mapTerms; } +const context::CDHashSet& SolverState::getGroupTerms() const +{ + return d_groupTerms; +} + std::shared_ptr> SolverState::getMapSkolemElements( Node n) { @@ -632,6 +646,20 @@ void SolverState::registerMapSkolemElement(const Node& n, const Node& element) d_mapSkolemElements[n].get()->insert(element); } +void SolverState::registerPartElementSkolem(Node group, Node skolemElement) +{ + Assert(group.getKind() == RELATION_GROUP); + Assert(skolemElement.getType() == group[0].getType().getSetElementType()); + d_partElementSkolems[group].get()->insert(skolemElement); +} + +std::shared_ptr> SolverState::getPartElementSkolems( + Node n) +{ + Assert(n.getKind() == RELATION_GROUP); + return d_partElementSkolems[n]; +} + } // namespace sets } // namespace theory } // namespace cvc5::internal diff --git a/src/theory/sets/solver_state.h b/src/theory/sets/solver_state.h index ab240ab22..3e3ee9df2 100644 --- a/src/theory/sets/solver_state.h +++ b/src/theory/sets/solver_state.h @@ -165,6 +165,8 @@ class SolverState : public TheoryState const std::vector& getFilterTerms() const; /** Get the list of all set.map terms in the current user context */ const context::CDHashSet& getMapTerms() const; + /** Get the list of all rel.group terms in the current user context */ + const context::CDHashSet& getGroupTerms() const; /** Get the list of all skolem elements generated for map terms down rules in * the current user context */ std::shared_ptr> getMapSkolemElements(Node n); @@ -197,6 +199,10 @@ class SolverState : public TheoryState /** register the skolem element for the set.map term n */ void registerMapSkolemElement(const Node& n, const Node& element); + /** register skolem element generated by grup count rule */ + void registerPartElementSkolem(Node group, Node skolemElement); + /** return skolem elements generated by group part count rule. */ + std::shared_ptr> getPartElementSkolems(Node n); private: /** constants */ @@ -224,6 +230,8 @@ class SolverState : public TheoryState std::vector d_filterTerms; /** User context collection of set.map terms */ context::CDHashSet d_mapTerms; + /** User context collection of rel.group terms */ + context::CDHashSet d_groupTerms; /** User context collection of skolem elements generated for set.map terms */ context::CDHashMap>> d_mapSkolemElements; @@ -283,6 +291,16 @@ class SolverState : public TheoryState * members if i=1. */ const std::map& getMembersInternal(Node r, unsigned i) const; + + /** + * A cache that stores skolem elements generated by inference rule + * InferenceId::RELATIONS_GROUP_PART_MEMBER. + * It maps rel.group nodes to generated skolem elements. + * The skolem elements need to persist during checking, and should only change + * when the user context changes. + */ + context::CDHashMap>> + d_partElementSkolems; }; /* class TheorySetsPrivate */ } // namespace sets diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index bf1022048..5794f8a90 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -23,6 +23,8 @@ #include "expr/skolem_manager.h" #include "options/sets_options.h" #include "smt/smt_statistics_registry.h" +#include "theory/datatypes/project_op.h" +#include "theory/datatypes/tuple_utils.h" #include "theory/sets/normal_form.h" #include "theory/sets/theory_sets.h" #include "theory/theory_model.h" @@ -31,6 +33,7 @@ using namespace std; using namespace cvc5::internal::kind; +using namespace cvc5::internal::theory::datatypes; namespace cvc5::internal { namespace theory { @@ -392,6 +395,13 @@ void TheorySetsPrivate::fullEffortCheck() { continue; } + // check group up + checkGroups(); + d_im.doPendingLemmas(); + if (d_im.hasSent()) + { + continue; + } // check disequalities checkDisequalities(); d_im.doPendingLemmas(); @@ -865,6 +875,378 @@ void TheorySetsPrivate::checkMapDown() } } +void TheorySetsPrivate::checkGroups() +{ + const context::CDHashSet& groupTerms = d_state.getGroupTerms(); + for (const Node& n : groupTerms) + { + checkGroup(n); + } +} + +void TheorySetsPrivate::checkGroup(Node n) +{ + Assert(n.getKind() == RELATION_GROUP); + groupNotEmpty(n); + d_im.doPendingLemmas(); + if (d_im.hasSent()) + { + return; + } + Node part = defineSkolemPartFunction(n); + Node A = d_state.getRepresentative(n[0]); + + const std::map& membersA = d_state.getMembers(A); + const std::map& negativeMembersA = d_state.getNegativeMembers(A); + std::shared_ptr> skolems = + d_state.getPartElementSkolems(n); + for (const auto& aPair : membersA) + { + if (skolems->contains(aPair.first)) + { + // skip skolem elements that were introduced by groupPartCount below. + continue; + } + Node aRep = d_state.getRepresentative(aPair.first); + groupUp1(n, aRep, part); + d_im.doPendingLemmas(); + if (d_im.hasSent()) + { + return; + } + } + for (const auto& aPair : negativeMembersA) + { + Node aRep = d_state.getRepresentative(aPair.first); + groupUp2(n, aRep, part); + d_im.doPendingLemmas(); + if (d_im.hasSent()) + { + return; + } + } + Node nRep = d_state.getRepresentative(n); + const std::map& parts = d_state.getMembers(nRep); + for (std::map::const_iterator partIt1 = parts.begin(); + partIt1 != parts.end(); + ++partIt1) + { + Node part1 = d_state.getRepresentative(partIt1->first); + std::vector partEqc; + d_state.getEquivalenceClass(part1, partEqc); + bool newPart = true; + for (Node p : partEqc) + { + if (p.getKind() == APPLY_UF && p.getOperator() == part) + { + newPart = false; + } + } + if (newPart) + { + // only apply the groupPartCount rule for a part that does not have + // nodes of the form (part x) introduced by the group up rule above. + groupPartMember(n, part1, part); + d_im.doPendingLemmas(); + if (d_im.hasSent()) + { + return; + } + } + Node part1Rep = d_state.getRepresentative(part1); + const std::map& partElements = d_state.getMembers(part1Rep); + for (std::map::const_iterator i = partElements.begin(); + i != partElements.end(); + ++i) + { + Node x = d_state.getRepresentative(i->first); + if (!skolems->contains(x)) + { + // only apply down rules for elements not generated by groupPartCount + // rule above + groupDown(n, part1, x, part); + d_im.doPendingLemmas(); + if (d_im.hasSent()) + { + return; + } + } + + std::map::const_iterator j = i; + ++j; + while (j != partElements.end()) + { + Node y = d_state.getRepresentative(j->first); + // x, y should have the same projection + groupSameProjection(n, part1, x, y, part); + d_im.doPendingLemmas(); + if (d_im.hasSent()) + { + return; + } + ++j; + } + + for (const auto& aPair : membersA) + { + Node y = d_state.getRepresentative(aPair.first); + if (x != y) + { + // x, y should have the same projection + groupSamePart(n, part1, x, y, part); + d_im.doPendingLemmas(); + if (d_im.hasSent()) + { + return; + } + } + } + } + } +} + +void TheorySetsPrivate::groupNotEmpty(Node n) +{ + Assert(n.getKind() == RELATION_GROUP); + NodeManager* nm = NodeManager::currentNM(); + TypeNode bagType = n.getType(); + Node A = n[0]; + Node emptyPart = nm->mkConst(EmptySet(A.getType())); + Node skolem = registerAndAssertSkolemLemma(n, "skolem_group"); + + Node A_isEmpty = A.eqNode(emptyPart); + std::vector exp; + exp.push_back(A_isEmpty); + Node singleton = nm->mkNode(SET_SINGLETON, emptyPart); + Node groupIsSingleton = skolem.eqNode(singleton); + + Node conclusion = groupIsSingleton; + d_im.assertInference( + conclusion, InferenceId::SETS_RELS_GROUP_NOT_EMPTY, exp, 1); +} + +void TheorySetsPrivate::groupUp1(Node n, Node x, Node part) +{ + Assert(n.getKind() == RELATION_GROUP); + Assert(x.getType() == n[0].getType().getSetElementType()); + NodeManager* nm = NodeManager::currentNM(); + + Node A = n[0]; + TypeNode setType = A.getType(); + + Node member_x_A = nm->mkNode(SET_MEMBER, x, A); + + std::vector exp; + exp.push_back(member_x_A); + + Node part_x = nm->mkNode(APPLY_UF, part, x); + part_x = registerAndAssertSkolemLemma(part_x, "part_x"); + + Node member_x_part_x = nm->mkNode(SET_MEMBER, x, part_x); + + Node skolem = registerAndAssertSkolemLemma(n, "skolem_group"); + Node member_part_x_n = nm->mkNode(SET_MEMBER, part_x, skolem); + + Node emptyPart = nm->mkConst(EmptySet(setType)); + Node member_emptyPart = nm->mkNode(SET_MEMBER, emptyPart, skolem); + Node emptyPart_not_member = member_emptyPart.notNode(); + + Node conclusion = + nm->mkNode(AND, {member_part_x_n, member_x_part_x, emptyPart_not_member}); + d_im.assertInference(conclusion, InferenceId::SETS_RELS_GROUP_UP1, exp, 1); +} + +void TheorySetsPrivate::groupUp2(Node n, Node x, Node part) +{ + Assert(n.getKind() == RELATION_GROUP); + Assert(x.getType() == n[0].getType().getSetElementType()); + NodeManager* nm = NodeManager::currentNM(); + Node A = n[0]; + TypeNode setType = A.getType(); + + Node member_x_A = nm->mkNode(SET_MEMBER, x, A); + + std::vector exp; + exp.push_back(member_x_A.notNode()); + + Node part_x = nm->mkNode(APPLY_UF, part, x); + part_x = registerAndAssertSkolemLemma(part_x, "part_x"); + Node part_x_is_empty = part_x.eqNode(nm->mkConst(EmptySet(setType))); + Node conclusion = part_x_is_empty; + d_im.assertInference(conclusion, InferenceId::SETS_RELS_GROUP_UP2, exp, 1); +} + +void TheorySetsPrivate::groupDown(Node n, Node B, Node x, Node part) +{ + Assert(n.getKind() == RELATION_GROUP); + Assert(B.getType() == n.getType().getSetElementType()); + Assert(x.getType() == n[0].getType().getSetElementType()); + NodeManager* nm = NodeManager::currentNM(); + Node A = n[0]; + TypeNode setType = A.getType(); + + Node member_x_B = nm->mkNode(SET_MEMBER, x, B); + + Node skolem = registerAndAssertSkolemLemma(n, "skolem_group"); + Node member_B_n = nm->mkNode(SET_MEMBER, B, skolem); + std::vector exp; + exp.push_back(member_B_n); + exp.push_back(member_x_B); + Node member_x_A = nm->mkNode(SET_MEMBER, x, A); + Node part_x = nm->mkNode(APPLY_UF, part, x); + part_x = registerAndAssertSkolemLemma(part_x, "part_x"); + Node part_x_is_B = part_x.eqNode(B); + Node conclusion = nm->mkNode(AND, member_x_A, part_x_is_B); + d_im.assertInference(conclusion, InferenceId::SETS_RELS_GROUP_DOWN, exp, 1); +} + +void TheorySetsPrivate::groupPartMember(Node n, Node B, Node part) +{ + Assert(n.getKind() == RELATION_GROUP); + Assert(B.getType() == n.getType().getSetElementType()); + + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); + + Node A = n[0]; + TypeNode setType = A.getType(); + Node empty = nm->mkConst(EmptySet(setType)); + + Node skolem = registerAndAssertSkolemLemma(n, "skolem_group"); + Node member_B_n = nm->mkNode(SET_MEMBER, B, skolem); + std::vector exp; + exp.push_back(member_B_n); + Node A_notEmpty = A.eqNode(empty).notNode(); + exp.push_back(A_notEmpty); + + Node x = sm->mkSkolemFunction(SkolemFunId::RELATIONS_GROUP_PART_ELEMENT, + setType.getSetElementType(), + {n, B}); + d_state.registerPartElementSkolem(n, x); + Node part_x = nm->mkNode(APPLY_UF, part, x); + part_x = registerAndAssertSkolemLemma(part_x, "part_x"); + Node B_is_part_x = B.eqNode(part_x); + Node member_x_A = nm->mkNode(SET_MEMBER, x, A); + Node member_x_B = nm->mkNode(SET_MEMBER, x, B); + + Node conclusion = nm->mkNode(AND, {B_is_part_x, member_x_B, member_x_A}); + d_im.assertInference( + conclusion, InferenceId::SETS_RELS_GROUP_PART_MEMBER, exp, 1); +} + +void TheorySetsPrivate::groupSameProjection( + Node n, Node B, Node x, Node y, Node part) +{ + Assert(n.getKind() == RELATION_GROUP); + Assert(B.getType() == n.getType().getSetElementType()); + Assert(x.getType() == n[0].getType().getSetElementType()); + Assert(y.getType() == n[0].getType().getSetElementType()); + NodeManager* nm = NodeManager::currentNM(); + + Node A = n[0]; + TypeNode setType = A.getType(); + + Node member_x_B = nm->mkNode(SET_MEMBER, x, B); + Node member_y_B = nm->mkNode(SET_MEMBER, y, B); + + Node skolem = registerAndAssertSkolemLemma(n, "skolem_group"); + Node member_B_n = nm->mkNode(SET_MEMBER, B, skolem); + + // premises + std::vector exp; + exp.push_back(member_B_n); + exp.push_back(member_x_B); + exp.push_back(member_y_B); + exp.push_back(x.eqNode(y).notNode()); + + const std::vector& indices = + n.getOperator().getConst().getIndices(); + + Node xProjection = TupleUtils::getTupleProjection(indices, x); + Node yProjection = TupleUtils::getTupleProjection(indices, y); + Node sameProjection = xProjection.eqNode(yProjection); + Node part_x = nm->mkNode(APPLY_UF, part, x); + part_x = registerAndAssertSkolemLemma(part_x, "part_x"); + Node part_y = nm->mkNode(APPLY_UF, part, y); + part_y = registerAndAssertSkolemLemma(part_y, "part_y"); + Node samePart = part_x.eqNode(part_y); + Node part_x_is_B = part_x.eqNode(B); + Node conclusion = nm->mkNode(AND, sameProjection, samePart, part_x_is_B); + d_im.assertInference( + conclusion, InferenceId::SETS_RELS_GROUP_SAME_PROJECTION, exp, 1); +} + +void TheorySetsPrivate::groupSamePart(Node n, Node B, Node x, Node y, Node part) +{ + Assert(n.getKind() == RELATION_GROUP); + Assert(B.getType() == n.getType().getSetElementType()); + Assert(x.getType() == n[0].getType().getSetElementType()); + Assert(y.getType() == n[0].getType().getSetElementType()); + NodeManager* nm = NodeManager::currentNM(); + Node A = n[0]; + TypeNode setType = A.getType(); + + std::vector exp; + Node member_x_B = nm->mkNode(SET_MEMBER, x, B); + Node member_y_A = nm->mkNode(SET_MEMBER, y, A); + Node member_y_B = nm->mkNode(SET_MEMBER, y, B); + + Node skolem = registerAndAssertSkolemLemma(n, "skolem_group"); + Node member_B_n = nm->mkNode(SET_MEMBER, B, skolem); + const std::vector& indices = + n.getOperator().getConst().getIndices(); + + Node xProjection = TupleUtils::getTupleProjection(indices, x); + Node yProjection = TupleUtils::getTupleProjection(indices, y); + + // premises + exp.push_back(member_B_n); + exp.push_back(member_x_B); + exp.push_back(member_y_A); + exp.push_back(x.eqNode(y).notNode()); + exp.push_back(xProjection.eqNode(yProjection)); + + Node part_x = nm->mkNode(APPLY_UF, part, x); + part_x = registerAndAssertSkolemLemma(part_x, "part_x"); + Node part_y = nm->mkNode(APPLY_UF, part, y); + part_y = registerAndAssertSkolemLemma(part_y, "part_y"); + Node samePart = part_x.eqNode(part_y); + Node part_x_is_B = part_x.eqNode(B); + Node conclusion = nm->mkNode(AND, member_y_B, samePart, part_x_is_B); + + d_im.assertInference( + conclusion, InferenceId::SETS_RELS_GROUP_SAME_PART, exp, 1); +} + +Node TheorySetsPrivate::defineSkolemPartFunction(Node n) +{ + Assert(n.getKind() == RELATION_GROUP); + Node A = n[0]; + TypeNode relationType = A.getType(); + TypeNode elementType = relationType.getSetElementType(); + + // declare an uninterpreted function part: T -> (Relation T) + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); + TypeNode partType = nm->mkFunctionType(elementType, relationType); + Node part = + sm->mkSkolemFunction(SkolemFunId::RELATIONS_GROUP_PART, partType, {n}); + return part; +} + +Node TheorySetsPrivate::registerAndAssertSkolemLemma(Node& n, + const std::string& prefix) +{ + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); + Node skolem = sm->mkPurifySkolem(n, prefix); + Node lemma = n.eqNode(skolem); + d_im.addPendingLemma(lemma, InferenceId::SETS_SKOLEM); + Trace("sets-skolems") << "sets-skolems: " << skolem << " = " << n + << std::endl; + return skolem; +} + void TheorySetsPrivate::checkDisequalities() { // disequalities diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 87ad4678e..e80aa7012 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -127,6 +127,151 @@ class TheorySetsPrivate : protected EnvObj * ) */ void checkMapDown(); + void checkGroups(); + void checkGroup(Node n); + /** + * @param n has form ((_ rel.group n1 ... nk) A) where A has type T + * @return an inference that represents: + * (=> + * (= A (as set.empty T)) + * (= skolem (set.singleton (as set.empty T))) + * ) + */ + void groupNotEmpty(Node n); + /** + * @param n has form ((_ rel.group n1 ... nk) A) where A has type (Relation T) + * @param e an element of type T + * @param part a skolem function of type T -> (Relation T) created uniquely + * for n by defineSkolemPartFunction function below + * @return an inference that represents: + * (=> + * (set.member x A) + * (and + * (set.member (part x) skolem) + * (set.member x (part x)) + * (not (set.member (as set.empty (Relation T)) skolem)) + * ) + * ) + * + * where skolem is a variable equals ((_ rel.group n1 ... nk) A) + */ + void groupUp1(Node n, Node x, Node part); + /** + * @param n has form ((_ rel.group n1 ... nk) A) where A has type (Relation T) + * @param e an element of type T + * @param part a skolem function of type T -> (Relation T) created uniquely + * for n by defineSkolemPartFunction function below + * @return an inference that represents: + * (=> + * (not (set.member x A)) + * (= (part x) (as set.empty (Relation T))) + * ) + * + * where skolem is a variable equals ((_ rel.group n1 ... nk) A) + */ + void groupUp2(Node n, Node x, Node part); + /** + * @param n has form ((_ rel.group n1 ... nk) A) where A has type (Relation T) + * @param B an element of type (Relation T) + * @param x an element of type T + * @param part a skolem function of type T -> (Relation T) created uniquely + * for n by defineSkolemPartFunction function below + * @return an inference that represents: + * (=> + * (and + * (set.member B skolem) + * (set.member x B) + * ) + * (and + * (set.member x A) + * (= (part x) B) + * ) + * ) + * where skolem is a variable equals ((_ table.group n1 ... nk) A). + */ + void groupDown(Node n, Node B, Node x, Node part); + /** + * @param n has form ((_ rel.group n1 ... nk) A) where A has type (Relation T) + * @param B an element of type (Relation T) and B is not of the form (part x) + * @param part a skolem function of type T -> (Relation T) created uniquely + * for n by defineSkolemPartFunction function below + * @return an inference that represents: + * (=> + * (and + * (set.member B skolem) + * (not (= A (as set.empty (Relation T))) + * ) + * (and + * (= B (part k_{n, B})) + * (set.member k_{n,B} B) + * (set.member k_{n,B} A) + * ) + * ) + * where skolem is a variable equals ((_ rel.group n1 ... nk) A), and + * k_{n, B} is a fresh skolem of type T. + */ + void groupPartMember(Node n, Node B, Node part); + /** + * @param n has form ((_ rel.group n1 ... nk) A) where A has type (Relation T) + * @param B an element of type (Relation T) + * @param x an element of type T + * @param y an element of type T + * @param part a skolem function of type T -> (Relation T) created uniquely + * for n by defineSkolemPartFunction function below + * @return an inference that represents: + * (=> + * (and + * (set.member B skolem) + * (set.member x B) + * (set.member y B) + * (distinct x y) + * ) + * (and + * (= ((_ tuple.project n1 ... nk) x) + * ((_ tuple.project n1 ... nk) y)) + * (= (part x) (part y)) + * (= (part x) B) + * ) + * ) + * where skolem is a variable equals ((_ rel.group n1 ... nk) A). + */ + void groupSameProjection(Node n, Node B, Node x, Node y, Node part); + /** + * @param n has form ((_ rel.group n1 ... nk) A) where A has type (Relation T) + * @param B an element of type (Relation T) + * @param x an element of type T + * @param y an element of type T + * @param part a skolem function of type T -> (Relation T) created uniquely + * for n by defineSkolemPartFunction function below + * @return an inference that represents: + * (=> + * (and + * (set.member B skolem) + * (set.member x B) + * (set.member y A) + * (distinct x y) + * (= ((_ tuple.project n1 ... nk) x) + * ((_ tuple.project n1 ... nk) y)) + * ) + * (and + * (set.member y B) + * (= (part x) (part y)) + * (= (part x) B) + * ) + * ) + * where skolem is a variable equals ((_ rel.group n1 ... nk) A). + */ + void groupSamePart(Node n, Node B, Node x, Node y, Node part); + /** + * @param n has form ((_ rel.group n1 ... nk) A) where A has type (Relation T) + * @return a function of type T -> (Relation T) that maps elements T to a + * part in the partition + */ + Node defineSkolemPartFunction(Node n); + /** + * generate skolem variable for node n and add pending lemma for the equality + */ + Node registerAndAssertSkolemLemma(Node& n, const std::string& prefix); /** * This implements a strategy for splitting for set disequalities which * roughly corresponds the SET DISEQUALITY rule from Bansal et al IJCAR 2016. diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 8ee9a33d1..5fcd15dd1 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -589,8 +589,8 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { break; } - default: - break; + case RELATION_GROUP: return postRewriteGroup(node); + default: break; } return RewriteResponse(REWRITE_DONE, node); @@ -741,6 +741,30 @@ RewriteResponse TheorySetsRewriter::postRewriteFold(TNode n) } } +RewriteResponse TheorySetsRewriter::postRewriteGroup(TNode n) +{ + Assert(n.getKind() == kind::RELATION_GROUP); + Node A = n[0]; + Kind k = A.getKind(); + if (k == SET_EMPTY || k == SET_SINGLETON) + { + NodeManager* nm = NodeManager::currentNM(); + // - ((_ rel.group n1 ... nk) (as set.empty (Relation T))) = + // (rel.singleton (as set.empty (Relation T) )) + // - ((_ rel.group n1 ... nk) (set.singleton x)) = + // (set.singleton (set.singleton x)) + Node singleton = nm->mkNode(SET_SINGLETON, A); + return RewriteResponse(REWRITE_AGAIN_FULL, singleton); + } + if (A.isConst()) + { + Node evaluation = RelsUtils::evaluateGroup(n); + return RewriteResponse(REWRITE_AGAIN_FULL, evaluation); + } + + return RewriteResponse(REWRITE_DONE, n); +} + } // namespace sets } // namespace theory } // namespace cvc5::internal diff --git a/src/theory/sets/theory_sets_rewriter.h b/src/theory/sets/theory_sets_rewriter.h index ba48e4030..dc4f64762 100644 --- a/src/theory/sets/theory_sets_rewriter.h +++ b/src/theory/sets/theory_sets_rewriter.h @@ -102,6 +102,15 @@ private: * where f: T -> S -> S, and t : S */ RewriteResponse postRewriteFold(TNode n); + /** + * rewrites for n include: + * - ((_ rel.group n1 ... nk) (as set.empty (Relation T))) = + * (rel.singleton (as set.empty (Relation T) )) + * - ((_ rel.group n1 ... nk) (set.singleton x)) = + * (set.singleton (set.singleton x)) + * - Evaluation of ((_ rel.group n1 ... nk) A) when A is a constant + */ + RewriteResponse postRewriteGroup(TNode n); }; /* class TheorySetsRewriter */ } // namespace sets diff --git a/src/theory/sets/theory_sets_type_rules.cpp b/src/theory/sets/theory_sets_type_rules.cpp index b2eb7987a..8a163489a 100644 --- a/src/theory/sets/theory_sets_type_rules.cpp +++ b/src/theory/sets/theory_sets_type_rules.cpp @@ -20,6 +20,8 @@ #include "theory/sets/normal_form.h" #include "util/cardinality.h" +#include "theory/datatypes/project_op.h" +#include "theory/datatypes/tuple_utils.h" namespace cvc5::internal { namespace theory { @@ -577,6 +579,39 @@ TypeNode RelIdenTypeRule::computeType(NodeManager* nodeManager, return nodeManager->mkSetType(nodeManager->mkTupleType(tupleTypes)); } +TypeNode RelationGroupTypeRule::computeType(NodeManager* nm, TNode n, bool check) +{ + Assert(n.getKind() == kind::RELATION_GROUP && n.hasOperator() + && n.getOperator().getKind() == kind::RELATION_GROUP_OP); + ProjectOp op = n.getOperator().getConst(); + const std::vector& indices = op.getIndices(); + + TypeNode setType = n[0].getType(check); + + if (check) + { + if (!setType.isSet()) + { + std::stringstream ss; + ss << "RELATION_GROUP operator expects a relation. Found '" << n[0] + << "' of type '" << setType << "'."; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + + TypeNode tupleType = setType.getSetElementType(); + if (!tupleType.isTuple()) + { + std::stringstream ss; + ss << "RELATION_GROUP operator expects a relation. Found '" << n[0] + << "' of type '" << setType << "'."; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + + datatypes::TupleUtils::checkTypeIndices(n, tupleType, indices); + } + return nm->mkSetType(setType); +} + Cardinality SetsProperties::computeCardinality(TypeNode type) { Assert(type.getKind() == kind::SET_TYPE); diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index 59ea66158..551513fe6 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -212,6 +212,17 @@ struct RelIdenTypeRule static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * Relation group operator is indexed by a list of indices (n_1, ..., n_k). It + * ensures that the argument is a relation whose arity is greater than each n_i + * for i = 1, ..., k. If the passed relation is of type T, then the returned + * type is (Set T), i.e., set of relations. + */ +struct RelationGroupTypeRule +{ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; /* struct RelationGroupTypeRule */ + struct SetsProperties { static Cardinality computeCardinality(TypeNode type); diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 1a159a942..0697ccb53 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -2505,6 +2505,11 @@ set(regress_1_tests regress1/sets/proj-issue164.smt2 regress1/sets/proj-issue178.smt2 regress1/sets/proj-issue494-finite-leafof.smt2 + regress1/sets/relation_group1.smt2 + regress1/sets/relation_group2.smt2 + regress1/sets/relation_group3.smt2 + regress1/sets/relation_group4.smt2 + regress1/sets/relation_group5.smt2 regress1/sets/remove_check_free_31_6.smt2 regress1/sets/sets-disequal.smt2 regress1/sets/sets-tuple-poly.cvc.smt2 diff --git a/test/regress/cli/regress1/sets/relation_group1.smt2 b/test/regress/cli/regress1/sets/relation_group1.smt2 new file mode 100644 index 000000000..867c1d6ab --- /dev/null +++ b/test/regress/cli/regress1/sets/relation_group1.smt2 @@ -0,0 +1,110 @@ +(set-logic HO_ALL) + +(set-info :status sat) + +(define-fun truthRelation () (Relation String String String) + (set.union + (set.singleton (tuple "A" "X" "0")) + (set.singleton (tuple "A" "X" "1")) + (set.singleton (tuple "A" "Y" "0")) + (set.singleton (tuple "A" "Y" "1")) + (set.singleton (tuple "B" "X" "0")) + (set.singleton (tuple "B" "X" "1")) + (set.singleton (tuple "B" "Y" "0")) + (set.singleton (tuple "B" "Y" "1")))) + +; parition by first column +(assert + (= ((_ rel.group 0) truthRelation) + (set.union + (set.singleton + (set.union (set.singleton (tuple "A" "X" "0")) + (set.singleton (tuple "A" "X" "1")) + (set.singleton (tuple "A" "Y" "0")) + (set.singleton (tuple "A" "Y" "1")))) + (set.singleton + (set.union (set.singleton (tuple "B" "X" "0")) + (set.singleton (tuple "B" "X" "1")) + (set.singleton (tuple "B" "Y" "0")) + (set.singleton (tuple "B" "Y" "1"))))))) + +; parition by second column +(assert + (= ((_ rel.group 1) truthRelation) + (set.union + (set.singleton + (set.union (set.singleton (tuple "A" "X" "0")) + (set.singleton (tuple "A" "X" "1")) + (set.singleton (tuple "B" "X" "0")) + (set.singleton (tuple "B" "X" "1")))) + (set.singleton + (set.union (set.singleton (tuple "A" "Y" "0")) + (set.singleton (tuple "A" "Y" "1")) + (set.singleton (tuple "B" "Y" "0")) + (set.singleton (tuple "B" "Y" "1"))))))) + +; parition by third column +(assert + (= ((_ rel.group 2) truthRelation) + (set.union + (set.singleton + (set.union (set.singleton (tuple "A" "X" "0")) + (set.singleton (tuple "A" "Y" "0")) + (set.singleton (tuple "B" "X" "0")) + (set.singleton (tuple "B" "Y" "0")))) + (set.singleton + (set.union (set.singleton (tuple "A" "X" "1")) + (set.singleton (tuple "A" "Y" "1")) + (set.singleton (tuple "B" "X" "1")) + (set.singleton (tuple "B" "Y" "1"))))))) + +; parition by first,second columns +(assert + (= ((_ rel.group 0 1) truthRelation) + (set.union + (set.singleton + (set.union (set.singleton (tuple "A" "X" "0")) + (set.singleton (tuple "A" "X" "1")))) + (set.singleton + (set.union (set.singleton (tuple "A" "Y" "0")) + (set.singleton (tuple "A" "Y" "1")))) + (set.singleton + (set.union (set.singleton (tuple "B" "X" "0")) + (set.singleton (tuple "B" "X" "1")))) + (set.singleton + (set.union (set.singleton (tuple "B" "Y" "0")) + (set.singleton (tuple "B" "Y" "1"))))))) + +; parition by no column +(assert + (= (rel.group truthRelation) + (set.singleton + (set.union + (set.singleton (tuple "A" "X" "0")) + (set.singleton (tuple "A" "X" "1")) + (set.singleton (tuple "A" "Y" "0")) + (set.singleton (tuple "A" "Y" "1")) + (set.singleton (tuple "B" "X" "0")) + (set.singleton (tuple "B" "X" "1")) + (set.singleton (tuple "B" "Y" "0")) + (set.singleton (tuple "B" "Y" "1")))))) + +; parition by all columns +(assert + (= ((_ rel.group 0 1 2) truthRelation) + (set.union + (set.singleton (set.singleton (tuple "A" "X" "0"))) + (set.singleton (set.singleton (tuple "A" "X" "1"))) + (set.singleton (set.singleton (tuple "A" "Y" "0"))) + (set.singleton (set.singleton (tuple "A" "Y" "1"))) + (set.singleton (set.singleton (tuple "B" "X" "0"))) + (set.singleton (set.singleton (tuple "B" "X" "1"))) + (set.singleton (set.singleton (tuple "B" "Y" "0"))) + (set.singleton (set.singleton (tuple "B" "Y" "1")))))) + +; group of set.empty +(assert + (= ((_ rel.group 0) (as set.empty (Relation String String String))) + (set.singleton (as set.empty (Relation String String String))))) + +(check-sat) diff --git a/test/regress/cli/regress1/sets/relation_group2.smt2 b/test/regress/cli/regress1/sets/relation_group2.smt2 new file mode 100644 index 000000000..992e6a230 --- /dev/null +++ b/test/regress/cli/regress1/sets/relation_group2.smt2 @@ -0,0 +1,16 @@ +(set-logic HO_ALL) + +(set-info :status sat) + +(declare-fun data () (Relation String String String)) +(declare-fun part1 () (Relation String String String)) +(declare-fun part2 () (Relation String String String)) +(declare-fun partition () (Set (Relation String String String))) + +(assert (distinct data part1 part2 (as set.empty (Relation String String String)))) + +(assert (= partition ((_ rel.group 0) data))) +(assert (set.member part1 partition)) +(assert (set.member part2 partition)) + +(check-sat) diff --git a/test/regress/cli/regress1/sets/relation_group3.smt2 b/test/regress/cli/regress1/sets/relation_group3.smt2 new file mode 100644 index 000000000..2af8f0cb8 --- /dev/null +++ b/test/regress/cli/regress1/sets/relation_group3.smt2 @@ -0,0 +1,21 @@ +; DISABLE-TESTER: lfsc +; Disabled since rel.group is not supported in LFSC +(set-logic HO_ALL) + +(set-info :status unsat) + +(declare-fun data () (Relation String String String)) +(declare-fun part1 () (Relation String String String)) +(declare-fun part2 () (Relation String String String)) +(declare-fun partition () (Set (Relation String String String))) + +(assert (distinct data part1 part2 (as set.empty (Relation String String String)))) + +(assert (= partition ((_ rel.group 0 1) data))) +(assert (set.member part1 partition)) +(assert (set.member part2 partition)) + +(assert (set.member (tuple "A" "X" "0") part1)) +(assert (set.member (tuple "A" "X" "1") part2)) + +(check-sat) diff --git a/test/regress/cli/regress1/sets/relation_group4.smt2 b/test/regress/cli/regress1/sets/relation_group4.smt2 new file mode 100644 index 000000000..33136c78f --- /dev/null +++ b/test/regress/cli/regress1/sets/relation_group4.smt2 @@ -0,0 +1,13 @@ +(set-logic HO_ALL) + +(set-info :status sat) + +(declare-fun data () (Relation String String String)) +(declare-fun groupBy0 () (Set (Relation String String String))) +(declare-fun groupBy1 () (Set (Relation String String String))) + +(assert (= groupBy0 ((_ rel.group 0) data))) +(assert (= groupBy1 ((_ rel.group 1) data))) +(assert (distinct groupBy0 groupBy1)) + +(check-sat) diff --git a/test/regress/cli/regress1/sets/relation_group5.smt2 b/test/regress/cli/regress1/sets/relation_group5.smt2 new file mode 100644 index 000000000..d9dc1bcd2 --- /dev/null +++ b/test/regress/cli/regress1/sets/relation_group5.smt2 @@ -0,0 +1,15 @@ +; DISABLE-TESTER: lfsc +; Disabled since table.group is not supported in LFSC +(set-logic HO_ALL) + +(set-info :status unsat) + +(declare-fun data () (Relation String String String)) +(declare-fun groupBy01 () (Set (Relation String String String))) +(declare-fun groupBy10 () (Set (Relation String String String))) + +(assert (= groupBy01 ((_ rel.group 0 1) data))) +(assert (= groupBy10 ((_ rel.group 1 0) data))) +(assert (distinct groupBy01 groupBy10)) + +(check-sat)