diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-05-29 20:13:52 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-06 15:40:36 -0400 |
commit | 5c42662fe5cea3051341c8292202357e2a5e7dd3 (patch) | |
tree | 94aa636b95c7a81594a3d82f236263c91b0f6d0f /examples/sets-translate | |
parent | 0dce010bea47bc6a318eece2bd92ed2305b64c21 (diff) |
Sets translate, and other short fixes
- $ is a simple symbol is smt2.
- ever found yourself counting in kind.h? no longer.
- expose parser "logic is set" state for smt/smt2 (any better way?)
- a more helpful assertion message in smt_engine
Diffstat (limited to 'examples/sets-translate')
-rw-r--r-- | examples/sets-translate/Makefile | 4 | ||||
-rw-r--r-- | examples/sets-translate/Makefile.am | 19 | ||||
-rw-r--r-- | examples/sets-translate/sets_translate.cpp | 286 |
3 files changed, 309 insertions, 0 deletions
diff --git a/examples/sets-translate/Makefile b/examples/sets-translate/Makefile new file mode 100644 index 000000000..8efe0c48e --- /dev/null +++ b/examples/sets-translate/Makefile @@ -0,0 +1,4 @@ +topdir = ../.. +srcdir = examples/sets-translate + +include $(topdir)/Makefile.subdir diff --git a/examples/sets-translate/Makefile.am b/examples/sets-translate/Makefile.am new file mode 100644 index 000000000..40b79e998 --- /dev/null +++ b/examples/sets-translate/Makefile.am @@ -0,0 +1,19 @@ +AM_CPPFLAGS = \ + -I@srcdir@/../../src/include -I@srcdir@/../../src -I@builddir@/../../src $(ANTLR_INCLUDES) +AM_CXXFLAGS = -Wall +AM_CFLAGS = -Wall + +noinst_PROGRAMS = \ + sets_translate + +noinst_DATA = + +sets_translate_SOURCES = \ + sets_translate.cpp +sets_translate_LDADD = \ + @builddir@/../../src/parser/libcvc4parser.la \ + @builddir@/../../src/libcvc4.la + +# for installation +examplesdir = $(docdir)/$(subdir) +examples_DATA = $(DIST_SOURCES) $(EXTRA_DIST) diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp new file mode 100644 index 000000000..6cf2b61e2 --- /dev/null +++ b/examples/sets-translate/sets_translate.cpp @@ -0,0 +1,286 @@ +/********************* */ +/*! \file sets-translate.cpp + ** \verbatim + ** Original author: Kshitij Bansal + ** Major contributors: None + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include <string> +#include <iostream> +#include <typeinfo> +#include <cassert> +#include <vector> + + +#include "options/options.h" +#include "expr/expr.h" +#include "theory/logic_info.h" +#include "expr/command.h" +#include "parser/parser.h" +#include "parser/parser_builder.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::parser; +using namespace CVC4::options; + +bool nonsense(char c) { return !isalnum(c); } + +class Mapper { + set< Type > setTypes; + map< Type, Type > mapTypes; + map< pair<Type, Kind>, Expr > setoperators; + hash_map< Expr, Expr, ExprHashFunction > substitutions; + ostringstream sout; + ExprManager* em; + + Expr add(SetType t, Expr e) { + + if(setTypes.find(t) == setTypes.end() ) { + // mark as processed + setTypes.insert(t); + + Type elementType = t.getElementType(); + string elementTypeAsString = elementType.toString(); + remove_if(elementTypeAsString.begin(), elementTypeAsString.end(), nonsense); + + // define-sort + ostringstream oss_name; + oss_name << Expr::setlanguage(language::output::LANG_SMTLIB_V2) + << "(Set " << elementType << ")"; + string name = oss_name.str(); + Type newt = em->mkArrayType(t.getElementType(), em->booleanType()); + mapTypes[t] = newt; + + // diffent types + vector<Type> t_t; + t_t.push_back(t); + t_t.push_back(t); + vector<Type> elet_t; + elet_t.push_back(elementType); + elet_t.push_back(t); + + 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; + 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; + 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; + 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; + 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; + 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; + setoperators[ make_pair(t, kind::SUBSET) ] = + em->mkVar( std::string("subseteq") + elementTypeAsString, + em->mkPredicateType( t_t ) ); + + } + Expr ret; + if(e.getKind() == kind::EMPTYSET) { + ret = setoperators[ make_pair(t, e.getKind()) ]; + } else { + vector<Expr> children = e.getChildren(); + children.insert(children.begin(), setoperators[ make_pair(t, e.getKind()) ]); + ret = em->mkExpr(kind::APPLY, children); + } + // cout << "returning " << ret << endl; + return ret; + } + +public: + Mapper(ExprManager* e) : em(e) { + sout << Expr::setlanguage(language::output::LANG_SMTLIB_V2); + } + + void defineSetSort() { + if(setTypes.empty()) { + cout << "(define-sort Set (X) (Array X Bool) )" << endl; + } + } + + + Expr collectSortsExpr(Expr e) + { + Expr old_e = e; + for(unsigned i = 0; i < e.getNumChildren(); ++i) { + collectSortsExpr(e[i]); + } + e = e.substitute(substitutions); + if(theory::kindToTheoryId(e.getKind()) == theory::THEORY_SETS) { + SetType t = SetType(e.getType().isBoolean() ? e[1].getType() : e.getType()); + substitutions[e] = add(t, e); + e = e.substitute(substitutions); + } + // cout << old_e << " => " << e << endl; + return e; + } + + void dump() { + cout << sout.str(); + } +}; + + +int main(int argc, char* argv[]) +{ + + try { + + // Get the filename + string input; + if(argv > 0) input = (argv[1]); + else input = "<stdin>"; + + // Create the expression manager + Options options; + options.set(inputLanguage, language::input::LANG_SMTLIB_V2); + cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2); + ExprManager exprManager(options); + + Mapper m(&exprManager); + + // Create the parser + ParserBuilder parserBuilder(&exprManager, input, options); + Parser* parser = parserBuilder.build(); + + // Variables and assertions + vector<string> variables; + vector<string> info_tags; + vector<string> info_data; + vector<Expr> assertions; + + Command* cmd = NULL; + CommandSequence commandsSequence; + bool logicisset = false; + + while ((cmd = parser->nextCommand())) { + + // till logic is set, don't do any modifications + if(!parser->logicIsSet()) { + cout << (*cmd) << endl; + delete cmd; + continue; + } + + // transform set-logic command, if there is one + SetBenchmarkLogicCommand* setlogic = dynamic_cast<SetBenchmarkLogicCommand*>(cmd); + if(setlogic) { + LogicInfo logicinfo(setlogic->getLogic()); + if(!logicinfo.isTheoryEnabled(theory::THEORY_SETS)) { + cerr << "Sets theory not enabled. Stopping translation." << endl; + return 0; + } + logicinfo = logicinfo.getUnlockedCopy(); + logicinfo.disableTheory(theory::THEORY_SETS); + logicinfo.enableTheory(theory::THEORY_ARRAY); + logicinfo.lock(); + // cout << SetBenchmarkLogicCommand(logicinfo.getLogicString()) << endl; + + delete cmd; + continue; + } + + // if we reach here, logic is set by now, so can define our sort + if( !logicisset ) { + logicisset = true; + m.defineSetSort(); + } + + // declare/define-sort commands are printed immediately + DeclareTypeCommand* declaresort = dynamic_cast<DeclareTypeCommand*>(cmd); + DefineTypeCommand* definesort = dynamic_cast<DefineTypeCommand*>(cmd); + if(declaresort || definesort) { + cout << *cmd << endl; + delete cmd; + continue; + } + + // other commands are queued up, while replacing with new function symbols + AssertCommand* assert = dynamic_cast<AssertCommand*>(cmd); + DeclareFunctionCommand* declarefun = dynamic_cast<DeclareFunctionCommand*>(cmd); + DefineFunctionCommand* definefun = dynamic_cast<DefineFunctionCommand*>(cmd); + + Command* new_cmd = NULL; + if(assert) { + Expr newexpr = m.collectSortsExpr(assert->getExpr()); + new_cmd = new AssertCommand(newexpr); + } else if(declarefun) { + Expr newfunc = m.collectSortsExpr(declarefun->getFunction()); + new_cmd = new DeclareFunctionCommand(declarefun->getSymbol(), newfunc, declarefun->getType()); + } else if(definefun) { + Expr newfunc = m.collectSortsExpr(definefun->getFunction()); + Expr newformula = m.collectSortsExpr(definefun->getFormula()); + new_cmd = new DefineFunctionCommand(definefun->getSymbol(), newfunc, definefun->getFormals(), newformula); + } + + if(new_cmd == NULL) { + commandsSequence.addCommand(cmd); + } else { + commandsSequence.addCommand(new_cmd); + delete cmd; + } + + } + + m.dump(); + cout << commandsSequence; + + + // Get rid of the parser + //delete parser; + } catch (Exception& e) { + cerr << e << endl; + } +} |