From 2a734a31217cd17bd1d51abb621b0cb409973285 Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Tue, 24 Jun 2014 14:29:12 -0400
Subject: rename subseteq to subset in smtlib, all kinds and smt operator names
 are now consistent

---
 examples/sets-translate/sets_translate.cpp | 32 +++++++++++++++---------------
 1 file changed, 16 insertions(+), 16 deletions(-)

(limited to 'examples/sets-translate')

diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp
index 5257915b0..14df2fac0 100644
--- 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) {
-- 
cgit v1.2.3