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

2 files changed, 67 insertions, 67 deletions

diff --git a/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2 b/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2
index 9bd49f714..56228e082 100644
--- a/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2
+++ b/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2
@@ -2,124 +2,124 @@
 (set-logic AUFLIA)
 (set-info :status unsat)
 
-;; don't use a datatypes for currently focusing in uf
+;; don't use a datatypes for currently focusing my_in uf
 (declare-sort elt 0)
 (declare-sort set 0)
 
-(declare-fun in (elt set) Bool)
+(declare-fun my_in (elt set) Bool)
 
 ;;;;;;;;;;;;;;;;;;;;
 ;; inter
 
 (declare-fun inter (set set)  set)
 (assert-propagation ((?s elt) (?t1 set) (?t2 set)) () ()
-                  ((in ?s (inter ?t1 ?t2))) (and (in ?s ?t1) (in ?s ?t2)))
+                  ((my_in ?s (inter ?t1 ?t2))) (and (my_in ?s ?t1) (my_in ?s ?t2)))
 
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((inter ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (inter ?t1 ?t2))) )
+                   (((inter ?t1 ?t2))) () ((not (my_in ?s ?t1))) (not (my_in ?s (inter ?t1 ?t2))) )
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((inter ?t1 ?t2))) () ((not (in ?s ?t2))) (not (in ?s (inter ?t1 ?t2))) )
+                   (((inter ?t1 ?t2))) () ((not (my_in ?s ?t2))) (not (my_in ?s (inter ?t1 ?t2))) )
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t1)) (not (in ?s ?t2)) )
+                   () () ((not (my_in ?s (inter ?t1 ?t2))) (my_in ?s ?t1)) (not (my_in ?s ?t2)) )
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t2)) (not (in ?s ?t1)))
+                   () () ((not (my_in ?s (inter ?t1 ?t2))) (my_in ?s ?t2)) (not (my_in ?s ?t1)))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((inter ?t1 ?t2))) () ((in ?s ?t1) (in ?s ?t2)) (in ?s (inter ?t1 ?t2)) )
+                   (((inter ?t1 ?t2))) () ((my_in ?s ?t1) (my_in ?s ?t2)) (my_in ?s (inter ?t1 ?t2)) )
 
 ;;;;;;;;;;;;;;;;;
 ;; union
 
-(declare-fun union (set set)  set)
+(declare-fun my_union (set set)  set)
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((not (in ?s (union ?t1 ?t2)))) (and (not (in ?s ?t1)) (not (in ?s ?t2))))
+                   () () ((not (my_in ?s (my_union ?t1 ?t2)))) (and (not (my_in ?s ?t1)) (not (my_in ?s ?t2))))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((union ?t1 ?t2))) () ((in ?s ?t1)) (in ?s (union ?t1 ?t2)))
+                   (((my_union ?t1 ?t2))) () ((my_in ?s ?t1)) (my_in ?s (my_union ?t1 ?t2)))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((union ?t1 ?t2))) () ((in ?s ?t2)) (in ?s (union ?t1 ?t2)))
+                   (((my_union ?t1 ?t2))) () ((my_in ?s ?t2)) (my_in ?s (my_union ?t1 ?t2)))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t1))) (in ?s ?t2))
+                   () () ((my_in ?s (my_union ?t1 ?t2)) (not (my_in ?s ?t1))) (my_in ?s ?t2))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t2))) (in ?s ?t1))
+                   () () ((my_in ?s (my_union ?t1 ?t2)) (not (my_in ?s ?t2))) (my_in ?s ?t1))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((union ?t1 ?t2))) () ((not (in ?s ?t1)) (not (in ?s ?t2))) (not (in ?s (union ?t1 ?t2))))
+                   (((my_union ?t1 ?t2))) () ((not (my_in ?s ?t1)) (not (my_in ?s ?t2))) (not (my_in ?s (my_union ?t1 ?t2))))
 
 ;;;;;;;;;;;;;;;;;;;;
 ;; diff
 
 (declare-fun diff (set set)  set)
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((in ?s (diff ?t1 ?t2))) (and (in ?s ?t1) (not (in ?s ?t2))))
+                   () () ((my_in ?s (diff ?t1 ?t2))) (and (my_in ?s ?t1) (not (my_in ?s ?t2))))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((diff ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (diff ?t1 ?t2))) )
+                   (((diff ?t1 ?t2))) () ((not (my_in ?s ?t1))) (not (my_in ?s (diff ?t1 ?t2))) )
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((diff ?t1 ?t2))) () ((in ?s ?t2)) (not (in ?s (diff ?t1 ?t2))))
+                   (((diff ?t1 ?t2))) () ((my_in ?s ?t2)) (not (my_in ?s (diff ?t1 ?t2))))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((not (in ?s (diff ?t1 ?t2))) (in ?s ?t1)) (in ?s ?t2))
+                   () () ((not (my_in ?s (diff ?t1 ?t2))) (my_in ?s ?t1)) (my_in ?s ?t2))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((not (in ?s (diff ?t1 ?t2))) (not (in ?s ?t2))) (not (in ?s ?t1)))
+                   () () ((not (my_in ?s (diff ?t1 ?t2))) (not (my_in ?s ?t2))) (not (my_in ?s ?t1)))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((diff ?t1 ?t2))) () ((in ?s ?t1) (not (in ?s ?t2))) (in ?s (diff ?t1 ?t2)) )
+                   (((diff ?t1 ?t2))) () ((my_in ?s ?t1) (not (my_in ?s ?t2))) (my_in ?s (diff ?t1 ?t2)) )
 
 ;;;;;;;;;;;;;;;;
 ;;sing
 
 (declare-fun sing (elt)  set)
 (assert-propagation ((?s elt))
-                   (((sing ?s))) () () (in ?s (sing ?s)) )
+                   (((sing ?s))) () () (my_in ?s (sing ?s)) )
 
 (assert-propagation ((?s elt) (?t1 elt))
-                   () () ((in ?s (sing ?t1))) (= ?s ?t1))
+                   () () ((my_in ?s (sing ?t1))) (= ?s ?t1))
 
 (assert-propagation ((?s elt) (?t1 elt))
-                   () () ((not (in ?s (sing ?t1)))) (not (= ?s ?t1)))
+                   () () ((not (my_in ?s (sing ?t1)))) (not (= ?s ?t1)))
 
 ;;;;;;;;;;;;;;;;;;;
 ;; fullfiling runned at Full effort
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((in ?s (union ?t1 ?t2))) (or (in ?s ?t1) (not (in ?s ?t1))))
+                   () () ((my_in ?s (my_union ?t1 ?t2))) (or (my_in ?s ?t1) (not (my_in ?s ?t1))))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((inter ?t1 ?t2))) () ((in ?s ?t1)) (or (in ?s ?t2) (not (in ?s ?t2))))
+                   (((inter ?t1 ?t2))) () ((my_in ?s ?t1)) (or (my_in ?s ?t2) (not (my_in ?s ?t2))))
 
 (assert-propagation ((?t1 set) (?t2 set))
-                   () () ((not (= ?t1 ?t2))) (exists ((?e elt)) (or (and (in ?e ?t1) (not (in ?e ?t2))) (and (not (in ?e ?t1)) (in ?e ?t2)))))
+                   () () ((not (= ?t1 ?t2))) (exists ((?e elt)) (or (and (my_in ?e ?t1) (not (my_in ?e ?t2))) (and (not (my_in ?e ?t1)) (my_in ?e ?t2)))))
 
 ;;;;;;;;;;;;;;;;;;;
 ;; shortcut
 (declare-fun subset (set set) Bool)
 (assert-reduction ((?t1 set) (?t2 set))
-                 () () ((subset ?t1 ?t2)) (= (union ?t1 ?t2) ?t2))
+                 () () ((subset ?t1 ?t2)) (= (my_union ?t1 ?t2) ?t2))
 
 (declare-fun e () elt)
 (declare-fun t1 () set)
 (declare-fun t2 () set)
 (declare-fun t3 () set)
 
-;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e (union t1 t1)))))
-;;(assert (not (=> (in e (union t1 t1)) (in e t1))))
+;;(assert (not (=> (my_in e (inter (my_union t1 t2) (my_union t1 t1))) (my_in e (my_union t1 t1)))))
+;;(assert (not (=> (my_in e (my_union t1 t1)) (my_in e t1))))
 
 ;; hyp
-;;(assert (=> (in e (union t1 t1)) (in e t1)))
+;;(assert (=> (my_in e (my_union t1 t1)) (my_in e t1)))
 
-;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e t1))))
+;;(assert (not (=> (my_in e (inter (my_union t1 t2) (my_union t1 t1))) (my_in e t1))))
 
-;;(assert (or (and (not (in e (union t1 (union t2 t3)))) (in e (union (union t1 t2) t3))) (and (in e (union t1 (union t2 t3))) (not (in e (union (union t1 t2) t3))))) )
-(assert (not (= (union t1 (union t2 t3)) (union (union t1 t2) t3))) )
+;;(assert (or (and (not (my_in e (my_union t1 (my_union t2 t3)))) (my_in e (my_union (my_union t1 t2) t3))) (and (my_in e (my_union t1 (my_union t2 t3))) (not (my_in e (my_union (my_union t1 t2) t3))))) )
+(assert (not (= (my_union t1 (my_union t2 t3)) (my_union (my_union t1 t2) t3))) )
 
 (check-sat)
 
diff --git a/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2 b/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2
index 4d65ffac5..2a7e59d6e 100644
--- a/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2
+++ b/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2
@@ -2,11 +2,11 @@
 (set-logic AUFLIA)
 (set-info :status sat)
 
-;; don't use a datatypes for currently focusing in uf
+;; don't use a datatypes for currently focusing my_in uf
 (declare-sort elt 0)
 (declare-sort set 0)
 
-(declare-fun in (elt set) Bool)
+(declare-fun my_in (elt set) Bool)
 
 
 ;;;;;;;;;;;;;;;;;;;;
@@ -14,112 +14,112 @@
 
 (declare-fun inter (set set)  set)
 (assert-propagation ((?s elt) (?t1 set) (?t2 set)) () ()
-                  ((in ?s (inter ?t1 ?t2))) (and (in ?s ?t1) (in ?s ?t2)))
+                  ((my_in ?s (inter ?t1 ?t2))) (and (my_in ?s ?t1) (my_in ?s ?t2)))
 
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((inter ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (inter ?t1 ?t2))) )
+                  (((inter ?t1 ?t2))) () ((not (my_in ?s ?t1))) (not (my_in ?s (inter ?t1 ?t2))) )
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((inter ?t1 ?t2))) () ((not (in ?s ?t2))) (not (in ?s (inter ?t1 ?t2))) )
+                  (((inter ?t1 ?t2))) () ((not (my_in ?s ?t2))) (not (my_in ?s (inter ?t1 ?t2))) )
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t1)) (not (in ?s ?t2)) )
+                  () () ((not (my_in ?s (inter ?t1 ?t2))) (my_in ?s ?t1)) (not (my_in ?s ?t2)) )
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t2)) (not (in ?s ?t1)))
+                  () () ((not (my_in ?s (inter ?t1 ?t2))) (my_in ?s ?t2)) (not (my_in ?s ?t1)))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((inter ?t1 ?t2))) () ((in ?s ?t1) (in ?s ?t2)) (in ?s (inter ?t1 ?t2)) )
+                  (((inter ?t1 ?t2))) () ((my_in ?s ?t1) (my_in ?s ?t2)) (my_in ?s (inter ?t1 ?t2)) )
 
 ;;;;;;;;;;;;;;;;;
 ;; union
 
-(declare-fun union (set set)  set)
+(declare-fun my_union (set set)  set)
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((not (in ?s (union ?t1 ?t2)))) (and (not (in ?s ?t1)) (not (in ?s ?t2))))
+                  () () ((not (my_in ?s (my_union ?t1 ?t2)))) (and (not (my_in ?s ?t1)) (not (my_in ?s ?t2))))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((union ?t1 ?t2))) () ((in ?s ?t1)) (in ?s (union ?t1 ?t2)))
+                  (((my_union ?t1 ?t2))) () ((my_in ?s ?t1)) (my_in ?s (my_union ?t1 ?t2)))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((union ?t1 ?t2))) () ((in ?s ?t2)) (in ?s (union ?t1 ?t2)))
+                  (((my_union ?t1 ?t2))) () ((my_in ?s ?t2)) (my_in ?s (my_union ?t1 ?t2)))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t1))) (in ?s ?t2))
+                  () () ((my_in ?s (my_union ?t1 ?t2)) (not (my_in ?s ?t1))) (my_in ?s ?t2))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t2))) (in ?s ?t1))
+                  () () ((my_in ?s (my_union ?t1 ?t2)) (not (my_in ?s ?t2))) (my_in ?s ?t1))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((union ?t1 ?t2))) () ((not (in ?s ?t1)) (not (in ?s ?t2))) (not (in ?s (union ?t1 ?t2))))
+                  (((my_union ?t1 ?t2))) () ((not (my_in ?s ?t1)) (not (my_in ?s ?t2))) (not (my_in ?s (my_union ?t1 ?t2))))
 
 ;;;;;;;;;;;;;;;;;;;;
 ;; diff
 
 (declare-fun diff (set set)  set)
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((in ?s (diff ?t1 ?t2))) (and (in ?s ?t1) (not (in ?s ?t2))))
+                  () () ((my_in ?s (diff ?t1 ?t2))) (and (my_in ?s ?t1) (not (my_in ?s ?t2))))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((diff ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (diff ?t1 ?t2))) )
+                  (((diff ?t1 ?t2))) () ((not (my_in ?s ?t1))) (not (my_in ?s (diff ?t1 ?t2))) )
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((diff ?t1 ?t2))) () ((in ?s ?t2)) (not (in ?s (diff ?t1 ?t2))))
+                  (((diff ?t1 ?t2))) () ((my_in ?s ?t2)) (not (my_in ?s (diff ?t1 ?t2))))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((not (in ?s (diff ?t1 ?t2))) (in ?s ?t1)) (in ?s ?t2))
+                  () () ((not (my_in ?s (diff ?t1 ?t2))) (my_in ?s ?t1)) (my_in ?s ?t2))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((not (in ?s (diff ?t1 ?t2))) (not (in ?s ?t2))) (not (in ?s ?t1)))
+                  () () ((not (my_in ?s (diff ?t1 ?t2))) (not (my_in ?s ?t2))) (not (my_in ?s ?t1)))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((diff ?t1 ?t2))) () ((in ?s ?t1) (not (in ?s ?t2))) (in ?s (diff ?t1 ?t2)) )
+                  (((diff ?t1 ?t2))) () ((my_in ?s ?t1) (not (my_in ?s ?t2))) (my_in ?s (diff ?t1 ?t2)) )
 
 ;;;;;;;;;;;;;;;;
 ;;sing
 
 (declare-fun sing (elt)  set)
 (assert-propagation ((?s elt))
-                  (((sing ?s))) () () (in ?s (sing ?s)) )
+                  (((sing ?s))) () () (my_in ?s (sing ?s)) )
 
 (assert-propagation ((?s elt) (?t1 elt))
-                  () () ((in ?s (sing ?t1))) (= ?s ?t1))
+                  () () ((my_in ?s (sing ?t1))) (= ?s ?t1))
 
 (assert-propagation ((?s elt) (?t1 elt))
-                  () () ((not (in ?s (sing ?t1)))) (not (= ?s ?t1)))
+                  () () ((not (my_in ?s (sing ?t1)))) (not (= ?s ?t1)))
 
 ;;;;;;;;;;;;;;;;;;;
 ;; fullfiling runned at Full effort
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((in ?s (union ?t1 ?t2))) (or (in ?s ?t1) (not (in ?s ?t1))))
+                  () () ((my_in ?s (my_union ?t1 ?t2))) (or (my_in ?s ?t1) (not (my_in ?s ?t1))))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((inter ?t1 ?t2))) () ((in ?s ?t1)) (or (in ?s ?t2) (not (in ?s ?t2))))
+                  (((inter ?t1 ?t2))) () ((my_in ?s ?t1)) (or (my_in ?s ?t2) (not (my_in ?s ?t2))))
 
 (assert-propagation ((?t1 set) (?t2 set))
-                  () () ((not (= ?t1 ?t2))) (exists ((?e elt)) (or (and (in ?e ?t1) (not (in ?e ?t2))) (and (not (in ?e ?t1)) (in ?e ?t2)))))
+                  () () ((not (= ?t1 ?t2))) (exists ((?e elt)) (or (and (my_in ?e ?t1) (not (my_in ?e ?t2))) (and (not (my_in ?e ?t1)) (my_in ?e ?t2)))))
 
 ;;;;;;;;;;;;;;;;;;;
 ;; shortcut
 (declare-fun subset (set set) Bool)
 (assert-reduction ((?t1 set) (?t2 set))
-                () () ((subset ?t1 ?t2)) (= (union ?t1 ?t2) ?t2))
+                () () ((subset ?t1 ?t2)) (= (my_union ?t1 ?t2) ?t2))
 
 (declare-fun e () elt)
 (declare-fun t1 () set)
 (declare-fun t2 () set)
 (declare-fun t3 () set)
 
-;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e (union t1 t1)))))
-;;(assert (not (=> (in e (union t1 t1)) (in e t1))))
+;;(assert (not (=> (my_in e (inter (my_union t1 t2) (my_union t1 t1))) (my_in e (my_union t1 t1)))))
+;;(assert (not (=> (my_in e (my_union t1 t1)) (my_in e t1))))
 
 ;; hyp
-;;(assert (=> (in e (union t1 t1)) (in e t1)))
+;;(assert (=> (my_in e (my_union t1 t1)) (my_in e t1)))
 
-;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e t1))))
+;;(assert (not (=> (my_in e (inter (my_union t1 t2) (my_union t1 t1))) (my_in e t1))))
 
-(assert (or (and (not (in e (union t1 (union t2 t3)))) (in e (union (union t1 t2) t3))) (and (in e (union t1 (union t2 t3))) (not (in e (union (union t2 t2) t3))))) )
+(assert (or (and (not (my_in e (my_union t1 (my_union t2 t3)))) (my_in e (my_union (my_union t1 t2) t3))) (and (my_in e (my_union t1 (my_union t2 t3))) (not (my_in e (my_union (my_union t2 t2) t3))))) )
 
 
 (check-sat)