Univeset Cardinality constraints for infinite types (#3712)

7 files changed, 110 insertions, 27 deletions

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)