Universe set cardinality for finite types with finite cardinality (#3392)

* rewrote set cardinality for finite-types

* small changes and format

18 files changed, 269 insertions, 0 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index a53201e3e..22848ff97 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1583,6 +1583,22 @@ set(regress_1_tests
   regress1/sets/comp-pos-member.smt2
   regress1/sets/copy_check_heap_access_33_4.smt2
   regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2
+  regress1/sets/finite-type/sets-card-arrcolor.smt2
+  regress1/sets/finite-type/sets-card-arrunit.smt2
+  regress1/sets/finite-type/sets-card-bool-1.smt2
+  regress1/sets/finite-type/sets-card-bool-2.smt2
+  regress1/sets/finite-type/sets-card-bool-3.smt2
+  regress1/sets/finite-type/sets-card-bool-4.smt2
+  regress1/sets/finite-type/sets-card-bool-rec.smt2
+  regress1/sets/finite-type/sets-card-bv-1.smt2
+  regress1/sets/finite-type/sets-card-bv-2.smt2
+  regress1/sets/finite-type/sets-card-bv-3.smt2
+  regress1/sets/finite-type/sets-card-bv-4.smt2
+  regress1/sets/finite-type/sets-card-color.smt2
+  regress1/sets/finite-type/sets-card-color-sat.smt2
+  regress1/sets/finite-type/sets-card-datatype-1.smt2
+  regress1/sets/finite-type/sets-card-datatype-2.smt2
+  regress1/sets/finite-type/sets-card-neg-mem-union-1.smt2
   regress1/sets/fuzz14418.smt2
   regress1/sets/fuzz15201.smt2
   regress1/sets/fuzz31811.smt2
@@ -2277,6 +2293,7 @@ set(regression_disabled_tests
   regress1/rewriterules/test_guards.smt2
   regress1/rewriterules/why3_vstte10_max_sum_harness2.smt2
   regress1/sets/setofsets-disequal.smt2
+  regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2
   regress1/simple-rdl-definefun.smt2
   # does not solve after minor modification to search
   regress1/sygus/car_3.lus.sy
diff --git a/test/regress/regress1/sets/finite-type/sets-card-arrcolor.smt2 b/test/regress/regress1/sets/finite-type/sets-card-arrcolor.smt2
new file mode 100644
index 000000000..2c7acf282
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-arrcolor.smt2
@@ -0,0 +1,11 @@
+(set-logic QF_ALL)
+(set-info :status sat)
+(set-option :produce-models true)
+(set-option :sets-ext true)
+(declare-datatype Color ((Red) (Green) (Blue)))
+(declare-fun A () (Set (Array Color Color)))
+(declare-fun B () (Set (Array Color Color)))
+(assert (> (card A) 25))
+(assert (> (card B) 25))
+(assert (distinct A B))
+(check-sat)
diff --git a/test/regress/regress1/sets/finite-type/sets-card-arrunit.smt2 b/test/regress/regress1/sets/finite-type/sets-card-arrunit.smt2
new file mode 100644
index 000000000..95d363397
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-arrunit.smt2
@@ -0,0 +1,10 @@
+(set-logic QF_ALL)
+(set-info :status unsat)
+(set-option :sets-ext true)
+(declare-datatype Unit ((mkUnit)))
+
+(declare-fun S () (Set (Array Int Unit)))
+
+(assert (> (card S) 1))
+
+(check-sat)
diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2
new file mode 100644
index 000000000..c455caa28
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2
@@ -0,0 +1,12 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(set-option :produce-models true)
+(set-option :sets-ext true)
+(declare-fun A () (Set Bool))
+(declare-fun B () (Set Bool))
+(declare-fun universe () (Set Bool))
+(assert (= (card A) 2))
+(assert (= (card B) 2))
+(assert (= (intersection A B) (as emptyset (Set Bool))))
+(assert (= universe (as univset (Set Bool))))
+(check-sat)
diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-2.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-2.smt2
new file mode 100644
index 000000000..977bf3795
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-bool-2.smt2
@@ -0,0 +1,10 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(set-option :produce-models true)
+(set-option :sets-ext true)
+(declare-fun A () (Set Bool))
+(declare-fun universe () (Set Bool))
+(assert (= (card A) 2))
+(assert (= universe (as univset (Set Bool))))
+(check-sat)
+
diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-3.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-3.smt2
new file mode 100644
index 000000000..623376e37
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-bool-3.smt2
@@ -0,0 +1,12 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(set-option :produce-models true)
+(set-option :sets-ext true)
+(declare-fun A () (Set Bool))
+(declare-fun B () (Set Bool))
+(declare-fun universe () (Set Bool))
+(assert (= (card A) 2))
+(assert (= (card B) 2))
+(assert (= universe (as univset (Set Bool))))
+(check-sat)
+
diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-4.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-4.smt2
new file mode 100644
index 000000000..1e18597dc
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-bool-4.smt2
@@ -0,0 +1,9 @@
+(set-logic QF_ALL)
+(set-info :status sat)
+(set-option :sets-ext true)
+(set-option :produce-models true)
+(declare-fun A () (Set Bool))
+(declare-fun x () Bool)
+(assert (member (member x A) A))
+(assert (> (card A) 1))
+(check-sat)
diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-rec.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-rec.smt2
new file mode 100644
index 000000000..150dd5cff
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-bool-rec.smt2
@@ -0,0 +1,10 @@
+(set-logic QF_ALL)
+(set-info :status sat)
+(set-option :sets-ext true)
+(declare-fun A () (Set Bool))
+(declare-fun x () Bool)
+(assert (member (member x A) A))
+(assert (> (card A) 1))
+(declare-fun U () (Set Bool))
+(assert (= U (as univset (Set Bool))))
+(check-sat)
diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-1.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-1.smt2
new file mode 100644
index 000000000..1388b9bfa
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-bv-1.smt2
@@ -0,0 +1,10 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(set-option :produce-models true)
+(set-option :sets-ext true)
+(declare-fun A () (Set (_ BitVec 3)))
+(declare-fun universe () (Set (_ BitVec 3)))
+(assert (= (card A) 3))
+(assert (= universe (as univset (Set (_ BitVec 3)))))
+(check-sat)
+
diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2
new file mode 100644
index 000000000..26ee05f3c
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2
@@ -0,0 +1,16 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(set-option :produce-models true)
+(set-option :sets-ext true)
+(declare-fun A () (Set (_ BitVec 3)))
+(declare-fun B () (Set (_ BitVec 3)))
+(declare-fun universe () (Set (_ BitVec 3)))
+(assert (= (card A) 5))
+(assert (= (card B) 5))
+(assert (not (= A B)))
+(assert (= (card (intersection A B)) 2))
+(assert (= (card (setminus A B)) 3))
+(assert (= (card (setminus B A)) 3))
+(assert (= universe (as univset (Set (_ BitVec 3)))))
+(check-sat)
+
diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2
new file mode 100644
index 000000000..8c92d1c6b
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2
@@ -0,0 +1,19 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(set-option :produce-models true)
+(set-option :sets-ext true)
+(declare-fun A () (Set (_ BitVec 3)))
+(declare-fun B () (Set (_ BitVec 3)))
+(declare-fun universe () (Set (_ BitVec 3)))
+(declare-fun x () (_ BitVec 3))
+(assert (= (card A) 3))
+(assert (= (card B) 3))
+(assert (not (= A B)))
+(assert (= (card (intersection A B)) 1))
+(assert (= (card (setminus A B)) 2))
+(assert (= (card (setminus B A)) 2))
+(assert (not (member x A)))
+(assert (not (member x B)))
+(assert (= universe (as univset (Set (_ BitVec 3)))))
+(check-sat)
+
diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2
new file mode 100644
index 000000000..d2c8a744d
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2
@@ -0,0 +1,18 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(set-option :produce-models true)
+(set-option :sets-ext true)
+(declare-fun A () (Set (_ BitVec 3)))
+(declare-fun B () (Set (_ BitVec 3)))
+(declare-fun universe () (Set (_ BitVec 3)))
+(declare-fun x () (_ BitVec 3))
+(assert (= (card A) 5))
+(assert (= (card B) 5))
+(assert (not (= A B)))
+(assert (= (card (intersection A B)) 2))
+(assert (= (card (setminus A B)) 3))
+(assert (= (card (setminus B A)) 3))
+(assert (= universe (as univset (Set (_ BitVec 3)))))
+(assert (not (member x A)))
+(assert (not (member x B)))
+(check-sat)
diff --git a/test/regress/regress1/sets/finite-type/sets-card-color-sat.smt2 b/test/regress/regress1/sets/finite-type/sets-card-color-sat.smt2
new file mode 100644
index 000000000..ca8015622
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-color-sat.smt2
@@ -0,0 +1,14 @@
+(set-logic QF_BVDTLIAFS)
+(set-info :status sat)
+(set-option :produce-models true)
+(set-option :sets-ext true)
+(declare-datatype Color ((Red) (Green) (Blue) (Purple)))
+(declare-fun A () (Set Color))
+(declare-fun B () (Set Color))
+(assert (> (card A) (card B) ))
+(assert (member Red B))
+(declare-fun d () Color)
+(assert (not (= d Red)))
+(assert (member d B))
+(assert (not (member Green A)))
+(check-sat)
diff --git a/test/regress/regress1/sets/finite-type/sets-card-color.smt2 b/test/regress/regress1/sets/finite-type/sets-card-color.smt2
new file mode 100644
index 000000000..4fe3f0428
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-color.smt2
@@ -0,0 +1,14 @@
+(set-logic QF_BVDTLIAFS)
+(set-info :status unsat)
+(set-option :produce-models true)
+(set-option :sets-ext true)
+(declare-datatype Color ((Red) (Green) (Blue)))
+(declare-fun A () (Set Color))
+(declare-fun B () (Set Color))
+(assert (> (card A) (card B) ))
+(assert (member Red B))
+(declare-fun d () Color)
+(assert (not (= d Red)))
+(assert (member d B))
+(assert (not (member Green A)))
+(check-sat)
diff --git a/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2 b/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2
new file mode 100644
index 000000000..0121479e9
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2
@@ -0,0 +1,14 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(set-option :produce-models true)
+(set-option :sets-ext true)
+(declare-datatype Rec ((mkRec (r1 (_ BitVec 2)) (r2 (_ BitVec 2)))))
+(declare-fun A () (Set Rec))
+(declare-fun B () (Set Rec))
+(declare-fun universe () (Set Rec))
+(declare-fun x () Rec)
+(assert (= (card A) 5))
+(assert (= (card B) 5))
+(assert (= (card (intersection A B)) 1))
+(assert (= universe (as univset (Set Rec))))
+(check-sat)
diff --git a/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2 b/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2
new file mode 100644
index 000000000..708ebb2ca
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2
@@ -0,0 +1,13 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(set-option :produce-models true)
+(set-option :sets-ext true)
+(declare-datatype Rec ((mkRec (r1 (_ BitVec 2)) (r2 (_ BitVec 2)))))
+(declare-fun A () (Set Rec))
+(declare-fun B () (Set Rec))
+(declare-fun universe () (Set Rec))
+(assert (= (card A) 9))
+(assert (= (card B) 9))
+(assert (= (card (intersection A B)) 1))
+(assert (= universe (as univset (Set Rec))))
+(check-sat)
diff --git a/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-1.smt2 b/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-1.smt2
new file mode 100644
index 000000000..b4bd97f1d
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-1.smt2
@@ -0,0 +1,30 @@
+(set-logic QF_ALL)
+(set-info :status unsat)
+(set-option :produce-models true)
+(set-option :sets-ext true)
+(declare-fun A () (Set (_ BitVec 2)))
+(declare-fun B () (Set (_ BitVec 2)))
+(declare-fun C () (Set (_ BitVec 2)))
+(declare-fun D () (Set (_ BitVec 2)))
+
+(declare-fun x () (_ BitVec 2))
+(assert (not (member x A)))
+(assert (not (member x B)))
+(assert (not (member x C)))
+(assert (not (member x D)))
+(declare-fun y () (_ BitVec 2))
+(assert (not (member y A)))
+(assert (not (member y B)))
+(assert (not (member y C)))
+(assert (not (member y D)))
+(declare-fun z () (_ BitVec 2))
+(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)))) 2))
+
+(check-sat)
diff --git a/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2 b/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2
new file mode 100644
index 000000000..88825a600
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2
@@ -0,0 +1,30 @@
+(set-logic QF_ALL)
+(set-info :status unsat)
+(set-option :produce-models true)
+(set-option :sets-ext true)
+(declare-fun A () (Set (_ BitVec 3)))
+(declare-fun B () (Set (_ BitVec 3)))
+(declare-fun C () (Set (_ BitVec 3)))
+(declare-fun D () (Set (_ BitVec 3)))
+
+(declare-fun x () (_ BitVec 3))
+(assert (not (member x A)))
+(assert (not (member x B)))
+(assert (not (member x C)))
+(assert (not (member x D)))
+(declare-fun y () (_ BitVec 3))
+(assert (not (member y A)))
+(assert (not (member y B)))
+(assert (not (member y C)))
+(assert (not (member y D)))
+(declare-fun z () (_ BitVec 3))
+(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))
+
+(check-sat)