From: mudathirmahgoub Date: Fri, 3 Jun 2022 22:24:39 +0000 (-0500) Subject: Add inference rules for set.map operator (#8849) X-Git-Tag: cvc5-1.0.1~71 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2abc3c3015d2ef0adb027f233f6558afd9b1091b;p=cvc5.git Add inference rules for set.map operator (#8849) --- diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp index 58276262b..d410da650 100644 --- a/src/expr/skolem_manager.cpp +++ b/src/expr/skolem_manager.cpp @@ -97,6 +97,7 @@ const char* toString(SkolemFunId id) case SkolemFunId::BAGS_DEQ_DIFF: return "BAGS_DEQ_DIFF"; case SkolemFunId::SETS_CHOOSE: return "SETS_CHOOSE"; case SkolemFunId::SETS_DEQ_DIFF: return "SETS_DEQ_DIFF"; + case SkolemFunId::SETS_MAP_DOWN_ELEMENT: return "SETS_MAP_DOWN_ELEMENT"; case SkolemFunId::HO_TYPE_MATCH_PRED: return "HO_TYPE_MATCH_PRED"; default: return "?"; } diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h index 9d4f225f9..1d9a74c7a 100644 --- a/src/expr/skolem_manager.h +++ b/src/expr/skolem_manager.h @@ -140,7 +140,7 @@ enum class SkolemFunId */ BAGS_CHOOSE, /** An uninterpreted function for bag.map operator: - * To compute (bag.count y (map f A)), we need to find the distinct + * To compute (bag.count y (bag.map f A)), we need to find the distinct * elements in A that are mapped to y by function f (i.e., preimage of {y}). * If n is the cardinality of this preimage, then * the preimage is the set {uf(1), ..., uf(n)} @@ -149,13 +149,13 @@ enum class SkolemFunId BAGS_MAP_PREIMAGE, /** * A skolem variable for the size of the preimage of {y} that is unique per - * terms (map f A), y which might be an element in (map f A). (see the + * terms (bag.map f A), y which might be an element in (bag.map f A). (see the * documentation for BAGS_MAP_PREIMAGE) */ BAGS_MAP_PREIMAGE_SIZE, /** * A skolem variable for the index that is unique per terms - * (map f A), y, preImageSize, y, e which might be an element in A. + * (bag.map f A), y, preImageSize, y, e which might be an element in A. * (see the documentation for BAGS_MAP_PREIMAGE) */ BAGS_MAP_PREIMAGE_INDEX, @@ -173,15 +173,21 @@ enum class SkolemFunId * (choose A) is expanded as * (witness ((x elementType)) * (ite - * (= A (as emptyset (Set E))) + * (= A (as set.empty (Set E))) * (= x (uf A)) - * (and (member x A) (= x uf(A))) + * (and (set.member x A) (= x uf(A))) * where uf: (Set E) -> E is a skolem function, and E is the type of elements * of A */ SETS_CHOOSE, /** set diff to witness (not (= A B)) */ SETS_DEQ_DIFF, + /** + * A skolem variable that is unique per terms (set.map f A), y which is an + * element in (set.map f A). The skolem is constrained to be an element in A, + * and it is mapped to y by f. + */ + SETS_MAP_DOWN_ELEMENT, /** Higher-order type match predicate, see HoTermDb */ HO_TYPE_MATCH_PRED }; diff --git a/src/theory/incomplete_id.cpp b/src/theory/incomplete_id.cpp index f374f834f..5da59b966 100644 --- a/src/theory/incomplete_id.cpp +++ b/src/theory/incomplete_id.cpp @@ -38,6 +38,7 @@ const char* toString(IncompleteId i) case IncompleteId::QUANTIFIERS_SYGUS_SOLVED: return "QUANTIFIERS_SYGUS_SOLVED"; case IncompleteId::SEP: return "SEP"; + case IncompleteId::SETS_HO_CARD: return "SETS_HO_CARD"; case IncompleteId::SETS_RELS_CARD: return "SETS_RELS_CARD"; case IncompleteId::STRINGS_LOOP_SKIP: return "STRINGS_LOOP_SKIP"; case IncompleteId::STRINGS_REGEXP_NO_SIMPLIFY: diff --git a/src/theory/incomplete_id.h b/src/theory/incomplete_id.h index 98ebd571b..8597b6030 100644 --- a/src/theory/incomplete_id.h +++ b/src/theory/incomplete_id.h @@ -49,6 +49,9 @@ enum class IncompleteId QUANTIFIERS_SYGUS_SOLVED, // incomplete due to separation logic SEP, + // Higher order operators like sets.map were used in combination with set + // cardinality constraints + SETS_HO_CARD, // relations were used in combination with set cardinality constraints SETS_RELS_CARD, // we skipped processing a looping word equation diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index 300cad111..3637a5e0e 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_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"; case InferenceId::SETS_MEM_EQ_CONFLICT: return "SETS_MEM_EQ_CONFLICT"; case InferenceId::SETS_PROXY: return "SETS_PROXY"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index 774a5b586..bd0e2fc7e 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_MAP_DOWN_POSITIVE, + SETS_MAP_UP, SETS_MEM_EQ, SETS_MEM_EQ_CONFLICT, SETS_PROXY, diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp index 70927d524..5c3874936 100644 --- a/src/theory/sets/solver_state.cpp +++ b/src/theory/sets/solver_state.cpp @@ -27,7 +27,11 @@ namespace theory { namespace sets { SolverState::SolverState(Env& env, Valuation val, SkolemCache& skc) - : TheoryState(env, val), d_skCache(skc), d_members(env.getContext()) + : TheoryState(env, val), + d_skCache(skc), + d_mapTerms(env.getUserContext()), + d_mapSkolemElements(env.getUserContext()), + d_members(env.getContext()) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -135,6 +139,16 @@ 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_MAP) + { + d_mapTerms.insert(n); + if (d_mapSkolemElements.find(n) == d_mapSkolemElements.end()) + { + std::shared_ptr> set = + std::make_shared>(d_env.getUserContext()); + d_mapSkolemElements[n] = set; + } + } else if (nk == SET_COMPREHENSION) { d_compSets[r].push_back(n); @@ -411,10 +425,12 @@ const std::vector& SolverState::getComprehensionSets(Node r) const const std::map& SolverState::getMembers(Node r) const { + Assert(r == getRepresentative(r)); return getMembersInternal(r, 0); } const std::map& SolverState::getNegativeMembers(Node r) const { + Assert(r == getRepresentative(r)); return getMembersInternal(r, 1); } const std::map& SolverState::getMembersInternal(Node r, @@ -456,6 +472,14 @@ const std::map >& SolverState::getOperatorList() const return d_op_list; } +const context::CDHashSet& SolverState::getMapTerms() const { return d_mapTerms; } + +std::shared_ptr> SolverState::getMapSkolemElements( + Node n) +{ + return d_mapSkolemElements[n]; +} + const std::vector& SolverState::getComprehensionSets() const { return d_allCompSets; @@ -593,6 +617,14 @@ bool SolverState::merge(TNode t1, return true; } +void SolverState::registerMapSkolemElement(const Node& n, const Node& element) +{ + Assert(n.getKind() == kind::SET_MAP); + Assert(element.getKind() == SKOLEM + && element.getType() == n[1].getType().getSetElementType()); + d_mapSkolemElements[n].get()->insert(element); +} + } // namespace sets } // namespace theory } // namespace cvc5::internal diff --git a/src/theory/sets/solver_state.h b/src/theory/sets/solver_state.h index de829e6c0..307d37c07 100644 --- a/src/theory/sets/solver_state.h +++ b/src/theory/sets/solver_state.h @@ -21,6 +21,7 @@ #include #include +#include "context/cdhashset.h" #include "theory/sets/skolem_cache.h" #include "theory/theory_state.h" #include "theory/uf/equality_engine.h" @@ -160,6 +161,11 @@ class SolverState : public TheoryState * map is a representative of its congruence class. */ const std::map >& getOperatorList() 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 + * the current user context */ + std::shared_ptr> getMapSkolemElements(Node n); /** Get the list of all comprehension sets in the current context */ const std::vector& getComprehensionSets() const; @@ -187,13 +193,17 @@ class SolverState : public TheoryState */ bool merge(TNode t1, TNode t2, std::vector& facts, TNode cset); + /** register the skolem element for the set.map term n */ + void registerMapSkolemElement(const Node& n, const Node& element); + private: /** constants */ Node d_true; Node d_false; /** the empty vector and map */ - std::vector d_emptyVec; - std::map d_emptyMap; + const std::vector d_emptyVec; + /** a convenient constant empty map */ + const std::map d_emptyMap; /** Reference to skolem cache */ SkolemCache& d_skCache; /** The list of all equivalence classes of type set in the current context */ @@ -208,6 +218,11 @@ 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; + /** User context collection of set.map terms */ + context::CDHashSet d_mapTerms; + /** User context collection of skolem elements generated for set.map terms */ + context::CDHashMap>> + d_mapSkolemElements; /** Map from equivalence classes to the list of comprehension sets in it */ std::map > d_compSets; /** Map from equivalence classes to a variable sets in it */ diff --git a/src/theory/sets/term_registry.cpp b/src/theory/sets/term_registry.cpp index 0ea0312c4..3f5bc414d 100644 --- a/src/theory/sets/term_registry.cpp +++ b/src/theory/sets/term_registry.cpp @@ -45,7 +45,8 @@ Node TermRegistry::getProxy(Node n) { Kind nk = n.getKind(); if (nk != SET_EMPTY && nk != SET_SINGLETON && nk != SET_INTER - && nk != SET_MINUS && nk != SET_UNION && nk != SET_UNIVERSE) + && nk != SET_MINUS && nk != SET_UNION && nk != SET_UNIVERSE + && nk != SET_MAP) { return n; } diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 253159361..aceaafe74 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -286,6 +286,10 @@ void TheorySetsPrivate::fullEffortCheck() { d_rels_enabled = true; } + else if(isHigherOrderKind(nk)) + { + d_higher_order_kinds_enabled = true; + } ++eqc_i; } Trace("sets-eqc") << std::endl; @@ -304,6 +308,12 @@ void TheorySetsPrivate::fullEffortCheck() } } + if (d_card_enabled && d_higher_order_kinds_enabled) + { + d_fullCheckIncomplete = true; + d_fullCheckIncompleteId = IncompleteId::SETS_HO_CARD; + } + // We may have sent lemmas while registering the terms in the loop above, // e.g. the cardinality solver. if (d_im.hasSent()) @@ -352,6 +362,20 @@ void TheorySetsPrivate::fullEffortCheck() { continue; } + // check map up rules + checkMapUp(); + d_im.doPendingLemmas(); + if (d_im.hasSent()) + { + continue; + } + // check map down rules + checkMapDown(); + d_im.doPendingLemmas(); + if (d_im.hasSent()) + { + continue; + } // check disequalities checkDisequalities(); d_im.doPendingLemmas(); @@ -653,6 +677,114 @@ void TheorySetsPrivate::checkUpwardsClosure() } } +void TheorySetsPrivate::checkMapUp() +{ + NodeManager* nm = NodeManager::currentNM(); + const context::CDHashSet& mapTerms = d_state.getMapTerms(); + + for (const Node& term : mapTerms) + { + Node f = term[0]; + Node A = term[1]; + const std::map& positiveMembers = + d_state.getMembers(d_state.getRepresentative(A)); + shared_ptr> skolemElements = + d_state.getMapSkolemElements(term); + for (const std::pair& pair : positiveMembers) + { + Node x = pair.first; + if (skolemElements->contains(x)) + { + // Break this cycle between inferences SETS_MAP_DOWN_POSITIVE + // and SETS_MAP_UP: + // 1- If (set.member y (set.map f A)) holds, then SETS_MAP_DOWN_POSITIVE + // inference would generate a fresh skolem x1 such that (= (f x1) y) + // and (set.member x1 A). + // 2- Since (set.member x1 A) holds, SETS_MAP_UP would infer + // (set.member (f x1) (set.map f A)). + // Since (set.member (f x1) (set.map f A)) holds, step 1 would repeat + // and generate a new skolem x2 such that (= (f x2) (f x1)) and + // (set.member x1 A). The cycle continues with step 2. + continue; + } + // (=> + // (and (set.member x B) (= A B)) + // (set.member (f x) (set.map f A)) + // ) + std::vector exp; + exp.push_back(pair.second); + Node B = pair.second[1]; + d_state.addEqualityToExp(A, B, exp); + Node f_x = nm->mkNode(APPLY_UF, f, x); + Node skolem = d_treg.getProxy(term); + Node memberMap = nm->mkNode(kind::SET_MEMBER, f_x, skolem); + d_im.assertInference(memberMap, InferenceId::SETS_MAP_UP, exp); + if (d_state.isInConflict()) + { + return; + } + } + } +} + +void TheorySetsPrivate::checkMapDown() +{ + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); + const context::CDHashSet& mapTerms = d_state.getMapTerms(); + for (const Node& term : mapTerms) + { + Node f = term[0]; + Node A = term[1]; + TypeNode elementType = A.getType().getSetElementType(); + 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 y = pair.first; + if (y.getKind() == APPLY_UF && y.getOperator() == f) + { + // special case + // (=> + // (set.member (f x) (set.map f A)) + // (set.member x A)) + Node x = y[0]; + Node memberA = nm->mkNode(SET_MEMBER, x, A); + d_im.assertInference(memberA, InferenceId::SETS_MAP_DOWN_POSITIVE, exp); + } + else + { + // general case + // (=> + // (and + // (set.member y B) + // (= B (set.map f A))) + // (and + // (set.member x A) + // (= (f x) y)) + // ) + Node x = sm->mkSkolemFunction( + SkolemFunId::SETS_MAP_DOWN_ELEMENT, elementType, {term, y}); + + d_state.registerMapSkolemElement(term, x); + Node memberA = nm->mkNode(kind::SET_MEMBER, x, A); + Node f_x = nm->mkNode(APPLY_UF, f, x); + Node equal = f_x.eqNode(y); + Node fact = memberA.andNode(equal); + d_im.assertInference(fact, InferenceId::SETS_MAP_DOWN_POSITIVE, exp); + } + if (d_state.isInConflict()) + { + return; + } + } + } +} + void TheorySetsPrivate::checkDisequalities() { // disequalities @@ -1030,6 +1162,9 @@ 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; } + Node TheorySetsPrivate::explain(TNode literal) { Trace("sets") << "TheorySetsPrivate::explain(" << literal << ")" << std::endl; @@ -1094,12 +1229,6 @@ void TheorySetsPrivate::preRegisterTerm(TNode node) } } break; - case kind::SET_MAP: - { - throw LogicException( - "set.map not currently supported by the sets theory solver"); - } - break; default: d_equalityEngine->addTerm(node); break; } } diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 2a89b7933..cda1fae37 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -75,6 +75,35 @@ class TheorySetsPrivate : protected EnvObj * difference. */ void checkUpwardsClosure(); + + /** + * Apply the following rule for map terms (set.map f A): + * Positive member rule: + * (=> + * (set.member x A) + * (set.member (f x) (set.map f A) + * ) + */ + void checkMapUp(); + /** + * Apply the following rules for map terms (set.map f A) where A has type + * (Set T): + * - General case: + * (=> + * (set.member y (set.map f A)) + * (and + * (= (f x) y) + * (set.member x A) + * ) + * ) + * where x is a fresh skolem + * - Special case where we can avoid skolems + * (=> + * (set.member (f x) (set.map f A)) + * (set.member x A) + * ) + */ + void checkMapDown(); /** * This implements a strategy for splitting for set disequalities which * roughly corresponds the SET DISEQUALITY rule from Bansal et al IJCAR 2016. @@ -155,7 +184,6 @@ class TheorySetsPrivate : protected EnvObj //--------------------------------- end standard check /** Collect model values in m based on the relevant terms given by termSet */ - void addSharedTerm(TNode); bool collectModelValues(TheoryModel* m, const std::set& termSet); void computeCareGraph(); @@ -180,6 +208,9 @@ class TheorySetsPrivate : protected EnvObj */ void processCarePairArgs(TNode a, TNode b); + /** returns whether the given kind is a higher order kind for sets. */ + bool isHigherOrderKind(Kind k); + private: TheorySets& d_external; /** The state of the sets solver at full effort */ @@ -221,6 +252,13 @@ class TheorySetsPrivate : protected EnvObj */ bool d_card_enabled; + /** are higher order set operators enabled? + * + * This flag is set to true during a full effort check if any + * higher order constraints is asserted to this theory. + */ + bool d_higher_order_kinds_enabled; + /** The theory rewriter for this theory. */ TheorySetsRewriter d_rewriter; diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index f156f3db5..d356ddbe7 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -223,7 +223,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { } // we don't merge non-constant intersections break; - } // kind::INTERSECION + } // kind::INTERSECTION case kind::SET_UNION: { diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 2dc30a0f6..d13f8ba78 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -2502,6 +2502,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_map_card_incomplete.smt2 + regress1/sets/set_map_negative_members.smt2 + regress1/sets/set_map_positive_members.smt2 + regress1/sets/set_map_unsat1.smt2 regress1/sets/sharingbug.smt2 regress1/sets/univ-set-uf-elim.smt2 regress1/simplification_bug4.smt2 diff --git a/test/regress/cli/regress1/sets/set_map_card_incomplete.smt2 b/test/regress/cli/regress1/sets/set_map_card_incomplete.smt2 new file mode 100644 index 000000000..dab877010 --- /dev/null +++ b/test/regress/cli/regress1/sets/set_map_card_incomplete.smt2 @@ -0,0 +1,19 @@ +; EXPECT: unknown +(set-logic HO_ALL) +; this problem is unsat, but the solver returns unknown for now +; because set.map and set.card are used together +;(set-info :status unsat) +(set-info :status unknown) +(declare-fun A () (Set Int)) +(declare-fun B () (Set Int)) +(declare-fun f (Int) Int) +(declare-fun x1 () Int) +(declare-fun x2 () Int) +(assert (distinct x1 x2)) +(assert (set.member x1 A)) +(assert (set.member x2 A)) +(assert (= (f x1) (f x2))) +(assert (= B (set.map f A))) +(assert (= (set.card B) (set.card A))) + +(check-sat) diff --git a/test/regress/cli/regress1/sets/set_map_negative_members.smt2 b/test/regress/cli/regress1/sets/set_map_negative_members.smt2 new file mode 100644 index 000000000..1c231dbf5 --- /dev/null +++ b/test/regress/cli/regress1/sets/set_map_negative_members.smt2 @@ -0,0 +1,21 @@ +(set-logic HO_ALL) + +(set-info :status sat) +(set-option :finite-model-find true) +(declare-fun A () (Set Int)) +(declare-fun B () (Set Int)) +(declare-fun f (Int) Int) + +(declare-const x Int) +(declare-const y1 Int) +(declare-const y2 Int) +(declare-const y3 Int) + +(assert (distinct x y1 y2 y3)) +(assert (set.member x A)) +(assert (set.member y1 B)) +(assert (set.member y2 B)) +(assert (not (set.member y3 B))) +(assert (= B (set.map f A))) + +(check-sat) diff --git a/test/regress/cli/regress1/sets/set_map_positive_members.smt2 b/test/regress/cli/regress1/sets/set_map_positive_members.smt2 new file mode 100644 index 000000000..f5047aea9 --- /dev/null +++ b/test/regress/cli/regress1/sets/set_map_positive_members.smt2 @@ -0,0 +1,21 @@ +(set-logic HO_ALL) + +(set-info :status sat) + +(declare-fun A () (Set Int)) +(declare-fun B () (Set Int)) +(declare-fun f (Int) Int) + +(declare-const x Int) +(declare-const y1 Int) +(declare-const y2 Int) +(declare-const y3 Int) + +(assert (distinct x y1 y2 y3)) +(assert (set.member x A)) +(assert (set.member y1 B)) +(assert (set.member y2 B)) +(assert (set.member y3 B)) +(assert (= B (set.map f A))) + +(check-sat) diff --git a/test/regress/cli/regress1/sets/set_map_unsat1.smt2 b/test/regress/cli/regress1/sets/set_map_unsat1.smt2 new file mode 100644 index 000000000..974d57d42 --- /dev/null +++ b/test/regress/cli/regress1/sets/set_map_unsat1.smt2 @@ -0,0 +1,9 @@ +(set-logic HO_ALL) +(set-info :status unsat) +(declare-fun A () (Set Int)) +(declare-fun B () (Set Int)) +(define-fun f ((x Int)) Int (+ x 1)) +(assert (= B (set.map f A))) +(assert (set.member (- 2) B)) +(assert (= A (as set.empty (Set Int)))) +(check-sat)