From: Morgan Deters Date: Tue, 17 Jun 2014 19:58:04 +0000 (-0400) Subject: New translator features: expand define-funs and combine assertions. X-Git-Tag: cvc5-1.0.0~6758^2~16 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=40f3b400173c637185eb9ad20e649bd92030c82b;p=cvc5.git New translator features: expand define-funs and combine assertions. --- diff --git a/examples/translator.cpp b/examples/translator.cpp index b7e6f618a..7aa969e06 100644 --- a/examples/translator.cpp +++ b/examples/translator.cpp @@ -21,6 +21,7 @@ #include #include #include +#include "smt/smt_engine.h" #include "util/language.h" #include "expr/command.h" #include "expr/expr.h" @@ -38,11 +39,15 @@ enum { OUTPUT_FILE = 'o', HELP = 'h', DEFAULT_DAG_THRESH, + EXPAND_DEFINITIONS, + COMBINE_ASSERTIONS, };/* enum */ const struct option longopts[] = { { "output-lang", required_argument, NULL, OUTPUT_LANG }, { "output-language", required_argument, NULL, OUTPUT_LANG }, + { "expand-definitions", no_argument, NULL, EXPAND_DEFINITIONS }, + { "combine-assertions", no_argument, NULL, COMBINE_ASSERTIONS }, { "default-dag-thresh", required_argument, NULL, DEFAULT_DAG_THRESH }, { "lang", required_argument, NULL, INPUT_LANG }, { "language", required_argument, NULL, INPUT_LANG }, @@ -57,6 +62,8 @@ static void showHelp() { << " --input-language | -L set input language (default auto)" << endl << " --out | -o set output file (- for stdout)" << endl << " --default-dag-thresh=N set DAG threshold" << endl + << " --expand-definitions expand define-funs" << endl + << " --combine-assertions combine all assertions into one" << endl << " --help | -h this help" << endl << "Options and input filenames can be intermixed, and order is important." << endl << "For instance, \"-O smt2 x -O cvc4 y\" reads file x in smt2 format and" @@ -65,7 +72,7 @@ static void showHelp() { << "Comments and formatting are not preserved." << endl; } -static void readFile(const char* filename, InputLanguage fromLang, OutputLanguage toLang, ostream* out) { +static void readFile(const char* filename, InputLanguage fromLang, OutputLanguage toLang, bool expand_definitions, bool combine_assertions, ostream* out) { if(fromLang == input::LANG_AUTO) { unsigned len = strlen(filename); if(len >= 5 && !strcmp(".smt2", filename + len - 5)) { @@ -100,15 +107,87 @@ static void readFile(const char* filename, InputLanguage fromLang, OutputLanguag parserBuilder.withLineBufferedStreamInput(cin); } Parser *parser = parserBuilder.build(); + // we only use the SmtEngine to do definition expansion for us + SmtEngine *smt = expand_definitions ? new SmtEngine(&exprMgr) : NULL; + // store up the assertions into one big conjunction + std::vector assertions; while(Command* cmd = parser->nextCommand()) { - *out << cmd << endl; + if(expand_definitions && dynamic_cast(cmd) != NULL) { + // tell the SmtEngine about the definition, but don't print it + cmd->invoke(smt); + } else { + // have to switch on the command and expand definitions inside it + if(expand_definitions && dynamic_cast(cmd) != NULL) { + Expr e = static_cast(cmd)->getExpr(); + delete cmd; + cmd = new AssertCommand(smt->expandDefinitions(e)); + } else if(expand_definitions && dynamic_cast(cmd) != NULL) { + Expr e = static_cast(cmd)->getExpr(); + delete cmd; + cmd = new QueryCommand(smt->expandDefinitions(e)); + } else if(expand_definitions && dynamic_cast(cmd) != NULL) { + Expr e = static_cast(cmd)->getExpr(); + delete cmd; + cmd = new CheckSatCommand(smt->expandDefinitions(e)); + } else if(expand_definitions && dynamic_cast(cmd) != NULL) { + Expr e = static_cast(cmd)->getTerm(); + delete cmd; + cmd = new SimplifyCommand(smt->expandDefinitions(e)); + } else if(expand_definitions && dynamic_cast(cmd) != NULL) { + Expr e = static_cast(cmd)->getTerm(); + delete cmd; + cmd = new ExpandDefinitionsCommand(smt->expandDefinitions(e)); + } else if(expand_definitions && dynamic_cast(cmd) != NULL) { + vector terms = static_cast(cmd)->getTerms(); + delete cmd; + for(size_t i = 0; i < terms.size(); ++i) { + terms[i] = smt->expandDefinitions(terms[i]); + } + cmd = new GetValueCommand(terms); + } + + if(combine_assertions && dynamic_cast(cmd) != NULL) { + // store up the assertion, don't print it yet + assertions.push_back(static_cast(cmd)->getExpr()); + } else { + if(combine_assertions && + ( dynamic_cast(cmd) != NULL || + dynamic_cast(cmd) != NULL || + dynamic_cast(cmd) != NULL || + dynamic_cast(cmd) != NULL || + dynamic_cast(cmd) != NULL || + dynamic_cast(cmd) != NULL )) { + // combine all the stored assertions and print them at this point + if(!assertions.empty()) { + if(assertions.size() > 1) { + *out << AssertCommand(exprMgr.mkExpr(kind::AND, assertions)) << endl; + } else { + *out << AssertCommand(assertions[0]) << endl; + } + assertions.clear(); + } + } + + // now print the cmd we just parsed + *out << cmd << endl; + } + } if(dynamic_cast(cmd) != NULL) { delete cmd; break; } delete cmd; } + if(!assertions.empty()) { + if(assertions.size() > 1) { + *out << AssertCommand(exprMgr.mkExpr(kind::AND, assertions)) << endl; + } else { + *out << AssertCommand(assertions[0]) << endl; + } + assertions.clear(); + } *out << flush; + delete smt; delete parser; } @@ -121,6 +200,8 @@ int main(int argc, char* argv[]) { OutputLanguage toLang = output::LANG_SMTLIB_V2; size_t files = 0; int dag_thresh = 1; + bool expand_definitions = false; + bool combine_assertions = false; try { int c; @@ -129,7 +210,7 @@ int main(int argc, char* argv[]) { case 1: ++files; *out << Expr::dag(dag_thresh); - readFile(optarg, (!strcmp(optarg, "-") && fromLang == input::LANG_AUTO) ? input::LANG_CVC4 : fromLang, toLang, out); + readFile(optarg, (!strcmp(optarg, "-") && fromLang == input::LANG_AUTO) ? input::LANG_CVC4 : fromLang, toLang, expand_definitions, combine_assertions, out); break; case INPUT_LANG: if(!strcmp(optarg, "help")) { @@ -173,6 +254,12 @@ int main(int argc, char* argv[]) { dag_thresh = ul > INT_MAX ? INT_MAX : int(ul); } break; + case EXPAND_DEFINITIONS: + expand_definitions = true; + break; + case COMBINE_ASSERTIONS: + combine_assertions = true; + break; case 'h': showHelp(); exit(0); @@ -188,7 +275,7 @@ int main(int argc, char* argv[]) { if(files == 0) { *out << Expr::dag(dag_thresh); - readFile("-", fromLang == input::LANG_AUTO ? input::LANG_CVC4 : fromLang, toLang, out); + readFile("-", fromLang == input::LANG_AUTO ? input::LANG_CVC4 : fromLang, toLang, expand_definitions, combine_assertions, out); exit(0); } } catch(Exception& e) { diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 28a45206f..f82fc86ed 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -528,7 +528,7 @@ public: /** * Expand definitions in n. */ - Node expandDefinitions(TNode n, hash_map& cache) + Node expandDefinitions(TNode n, hash_map& cache, bool expandOnly = false) throw(TypeCheckingException, LogicException); /** @@ -1501,10 +1501,7 @@ void SmtEngine::defineFunction(Expr func, d_definedFunctions->insert(funcNode, def); } - - - -Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map& cache) +Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map& cache, bool expandOnly) throw(TypeCheckingException, LogicException) { stack< triple > worklist; @@ -1586,12 +1583,14 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_maptheoryOf(node); Assert(t != NULL); @@ -3478,7 +3477,7 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, L Dump("benchmark") << ExpandDefinitionsCommand(e); } hash_map cache; - Node n = d_private->expandDefinitions(Node::fromExpr(e), cache); + Node n = d_private->expandDefinitions(Node::fromExpr(e), cache, /* expandOnly = */ true); n = postprocess(n, TypeNode::fromType(e.getType())); return n.toExpr();