projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 831feca)
Revert "fix naming conflicts in benchmarks"
authorKshitij Bansal <kshitij@cs.nyu.edu>
Fri, 28 Feb 2014 15:19:26 +0000 (10:19 -0500)
committerKshitij Bansal <kshitij@cs.nyu.edu>
Wed, 5 Mar 2014 19:53:44 +0000 (14:53 -0500)
This reverts commit 4cac1b63f76a0a973a015ea6f8e21ad31d84d971.

test/regress/regress0/quantifiers/set8.smt2 patch | blob | history
test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2 patch | blob | history
test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2 patch | blob | history

diff --git a/test/regress/regress0/quantifiers/set8.smt2 b/test/regress/regress0/quantifiers/set8.smt2
index 6e4a846727fe6e3b4fd09e0bb178b8a8b2318d8f..684d94b7ae75dc6c7eda0cfc16e06651dc7ed99b 100644 (file)
--- a/test/regress/regress0/quantifiers/set8.smt2
+++ b/test/regress/regress0/quantifiers/set8.smt2
@@ -1,26 +1,26 @@
 (set-logic AUFLIA)
-(set-info :source | mySet theory. |)
+(set-info :source | Set theory. |)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
 (set-info :status unsat)
-(declare-sort mySet 0)
+(declare-sort Set 0)
 (declare-sort Elem 0)
-(declare-fun member (Elem mySet) Bool)
-(declare-fun subset (mySet mySet) Bool)
-(assert (forall ((?x Elem) (?s1 mySet) (?s2 mySet)) (=> (and (member ?x ?s1) (subset ?s1 ?s2)) (member ?x ?s2))))
-(assert (forall ((?s1 mySet) (?s2 mySet)) (=> (not (subset ?s1 ?s2)) (exists ((?x Elem)) (and (member ?x ?s1) (not (member ?x ?s2)))))))
-(assert (forall ((?s1 mySet) (?s2 mySet)) (=> (forall ((?x Elem)) (=> (member ?x ?s1) (member ?x ?s2))) (subset ?s1 ?s2))))
-(declare-fun seteq (mySet mySet) Bool)
-(assert (forall ((?s1 mySet) (?s2 mySet)) (= (seteq ?s1 ?s2) (= ?s1 ?s2))))
-(assert (forall ((?s1 mySet) (?s2 mySet)) (= (seteq ?s1 ?s2) (and (subset ?s1 ?s2) (subset ?s2 ?s1)))))
-(declare-fun myunion (mySet mySet) mySet)
-(assert (forall ((?x Elem) (?s1 mySet) (?s2 mySet)) (= (member ?x (myunion ?s1 ?s2)) (or (member ?x ?s1) (member ?x ?s2)))))
-(declare-fun myintersection (mySet mySet) mySet)
-(assert (forall ((?x Elem) (?s1 mySet) (?s2 mySet)) (= (member ?x (myintersection ?s1 ?s2)) (and (member ?x ?s1) (member ?x ?s2)))))
-(declare-fun difference (mySet mySet) mySet)
-(assert (forall ((?x Elem) (?s1 mySet) (?s2 mySet)) (= (member ?x (difference ?s1 ?s2)) (and (member ?x ?s1) (not (member ?x ?s2))))))
-(declare-fun a () mySet)
-(declare-fun b () mySet)
-(assert (not (seteq (myintersection a b) (myintersection b a))))
+(declare-fun member (Elem Set) Bool)
+(declare-fun subset (Set Set) Bool)
+(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (=> (and (member ?x ?s1) (subset ?s1 ?s2)) (member ?x ?s2))))
+(assert (forall ((?s1 Set) (?s2 Set)) (=> (not (subset ?s1 ?s2)) (exists ((?x Elem)) (and (member ?x ?s1) (not (member ?x ?s2)))))))
+(assert (forall ((?s1 Set) (?s2 Set)) (=> (forall ((?x Elem)) (=> (member ?x ?s1) (member ?x ?s2))) (subset ?s1 ?s2))))
+(declare-fun seteq (Set Set) Bool)
+(assert (forall ((?s1 Set) (?s2 Set)) (= (seteq ?s1 ?s2) (= ?s1 ?s2))))
+(assert (forall ((?s1 Set) (?s2 Set)) (= (seteq ?s1 ?s2) (and (subset ?s1 ?s2) (subset ?s2 ?s1)))))
+(declare-fun union (Set Set) Set)
+(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (member ?x (union ?s1 ?s2)) (or (member ?x ?s1) (member ?x ?s2)))))
+(declare-fun intersection (Set Set) Set)
+(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (member ?x (intersection ?s1 ?s2)) (and (member ?x ?s1) (member ?x ?s2)))))
+(declare-fun difference (Set Set) Set)
+(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (member ?x (difference ?s1 ?s2)) (and (member ?x ?s1) (not (member ?x ?s2))))))
+(declare-fun a () Set)
+(declare-fun b () Set)
+(assert (not (seteq (intersection a b) (intersection b a))))
 (check-sat)
 (exit)
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 56228e0829030f9d8543794f0a8436fae1eaceeb..9bd49f71463c607ac22cfcc67227172cca640995 100644 (file)
--- 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 my_in uf
+;; don't use a datatypes for currently focusing in uf
 (declare-sort elt 0)
 (declare-sort set 0)
 
-(declare-fun my_in (elt set) Bool)
+(declare-fun in (elt set) Bool)
 
 ;;;;;;;;;;;;;;;;;;;;
 ;; inter
 
 (declare-fun inter (set set)  set)
 (assert-propagation ((?s elt) (?t1 set) (?t2 set)) () ()
-                  ((my_in ?s (inter ?t1 ?t2))) (and (my_in ?s ?t1) (my_in ?s ?t2)))
+                  ((in ?s (inter ?t1 ?t2))) (and (in ?s ?t1) (in ?s ?t2)))
 
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((inter ?t1 ?t2))) () ((not (my_in ?s ?t1))) (not (my_in ?s (inter ?t1 ?t2))) )
+                   (((inter ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (inter ?t1 ?t2))) )
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((inter ?t1 ?t2))) () ((not (my_in ?s ?t2))) (not (my_in ?s (inter ?t1 ?t2))) )
+                   (((inter ?t1 ?t2))) () ((not (in ?s ?t2))) (not (in ?s (inter ?t1 ?t2))) )
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((not (my_in ?s (inter ?t1 ?t2))) (my_in ?s ?t1)) (not (my_in ?s ?t2)) )
+                   () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t1)) (not (in ?s ?t2)) )
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((not (my_in ?s (inter ?t1 ?t2))) (my_in ?s ?t2)) (not (my_in ?s ?t1)))
+                   () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t2)) (not (in ?s ?t1)))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((inter ?t1 ?t2))) () ((my_in ?s ?t1) (my_in ?s ?t2)) (my_in ?s (inter ?t1 ?t2)) )
+                   (((inter ?t1 ?t2))) () ((in ?s ?t1) (in ?s ?t2)) (in ?s (inter ?t1 ?t2)) )
 
 ;;;;;;;;;;;;;;;;;
 ;; union
 
-(declare-fun my_union (set set)  set)
+(declare-fun union (set set)  set)
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((not (my_in ?s (my_union ?t1 ?t2)))) (and (not (my_in ?s ?t1)) (not (my_in ?s ?t2))))
+                   () () ((not (in ?s (union ?t1 ?t2)))) (and (not (in ?s ?t1)) (not (in ?s ?t2))))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((my_union ?t1 ?t2))) () ((my_in ?s ?t1)) (my_in ?s (my_union ?t1 ?t2)))
+                   (((union ?t1 ?t2))) () ((in ?s ?t1)) (in ?s (union ?t1 ?t2)))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((my_union ?t1 ?t2))) () ((my_in ?s ?t2)) (my_in ?s (my_union ?t1 ?t2)))
+                   (((union ?t1 ?t2))) () ((in ?s ?t2)) (in ?s (union ?t1 ?t2)))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((my_in ?s (my_union ?t1 ?t2)) (not (my_in ?s ?t1))) (my_in ?s ?t2))
+                   () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t1))) (in ?s ?t2))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((my_in ?s (my_union ?t1 ?t2)) (not (my_in ?s ?t2))) (my_in ?s ?t1))
+                   () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t2))) (in ?s ?t1))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((my_union ?t1 ?t2))) () ((not (my_in ?s ?t1)) (not (my_in ?s ?t2))) (not (my_in ?s (my_union ?t1 ?t2))))
+                   (((union ?t1 ?t2))) () ((not (in ?s ?t1)) (not (in ?s ?t2))) (not (in ?s (union ?t1 ?t2))))
 
 ;;;;;;;;;;;;;;;;;;;;
 ;; diff
 
 (declare-fun diff (set set)  set)
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((my_in ?s (diff ?t1 ?t2))) (and (my_in ?s ?t1) (not (my_in ?s ?t2))))
+                   () () ((in ?s (diff ?t1 ?t2))) (and (in ?s ?t1) (not (in ?s ?t2))))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((diff ?t1 ?t2))) () ((not (my_in ?s ?t1))) (not (my_in ?s (diff ?t1 ?t2))) )
+                   (((diff ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (diff ?t1 ?t2))) )
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((diff ?t1 ?t2))) () ((my_in ?s ?t2)) (not (my_in ?s (diff ?t1 ?t2))))
+                   (((diff ?t1 ?t2))) () ((in ?s ?t2)) (not (in ?s (diff ?t1 ?t2))))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((not (my_in ?s (diff ?t1 ?t2))) (my_in ?s ?t1)) (my_in ?s ?t2))
+                   () () ((not (in ?s (diff ?t1 ?t2))) (in ?s ?t1)) (in ?s ?t2))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((not (my_in ?s (diff ?t1 ?t2))) (not (my_in ?s ?t2))) (not (my_in ?s ?t1)))
+                   () () ((not (in ?s (diff ?t1 ?t2))) (not (in ?s ?t2))) (not (in ?s ?t1)))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((diff ?t1 ?t2))) () ((my_in ?s ?t1) (not (my_in ?s ?t2))) (my_in ?s (diff ?t1 ?t2)) )
+                   (((diff ?t1 ?t2))) () ((in ?s ?t1) (not (in ?s ?t2))) (in ?s (diff ?t1 ?t2)) )
 
 ;;;;;;;;;;;;;;;;
 ;;sing
 
 (declare-fun sing (elt)  set)
 (assert-propagation ((?s elt))
-                   (((sing ?s))) () () (my_in ?s (sing ?s)) )
+                   (((sing ?s))) () () (in ?s (sing ?s)) )
 
 (assert-propagation ((?s elt) (?t1 elt))
-                   () () ((my_in ?s (sing ?t1))) (= ?s ?t1))
+                   () () ((in ?s (sing ?t1))) (= ?s ?t1))
 
 (assert-propagation ((?s elt) (?t1 elt))
-                   () () ((not (my_in ?s (sing ?t1)))) (not (= ?s ?t1)))
+                   () () ((not (in ?s (sing ?t1)))) (not (= ?s ?t1)))
 
 ;;;;;;;;;;;;;;;;;;;
 ;; fullfiling runned at Full effort
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((my_in ?s (my_union ?t1 ?t2))) (or (my_in ?s ?t1) (not (my_in ?s ?t1))))
+                   () () ((in ?s (union ?t1 ?t2))) (or (in ?s ?t1) (not (in ?s ?t1))))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((inter ?t1 ?t2))) () ((my_in ?s ?t1)) (or (my_in ?s ?t2) (not (my_in ?s ?t2))))
+                   (((inter ?t1 ?t2))) () ((in ?s ?t1)) (or (in ?s ?t2) (not (in ?s ?t2))))
 
 (assert-propagation ((?t1 set) (?t2 set))
-                   () () ((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)))))
+                   () () ((not (= ?t1 ?t2))) (exists ((?e elt)) (or (and (in ?e ?t1) (not (in ?e ?t2))) (and (not (in ?e ?t1)) (in ?e ?t2)))))
 
 ;;;;;;;;;;;;;;;;;;;
 ;; shortcut
 (declare-fun subset (set set) Bool)
 (assert-reduction ((?t1 set) (?t2 set))
-                 () () ((subset ?t1 ?t2)) (= (my_union ?t1 ?t2) ?t2))
+                 () () ((subset ?t1 ?t2)) (= (union ?t1 ?t2) ?t2))
 
 (declare-fun e () elt)
 (declare-fun t1 () set)
 (declare-fun t2 () set)
 (declare-fun t3 () set)
 
-;;(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))))
+;;(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))))
 
 ;; hyp
-;;(assert (=> (my_in e (my_union t1 t1)) (my_in e t1)))
+;;(assert (=> (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 t1))))
+;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e t1))))
 
-;;(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))) )
+;;(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))) )
 
 (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 2a7e59d6e55367d93f16582ef12c5d138ba12483..4d65ffac5b3fddbaf594514fa186beb1a7e46815 100644 (file)
--- 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 my_in uf
+;; don't use a datatypes for currently focusing in uf
 (declare-sort elt 0)
 (declare-sort set 0)
 
-(declare-fun my_in (elt set) Bool)
+(declare-fun in (elt set) Bool)
 
 
 ;;;;;;;;;;;;;;;;;;;;
@@ -14,112 +14,112 @@
 
 (declare-fun inter (set set)  set)
 (assert-propagation ((?s elt) (?t1 set) (?t2 set)) () ()
-                  ((my_in ?s (inter ?t1 ?t2))) (and (my_in ?s ?t1) (my_in ?s ?t2)))
+                  ((in ?s (inter ?t1 ?t2))) (and (in ?s ?t1) (in ?s ?t2)))
 
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((inter ?t1 ?t2))) () ((not (my_in ?s ?t1))) (not (my_in ?s (inter ?t1 ?t2))) )
+                  (((inter ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (inter ?t1 ?t2))) )
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((inter ?t1 ?t2))) () ((not (my_in ?s ?t2))) (not (my_in ?s (inter ?t1 ?t2))) )
+                  (((inter ?t1 ?t2))) () ((not (in ?s ?t2))) (not (in ?s (inter ?t1 ?t2))) )
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((not (my_in ?s (inter ?t1 ?t2))) (my_in ?s ?t1)) (not (my_in ?s ?t2)) )
+                  () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t1)) (not (in ?s ?t2)) )
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((not (my_in ?s (inter ?t1 ?t2))) (my_in ?s ?t2)) (not (my_in ?s ?t1)))
+                  () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t2)) (not (in ?s ?t1)))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((inter ?t1 ?t2))) () ((my_in ?s ?t1) (my_in ?s ?t2)) (my_in ?s (inter ?t1 ?t2)) )
+                  (((inter ?t1 ?t2))) () ((in ?s ?t1) (in ?s ?t2)) (in ?s (inter ?t1 ?t2)) )
 
 ;;;;;;;;;;;;;;;;;
 ;; union
 
-(declare-fun my_union (set set)  set)
+(declare-fun union (set set)  set)
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((not (my_in ?s (my_union ?t1 ?t2)))) (and (not (my_in ?s ?t1)) (not (my_in ?s ?t2))))
+                  () () ((not (in ?s (union ?t1 ?t2)))) (and (not (in ?s ?t1)) (not (in ?s ?t2))))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((my_union ?t1 ?t2))) () ((my_in ?s ?t1)) (my_in ?s (my_union ?t1 ?t2)))
+                  (((union ?t1 ?t2))) () ((in ?s ?t1)) (in ?s (union ?t1 ?t2)))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((my_union ?t1 ?t2))) () ((my_in ?s ?t2)) (my_in ?s (my_union ?t1 ?t2)))
+                  (((union ?t1 ?t2))) () ((in ?s ?t2)) (in ?s (union ?t1 ?t2)))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((my_in ?s (my_union ?t1 ?t2)) (not (my_in ?s ?t1))) (my_in ?s ?t2))
+                  () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t1))) (in ?s ?t2))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((my_in ?s (my_union ?t1 ?t2)) (not (my_in ?s ?t2))) (my_in ?s ?t1))
+                  () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t2))) (in ?s ?t1))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((my_union ?t1 ?t2))) () ((not (my_in ?s ?t1)) (not (my_in ?s ?t2))) (not (my_in ?s (my_union ?t1 ?t2))))
+                  (((union ?t1 ?t2))) () ((not (in ?s ?t1)) (not (in ?s ?t2))) (not (in ?s (union ?t1 ?t2))))
 
 ;;;;;;;;;;;;;;;;;;;;
 ;; diff
 
 (declare-fun diff (set set)  set)
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((my_in ?s (diff ?t1 ?t2))) (and (my_in ?s ?t1) (not (my_in ?s ?t2))))
+                  () () ((in ?s (diff ?t1 ?t2))) (and (in ?s ?t1) (not (in ?s ?t2))))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((diff ?t1 ?t2))) () ((not (my_in ?s ?t1))) (not (my_in ?s (diff ?t1 ?t2))) )
+                  (((diff ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (diff ?t1 ?t2))) )
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((diff ?t1 ?t2))) () ((my_in ?s ?t2)) (not (my_in ?s (diff ?t1 ?t2))))
+                  (((diff ?t1 ?t2))) () ((in ?s ?t2)) (not (in ?s (diff ?t1 ?t2))))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((not (my_in ?s (diff ?t1 ?t2))) (my_in ?s ?t1)) (my_in ?s ?t2))
+                  () () ((not (in ?s (diff ?t1 ?t2))) (in ?s ?t1)) (in ?s ?t2))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((not (my_in ?s (diff ?t1 ?t2))) (not (my_in ?s ?t2))) (not (my_in ?s ?t1)))
+                  () () ((not (in ?s (diff ?t1 ?t2))) (not (in ?s ?t2))) (not (in ?s ?t1)))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((diff ?t1 ?t2))) () ((my_in ?s ?t1) (not (my_in ?s ?t2))) (my_in ?s (diff ?t1 ?t2)) )
+                  (((diff ?t1 ?t2))) () ((in ?s ?t1) (not (in ?s ?t2))) (in ?s (diff ?t1 ?t2)) )
 
 ;;;;;;;;;;;;;;;;
 ;;sing
 
 (declare-fun sing (elt)  set)
 (assert-propagation ((?s elt))
-                  (((sing ?s))) () () (my_in ?s (sing ?s)) )
+                  (((sing ?s))) () () (in ?s (sing ?s)) )
 
 (assert-propagation ((?s elt) (?t1 elt))
-                  () () ((my_in ?s (sing ?t1))) (= ?s ?t1))
+                  () () ((in ?s (sing ?t1))) (= ?s ?t1))
 
 (assert-propagation ((?s elt) (?t1 elt))
-                  () () ((not (my_in ?s (sing ?t1)))) (not (= ?s ?t1)))
+                  () () ((not (in ?s (sing ?t1)))) (not (= ?s ?t1)))
 
 ;;;;;;;;;;;;;;;;;;;
 ;; fullfiling runned at Full effort
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((my_in ?s (my_union ?t1 ?t2))) (or (my_in ?s ?t1) (not (my_in ?s ?t1))))
+                  () () ((in ?s (union ?t1 ?t2))) (or (in ?s ?t1) (not (in ?s ?t1))))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((inter ?t1 ?t2))) () ((my_in ?s ?t1)) (or (my_in ?s ?t2) (not (my_in ?s ?t2))))
+                  (((inter ?t1 ?t2))) () ((in ?s ?t1)) (or (in ?s ?t2) (not (in ?s ?t2))))
 
 (assert-propagation ((?t1 set) (?t2 set))
-                  () () ((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)))))
+                  () () ((not (= ?t1 ?t2))) (exists ((?e elt)) (or (and (in ?e ?t1) (not (in ?e ?t2))) (and (not (in ?e ?t1)) (in ?e ?t2)))))
 
 ;;;;;;;;;;;;;;;;;;;
 ;; shortcut
 (declare-fun subset (set set) Bool)
 (assert-reduction ((?t1 set) (?t2 set))
-                () () ((subset ?t1 ?t2)) (= (my_union ?t1 ?t2) ?t2))
+                () () ((subset ?t1 ?t2)) (= (union ?t1 ?t2) ?t2))
 
 (declare-fun e () elt)
 (declare-fun t1 () set)
 (declare-fun t2 () set)
 (declare-fun t3 () set)
 
-;;(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))))
+;;(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))))
 
 ;; hyp
-;;(assert (=> (my_in e (my_union t1 t1)) (my_in e t1)))
+;;(assert (=> (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 t1))))
+;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e t1))))
 
-(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))))) )
+(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))))) )
 
 
 (check-sat)