rename subseteq to subset in smtlib, all kinds and smt operator names…

… are now consistent
kbansal · Jun 25, 2014 · 2a734a3 · 2a734a3
1 parent b8ddf76
commit 2a734a3
Show file tree

Hide file tree

Showing 15 changed files with 31 additions and 31 deletions.
diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp
@@ -44,37 +44,37 @@ const bool enableAxioms = false;
 #endif
 
 string setaxioms[] = {
-  "(declare-fun inHOLDA (HOLDB (Set HOLDB)) Bool)",
+  "(declare-fun memberHOLDA (HOLDB (Set HOLDB)) Bool)",
   "",
   "(declare-fun unionHOLDA ((Set HOLDB) (Set HOLDB)) (Set HOLDB))",
   "(assert (forall ((?X (Set HOLDB)) (?Y (Set HOLDB)) (?x HOLDB))",
-  "                (= (inHOLDA ?x (unionHOLDA ?X ?Y))",
-  "                     (or (inHOLDA ?x ?X) (inHOLDA ?x ?Y))",
+  "                (= (memberHOLDA ?x (unionHOLDA ?X ?Y))",
+  "                     (or (memberHOLDA ?x ?X) (memberHOLDA ?x ?Y))",
   "                ) ) )",
   "",
   "",
   "(declare-fun intersectionHOLDA ((Set HOLDB) (Set HOLDB)) (Set HOLDB))",
   "(assert (forall ((?X (Set HOLDB)) (?Y (Set HOLDB)) (?x HOLDB))",
-  "                (= (inHOLDA ?x (intersectionHOLDA ?X ?Y))",
-  "                     (and (inHOLDA ?x ?X) (inHOLDA ?x ?Y))",
+  "                (= (memberHOLDA ?x (intersectionHOLDA ?X ?Y))",
+  "                     (and (memberHOLDA ?x ?X) (memberHOLDA ?x ?Y))",
   "                ) ) )",
   "",
   "(declare-fun setminusHOLDA ((Set HOLDB) (Set HOLDB)) (Set HOLDB))",
   "(assert (forall ((?X (Set HOLDB)) (?Y (Set HOLDB)) (?x HOLDB))",
-  "                (= (inHOLDA ?x (setminusHOLDA ?X ?Y))",
-  "                     (and (inHOLDA ?x ?X) (not (inHOLDA ?x ?Y)))",
+  "                (= (memberHOLDA ?x (setminusHOLDA ?X ?Y))",
+  "                     (and (memberHOLDA ?x ?X) (not (memberHOLDA ?x ?Y)))",
   "                ) ) )",
   "",
-  "(declare-fun setenumHOLDA (HOLDB) (Set HOLDB))",
+  "(declare-fun singletonHOLDA (HOLDB) (Set HOLDB))",
   "(assert (forall ((?x HOLDB) (?y HOLDB))",
-  "                (= (inHOLDA ?x (setenumHOLDA ?y))",
+  "                (= (memberHOLDA ?x (singletonHOLDA ?y))",
   "                     (= ?x ?y)",
   "                ) ) )",
   "",
   "(declare-fun emptysetHOLDA () (Set HOLDB))",
-  "(assert (forall ((?x HOLDB)) (not (inHOLDA ?x emptysetHOLDA)) ) )",
+  "(assert (forall ((?x HOLDB)) (not (memberHOLDA ?x emptysetHOLDA)) ) )",
   "",
-  "(define-fun subseteqHOLDA ((X (Set HOLDB)) (Y (Set HOLDB))) Bool (= (unionHOLDA X Y) Y))",
+  "(define-fun subsetHOLDA ((X (Set HOLDB)) (Y (Set HOLDB))) Bool (= (unionHOLDA X Y) Y))",
   ""
 };
 
@@ -123,12 +123,12 @@ class Mapper {
                    t);
 
       if(!enableAxioms)
-        sout << "(define-fun setenum" << elementTypeAsString << "     "
+        sout << "(define-fun singleton" << elementTypeAsString << "     "
              << " ( (x " << elementType << ") )"
              << " " << name << ""
              << " (store emptyset" << elementTypeAsString << " x true) )" << endl;
       setoperators[ make_pair(t, kind::SINGLETON) ] =
-        em->mkVar( std::string("setenum") + elementTypeAsString,
+        em->mkVar( std::string("singleton") + elementTypeAsString,
                    em->mkFunctionType( elementType, t ) );
 
       if(!enableAxioms)
@@ -164,16 +164,16 @@ class Mapper {
              << " Bool"
              << " (select s x) )" << endl;
       setoperators[ make_pair(t, kind::MEMBER) ] =
-        em->mkVar( std::string("in") + elementTypeAsString,
+        em->mkVar( std::string("member") + elementTypeAsString,
                    em->mkPredicateType( elet_t ) );
 
       if(!enableAxioms)
-        sout << "(define-fun subseteq" << elementTypeAsString << "    "
+        sout << "(define-fun subset" << elementTypeAsString << "    "
              << " ( (s1 " << name << ") (s2 " << name << ") )"
              << " Bool"
              <<" (= emptyset" << elementTypeAsString << " (setminus" << elementTypeAsString << " s1 s2)) )" << endl;
       setoperators[ make_pair(t, kind::SUBSET) ] =
-        em->mkVar( std::string("subseteq") + elementTypeAsString,
+        em->mkVar( std::string("subset") + elementTypeAsString,
                    em->mkPredicateType( t_t ) );
 
       if(enableAxioms) {

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
@@ -149,7 +149,7 @@ void Smt2::addTheory(Theory theory) {
     addOperator(kind::UNION, "union");
     addOperator(kind::INTERSECTION, "intersection");
     addOperator(kind::SETMINUS, "setminus");
-    addOperator(kind::SUBSET, "subseteq");
+    addOperator(kind::SUBSET, "subset");
     addOperator(kind::MEMBER, "member");
     addOperator(kind::SINGLETON, "singleton");
     break;

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
@@ -609,7 +609,7 @@ static string smtKindString(Kind k) throw() {
   case kind::UNION: return "union";
   case kind::INTERSECTION: return "intersection";
   case kind::SETMINUS: return "setminus";
-  case kind::SUBSET: return "subseteq";
+  case kind::SUBSET: return "subset";
   case kind::MEMBER: return "member";
   case kind::SET_TYPE: return "Set";
   case kind::SINGLETON: return "singleton";

diff --git a/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 b/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2
@@ -11,7 +11,7 @@
 ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
 ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
-(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2))
 (declare-fun z3v58 () Int)
 (declare-fun z3v59 () Int)
 (assert (distinct z3v58 z3v59))

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
@@ -10,7 +10,7 @@
 
 (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))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2))
 (declare-fun z3v58 () Int)
 (declare-fun z3v59 () Int)
 (assert (distinct z3v58 z3v59))

diff --git a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2
@@ -10,7 +10,7 @@
 ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
 ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
-(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2))
 (declare-fun z3v54 () Int)
 (declare-fun z3f55 (Int) Int)
 (declare-fun z3v56 () Int)

diff --git a/test/regress/regress0/sets/jan27/ListElem.hs.fqout.cvc4.38.smt2 b/test/regress/regress0/sets/jan27/ListElem.hs.fqout.cvc4.38.smt2
@@ -16,7 +16,7 @@
 ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
 ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
-(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2))
 (declare-fun z3v56 () Int)
 (declare-fun z3v57 () Int)
 (assert (distinct z3v56 z3v57))

diff --git a/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 b/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2
@@ -11,7 +11,7 @@
 ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
 ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
-(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2))
 (declare-fun z3v58 () Int)
 (declare-fun z3v59 () Int)
 (assert (distinct z3v58 z3v59))

diff --git a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2
@@ -11,7 +11,7 @@
 ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
 ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
-(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2))
 (declare-fun z3v60 () Int)
 (declare-fun z3v61 () Int)
 (assert (distinct z3v60 z3v61))

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
@@ -8,7 +8,7 @@
 (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))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2))
 (declare-fun z3v66 () Int)
 (declare-fun z3v67 () Int)
 (assert (distinct z3v66 z3v67))

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
@@ -10,7 +10,7 @@
 ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
 ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
-(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2))
 (declare-fun z3v66 () Int)
 (declare-fun z3v67 () Int)
 (assert (distinct z3v66 z3v67))

diff --git a/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2 b/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2
@@ -8,7 +8,7 @@
 (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))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2))
 
 (declare-fun z3v66 () Int)
 (declare-fun z3v67 () Int)

diff --git a/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2 b/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2
@@ -8,7 +8,7 @@
 (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))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2))
 
 (declare-fun z3f70 (Int) mySet)
 (declare-fun z3f72 (Int) mySet)
@@ -177,7 +177,7 @@
                         (z3f70 z3v270))))
 (assert (= z3v242 (z3f77 z3v271 z3v270)))
 (assert (= z3v242 z3v243))
-(assert (subseteq (z3f70 z3v242)
+(assert (subset (z3f70 z3v242)
                   (z3f70 z3v244)))
 (assert (= (z3f72 z3v243) smt_set_emp))
 (assert (= (z3f72 z3v244)

diff --git a/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2 b/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2
@@ -31,7 +31,7 @@
 ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
 ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
-(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2))
 
 (declare-fun z3v58 () Int)
 (declare-fun z3v59 () Int)

diff --git a/test/regress/regress0/sets/sets-sample.smt2 b/test/regress/regress0/sets/sets-sample.smt2
@@ -16,7 +16,7 @@
 (assert (= c (union a b) ))
 (assert (not (= c (intersection a b) )))
 (assert (= c (setminus a b) ))
-(assert (subseteq a b))
+(assert (subset a b))
 (assert (member e c))
 (assert (member e a))
 (assert (member e (intersection a b)))