Trace("sets-card-debug") << "...finished register term" << std::endl;
}
-void CardinalityExtension::checkFiniteTypes()
+void CardinalityExtension::checkCardinalityExtended()
{
for (std::pair<const TypeNode, bool>& 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;
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<Node, Node>::iterator it = d_univProxy.find(univ);
Node proxy;
// get all equivalent classes of type t
vector<Node> 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
void CardinalityExtension::check()
{
- checkFiniteTypes();
+ checkCardinalityExtended();
checkRegister();
if (d_im.hasProcessed())
{
// 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);
void checkNormalForm(Node eqc, std::vector<Node>& 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<TypeNode, bool> d_t_card_enabled;
std::map<Node, Node> 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<Node, Node> d_univProxy;
*/
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<TypeNode, Node> d_infiniteTypeUnivCardSkolems;
+
}; /* class CardinalityExtension */
} // namespace sets
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
// 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
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
--- /dev/null
+(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)
--- /dev/null
+(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)
--- /dev/null
+(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)
--- /dev/null
+(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)
--- /dev/null
+(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)
-(set-logic ALL_SUPPORTED)\r
-(set-info :status unsat)\r
-\r
-; conjecture set nonempty(~b & ~c)\r
-\r
-(declare-fun n () Int)\r
-(declare-fun f () Int)\r
-(declare-fun m () Int)\r
-\r
-(declare-fun b () (Set Int))\r
-(declare-fun c () (Set Int))\r
-(declare-fun UNIVERALSET () (Set Int))\r
-(assert (subset b UNIVERALSET))\r
-(assert (subset c UNIVERALSET))\r
-\r
-(assert (> n 0))\r
-(assert (= (card UNIVERALSET) n))\r
-(assert (= (card b) m))\r
-(assert (= (card c) (- f m)))\r
-(assert (>= m 0))\r
-(assert (>= f m))\r
-(assert (> n (+ (* 2 f) m)))\r
-\r
-\r
-(assert (>= (card (setminus UNIVERALSET (intersection (setminus UNIVERALSET b) (setminus UNIVERALSET c)))) n))\r
-\r
-(check-sat)\r
+(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)
projects / cvc5.git / commitdiff