sets translate: a different translation using axioms

todo: set logic correctly, split the code for two translators

1 files changed, 85 insertions, 28 deletions

diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp
index 5b0a9c3d0..dbc7100c0 100644
--- a/examples/sets-translate/sets_translate.cpp
+++ b/examples/sets-translate/sets_translate.cpp
@@ -20,6 +20,7 @@
 #include <typeinfo>
 #include <cassert>
 #include <vector>
+#include <boost/algorithm/string.hpp> // include Boost, a C++ library
 
 
 #include "options/options.h"
@@ -36,6 +37,43 @@ using namespace CVC4::options;
 
 bool nonsense(char c) { return !isalnum(c); } 
 
+const bool enableAxioms = true;
+
+string setaxioms[] = {
+  "(declare-fun inHOLDA (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))",
+  "                ) ) )",
+  "",
+  "",
+  "(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))",
+  "                ) ) )",
+  "",
+  "(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)))",
+  "                ) ) )",
+  "",
+  "(declare-fun setenumHOLDA (HOLDB) (Set HOLDB))",
+  "(assert (forall ((?x HOLDB) (?y HOLDB))",
+  "                (= (inHOLDA ?x (setenumHOLDA ?y))",
+  "                     (= ?x ?y)",
+  "                ) ) )",
+  "",
+  "(declare-fun emptysetHOLDA () (Set HOLDB))",
+  "(assert (forall ((?x HOLDB)) (not (inHOLDA ?x emptysetHOLDA)) ) )",
+  "",
+  "(define-fun subseteqHOLDA ((X (Set HOLDB)) (Y (Set HOLDB))) Bool (= (unionHOLDA X Y) Y))",
+  ""
+};
+
 class Mapper {
   set< Type > setTypes;
   map< Type, Type > mapTypes;
@@ -71,62 +109,81 @@ class Mapper {
       elet_t.push_back(elementType);
       elet_t.push_back(t);
 
-      sout << "(define-fun emptyset" << elementTypeAsString << "    "
-           << " ()"
-           << " " << name
-           << " ( (as const " << name << ") false ) )" << endl;
+      if(!enableAxioms)
+        sout << "(define-fun emptyset" << elementTypeAsString << "    "
+             << " ()"
+             << " " << name
+             << " ( (as const " << name << ") false ) )" << endl;
       setoperators[ make_pair(t, kind::EMPTYSET) ] =
         em->mkVar( std::string("emptyset") + elementTypeAsString,
                    t);
 
-      sout << "(define-fun setenum" << elementTypeAsString << "     "
-           << " ( (x " << elementType << ") )"
-           << " " << name << ""
-           << " (store emptyset" << elementTypeAsString << " x true) )" << endl;
+      if(!enableAxioms)
+        sout << "(define-fun setenum" << elementTypeAsString << "     "
+             << " ( (x " << elementType << ") )"
+             << " " << name << ""
+             << " (store emptyset" << elementTypeAsString << " x true) )" << endl;
       setoperators[ make_pair(t, kind::SET_SINGLETON) ] =
         em->mkVar( std::string("setenum") + elementTypeAsString,
                    em->mkFunctionType( elementType, t ) );
 
-      sout << "(define-fun union" << elementTypeAsString << "       "
-           << " ( (s1 " << name << ") (s2 " << name << ") )"
-           << " " << name << ""
-           << " ((_ map or) s1 s2))" << endl;
+      if(!enableAxioms)
+        sout << "(define-fun union" << elementTypeAsString << "       "
+             << " ( (s1 " << name << ") (s2 " << name << ") )"
+             << " " << name << ""
+             << " ((_ map or) s1 s2))" << endl;
       setoperators[ make_pair(t, kind::UNION) ] =
         em->mkVar( std::string("union") + elementTypeAsString,
                    em->mkFunctionType( t_t, t ) );
 
-      sout << "(define-fun intersection" << elementTypeAsString << ""
-           << " ( (s1 " << name << ") (s2 " << name << ") )"
-           << " " << name << ""
-           << " ((_ map and) s1 s2))" << endl;
+      if(!enableAxioms)
+        sout << "(define-fun intersection" << elementTypeAsString << ""
+             << " ( (s1 " << name << ") (s2 " << name << ") )"
+             << " " << name << ""
+             << " ((_ map and) s1 s2))" << endl;
       setoperators[ make_pair(t, kind::INTERSECTION) ] =
         em->mkVar( std::string("intersection") + elementTypeAsString,
                    em->mkFunctionType( t_t, t ) );
 
-      sout << "(define-fun setminus" << elementTypeAsString << "    "
-           << " ( (s1 " << name << ") (s2 " << name << ") )"
-           << " " << name << ""
-           << " (intersection" << elementTypeAsString << " s1 ((_ map not) s2)))" << endl;
+      if(!enableAxioms)
+        sout << "(define-fun setminus" << elementTypeAsString << "    "
+             << " ( (s1 " << name << ") (s2 " << name << ") )"
+             << " " << name << ""
+             << " (intersection" << elementTypeAsString << " s1 ((_ map not) s2)))" << endl;
       setoperators[ make_pair(t, kind::SETMINUS) ] =
         em->mkVar( std::string("setminus") + elementTypeAsString,
                    em->mkFunctionType( t_t, t ) );
 
-      sout << "(define-fun in" << elementTypeAsString << "          "
-           << " ( (x " << elementType << ")" << " (s " << name << "))"
-           << " Bool"
-           << " (select s x) )" << endl;
+      if(!enableAxioms)
+        sout << "(define-fun in" << elementTypeAsString << "          "
+             << " ( (x " << elementType << ")" << " (s " << name << "))"
+             << " Bool"
+             << " (select s x) )" << endl;
       setoperators[ make_pair(t, kind::MEMBER) ] =
         em->mkVar( std::string("in") + elementTypeAsString,
                    em->mkPredicateType( elet_t ) );
 
-      sout << "(define-fun subseteq" << elementTypeAsString << "    "
-           << " ( (s1 " << name << ") (s2 " << name << ") )"
-           << " Bool"
-           <<" (= emptyset" << elementTypeAsString << " (setminus" << elementTypeAsString << " s1 s2)) )" << endl;
+      if(!enableAxioms)
+        sout << "(define-fun subseteq" << 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->mkPredicateType( t_t ) );
 
+      if(enableAxioms) {
+        int N = sizeof(setaxioms) / sizeof(setaxioms[0]);
+        for(int i = 0; i < N; ++i) {
+          string s = setaxioms[i];
+          ostringstream oss; oss << Expr::setlanguage(language::output::LANG_SMTLIB_V2) << elementType;
+          boost::replace_all(s, "HOLDA", elementTypeAsString);
+          boost::replace_all(s, "HOLDB", oss.str());
+          if( s == "" ) continue;
+          sout << s << endl;
+        }
+      }
+
     }
     Expr ret;
     if(e.getKind() == kind::EMPTYSET) {