diff options
Diffstat (limited to 'examples/nra-translate/smt2tomathematica.cpp')
-rw-r--r-- | examples/nra-translate/smt2tomathematica.cpp | 310 |
1 files changed, 310 insertions, 0 deletions
diff --git a/examples/nra-translate/smt2tomathematica.cpp b/examples/nra-translate/smt2tomathematica.cpp new file mode 100644 index 000000000..25bc850ae --- /dev/null +++ b/examples/nra-translate/smt2tomathematica.cpp @@ -0,0 +1,310 @@ +#include <string> +#include <iostream> +#include <typeinfo> +#include <cassert> +#include <vector> +#include <map> + + +#include "util/options.h" +#include "expr/expr.h" +#include "expr/command.h" +#include "parser/parser.h" +#include "parser/parser_builder.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::parser; + +void translate_to_mathematica( + string input, + const vector<string>& info_tags, + const vector<string>& info_data, + const map<Expr, unsigned>& variables, + const vector<BoolExpr>& assertions); + +int main(int argc, char* argv[]) +{ + + // Get the filename + string input(argv[1]); + + // Create the expression manager + Options options; + options.inputLanguage = language::input::LANG_SMTLIB_V2; + ExprManager exprManager(options); + + // Create the parser + ParserBuilder parserBuilder(&exprManager, input, options); + Parser* parser = parserBuilder.build(); + + // Variables and assertions + std::map<Expr, unsigned> variables; + vector<string> info_tags; + vector<string> info_data; + vector<BoolExpr> assertions; + + Command* cmd; + while ((cmd = parser->nextCommand())) { + + SetInfoCommand* setinfo = dynamic_cast<SetInfoCommand*>(cmd); + if (setinfo) { + info_tags.push_back(setinfo->getFlag()); + info_data.push_back(setinfo->getSExpr().getValue()); + delete cmd; + continue; + } + + DeclareFunctionCommand* declare = dynamic_cast<DeclareFunctionCommand*>(cmd); + if (declare) { + string name = declare->getSymbol(); + Expr var = parser->getVariable(name); + unsigned n = variables.size(); + variables[var] = n; + delete cmd; + continue; + } + + AssertCommand* assert = dynamic_cast<AssertCommand*>(cmd); + if (assert) { + assertions.push_back(assert->getExpr()); + delete cmd; + continue; + } + + delete cmd; + } + + // Do the translation + translate_to_mathematica(input, info_tags, info_data, variables, assertions); + + // Get rid of the parser + delete parser; +} + +void translate_to_mathematica_term(const map<Expr, unsigned>& variables, const Expr& term) { + bool first; + + unsigned n = term.getNumChildren(); + + if (n == 0) { + if (term.getKind() == kind::CONST_RATIONAL) { + cout << term.getConst<Rational>(); + } else { + assert(variables.find(term) != variables.end()); + cout << "x" << variables.find(term)->second; + } + } else { + + switch (term.getKind()) { + case kind::PLUS: + cout << "("; + first = true; + for (unsigned i = 0; i < n; ++ i) { + if (!first) { + cout << " + "; + } + first = false; + translate_to_mathematica_term(variables, term[i]); + } + cout << ")"; + break; + case kind::MULT: + cout << "("; + first = true; + for (unsigned i = 0; i < n; ++ i) { + if (!first) { + cout << " * "; + } + first = false; + translate_to_mathematica_term(variables, term[i]); + } + cout << ")"; + break; + case kind::MINUS: + cout << "("; + translate_to_mathematica_term(variables, term[0]); + cout << " - "; + translate_to_mathematica_term(variables, term[1]); + cout << ")"; + break; + case kind::DIVISION: + // we only allow division by constant + assert(term[1].getKind() == kind::CONST_RATIONAL); + cout << "("; + translate_to_mathematica_term(variables, term[0]); + cout << " / "; + translate_to_mathematica_term(variables, term[1]); + cout << ")"; + break; + case kind::UMINUS: + cout << "(-("; + translate_to_mathematica_term(variables, term[0]); + cout << "))"; + break; + default: + assert(false); + break; + } + } +} + +void translate_to_mathematica(const map<Expr, unsigned>& variables, const BoolExpr& assertion) { + bool first; + + unsigned n = assertion.getNumChildren(); + + if (n == 0) { + assert(false); + } else { + + std::string op; + bool binary = false; + bool theory = false; + + + switch (assertion.getKind()) { + case kind::NOT: + cout << "!"; + translate_to_mathematica(variables, assertion[0]); + break; + case kind::OR: + first = true; + cout << "("; + for (unsigned i = 0; i < n; ++ i) { + if (!first) { + cout << " || "; + } + first = false; + translate_to_mathematica(variables, assertion[i]); + } + cout << ")"; + break; + case kind::AND: + first = true; + cout << "("; + for (unsigned i = 0; i < n; ++ i) { + if (!first) { + cout << " && "; + } + first = false; + translate_to_mathematica(variables, assertion[i]); + } + cout << ")"; + break; + case kind::IMPLIES: + cout << "Implies["; + translate_to_mathematica(variables, assertion[0]); + cout << ","; + translate_to_mathematica(variables, assertion[1]); + cout << "]"; + break; + case kind::IFF: + cout << "Equivalent["; + translate_to_mathematica(variables, assertion[0]); + cout << ","; + translate_to_mathematica(variables, assertion[1]); + cout << "]"; + break; + case kind::EQUAL: + op = "=="; + theory = true; + break; + case kind::LT: + op = "<"; + theory = true; + break; + case kind::LEQ: + op = "<="; + theory = true; + break; + case kind::GT: + op = ">"; + theory = true; + break; + case kind::GEQ: + op = ">="; + theory = true; + break; + default: + assert(false); + break; + } + + if (binary) { + cout << "("; + translate_to_mathematica(variables, assertion[0]); + cout << " " << op << " "; + translate_to_mathematica(variables, assertion[1]); + cout << ")"; + } + + if (theory) { + cout << "("; + translate_to_mathematica_term(variables, assertion[0]); + cout << " " << op << " "; + translate_to_mathematica_term(variables, assertion[1]); + cout << ")"; + } + } +} + +void translate_to_mathematica( + string input, + const vector<string>& info_tags, + const vector<string>& info_data, + const std::map<Expr, unsigned>& variables, + const vector<BoolExpr>& assertions) +{ + bool first; + + // Dump out the information + cout << "(* translated from " << input << " "; + + bool dump_tags = false; + if (dump_tags) { + first = true; + for (unsigned i = 0; i < info_tags.size(); ++ i) { + if (!first) { + cout << ", "; + } + first = false; + cout << info_tags[i] << " = " << info_data[i]; + } + } + + cout << "*)" << endl; + + cout << "Resolve["; + + // Formula + cout << "Exists[{"; + first = true; + for (unsigned i = 0; i < variables.size(); ++ i) { + if (!first) { + cout << ","; + } + first = false; + cout << "x" << i; + } + cout << "}, "; + + if (assertions.size() > 1) { + first = true; + for (unsigned i = 0; i < assertions.size(); ++ i) { + if (!first) { + cout << " && "; + } + first = false; + translate_to_mathematica(variables, assertions[i]); + } + } else { + translate_to_mathematica(variables, assertions[0]); + } + cout << "]"; + + + // End resolve + cout << ", Reals]" << endl; +} + |