From a928211cee1c0e1e0cf46f28e65854c0cee94ca5 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Tue, 7 Jun 2022 13:37:07 -0500 Subject: [PATCH] Add set.filter operator and its inference rules (#8856) --- proofs/lfsc/signatures/theory_def.plf | 2 + src/api/cpp/cvc5.cpp | 2 + src/api/cpp/cvc5_kind.h | 41 +++++++-- src/parser/smt2/smt2.cpp | 1 + src/printer/smt2/smt2_printer.cpp | 1 + src/theory/bags/bag_solver.cpp | 4 +- src/theory/bags/inference_generator.cpp | 4 +- src/theory/bags/inference_generator.h | 4 +- src/theory/bags/kinds | 2 +- src/theory/inference_id.cpp | 2 + src/theory/inference_id.h | 2 + src/theory/sets/kinds | 5 ++ src/theory/sets/solver_state.cpp | 7 ++ src/theory/sets/solver_state.h | 4 + src/theory/sets/theory_sets_private.cpp | 84 ++++++++++++++++++- src/theory/sets/theory_sets_private.h | 23 +++++ src/theory/sets/theory_sets_rewriter.cpp | 36 ++++++++ src/theory/sets/theory_sets_rewriter.h | 11 +++ src/theory/sets/theory_sets_type_rules.cpp | 42 ++++++++++ src/theory/sets/theory_sets_type_rules.h | 9 ++ test/regress/cli/CMakeLists.txt | 4 + test/regress/cli/regress1/bags/filter3.smt2 | 2 +- .../cli/regress1/sets/set_filter1.smt2 | 11 +++ .../cli/regress1/sets/set_filter2.smt2 | 9 ++ .../cli/regress1/sets/set_filter3.smt2 | 11 +++ .../cli/regress1/sets/set_filter4.smt2 | 11 +++ 26 files changed, 315 insertions(+), 19 deletions(-) create mode 100644 test/regress/cli/regress1/sets/set_filter1.smt2 create mode 100644 test/regress/cli/regress1/sets/set_filter2.smt2 create mode 100644 test/regress/cli/regress1/sets/set_filter3.smt2 create mode 100644 test/regress/cli/regress1/sets/set_filter4.smt2 diff --git a/proofs/lfsc/signatures/theory_def.plf b/proofs/lfsc/signatures/theory_def.plf index 04ac320ae..30f00dc29 100644 --- a/proofs/lfsc/signatures/theory_def.plf +++ b/proofs/lfsc/signatures/theory_def.plf @@ -487,6 +487,8 @@ (define rel.join_image (# x term (# y term (apply (apply f_rel.join_image x) y)))) (declare f_set.insert term) (define set.insert (# x term (# y term (apply (apply f_set.insert x) y)))) +(declare f_set.filter term) +(define set.filter (# x term (# y term (apply (apply f_set.filter x) y)))) (declare f_set.map term) (define set.map (# x term (# y term (apply (apply f_set.map x) y)))) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 9705757b9..baa94039a 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -301,6 +301,7 @@ const static std::unordered_map> KIND_ENUM(SET_CHOOSE, internal::Kind::SET_CHOOSE), KIND_ENUM(SET_IS_SINGLETON, internal::Kind::SET_IS_SINGLETON), KIND_ENUM(SET_MAP, internal::Kind::SET_MAP), + KIND_ENUM(SET_FILTER, internal::Kind::SET_FILTER), /* Relations -------------------------------------------------------- */ KIND_ENUM(RELATION_JOIN, internal::Kind::RELATION_JOIN), KIND_ENUM(RELATION_PRODUCT, internal::Kind::RELATION_PRODUCT), @@ -623,6 +624,7 @@ const static std::unordered_map&) 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 + */ + SET_FILTER, /* Relations ------------------------------------------------------------- */ /** @@ -3624,15 +3651,15 @@ enum Kind : int32_t * \rst * This operator filters the elements of a bag. * (bag.filter :math:`p \; B`) takes a predicate :math:`p` of Sort - * :math:`(\rightarrow S_1 \; S_2)` as a first argument, and a bag :math:`B` - * of Sort (Bag :math:`S`) as a second argument, and returns a subbag of Sort + * :math:`(\rightarrow T \; Bool)` as a first argument, and a bag :math:`B` + * of Sort (Bag :math:`T`) as a second argument, and returns a subbag of Sort * (Bag :math:`T`) that includes all elements of :math:`B` that satisfy * :math:`p` with the same multiplicity. * * - Arity: ``2`` * - * - ``1:`` Term of function Sort :math:`(\rightarrow S_1 \; S_2)` - * - ``2:`` Term of bag Sort (Bag :math:`S_1`) + * - ``1:`` Term of function Sort :math:`(\rightarrow T \; Bool)` + * - ``2:`` Term of bag Sort (Bag :math:`T`) * \endrst * * - Create Term of this Kind with: @@ -3640,10 +3667,6 @@ enum Kind : int32_t * - Solver::mkTerm(Kind, const std::vector&) const * - Solver::mkTerm(const Op&, const std::vector&) const * - * - Create Op of this kind with: - * - * - Solver::mkOp(Kind, const std::vector&) const - * * \rst * .. warning:: This kind is experimental and may be changed or removed in * future versions. diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 66f2db214..cbf699f6b 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -605,6 +605,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) addOperator(cvc5::SET_CHOOSE, "set.choose"); addOperator(cvc5::SET_IS_SINGLETON, "set.is_singleton"); addOperator(cvc5::SET_MAP, "set.map"); + addOperator(cvc5::SET_FILTER, "set.filter"); addOperator(cvc5::RELATION_JOIN, "rel.join"); addOperator(cvc5::RELATION_PRODUCT, "rel.product"); addOperator(cvc5::RELATION_TRANSPOSE, "rel.transpose"); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 6a7b8ccb6..5908e82e7 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1152,6 +1152,7 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v) case kind::SET_CHOOSE: return "set.choose"; case kind::SET_IS_SINGLETON: return "set.is_singleton"; case kind::SET_MAP: return "set.map"; + case kind::SET_FILTER: return "set.filter"; case kind::RELATION_JOIN: return "rel.join"; case kind::RELATION_PRODUCT: return "rel.product"; case kind::RELATION_TRANSPOSE: return "rel.transpose"; diff --git a/src/theory/bags/bag_solver.cpp b/src/theory/bags/bag_solver.cpp index 5118df462..5f52c6215 100644 --- a/src/theory/bags/bag_solver.cpp +++ b/src/theory/bags/bag_solver.cpp @@ -302,12 +302,12 @@ void BagSolver::checkFilter(Node n) for (const Node& e : elements) { - InferInfo i = d_ig.filterDownwards(n, d_state.getRepresentative(e)); + InferInfo i = d_ig.filterDown(n, d_state.getRepresentative(e)); d_im.lemmaTheoryInference(&i); } for (const Node& e : elements) { - InferInfo i = d_ig.filterUpwards(n, d_state.getRepresentative(e)); + InferInfo i = d_ig.filterUp(n, d_state.getRepresentative(e)); d_im.lemmaTheoryInference(&i); } } diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp index 8d8ee22c5..31509fa9c 100644 --- a/src/theory/bags/inference_generator.cpp +++ b/src/theory/bags/inference_generator.cpp @@ -533,7 +533,7 @@ InferInfo InferenceGenerator::mapUp( return inferInfo; } -InferInfo InferenceGenerator::filterDownwards(Node n, Node e) +InferInfo InferenceGenerator::filterDown(Node n, Node e) { Assert(n.getKind() == BAG_FILTER && n[1].getType().isBag()); Assert(e.getType() == n[1].getType().getBagElementType()); @@ -555,7 +555,7 @@ InferInfo InferenceGenerator::filterDownwards(Node n, Node e) return inferInfo; } -InferInfo InferenceGenerator::filterUpwards(Node n, Node e) +InferInfo InferenceGenerator::filterUp(Node n, Node e) { Assert(n.getKind() == BAG_FILTER && n[1].getType().isBag()); Assert(e.getType() == n[1].getType().getBagElementType()); diff --git a/src/theory/bags/inference_generator.h b/src/theory/bags/inference_generator.h index 7d92ea4b0..91a3ea08a 100644 --- a/src/theory/bags/inference_generator.h +++ b/src/theory/bags/inference_generator.h @@ -289,7 +289,7 @@ class InferenceGenerator * (= (bag.count e skolem) (bag.count e A))) * where skolem is a variable equals (bag.filter p A) */ - InferInfo filterDownwards(Node n, Node e); + InferInfo filterDown(Node n, Node e); /** * @param n is (bag.filter p A) where p is a function (-> E Bool), @@ -303,7 +303,7 @@ class InferenceGenerator * (and (not (p e)) (= (bag.count e skolem) 0))) * where skolem is a variable equals (bag.filter p A) */ - InferInfo filterUpwards(Node n, Node e); + InferInfo filterUp(Node n, Node e); /** * @param n is a (table.product A B) where A, B are tables diff --git a/src/theory/bags/kinds b/src/theory/bags/kinds index 2522585bd..9961b5864 100644 --- a/src/theory/bags/kinds +++ b/src/theory/bags/kinds @@ -71,7 +71,7 @@ operator BAG_CHOOSE 1 "return an element in the bag given as a parameter operator BAG_MAP 2 "bag map function" # The bag.filter operator takes a predicate of type (-> T Bool) and a bag of type (Bag T) -# and return the same bag excluding those elements that do not satisfy the predicate +# and returns the same bag excluding those elements that do not satisfy the predicate operator BAG_FILTER 2 "bag filter operator" # bag.fold operator combines elements of a bag into a single value. diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index 3637a5e0e..55cb72451 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -333,6 +333,8 @@ const char* toString(InferenceId i) case InferenceId::SETS_EQ_CONFLICT: return "SETS_EQ_CONFLICT"; case InferenceId::SETS_EQ_MEM: return "SETS_EQ_MEM"; case InferenceId::SETS_EQ_MEM_CONFLICT: return "SETS_EQ_MEM_CONFLICT"; + case InferenceId::SETS_FILTER_DOWN: return "SETS_FILTER_DOWN"; + case InferenceId::SETS_FILTER_UP: return "SETS_FILTER_UP"; case InferenceId::SETS_MAP_DOWN_POSITIVE: return "SETS_MAP_DOWN_POSITIVE"; case InferenceId::SETS_MAP_UP: return "SETS_MAP_UP"; case InferenceId::SETS_MEM_EQ: return "SETS_MEM_EQ"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index bd0e2fc7e..3a6452e45 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -486,6 +486,8 @@ enum class InferenceId SETS_EQ_CONFLICT, SETS_EQ_MEM, SETS_EQ_MEM_CONFLICT, + SETS_FILTER_DOWN, + SETS_FILTER_UP, SETS_MAP_DOWN_POSITIVE, SETS_MAP_UP, SETS_MEM_EQ, diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index da7c2b930..d1e22cab1 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -77,6 +77,10 @@ operator SET_IS_SINGLETON 1 "return whether the given set is a singleton" # of the second argument, a set of type (Set T1), and returns a set of type (Set T2). operator SET_MAP 2 "set map function" +# The set.filter operator takes a predicate of type (-> T Bool) and a set of type (Set T) +# and returns the same set excluding those elements that do not satisfy the predicate +operator SET_FILTER 2 "set filter operator" + operator RELATION_JOIN 2 "relation join" operator RELATION_PRODUCT 2 "relation cartesian product" operator RELATION_TRANSPOSE 1 "relation transpose" @@ -99,6 +103,7 @@ typerule SET_COMPREHENSION ::cvc5::internal::theory::sets::ComprehensionTypeRul typerule SET_CHOOSE ::cvc5::internal::theory::sets::ChooseTypeRule typerule SET_IS_SINGLETON ::cvc5::internal::theory::sets::IsSingletonTypeRule typerule SET_MAP ::cvc5::internal::theory::sets::SetMapTypeRule +typerule SET_FILTER ::cvc5::internal::theory::sets::SetFilterTypeRule typerule RELATION_JOIN ::cvc5::internal::theory::sets::RelBinaryOperatorTypeRule typerule RELATION_PRODUCT ::cvc5::internal::theory::sets::RelBinaryOperatorTypeRule diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp index 5c3874936..cb02f4b06 100644 --- a/src/theory/sets/solver_state.cpp +++ b/src/theory/sets/solver_state.cpp @@ -54,6 +54,7 @@ void SolverState::reset() d_bop_index.clear(); d_op_list.clear(); d_allCompSets.clear(); + d_filterTerms.clear(); } void SolverState::registerEqc(TypeNode tn, Node r) @@ -139,6 +140,10 @@ void SolverState::registerTerm(Node r, TypeNode tnn, Node n) d_nvar_sets[r].push_back(n); Trace("sets-debug2") << "Non-var-set[" << r << "] : " << n << std::endl; } + else if (nk == SET_FILTER) + { + d_filterTerms.push_back(n); + } else if (nk == SET_MAP) { d_mapTerms.insert(n); @@ -472,6 +477,8 @@ const std::map >& SolverState::getOperatorList() const return d_op_list; } +const std::vector& SolverState::getFilterTerms() const { return d_filterTerms; } + const context::CDHashSet& SolverState::getMapTerms() const { return d_mapTerms; } std::shared_ptr> SolverState::getMapSkolemElements( diff --git a/src/theory/sets/solver_state.h b/src/theory/sets/solver_state.h index 307d37c07..ab240ab22 100644 --- a/src/theory/sets/solver_state.h +++ b/src/theory/sets/solver_state.h @@ -161,6 +161,8 @@ class SolverState : public TheoryState * map is a representative of its congruence class. */ const std::map >& getOperatorList() const; + /** Get the list of all set.filter terms */ + 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 skolem elements generated for map terms down rules in @@ -218,6 +220,8 @@ class SolverState : public TheoryState std::map d_congruent; /** Map from equivalence classes to the list of non-variable sets in it */ std::map > d_nvar_sets; + /** A list of filter terms. It is initialized during full effort check */ + std::vector d_filterTerms; /** User context collection of set.map terms */ context::CDHashSet d_mapTerms; /** User context collection of skolem elements generated for set.map terms */ diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 4aae37ecf..8c2665eb8 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -364,6 +364,20 @@ void TheorySetsPrivate::fullEffortCheck() { continue; } + // check filter up rule + checkFilterUp(); + d_im.doPendingLemmas(); + if (d_im.hasSent()) + { + continue; + } + // check filter down rules + checkFilterDown(); + d_im.doPendingLemmas(); + if (d_im.hasSent()) + { + continue; + } // check map up rules checkMapUp(); d_im.doPendingLemmas(); @@ -679,6 +693,70 @@ void TheorySetsPrivate::checkUpwardsClosure() } } +void TheorySetsPrivate::checkFilterUp() +{ + NodeManager* nm = NodeManager::currentNM(); + const std::vector& filterTerms = d_state.getFilterTerms(); + + for (const Node& term : filterTerms) + { + Node p = term[0]; + Node A = term[1]; + const std::map& positiveMembers = + d_state.getMembers(d_state.getRepresentative(A)); + for (const std::pair& pair : positiveMembers) + { + Node x = pair.first; + std::vector exp; + exp.push_back(pair.second); + Node B = pair.second[1]; + d_state.addEqualityToExp(A, B, exp); + Node p_x = nm->mkNode(APPLY_UF, p, x); + Node skolem = d_treg.getProxy(term); + Node memberFilter = nm->mkNode(kind::SET_MEMBER, x, skolem); + Node not_p_x = p_x.notNode(); + Node not_memberFilter = memberFilter.notNode(); + Node orNode = + p_x.andNode(memberFilter).orNode(not_p_x.andNode(not_memberFilter)); + d_im.assertInference(orNode, InferenceId::SETS_FILTER_UP, exp); + if (d_state.isInConflict()) + { + return; + } + } + } +} + +void TheorySetsPrivate::checkFilterDown() +{ + NodeManager* nm = NodeManager::currentNM(); + const std::vector& filterTerms = d_state.getFilterTerms(); + for (const Node& term : filterTerms) + { + Node p = term[0]; + Node A = term[1]; + + const std::map& positiveMembers = + d_state.getMembers(d_state.getRepresentative(term)); + for (const std::pair& pair : positiveMembers) + { + std::vector exp; + Node B = pair.second[1]; + exp.push_back(pair.second); + d_state.addEqualityToExp(B, term, exp); + Node x = pair.first; + Node memberA = nm->mkNode(kind::SET_MEMBER, x, A); + Node p_x = nm->mkNode(APPLY_UF, p, x); + Node fact = memberA.andNode(p_x); + d_im.assertInference(fact, InferenceId::SETS_FILTER_DOWN, exp); + if (d_state.isInConflict()) + { + return; + } + } + } +} + void TheorySetsPrivate::checkMapUp() { NodeManager* nm = NodeManager::currentNM(); @@ -1164,8 +1242,10 @@ void TheorySetsPrivate::processCarePairArgs(TNode a, TNode b) } } -/** returns whether the given kind is a higher order kind for sets. */ -bool TheorySetsPrivate::isHigherOrderKind(Kind k) { return k == SET_MAP; } +bool TheorySetsPrivate::isHigherOrderKind(Kind k) +{ + return k == SET_MAP || k == SET_FILTER; +} Node TheorySetsPrivate::explain(TNode literal) { diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index cda1fae37..87ad4678e 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -76,6 +76,29 @@ class TheorySetsPrivate : protected EnvObj */ void checkUpwardsClosure(); + /** + * Apply the following rule for filter terms (set.filter p A): + * (=> + * (and (set.member x B) (= A B)) + * (or + * (and (p x) (set.member x (set.filter p A))) + * (and (not (p x)) (not (set.member x (set.filter p A)))) + * ) + * ) + */ + void checkFilterUp(); + /** + * Apply the following rule for filter terms (set.filter p A): + * (=> + * (bag.member x (set.filter p A)) + * (and + * (p x) + * (set.member x A) + * ) + * ) + */ + void checkFilterDown(); + /** * Apply the following rule for map terms (set.map f A): * Positive member rule: diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index d356ddbe7..9a0b5a875 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -333,6 +333,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { } // kind::SET_IS_SINGLETON case SET_MAP: return postRewriteMap(node); + case SET_FILTER: return postRewriteFilter(node); case kind::RELATION_TRANSPOSE: { @@ -669,6 +670,41 @@ RewriteResponse TheorySetsRewriter::postRewriteMap(TNode n) } } +RewriteResponse TheorySetsRewriter::postRewriteFilter(TNode n) +{ + Assert(n.getKind() == kind::SET_FILTER); + NodeManager* nm = NodeManager::currentNM(); + Kind k = n[1].getKind(); + switch (k) + { + case SET_EMPTY: + { + // (set.filter p (as set.empty (Set T)) = (as set.empty (Set T)) + return RewriteResponse(REWRITE_DONE, n[1]); + } + case SET_SINGLETON: + { + // (set.filter p (set.singleton x)) = + // (ite (p x) (set.singleton x) (as set.empty (Set T))) + Node empty = nm->mkConst(EmptySet(n.getType())); + Node condition = nm->mkNode(APPLY_UF, n[0], n[1][0]); + Node ret = nm->mkNode(ITE, condition, n[1], empty); + return RewriteResponse(REWRITE_AGAIN_FULL, ret); + } + case SET_UNION: + { + // (set.filter p (set.union A B)) = + // (set.union (set.filter p A) (set.filter p B)) + Node a = nm->mkNode(SET_FILTER, n[0], n[1][0]); + Node b = nm->mkNode(SET_FILTER, n[0], n[1][1]); + Node ret = nm->mkNode(SET_UNION, a, b); + return RewriteResponse(REWRITE_AGAIN_FULL, ret); + } + + default: 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 ee9c7f8ed..74735a878 100644 --- a/src/theory/sets/theory_sets_rewriter.h +++ b/src/theory/sets/theory_sets_rewriter.h @@ -83,6 +83,17 @@ private: * where f: T1 -> T2 */ RewriteResponse postRewriteMap(TNode n); + + /** + * rewrites for n include: + * - (set.filter p (as set.empty (Set T)) = (as set.empty (Set T)) + * - (set.filter p (set.singleton x)) = + * (ite (p x) (set.singleton x) (as set.empty (Set T))) + * - (set.filter p (set.union A B)) = + * (set.union (set.filter p A) (set.filter p B)) + * where p: T -> Bool + */ + RewriteResponse postRewriteFilter(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 27583e71f..49bd24e17 100644 --- a/src/theory/sets/theory_sets_type_rules.cpp +++ b/src/theory/sets/theory_sets_type_rules.cpp @@ -314,6 +314,48 @@ TypeNode SetMapTypeRule::computeType(NodeManager* nodeManager, return retType; } +TypeNode SetFilterTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + Assert(n.getKind() == kind::SET_FILTER); + TypeNode functionType = n[0].getType(check); + TypeNode setType = n[1].getType(check); + if (check) + { + if (!setType.isSet()) + { + throw TypeCheckingExceptionPrivate( + n, + "set.filter operator expects a set in the second argument, " + "a non-set is found"); + } + + TypeNode elementType = setType.getSetElementType(); + + if (!(functionType.isFunction())) + { + std::stringstream ss; + ss << "Operator " << n.getKind() << " expects a function of type (-> " + << elementType << " Bool) as a first argument. " + << "Found a term of type '" << functionType << "'."; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + std::vector argTypes = functionType.getArgTypes(); + NodeManager* nm = NodeManager::currentNM(); + if (!(argTypes.size() == 1 && argTypes[0] == elementType + && functionType.getRangeType() == nm->booleanType())) + { + std::stringstream ss; + ss << "Operator " << n.getKind() << " expects a function of type (-> " + << elementType << " Bool). " + << "Found a function of type '" << functionType << "'."; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + } + return setType; +} + TypeNode RelBinaryOperatorTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check) diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index ee1fc06c7..7461ec4cc 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -140,6 +140,15 @@ struct SetMapTypeRule static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; /* struct SetMapTypeRule */ +/** + * Type rule for (set.filter p A) to make sure p is a unary predicate of type + * (-> T Bool) where A is a set of type (Set T) + */ +struct SetFilterTypeRule +{ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; /* struct SetFilterTypeRule */ + /** * Type rule for binary operators (rel.join, rel.product) to check * if the two arguments are relations (set of tuples). diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index ec6772707..763270a6f 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -2503,6 +2503,10 @@ set(regress_1_tests regress1/sets/sets-tuple-poly.cvc.smt2 regress1/sets/sets-uc-wrong.smt2 regress1/sets/set-comp-sat.smt2 + regress1/sets/set_filter1.smt2 + regress1/sets/set_filter2.smt2 + regress1/sets/set_filter3.smt2 + regress1/sets/set_filter4.smt2 regress1/sets/set_map_card_incomplete.smt2 regress1/sets/set_map_negative_members.smt2 regress1/sets/set_map_positive_members.smt2 diff --git a/test/regress/cli/regress1/bags/filter3.smt2 b/test/regress/cli/regress1/bags/filter3.smt2 index 10f637015..7453cc00d 100644 --- a/test/regress/cli/regress1/bags/filter3.smt2 +++ b/test/regress/cli/regress1/bags/filter3.smt2 @@ -5,6 +5,6 @@ (declare-fun B () (Bag Int)) (define-fun p ((x Int)) Bool (> x 1)) (assert (= B (bag.filter p A))) -(assert (= (bag.count 3 B) 57)) +(assert (= (bag.count 3 A) 57)) (assert (= (bag.count 3 B) 58)) (check-sat) diff --git a/test/regress/cli/regress1/sets/set_filter1.smt2 b/test/regress/cli/regress1/sets/set_filter1.smt2 new file mode 100644 index 000000000..32e3251a3 --- /dev/null +++ b/test/regress/cli/regress1/sets/set_filter1.smt2 @@ -0,0 +1,11 @@ +(set-logic ALL) +(set-info :status sat) +(declare-fun A () (Set Int)) +(declare-fun B () (Set Int)) +(declare-fun x () Int) +(declare-fun y () Int) +(declare-fun p (Int) Bool) +(assert (= A (set.union (set.singleton x) (set.singleton y)))) +(assert (= B (set.filter p A))) +(assert (distinct (p x) (p y))) +(check-sat) diff --git a/test/regress/cli/regress1/sets/set_filter2.smt2 b/test/regress/cli/regress1/sets/set_filter2.smt2 new file mode 100644 index 000000000..d7c08ae2f --- /dev/null +++ b/test/regress/cli/regress1/sets/set_filter2.smt2 @@ -0,0 +1,9 @@ +(set-logic HO_ALL) +(set-info :status sat) +(set-option :fmf-bound true) +(declare-fun A () (Set Int)) +(declare-fun B () (Set Int)) +(declare-fun p (Int) Bool) +(assert (= B (set.filter p A))) +(assert (set.member (- 2) B)) +(check-sat) diff --git a/test/regress/cli/regress1/sets/set_filter3.smt2 b/test/regress/cli/regress1/sets/set_filter3.smt2 new file mode 100644 index 000000000..bf96f92a3 --- /dev/null +++ b/test/regress/cli/regress1/sets/set_filter3.smt2 @@ -0,0 +1,11 @@ +(set-logic HO_ALL) +(set-info :status unsat) +(declare-fun A () (Set Int)) +(declare-fun B () (Set Int)) +(declare-fun element () Int) +(declare-fun p (Int) Bool) +(assert (= B (set.filter p A))) +(assert (p element)) +(assert (not (set.member element B))) +(assert (set.member element A)) +(check-sat) diff --git a/test/regress/cli/regress1/sets/set_filter4.smt2 b/test/regress/cli/regress1/sets/set_filter4.smt2 new file mode 100644 index 000000000..858cdc0d4 --- /dev/null +++ b/test/regress/cli/regress1/sets/set_filter4.smt2 @@ -0,0 +1,11 @@ +(set-logic HO_ALL) +(set-info :status unsat) +(declare-fun A () (Set Int)) +(declare-fun B () (Set Int)) +(declare-fun element () Int) +(declare-fun p (Int) Bool) +(assert (= B (set.filter p A))) +(assert (p element)) +(assert (not (set.member element A))) +(assert (set.member element B)) +(check-sat) -- 2.30.2