add new theory (sets)

Specification (smt2) -- as per this commit, subject to change

- Parameterized sort Set, e.g. (Set Int)

- Empty set constant (typed), use with "as" to specify the type, e.g.
    (as emptyset (Set Int))

- Create a singleton set
    (setenum X (Set X)) : creates singleton set

- Functions/operators
    (union (Set X) (Set X) (Set X))
    (intersection (Set X) (Set X) (Set X))
    (setminus (Set X) (Set X) (Set X))

- Predicates
    (in X (Set X) Bool) : membership
    (subseteq (Set X) (Set X) Bool) : set containment

1 files changed, 75 insertions, 0 deletions

diff --git a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2
new file mode 100644
index 000000000..b90563199
--- /dev/null
+++ b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2
@@ -0,0 +1,75 @@
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status unsat)
+(define-sort Elt () Int)
+(define-sort mySet () (Set Elt ))
+(define-fun smt_set_emp () mySet (as emptyset mySet))
+(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (in x s))
+(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x)))
+(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2))
+
+(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
+
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(declare-fun z3v58 () Int)
+(declare-fun z3v59 () Int)
+(assert (distinct z3v58 z3v59))
+
+(declare-fun z3f60 (Int) Bool)
+(declare-fun z3v61 () Int)
+(declare-fun z3f62 (Int) Int)
+(declare-fun z3v63 () Int)
+(declare-fun z3v64 () Int)
+(declare-fun z3v65 () Int)
+(declare-fun z3v66 () Int)
+(declare-fun z3f67 (Int) mySet)
+(declare-fun z3v69 () Int)
+(declare-fun z3f70 (Int) Int)
+(declare-fun z3v76 () Int)
+(declare-fun z3v77 () Int)
+(declare-fun z3v78 () Int)
+(declare-fun z3v79 () Int)
+(declare-fun z3v80 () Int)
+(declare-fun z3v81 () Int)
+(declare-fun z3v82 () Int)
+(declare-fun z3f83 (Int) Int)
+(declare-fun z3f84 (Int) Int)
+(declare-fun z3v85 () Int)
+(declare-fun z3f86 (Int) Int)
+(declare-fun z3f87 (Int Int) Int)
+(declare-fun z3v88 () Int)
+(declare-fun z3v89 () Int)
+(declare-fun z3f90 (Int) mySet)
+(declare-fun z3f91 (Int) Bool)
+(declare-fun z3f92 (Int Int) Int)
+(declare-fun z3v93 () Int)
+(declare-fun z3v94 () Int)
+(declare-fun z3v95 () Int)
+(declare-fun z3v96 () Int)
+(declare-fun z3v97 () Int)
+(declare-fun z3v99 () Int)
+
+(assert (= z3v99 z3v89))
+(assert (>= (z3f70 z3v99) 0))
+
+(assert (and (not (z3f60 z3v79))
+             (not (z3f60 z3v79))
+             (= z3v79 z3v80)
+             (= (z3f60 z3v79)
+                (= z3v76 z3v81))
+             (= (z3f60 z3v80)
+                (= z3v76 z3v81))
+             (= (z3f83 z3v82) z3v81)
+             (= (z3f91 z3v78) false)
+             (= z3v78 (z3f92 z3v88 z3v89))
+             (= z3v82 z3v88)
+             (= (z3f67 z3v78)
+                (smt_set_cup (smt_set_add smt_set_emp (z3f83 z3v88))
+                             (z3f67 z3v89)))
+             (= (z3f62 z3v64) z3v64)))
+
+(assert (smt_set_mem z3v76 (z3f67 z3v78)))
+(assert (<= z3v95 z3v93))
+(assert (>= z3v95 z3v93))
+(assert (not (smt_set_mem z3v76 (z3f67 z3v99))))
+(check-sat)