Univeset Cardinality constraints for infinite types (#3712)

11 files changed, 170 insertions, 70 deletions

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<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;
@@ -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<Node, Node>::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<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
@@ -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<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;
@@ -375,7 +379,7 @@ class CardinalityExtension
   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;
 
@@ -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<TypeNode, Node> 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)