cardinality operation for finite sets (based on my thesis / ijcar16 paper)

Some further cleanup/fixes pending

This is squash of 39 commits (kbansal/card branch + cleanup):
* add card operator
* local reasoning
* towards graph building
* first implementation
* close cardinality terms
* model building
* more
* more
* more
* Add aggressive sets rewriting.
* Recursively aggressive rewrite sets.
* Fix
* incomplete card2 implementation
* ...
* Avoid using auto in sets.
* fix merge
* more
* ...
* more
* ...
* Fixed for loops
* Slight modification to computeRelevantTerms
* more
* ..
* more
* ...
* mv empty set lemma generation to later point
* more options/reordering
* debug related
* more trace
* ...
* fix merge_nodes, models
* rm warnigns
* fix compile errors
* warning
* bug fixes/cleanup
* mroe fixes
* cleanup
* ...

7 files changed, 138 insertions, 0 deletions

diff --git a/test/regress/regress0/sets/card-2.smt2 b/test/regress/regress0/sets/card-2.smt2
new file mode 100644
index 000000000..cb414dbef
--- /dev/null
+++ b/test/regress/regress0/sets/card-2.smt2
@@ -0,0 +1,10 @@
+(set-logic QF_UFLIAFS)
+(declare-sort E 0)
+(declare-fun s () (Set E))
+(declare-fun t () (Set E))
+(declare-fun u () (Set E))
+(assert (>= (card s) 5))
+(assert (>= (card t) 5))
+(assert (<= (card u) 6))
+(assert (= u (union s t)))
+(check-sat)
diff --git a/test/regress/regress0/sets/card-3.smt2 b/test/regress/regress0/sets/card-3.smt2
new file mode 100644
index 000000000..949ed3457
--- /dev/null
+++ b/test/regress/regress0/sets/card-3.smt2
@@ -0,0 +1,11 @@
+(set-logic QF_UFLIAFS)
+(declare-sort E 0)
+(declare-fun s () (Set E))
+(declare-fun t () (Set E))
+(declare-fun u () (Set E))
+(assert (>= (card (union s t)) 8))
+(assert (>= (card (union s u)) 8))
+(assert (<= (card (union t u)) 5))
+(assert (<= (card s) 5))
+(assert (= (as emptyset (Set E)) (intersection t u)))
+(check-sat)
diff --git a/test/regress/regress0/sets/card-4.smt2 b/test/regress/regress0/sets/card-4.smt2
new file mode 100644
index 000000000..ea7fe42f3
--- /dev/null
+++ b/test/regress/regress0/sets/card-4.smt2
@@ -0,0 +1,23 @@
+(set-logic QF_UFLIAFS)
+(declare-sort E 0)
+(declare-fun s () (Set E))
+(declare-fun t () (Set E))
+(declare-fun u () (Set E))
+(assert (>= (card (union s t)) 8))
+(assert (>= (card (union s u)) 8))
+;(assert (<= (card (union t u)) 5))
+(assert (<= (card s) 5))
+(assert (= (as emptyset (Set E)) (intersection t u)))
+(declare-fun x1 () E)
+(declare-fun x2 () E)
+(declare-fun x3 () E)
+(declare-fun x4 () E)
+(declare-fun x5 () E)
+(declare-fun x6 () E)
+(assert (member x1 s))
+(assert (member x2 s))
+(assert (member x3 s))
+(assert (member x4 s))
+(assert (member x5 s))
+(assert (member x6 s))
+(check-sat)
diff --git a/test/regress/regress0/sets/card-5.smt2 b/test/regress/regress0/sets/card-5.smt2
new file mode 100644
index 000000000..65135e7b4
--- /dev/null
+++ b/test/regress/regress0/sets/card-5.smt2
@@ -0,0 +1,24 @@
+(set-logic QF_UFLIAFS)
+(declare-sort E 0)
+(declare-fun s () (Set E))
+(declare-fun t () (Set E))
+(declare-fun u () (Set E))
+(assert (>= (card (union s t)) 8))
+(assert (>= (card (union s u)) 8))
+;(assert (<= (card (union t u)) 5))
+(assert (<= (card s) 5))
+(assert (= (as emptyset (Set E)) (intersection t u)))
+(declare-fun x1 () E)
+(declare-fun x2 () E)
+(declare-fun x3 () E)
+(declare-fun x4 () E)
+(declare-fun x5 () E)
+(declare-fun x6 () E)
+(assert (member x1 s))
+(assert (member x2 s))
+(assert (member x3 s))
+(assert (member x4 s))
+(assert (member x5 s))
+(assert (member x6 s))
+(assert (distinct x1 x2 x3 x4 x5 x6))
+(check-sat)
diff --git a/test/regress/regress0/sets/card-6.smt2 b/test/regress/regress0/sets/card-6.smt2
new file mode 100644
index 000000000..1611952b7
--- /dev/null
+++ b/test/regress/regress0/sets/card-6.smt2
@@ -0,0 +1,16 @@
+(set-logic QF_UFLIAFS)
+(declare-sort E 0)
+(declare-fun A () (Set E))
+(declare-fun B () (Set E))
+(declare-fun C () (Set E))
+(assert
+  (and
+    (= (as emptyset (Set E))
+       (intersection A B))
+    (subset C (union A B))
+    (>= (card C) 5)
+    (<= (card A) 2)
+    (<= (card B) 2)
+  )
+)
+(check-sat)
diff --git a/test/regress/regress0/sets/card-7.smt2 b/test/regress/regress0/sets/card-7.smt2
new file mode 100644
index 000000000..94468dc57
--- /dev/null
+++ b/test/regress/regress0/sets/card-7.smt2
@@ -0,0 +1,46 @@
+(set-logic QF_UFLIAFS)
+(declare-sort E 0)
+(declare-fun A1 () (Set E))
+(declare-fun A2 () (Set E))
+(declare-fun A3 () (Set E))
+(declare-fun A4 () (Set E))
+(declare-fun A5 () (Set E))
+(declare-fun A6 () (Set E))
+(declare-fun A7 () (Set E))
+(declare-fun A8 () (Set E))
+(declare-fun A9 () (Set E))
+(declare-fun A10 () (Set E))
+(declare-fun A11 () (Set E))
+(declare-fun A12 () (Set E))
+(declare-fun A13 () (Set E))
+(declare-fun A14 () (Set E))
+(declare-fun A15 () (Set E))
+(declare-fun A16 () (Set E))
+(declare-fun A17 () (Set E))
+(declare-fun A18 () (Set E))
+(declare-fun A19 () (Set E))
+(declare-fun A20 () (Set E))
+(assert (and
+  (= (card A1) 1)
+  (= (card A2) 1)
+  (= (card A3) 1)
+  (= (card A4) 1)
+  (= (card A5) 1)
+  (= (card A6) 1)
+  (= (card A7) 1)
+  (= (card A8) 1)
+  (= (card A9) 1)
+  (= (card A10) 1)
+  (= (card A11) 1)
+  (= (card A12) 1)
+  (= (card A13) 1)
+  (= (card A14) 1)
+  (= (card A15) 1)
+  (= (card A16) 1)
+  (= (card A17) 1)
+  (= (card A18) 1)
+  (= (card A19) 1)
+  (= (card A20) 1)
+))
+(assert (= 20 (+ (card A1) (card A2) (card A3) (card A4) (card A5) (card A6) (card A7) (card A8) (card A9) (card A10) (card A11) (card A12) (card A13) (card A14) (card A15) (card A16) (card A17) (card A18) (card A19) (card A20))))
+(check-sat)
diff --git a/test/regress/regress0/sets/card.smt2 b/test/regress/regress0/sets/card.smt2
new file mode 100644
index 000000000..6b8c536d5
--- /dev/null
+++ b/test/regress/regress0/sets/card.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_UFLIAFS)
+(declare-sort E 0)
+(declare-fun s () (Set E))
+(declare-fun t () (Set E))
+(assert (>= (card s) 5))
+(assert (>= (card t) 5))
+(assert (<= (card (union s t)) 4))
+(check-sat)