From 5c42662fe5cea3051341c8292202357e2a5e7dd3 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Thu, 29 May 2014 20:13:52 -0400 Subject: [PATCH] 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 --- examples/Makefile.am | 4 +- examples/sets-translate/Makefile | 4 + examples/sets-translate/Makefile.am | 19 ++ examples/sets-translate/sets_translate.cpp | 286 +++++++++++++++++++++ src/expr/mkkind | 3 +- src/parser/parser.h | 4 + src/printer/smt2/smt2_printer.cpp | 2 +- src/smt/smt_engine.cpp | 3 +- 8 files changed, 321 insertions(+), 4 deletions(-) create mode 100644 examples/sets-translate/Makefile create mode 100644 examples/sets-translate/Makefile.am create mode 100644 examples/sets-translate/sets_translate.cpp diff --git a/examples/Makefile.am b/examples/Makefile.am index 940af06ff..0f5c7db98 100644 --- a/examples/Makefile.am +++ b/examples/Makefile.am @@ -1,14 +1,16 @@ -SUBDIRS = nra-translate hashsmt api . +SUBDIRS = nra-translate sets-translate hashsmt api . AM_CPPFLAGS = \ -I@srcdir@/../src/include -I@srcdir@/../src -I@builddir@/../src $(ANTLR_INCLUDES) AM_CXXFLAGS = -Wall AM_CFLAGS = -Wall + noinst_PROGRAMS = \ simple_vc_cxx \ translator + if CVC4_BUILD_LIBCOMPAT noinst_PROGRAMS += \ simple_vc_compat_cxx 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 +#include +#include +#include +#include + + +#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, 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 t_t; + t_t.push_back(t); + t_t.push_back(t); + vector 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 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 = ""; + + // 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 variables; + vector info_tags; + vector info_data; + vector 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(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(cmd); + DefineTypeCommand* definesort = dynamic_cast(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(cmd); + DeclareFunctionCommand* declarefun = dynamic_cast(cmd); + DefineFunctionCommand* definefun = dynamic_cast(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; + } +} diff --git a/src/expr/mkkind b/src/expr/mkkind index 987feafac..d54aa3a83 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -333,8 +333,9 @@ function register_kind { r=$1 nc=$2 comment=$3 + register_kind_counter=$[register_kind_counter+1] - kind_decls="${kind_decls} $r, /**< $comment */ + kind_decls="${kind_decls} $r, /**< $comment ($register_kind_counter) */ " kind_printers="${kind_printers} case $r: out << \"$r\"; break; " diff --git a/src/parser/parser.h b/src/parser/parser.h index 3f5e66492..2f30460d2 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -272,6 +272,10 @@ public: void disallowIncludeFile() { d_canIncludeFile = false; } bool canIncludeFile() const { return d_canIncludeFile; } + /** Expose the functionality from SMT/SMT2 parsers, while making + implementation optional by returning false by default. */ + virtual bool logicIsSet() { return false; } + void forceLogic(const std::string& logic) { assert(!d_logicIsForced); d_logicIsForced = true; d_forcedLogic = logic; } const std::string& getForcedLogic() const { return d_forcedLogic; } bool logicIsForced() const { return d_logicIsForced; } diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 8201c9b7c..8e5a9dae4 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -713,7 +713,7 @@ static inline void toStream(std::ostream& out, const SExpr& sexpr) throw() { // SMT-LIB quoting for symbols static std::string quoteSymbol(std::string s) { - if(s.find_first_not_of("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789~!@%^&*_-+=<>.?/") == std::string::npos) { + if(s.find_first_not_of("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789~!@$%^&*_-+=<>.?/") == std::string::npos) { // simple unquoted symbol return s; } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f9ac1e9db..33496ac3b 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3444,7 +3444,8 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin Trace("smt") << "--- model-post expected " << expectedType << endl; // type-check the result we got - Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(expectedType)); + Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(expectedType), + "Run with -t smt for details."); // ensure it's a constant Assert(resultNode.getKind() == kind::LAMBDA || resultNode.isConst()); -- 2.30.2