Renaming of SMT2 operator names, kinds for set theory

* SET_SINGLETON kind renamed to just SINGLETON
* "setenum" smt2 opertor renamed to "singleton"[1]
* "in" smt2 operator renamed to "member"[2]

[1] It was anyhow accepting exactly one argument, so was bit misleading
    to call set enumerator.

[2] The corresponding kind was called MEMBER, so this will also make them
    consistent. Only inconsistency now is for subset: kind is called
    SUBSET but operator is called "subseteq".

4 files changed, 10 insertions, 10 deletions

diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.smt2
index f37a8ccfe..e17911327 100644
--- a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.smt2
+++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.smt2
@@ -3,8 +3,8 @@
 (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_mem ((x Elt) (s mySet)) Bool (member x s))
+(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (singleton 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))
diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2
index 59cc1a00e..bea016683 100644
--- a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2
+++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2
@@ -3,8 +3,8 @@
 (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_mem ((x Elt) (s mySet)) Bool (member x s))
+(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (singleton 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_com ((s mySet)) mySet ((_ map not) s))
diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2
index 5fa5101f0..df659f0fb 100644
--- a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2
+++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2
@@ -8,12 +8,12 @@
 ; What was going on?
 ;
 ; The solver was unable to reason that (emptyset) cannot equal
-; (setenum 0). There were no membership predicates anywhere, just
+; (singleton 0). There were no membership predicates anywhere, just
 ; equalities.
 ;
 ; Fix
 ;
-; Add the propagation rule: (true) => (in x (setenum x))
+; Add the propagation rule: (true) => (member x (singleton x))
 
 (declare-fun z3f70 (Int) (Set Int))
 (declare-fun z3v85 () Int)
@@ -21,7 +21,7 @@
 (declare-fun z3v87 () Int)
 (declare-fun z3v90 () Int)
 
-(assert (= (z3f70 z3v90) (union (z3f70 z3v85) (union (as emptyset (Set Int)) (setenum z3v86)))))
+(assert (= (z3f70 z3v90) (union (z3f70 z3v85) (union (as emptyset (Set Int)) (singleton z3v86)))))
 (assert (= (z3f70 z3v90) (z3f70 z3v87)))
 (assert (= (as emptyset (Set Int)) (z3f70 z3v87)))
 (check-sat)
diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2
index d01b7468e..af67a69a7 100644
--- a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2
+++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2
@@ -9,10 +9,10 @@
 (declare-fun T () (Set Int))
 (declare-fun x () Int)
 
-(assert (or (not (= S smt_set_emp)) (in x T)))
+(assert (or (not (= S smt_set_emp)) (member x T)))
 
 (assert (= smt_set_emp 
-           (ite (in x T) 
-                (union (union smt_set_emp (setenum x)) S) 
+           (ite (member x T) 
+                (union (union smt_set_emp (singleton x)) S) 
                 S)))
 (check-sat)