rename subseteq to subset in smtlib, all kinds and smt operator names are now consistent

diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp
index 5257915b035790e75f50277f2b0815be968ace02..14df2fac0a3521db166d3d6b461ce3a917adb963 100644 (file)
--- 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
index a0d759cc2f80f428e32b701731fa12f959cfb73c..3f1e59e6d0065fdada435b7cd911c839b61c597c 100644 (file)
--- 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
index dbdc65ba95c47e12bdcba6510a07d10acfd4da1a..3c0f4ebc5ee627e9c0c70008c7bc86f02851ce1c 100644 (file)
--- 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
index 87cb9b73d90c98e3c9d1454c1535e5e94f6d5570..7b5294aecf91048a031e82b4c54722777388d79a 100644 (file)
--- 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
index bc919673dd76cf68b63be0b413154679b775b3fb..71bb8a3e65329ecf8d8b46ed13e1ef5c01b59a3f 100644 (file)
--- 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
index f055a8e1c7c7c48a096de1f99af1a8bd2f8b6756..eb48b023af23ec3ac25b7c0a93b41de47e4c8755 100644 (file)
--- 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
index 81b8794e5ea63612c837ad0171cacc99986ba584..3c0ef1ddad784f60915a4796919eedec24659296 100644 (file)
--- 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
index 8b84c9153a03da1db42d8fda90b1ca87dd4b202a..83dfe41e582198c87c0907166d7044d5d774a09c 100644 (file)
--- 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
index ac5fdf48da98a0d12ce526f44de9d4afd8239a71..282325f14d96df7ff6de14fe31d976b51fec4401 100644 (file)
--- 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
index e17911327ab573ff61e4c88ef35afbef70bbd287..10ed4be7c7ad72ee41f782bd3899fc868cde9e01 100644 (file)
--- 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
index bea016683e777daad795b0506ecf9adfc41e6fda..6165b98de878f6e61bd378d8ef8eee66b9dbbca8 100644 (file)
--- 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
index 9175a87234d38904736c11a53e931e0e0aca31ba..38477c46a315cf5be952aad40af2f3c9ed4b805f 100644 (file)
--- 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
index 81117134c163d2cedb8827cf89bd537343b2c608..e282e446eda2ca3f6a8e65c3a0ef8cc6327c7fb6 100644 (file)
--- 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
index 1e848695d367c664f708ee78fb2ef022afab8775..0fc8ca067f2f9fe5f799eac310e7f0fded79bf21 100644 (file)
--- 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
index 4838c6cf283c430f7750e060c7f591c23c6d21f3..a040b0bec0dd811b4888716d02b5ec7d355f3500 100644 (file)
--- 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)))