From b14e52e64520e5f344811db5969bb02b5fa8eb17 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Sun, 8 Jun 2014 17:01:54 -0400 Subject: [PATCH] sets translate: a different translation using axioms todo: set logic correctly, split the code for two translators --- examples/sets-translate/sets_translate.cpp | 113 ++++++++++++++++----- 1 file 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 #include #include +#include // 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) { -- 2.30.2