From 0f24023a582da003e4a23fb285e66f3f41b2a842 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Fri, 7 Feb 2020 17:49:58 -0600 Subject: Univeset Cardinality constraints for infinite types (#3712) --- src/theory/sets/cardinality_extension.cpp | 58 ++++++++++++---------- src/theory/sets/cardinality_extension.h | 28 +++++++---- src/theory/sets/solver_state.h | 2 +- src/theory/sets/theory_sets_private.cpp | 15 +++--- test/regress/CMakeLists.txt | 4 ++ .../sets/infinite-type/sets-card-array-int-1.smt2 | 12 +++++ .../sets/infinite-type/sets-card-array-int-2.smt2 | 12 +++++ .../sets/infinite-type/sets-card-int-1.smt2 | 12 +++++ .../sets/infinite-type/sets-card-int-2.smt2 | 12 +++++ .../infinite-type/sets-card-neg-mem-union-2.smt2 | 32 ++++++++++++ test/regress/regress1/sets/issue2904.smt2 | 53 ++++++++++---------- 11 files changed, 170 insertions(+), 70 deletions(-) create mode 100644 test/regress/regress1/sets/infinite-type/sets-card-array-int-1.smt2 create mode 100644 test/regress/regress1/sets/infinite-type/sets-card-array-int-2.smt2 create mode 100644 test/regress/regress1/sets/infinite-type/sets-card-int-1.smt2 create mode 100644 test/regress/regress1/sets/infinite-type/sets-card-int-2.smt2 create mode 100644 test/regress/regress1/sets/infinite-type/sets-card-neg-mem-union-2.smt2 diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index babe1bd03..15e22104c 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -69,29 +69,34 @@ void CardinalityExtension::registerTerm(Node n) Trace("sets-card-debug") << "...finished register term" << std::endl; } -void CardinalityExtension::checkFiniteTypes() +void CardinalityExtension::checkCardinalityExtended() { for (std::pair& pair : d_t_card_enabled) { TypeNode type = pair.first; - if (pair.second && type.isInterpretedFinite()) + if (pair.second) { - checkFiniteType(type); + checkCardinalityExtended(type); } } } -void CardinalityExtension::checkFiniteType(TypeNode& t) +void CardinalityExtension::checkCardinalityExtended(TypeNode& t) { - Assert(t.isInterpretedFinite()); + NodeManager* nm = NodeManager::currentNM(); + TypeNode setType = nm->mkSetType(t); + // skip infinite types that do not have univset terms + if (!t.isInterpretedFinite() && d_state.getUnivSetEqClass(setType).isNull()) + { + return; + } // get the cardinality of the finite type t Cardinality card = t.getCardinality(); // cardinality of an interpreted finite type t is infinite when t // is infinite without --fmf - - if (card.isInfinite()) + if (t.isInterpretedFinite() && card.isInfinite()) { // TODO (#1123): support uninterpreted sorts with --finite-model-find std::stringstream message; @@ -100,9 +105,9 @@ void CardinalityExtension::checkFiniteType(TypeNode& t) throw LogicException(message.str()); } - // get the universe set (as univset (Set t)) - NodeManager* nm = NodeManager::currentNM(); - Node univ = d_state.getUnivSet(nm->mkSetType(t)); + // here we call getUnivSet instead of getUnivSetEqClass to generate + // a univset term for finite types even if they are not used in the input + Node univ = d_state.getUnivSet(setType); std::map::iterator it = d_univProxy.find(univ); Node proxy; @@ -121,18 +126,21 @@ void CardinalityExtension::checkFiniteType(TypeNode& t) // get all equivalent classes of type t vector representatives = d_state.getSetsEqClasses(t); - Node typeCardinality = nm->mkConst(Rational(card.getFiniteCardinality())); - - Node cardUniv = nm->mkNode(kind::CARD, proxy); - Node leq = nm->mkNode(kind::LEQ, cardUniv, typeCardinality); - - // (=> true (<= (card (as univset t)) cardUniv) - if (!d_state.isEntailed(leq, true)) + if (t.isInterpretedFinite()) { - d_im.assertInference(leq, d_true, "finite type cardinality", 1); + Node typeCardinality = nm->mkConst(Rational(card.getFiniteCardinality())); + Node cardUniv = nm->mkNode(kind::CARD, proxy); + Node leq = nm->mkNode(kind::LEQ, cardUniv, typeCardinality); + + // (=> true (<= (card (as univset t)) cardUniv) + if (!d_state.isEntailed(leq, true)) + { + d_im.assertInference( + leq, d_true, "univset cardinality <= type cardinality", 1); + } } - // add subset lemmas for sets, and membership lemmas for negative members + // add subset lemmas for sets and membership lemmas for negative members for (Node& representative : representatives) { // the universe set is a subset of itself @@ -179,7 +187,7 @@ void CardinalityExtension::checkFiniteType(TypeNode& t) void CardinalityExtension::check() { - checkFiniteTypes(); + checkCardinalityExtended(); checkRegister(); if (d_im.hasProcessed()) { @@ -998,11 +1006,11 @@ void CardinalityExtension::mkModelValueElementsFor( // cardinality constraints are satisfied. Since this type is finite, // there is only one single cardinality graph for all sets of this // type because the universe cardinality constraint has been added by - // CardinalityExtension::checkFiniteType. This means we have enough - // slack elements of this finite type for all disjoint leaves in the - // cardinality graph. Therefore we can safely add new distinct slack - // elements for the leaves without worrying about conflicts with the - // current members of this finite type. + // CardinalityExtension::checkCardinalityExtended. This means we have + // enough slack elements of this finite type for all disjoint leaves + // in the cardinality graph. Therefore we can safely add new distinct + // slack elements for the leaves without worrying about conflicts with + // the current members of this finite type. Node slack = nm->mkSkolem("slack", elementType); Node singleton = nm->mkNode(SINGLETON, slack); diff --git a/src/theory/sets/cardinality_extension.h b/src/theory/sets/cardinality_extension.h index bf9c5eeaa..284cf37d0 100644 --- a/src/theory/sets/cardinality_extension.h +++ b/src/theory/sets/cardinality_extension.h @@ -324,18 +324,22 @@ class CardinalityExtension void checkNormalForm(Node eqc, std::vector& intro_sets); /** - * add cardinality lemmas for each finite type + * Add cardinality lemmas for the univset of each type with cardinality terms. + * The lemmas are explained below. */ - void checkFiniteTypes(); + void checkCardinalityExtended(); /** - * This function adds the following lemmas for the finite type t for each S - * where S is a (a representative) set term of type t, and for each negative - * member x not in S 1- (=> true (<= (card (as univset t)) n) where n is the - * cardinality of t 2- (=> true (subset S (as univset t)) where S is a set - * term of type t 3- (=> (not (member negativeMember S))) (member + * This function adds the following lemmas for type t for each S + * where S is a (representative) set term of type t, and for each negative + * member x not in S: + * 1- (=> true (<= (card (as univset t)) n) where n is the + * cardinality of t, which may be symbolic + * 2- (=> true (subset S (as univset t)) where S is a set + * term of type t + * 3- (=> (not (member negativeMember S))) (member * negativeMember (as univset t))) */ - void checkFiniteType(TypeNode& t); + void checkCardinalityExtended(TypeNode& t); /** element types of sets for which cardinality is enabled */ std::map d_t_card_enabled; @@ -375,7 +379,7 @@ class CardinalityExtension std::map d_localBase; /** - * a map to store proxy nodes for the universe sets of finite types + * a map to store proxy nodes for the universe sets */ std::map d_univProxy; @@ -399,6 +403,12 @@ class CardinalityExtension */ bool d_finite_type_constants_processed; + /* + * a map that stores skolem nodes n that satisfies the constraint + * (<= (card t) n) where t is an infinite type + */ + std::map d_infiniteTypeUnivCardSkolems; + }; /* class CardinalityExtension */ } // namespace sets diff --git a/src/theory/sets/solver_state.h b/src/theory/sets/solver_state.h index 5bf20daca..b95081b69 100644 --- a/src/theory/sets/solver_state.h +++ b/src/theory/sets/solver_state.h @@ -198,7 +198,7 @@ class SolverState Node getProxy(Node n); /** Get the empty set of type tn */ Node getEmptySet(TypeNode tn); - /** Get the universe set of type tn */ + /** Get the universe set of type tn if it exists or create a new one */ Node getUnivSet(TypeNode tn); /** * Get the skolem cache of this theory, which manages a database of introduced diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index ad9a8cbdb..f1a11baf8 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -427,21 +427,20 @@ void TheorySetsPrivate::fullEffortCheck() // if we do not handle the kind, set incomplete Kind nk = n[0].getKind(); // some kinds of cardinality we cannot handle - if ((nk == kind::UNIVERSE_SET - && !n[0].getType().isInterpretedFinite()) - || d_rels->isRelationKind(nk)) + if (d_rels->isRelationKind(nk)) { d_full_check_incomplete = true; Trace("sets-incomplete") << "Sets : incomplete because of " << n << "." << std::endl; // TODO (#1124): The issue can be divided into 4 parts // 1- Supporting the universe cardinality for finite types with - // finite cardinality (done) 2- Supporting the universe cardinality - // for for uninterpreted sorts with finite-model-find (pending) - // See the implementation of - // CardinalityExtension::checkFiniteType + // finite cardinality (done) + // 2- Supporting the universe cardinality for uninterpreted sorts + // with finite-model-find (pending) See the implementation of + // CardinalityExtension::checkCardinalityExtended // 3- Supporting the universe cardinality for non-finite types - // (pending, easy) 4- Supporting cardinality for relations (hard) + // (done) + // 4- Supporting cardinality for relations (hard) } } else diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index ada5230d9..4ea9a3d1c 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1626,6 +1626,10 @@ set(regress_1_tests regress1/sets/fuzz14418.smt2 regress1/sets/fuzz15201.smt2 regress1/sets/fuzz31811.smt2 + regress1/sets/infinite-type/sets-card-array-int-1.smt2 + regress1/sets/infinite-type/sets-card-array-int-2.smt2 + regress1/sets/infinite-type/sets-card-int-1.smt2 + regress1/sets/infinite-type/sets-card-int-2.smt2 regress1/sets/insert_invariant_37_2.smt2 regress1/sets/issue2568.smt2 regress1/sets/issue2904.smt2 diff --git a/test/regress/regress1/sets/infinite-type/sets-card-array-int-1.smt2 b/test/regress/regress1/sets/infinite-type/sets-card-array-int-1.smt2 new file mode 100644 index 000000000..ee697065f --- /dev/null +++ b/test/regress/regress1/sets/infinite-type/sets-card-array-int-1.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_ALL) +(set-info :status unsat) +(set-option :sets-ext true) +(declare-const universe (Set (Array Int Int))) +(declare-const A (Set (Array Int Int))) +(declare-const B (Set (Array Int Int))) +(assert (= (card universe) 3)) +(assert (= (card A) 2)) +(assert (= (card B) 2)) +(assert (= (intersection A B) (as emptyset (Set (Array Int Int))))) +(assert (= universe (as univset (Set (Array Int Int))))) +(check-sat) diff --git a/test/regress/regress1/sets/infinite-type/sets-card-array-int-2.smt2 b/test/regress/regress1/sets/infinite-type/sets-card-array-int-2.smt2 new file mode 100644 index 000000000..fe8ce9142 --- /dev/null +++ b/test/regress/regress1/sets/infinite-type/sets-card-array-int-2.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_ALL) +(set-info :status sat) +(set-option :sets-ext true) +(declare-const universe (Set (Array Int Int))) +(declare-const A (Set (Array Int Int))) +(declare-const B (Set (Array Int Int))) +(assert (= (card universe) 3)) +(assert (= (card A) 1)) +(assert (= (card B) 2)) +(assert (= (intersection A B) (as emptyset (Set (Array Int Int))))) +(assert (= universe (as univset (Set (Array Int Int))))) +(check-sat) diff --git a/test/regress/regress1/sets/infinite-type/sets-card-int-1.smt2 b/test/regress/regress1/sets/infinite-type/sets-card-int-1.smt2 new file mode 100644 index 000000000..573ff56da --- /dev/null +++ b/test/regress/regress1/sets/infinite-type/sets-card-int-1.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_ALL) +(set-option :sets-ext true) +(set-info :status unsat) +(assert (= (card (as univset (Set Int))) 10)) +(declare-const universe (Set Int)) +(declare-const A (Set Int)) +(declare-const B (Set Int)) +(assert (= (card A) 6)) +(assert (= (card B) 5)) +(assert (= (intersection A B) (as emptyset (Set Int)))) +(assert (= universe (as univset (Set Int)))) +(check-sat) diff --git a/test/regress/regress1/sets/infinite-type/sets-card-int-2.smt2 b/test/regress/regress1/sets/infinite-type/sets-card-int-2.smt2 new file mode 100644 index 000000000..9d8fee7c3 --- /dev/null +++ b/test/regress/regress1/sets/infinite-type/sets-card-int-2.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_ALL) +(set-option :sets-ext true) +(set-info :status sat) +(assert (= (card (as univset (Set Int))) 10)) +(declare-const universe (Set Int)) +(declare-const A (Set Int)) +(declare-const B (Set Int)) +(assert (= (card A) 5)) +(assert (= (card B) 5)) +(assert (= (intersection A B) (as emptyset (Set Int)))) +(assert (= universe (as univset (Set Int)))) +(check-sat) diff --git a/test/regress/regress1/sets/infinite-type/sets-card-neg-mem-union-2.smt2 b/test/regress/regress1/sets/infinite-type/sets-card-neg-mem-union-2.smt2 new file mode 100644 index 000000000..baeb1387a --- /dev/null +++ b/test/regress/regress1/sets/infinite-type/sets-card-neg-mem-union-2.smt2 @@ -0,0 +1,32 @@ +(set-logic QF_ALL) +(set-info :status unsat) +(set-option :produce-models true) +(set-option :sets-ext true) +(declare-fun A () (Set Int)) +(declare-fun B () (Set Int)) +(declare-fun C () (Set Int)) +(declare-fun D () (Set Int)) + +(declare-fun x () Int) +(assert (not (member x A))) +(assert (not (member x B))) +(assert (not (member x C))) +(assert (not (member x D))) +(declare-fun y () Int) +(assert (not (member y A))) +(assert (not (member y B))) +(assert (not (member y C))) +(assert (not (member y D))) +(declare-fun z () Int) +(assert (not (member z A))) +(assert (not (member z B))) +(assert (not (member z C))) +(assert (not (member z D))) + +(assert (distinct x y z)) + +(assert (= (card (union A (union B (union C D)))) 6)) + +(assert (= (card (as univset (Set Int))) 8)) + +(check-sat) diff --git a/test/regress/regress1/sets/issue2904.smt2 b/test/regress/regress1/sets/issue2904.smt2 index 13ca789f6..e9fca1716 100644 --- a/test/regress/regress1/sets/issue2904.smt2 +++ b/test/regress/regress1/sets/issue2904.smt2 @@ -1,27 +1,26 @@ -(set-logic ALL_SUPPORTED) -(set-info :status unsat) - -; conjecture set nonempty(~b & ~c) - -(declare-fun n () Int) -(declare-fun f () Int) -(declare-fun m () Int) - -(declare-fun b () (Set Int)) -(declare-fun c () (Set Int)) -(declare-fun UNIVERALSET () (Set Int)) -(assert (subset b UNIVERALSET)) -(assert (subset c UNIVERALSET)) - -(assert (> n 0)) -(assert (= (card UNIVERALSET) n)) -(assert (= (card b) m)) -(assert (= (card c) (- f m))) -(assert (>= m 0)) -(assert (>= f m)) -(assert (> n (+ (* 2 f) m))) - - -(assert (>= (card (setminus UNIVERALSET (intersection (setminus UNIVERALSET b) (setminus UNIVERALSET c)))) n)) - -(check-sat) +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +; conjecture set nonempty(~b & ~c) + +(declare-fun n () Int) +(declare-fun f () Int) +(declare-fun m () Int) + +(declare-fun b () (Set Int)) +(declare-fun c () (Set Int)) +(declare-fun UNIVERALSET () (Set Int)) +(assert (subset b UNIVERALSET)) +(assert (subset c UNIVERALSET)) + +(assert (> n 0)) +(assert (= (card UNIVERALSET) n)) +(assert (= (card b) m)) +(assert (= (card c) (- f m))) +(assert (>= m 0)) +(assert (>= f m)) +(assert (> n (+ (* 2 f) m))) + + +(assert (>= (card (setminus UNIVERALSET (intersection (setminus UNIVERALSET b) (setminus UNIVERALSET c)))) n)) + +(check-sat) -- cgit v1.2.3