From: Dejan Jovanović Date: Tue, 10 Jul 2012 15:24:22 +0000 (+0000) Subject: * fixing the simple_vc_cxx.cpp compile issue (no more Integer constants) X-Git-Tag: cvc5-1.0.0~7937 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ff5ecc85124857dccb6fa6ed542bb90e678bdc77;p=cvc5.git * fixing the simple_vc_cxx.cpp compile issue (no more Integer constants) * adding as examples the programs i used to translate nonlinear smt2 problems to other formats --- diff --git a/examples/Makefile.am b/examples/Makefile.am index d765e4d7a..484097740 100644 --- a/examples/Makefile.am +++ b/examples/Makefile.am @@ -1,3 +1,5 @@ +SUBDIRS = nra-translate . + AM_CPPFLAGS = \ -I@srcdir@/../src/include -I@srcdir@/../src -I@builddir@/../src $(ANTLR_INCLUDES) AM_CXXFLAGS = -Wall diff --git a/examples/nra-translate/Makefile b/examples/nra-translate/Makefile new file mode 100644 index 000000000..85400a5c7 --- /dev/null +++ b/examples/nra-translate/Makefile @@ -0,0 +1,4 @@ +topdir = ../.. +srcdir = examples/nra-translate + +include $(topdir)/Makefile.subdir diff --git a/examples/nra-translate/Makefile.am b/examples/nra-translate/Makefile.am new file mode 100644 index 000000000..63bd8c0c1 --- /dev/null +++ b/examples/nra-translate/Makefile.am @@ -0,0 +1,57 @@ +AM_CPPFLAGS = \ + -I@srcdir@/../../src/include -I@srcdir@/../../src -I@builddir@/../../src $(ANTLR_INCLUDES) +AM_CXXFLAGS = -Wall +AM_CFLAGS = -Wall + +noinst_PROGRAMS = \ + smt2toqepcad \ + smt2tomathematica \ + smt2toisat \ + smt2toredlog \ + smt2todreal \ + normalize \ + smt2info + +noinst_DATA = + +smt2toqepcad_SOURCES = \ + smt2toqepcad.cpp +smt2toqepcad_LDADD = \ + @builddir@/../../src/parser/libcvc4parser.la \ + @builddir@/../../src/libcvc4.la + +smt2tomathematica_SOURCES = \ + smt2tomathematica.cpp +smt2tomathematica_LDADD = \ + @builddir@/../../src/parser/libcvc4parser.la \ + @builddir@/../../src/libcvc4.la + +smt2toisat_SOURCES = \ + smt2toisat.cpp +smt2toisat_LDADD = \ + @builddir@/../../src/parser/libcvc4parser.la \ + @builddir@/../../src/libcvc4.la + +smt2toredlog_SOURCES = \ + smt2toredlog.cpp +smt2toredlog_LDADD = \ + @builddir@/../../src/parser/libcvc4parser.la \ + @builddir@/../../src/libcvc4.la + +smt2todreal_SOURCES = \ + smt2todreal.cpp +smt2todreal_LDADD = \ + @builddir@/../../src/parser/libcvc4parser.la \ + @builddir@/../../src/libcvc4.la + +smt2info_SOURCES = \ + smt2info.cpp +smt2info_LDADD = \ + @builddir@/../../src/parser/libcvc4parser.la \ + @builddir@/../../src/libcvc4.la + +normalize_SOURCES = \ + normalize.cpp +normalize_LDADD = \ + @builddir@/../../src/parser/libcvc4parser.la \ + @builddir@/../../src/libcvc4.la diff --git a/examples/nra-translate/normalize.cpp b/examples/nra-translate/normalize.cpp new file mode 100644 index 000000000..598055ea3 --- /dev/null +++ b/examples/nra-translate/normalize.cpp @@ -0,0 +1,70 @@ +#include +#include +#include +#include +#include +#include + + +#include "util/options.h" +#include "expr/expr.h" +#include "expr/command.h" +#include "parser/parser.h" +#include "parser/parser_builder.h" +#include "smt/smt_engine.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::parser; +using namespace CVC4::theory; + +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); + + cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2) << Expr::setdepth(-1); + + // Create the parser + ParserBuilder parserBuilder(&exprManager, input, options); + Parser* parser = parserBuilder.build(); + + // Smt manager for simplifications + SmtEngine engine(&exprManager); + + // Variables and assertions + vector assertions; + + Command* cmd; + while ((cmd = parser->nextCommand())) { + + AssertCommand* assert = dynamic_cast(cmd); + if (assert) { + Expr normalized = engine.simplify(assert->getExpr()); + cout << "(assert " << normalized << ")" << endl; + delete cmd; + continue; + } + + CheckSatCommand* checksat = dynamic_cast(cmd); + if (checksat) { + delete cmd; + continue; + } + + cout << *cmd << endl; + delete cmd; + } + + cout << "(check-sat)" << endl; + + // Get rid of the parser + delete parser; +} + diff --git a/examples/nra-translate/smt2info.cpp b/examples/nra-translate/smt2info.cpp new file mode 100644 index 000000000..a789bb8d9 --- /dev/null +++ b/examples/nra-translate/smt2info.cpp @@ -0,0 +1,118 @@ +#include +#include +#include +#include +#include + + +#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; + +unsigned compute_degree(ExprManager& exprManager, const Expr& term) { + unsigned n = term.getNumChildren(); + unsigned degree = 0; + + // boolean stuff + if (term.getType() == exprManager.booleanType()) { + for (unsigned i = 0; i < n; ++ i) { + degree = std::max(degree, compute_degree(exprManager, term[i])); + } + return degree; + } + + // terms + if (n == 0) { + if (term.getKind() == kind::CONST_RATIONAL) { + return 0; + } else { + return 1; + } + } else { + unsigned degree = 0; + if (term.getKind() == kind::MULT) { + for (unsigned i = 0; i < n; ++ i) { + degree += std::max(degree, compute_degree(exprManager, term[i])); + } + } else { + for (unsigned i = 0; i < n; ++ i) { + degree = std::max(degree, compute_degree(exprManager, term[i])); + } + } + return degree; + } +} + + +int main(int argc, char* argv[]) +{ + + try { + + // 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 + vector variables; + vector info_tags; + vector info_data; + vector assertions; + + Command* cmd; + while ((cmd = parser->nextCommand())) { + + SetInfoCommand* setinfo = dynamic_cast(cmd); + if (setinfo) { + info_tags.push_back(setinfo->getFlag()); + info_data.push_back(setinfo->getSExpr().getValue()); + delete cmd; + continue; + } + + DeclareFunctionCommand* declare = dynamic_cast(cmd); + if (declare) { + variables.push_back(declare->getSymbol()); + delete cmd; + continue; + } + + AssertCommand* assert = dynamic_cast(cmd); + if (assert) { + assertions.push_back(assert->getExpr()); + delete cmd; + continue; + } + + delete cmd; + } + + cout << "variables: " << variables.size() << endl; + + unsigned total_degree = 0; + for (unsigned i = 0; i < assertions.size(); ++ i) { + total_degree = std::max(total_degree, compute_degree(exprManager, assertions[i])); + } + + cout << "degree: " << total_degree << endl; + + // Get rid of the parser + delete parser; + } catch (Exception& e) { + cerr << e << endl; + } +} diff --git a/examples/nra-translate/smt2todreal.cpp b/examples/nra-translate/smt2todreal.cpp new file mode 100644 index 000000000..34e28bb75 --- /dev/null +++ b/examples/nra-translate/smt2todreal.cpp @@ -0,0 +1,66 @@ +#include +#include +#include +#include +#include +#include + +#include "util/options.h" +#include "expr/expr.h" +#include "expr/command.h" +#include "parser/parser.h" +#include "parser/parser_builder.h" +#include "smt/smt_engine.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::parser; + +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; + options.outputLanguage = language::output::LANG_SMTLIB_V2; + ExprManager exprManager(options); + + cout << Expr::dag(0) << Expr::setdepth(-1); + + // Create the parser + ParserBuilder parserBuilder(&exprManager, input, options); + Parser* parser = parserBuilder.build(); + + // Smt manager for simplifications + SmtEngine engine(&exprManager); + + // Variables and assertions + std::map variables; + vector info_tags; + vector info_data; + vector assertions; + + Command* cmd; + while ((cmd = parser->nextCommand())) { + + DeclareFunctionCommand* declare = dynamic_cast(cmd); + if (declare) { + cout << "[-10000, 10000] " << declare->getSymbol() << ";" << endl; + } + + AssertCommand* assert = dynamic_cast(cmd); + if (assert) { + cout << assert->getExpr() << ";" << endl; + } + + delete cmd; + } + + // Get rid of the parser + delete parser; +} + + diff --git a/examples/nra-translate/smt2toisat.cpp b/examples/nra-translate/smt2toisat.cpp new file mode 100644 index 000000000..1ad56805b --- /dev/null +++ b/examples/nra-translate/smt2toisat.cpp @@ -0,0 +1,295 @@ +#include +#include +#include +#include +#include +#include + + +#include "util/options.h" +#include "expr/expr.h" +#include "expr/command.h" +#include "parser/parser.h" +#include "parser/parser_builder.h" +#include "smt/smt_engine.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::parser; + +void translate_to_isat( + string input, + const vector& info_tags, + const vector& info_data, + const map& variables, + const vector& 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(); + + // Smt manager for simplifications + SmtEngine engine(&exprManager); + + // Variables and assertions + std::map variables; + vector info_tags; + vector info_data; + vector assertions; + + Command* cmd; + while ((cmd = parser->nextCommand())) { + + SetInfoCommand* setinfo = dynamic_cast(cmd); + if (setinfo) { + info_tags.push_back(setinfo->getFlag()); + info_data.push_back(setinfo->getSExpr().getValue()); + delete cmd; + continue; + } + + DeclareFunctionCommand* declare = dynamic_cast(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(cmd); + if (assert) { + assertions.push_back(engine.simplify(assert->getExpr())); + delete cmd; + continue; + } + + delete cmd; + } + + // Do the translation + translate_to_isat(input, info_tags, info_data, variables, assertions); + + // Get rid of the parser + delete parser; +} + +void translate_to_isat_term(const map& variables, const Expr& term) { + bool first; + + unsigned n = term.getNumChildren(); + + if (n == 0) { + if (term.getKind() == kind::CONST_RATIONAL) { + cout << term.getConst(); + } 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_isat_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_isat_term(variables, term[i]); + } + cout << ")"; + break; + case kind::MINUS: + cout << "("; + translate_to_isat_term(variables, term[0]); + cout << " - "; + translate_to_isat_term(variables, term[1]); + cout << ")"; + break; + case kind::DIVISION: + assert(false); + break; + case kind::UMINUS: + cout << "(-("; + translate_to_isat_term(variables, term[0]); + cout << "))"; + break; + default: + assert(false); + break; + } + } +} + +void translate_to_isat(const map& variables, const BoolExpr& assertion) { + bool first; + + unsigned n = assertion.getNumChildren(); + + if (n == 0) { + if (assertion.isConst()) { + if (assertion.getConst()) { + cout << "(1 > 0)"; + } else { + cout << "(1 < 0)"; + } + } else { + assert(false); + } + } else { + + std::string op; + bool binary = false; + bool theory = false; + + switch (assertion.getKind()) { + case kind::NOT: + cout << "!"; + translate_to_isat(variables, assertion[0]); + break; + case kind::OR: + first = true; + cout << "("; + for (unsigned i = 0; i < n; ++ i) { + if (!first) { + cout << " or "; + } + first = false; + translate_to_isat(variables, assertion[i]); + } + cout << ")"; + break; + case kind::AND: + first = true; + cout << "("; + for (unsigned i = 0; i < n; ++ i) { + if (!first) { + cout << " and "; + } + first = false; + translate_to_isat(variables, assertion[i]); + } + cout << ")"; + break; + case kind::IMPLIES: + cout << "("; + translate_to_isat(variables, assertion[0]); + cout << " -> "; + translate_to_isat(variables, assertion[1]); + cout << ")"; + break; + case kind::IFF: + cout << "("; + translate_to_isat(variables, assertion[0]); + cout << " <-> "; + translate_to_isat(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_isat(variables, assertion[0]); + cout << " " << op << " "; + translate_to_isat(variables, assertion[1]); + cout << ")"; + } + + if (theory) { + cout << "("; + translate_to_isat_term(variables, assertion[0]); + cout << " " << op << " "; + translate_to_isat_term(variables, assertion[1]); + cout << ")"; + } + } +} + +void translate_to_isat( + string input, + const vector& info_tags, + const vector& info_data, + const std::map& variables, + const vector& assertions) +{ + bool first; + + // Dump out the information + cout << "-- translated from " << input << endl; + + // Dump the variables + cout << "DECL" << endl; + cout << " -- the variables" << endl; + cout << " float [-1000, 1000]"; + first = true; + for (unsigned i = 0; i < variables.size(); ++ i) { + if (!first) { + cout << ","; + } + cout << " x" << i; + if (first) { + first = false; + } + } + cout << ";" << endl; + + // The assertions + cout << "EXPR" << endl; + cout << " -- the constraints to be solved" << endl; + for (unsigned i = 0; i < assertions.size(); ++ i) { + cout << " "; + translate_to_isat(variables, assertions[i]); + cout << ";" << endl; + } + +} + 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 +#include +#include +#include +#include +#include + + +#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& info_tags, + const vector& info_data, + const map& variables, + const vector& 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 variables; + vector info_tags; + vector info_data; + vector assertions; + + Command* cmd; + while ((cmd = parser->nextCommand())) { + + SetInfoCommand* setinfo = dynamic_cast(cmd); + if (setinfo) { + info_tags.push_back(setinfo->getFlag()); + info_data.push_back(setinfo->getSExpr().getValue()); + delete cmd; + continue; + } + + DeclareFunctionCommand* declare = dynamic_cast(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(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& variables, const Expr& term) { + bool first; + + unsigned n = term.getNumChildren(); + + if (n == 0) { + if (term.getKind() == kind::CONST_RATIONAL) { + cout << term.getConst(); + } 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& 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& info_tags, + const vector& info_data, + const std::map& variables, + const vector& 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; +} + diff --git a/examples/nra-translate/smt2toqepcad.cpp b/examples/nra-translate/smt2toqepcad.cpp new file mode 100644 index 000000000..fe3730382 --- /dev/null +++ b/examples/nra-translate/smt2toqepcad.cpp @@ -0,0 +1,334 @@ +#include +#include +#include +#include +#include +#include + +#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_qepcad( + string input, + const vector& info_tags, + const vector& info_data, + const map& variables, + const vector& assertions); + +int main(int argc, char* argv[]) +{ + std::map vars2id; + + // 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 variables; + vector info_tags; + vector info_data; + vector assertions; + + Command* cmd; + while ((cmd = parser->nextCommand())) { + + SetInfoCommand* setinfo = dynamic_cast(cmd); + if (setinfo) { + info_tags.push_back(setinfo->getFlag()); + info_data.push_back(setinfo->getSExpr().getValue()); + delete cmd; + continue; + } + + DeclareFunctionCommand* declare = dynamic_cast(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(cmd); + if (assert) { + assertions.push_back(assert->getExpr()); + delete cmd; + continue; + } + + delete cmd; + } + + // Do the translation + translate_to_qepcad(input, info_tags, info_data, variables, assertions); + + // Get rid of the parser + delete parser; +} + +void translate_to_qepcad_term(const std::map& variables, const Expr& term) { + bool first; + + unsigned n = term.getNumChildren(); + + if (n == 0) { + if (term.getKind() == kind::CONST_RATIONAL) { + cout << term.getConst(); + } 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_qepcad_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_qepcad_term(variables, term[i]); + } + cout << ")"; + break; + case kind::MINUS: + cout << "("; + translate_to_qepcad_term(variables, term[0]); + cout << " - "; + translate_to_qepcad_term(variables, term[1]); + cout << ")"; + break; + case kind::UMINUS: + cout << "(-("; + translate_to_qepcad_term(variables, term[0]); + cout << "))"; + break; + case kind::DIVISION: + // we only allow division by constant + assert(term[1].getKind() == kind::CONST_RATIONAL); + cout << "("; + cout << "(1/"; + translate_to_qepcad_term(variables, term[1]); + cout << ") "; + translate_to_qepcad_term(variables, term[0]); + cout << ")"; + break; + default: + assert(false); + break; + } + } +} + +void translate_to_qepcad(const std::map& variables, const BoolExpr& assertion) { + bool first; + + unsigned n = assertion.getNumChildren(); + + if (n == 0) { + assert(false); + } else { + + std::string op; + bool theory = false; + bool binary = false; + + switch (assertion.getKind()) { + case kind::NOT: + cout << "[~"; + translate_to_qepcad(variables, assertion[0]); + cout << "]"; + break; + case kind::OR: + first = true; + cout << "["; + for (unsigned i = 0; i < n; ++ i) { + if (!first) { + cout << " \\/ "; + } + first = false; + translate_to_qepcad(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_qepcad(variables, assertion[i]); + } + cout << "]"; + break; + case kind::IMPLIES: + op = "==>"; + binary = true; + break; + case kind::IFF: + op = "<==>"; + binary = true; + 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 (theory) { + cout << "["; + translate_to_qepcad_term(variables, assertion[0]); + cout << " " << op << " "; + translate_to_qepcad_term(variables, assertion[1]); + cout << "]"; + } + + if (binary) { + cout << "["; + translate_to_qepcad(variables, assertion[0]); + cout << " " << op << " "; + translate_to_qepcad(variables, assertion[1]); + cout << "]"; + } + } +} + +void translate_to_qepcad( + string input, + const vector& info_tags, + const vector& info_data, + const std::map& variables, + const vector& 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; + + // Declare the variables + cout << "("; + + first = true; + for (unsigned i = 0; i < variables.size(); ++ i) { + if (!first) { + cout << ","; + } + first = false; + cout << "x" << i;; + } + + cout << ")" << endl; + + // Number of free variables + cout << "0" << endl; + + // The quantifiers first + for (unsigned i = 0; i < variables.size(); ++ i) { + cout << "(Ex" << i << ")"; + } + + // Now the formula + cout << "["; + if (assertions.size() > 1) { + first = true; + for (unsigned i = 0; i < assertions.size(); ++ i) { + if (!first) { + cout << " /\\ "; + } + first = false; + translate_to_qepcad(variables, assertions[i]); + } + } else { + translate_to_qepcad(variables, assertions[0]); + } + cout << "]." << endl; + + // Before normalization + cout << "go" << endl; + + // Before projection + if (variables.size() > 3) { + cout << "proj-op (m,m"; + for (unsigned i = 3; i < variables.size(); ++ i) { + cout << ",h"; + } + cout << ")" << endl; + } + cout << "go" << endl; + + // Before choice + cout << "d-stat" << endl; + + // Before solution + cout << "go" << endl; + + // Finish up + cout << "finish" << endl; +} + diff --git a/examples/nra-translate/smt2toredlog.cpp b/examples/nra-translate/smt2toredlog.cpp new file mode 100644 index 000000000..a7111e595 --- /dev/null +++ b/examples/nra-translate/smt2toredlog.cpp @@ -0,0 +1,311 @@ +#include +#include +#include +#include +#include +#include + + +#include "util/options.h" +#include "expr/expr.h" +#include "expr/command.h" +#include "parser/parser.h" +#include "parser/parser_builder.h" +#include "smt/smt_engine.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::parser; + +void translate_to_redlog( + string input, + string command, + const vector& info_tags, + const vector& info_data, + const map& variables, + const vector& assertions); + +int main(int argc, char* argv[]) +{ + + // Get the filename + string input(argv[1]); + // Get the redlog command + string command(argv[2]); + + // 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(); + + // Smt manager for simplifications + SmtEngine engine(&exprManager); + + // Variables and assertions + std::map variables; + vector info_tags; + vector info_data; + vector assertions; + + Command* cmd; + while ((cmd = parser->nextCommand())) { + + SetInfoCommand* setinfo = dynamic_cast(cmd); + if (setinfo) { + info_tags.push_back(setinfo->getFlag()); + info_data.push_back(setinfo->getSExpr().getValue()); + delete cmd; + continue; + } + + DeclareFunctionCommand* declare = dynamic_cast(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(cmd); + if (assert) { + assertions.push_back(engine.simplify(assert->getExpr())); + delete cmd; + continue; + } + + delete cmd; + } + + // Do the translation + translate_to_redlog(input, command, info_tags, info_data, variables, assertions); + + // Get rid of the parser + delete parser; +} + +void translate_to_redlog_term(const map& variables, const Expr& term) { + bool first; + + unsigned n = term.getNumChildren(); + + if (n == 0) { + if (term.getKind() == kind::CONST_RATIONAL) { + cout << term.getConst(); + } 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_redlog_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_redlog_term(variables, term[i]); + } + cout << ")"; + break; + case kind::MINUS: + cout << "("; + translate_to_redlog_term(variables, term[0]); + cout << " - "; + translate_to_redlog_term(variables, term[1]); + cout << ")"; + break; + case kind::DIVISION: + cout << "("; + translate_to_redlog_term(variables, term[0]); + cout << " / "; + translate_to_redlog_term(variables, term[1]); + cout << ")"; + break; + case kind::UMINUS: + cout << "(-("; + translate_to_redlog_term(variables, term[0]); + cout << "))"; + break; + default: + assert(false); + break; + } + } +} + +void translate_to_redlog(const map& variables, const BoolExpr& assertion) { + bool first; + + unsigned n = assertion.getNumChildren(); + + if (n == 0) { + if (assertion.isConst()) { + if (assertion.getConst()) { + cout << "(1 > 0)"; + } else { + cout << "(1 < 0)"; + } + } else { + assert(false); + } + } else { + + std::string op; + bool binary = false; + bool theory = false; + + switch (assertion.getKind()) { + case kind::NOT: + cout << "(not "; + translate_to_redlog(variables, assertion[0]); + cout << ")"; + break; + case kind::OR: + first = true; + cout << "("; + for (unsigned i = 0; i < n; ++ i) { + if (!first) { + cout << " or "; + } + first = false; + translate_to_redlog(variables, assertion[i]); + } + cout << ")"; + break; + case kind::AND: + first = true; + cout << "("; + for (unsigned i = 0; i < n; ++ i) { + if (!first) { + cout << " and "; + } + first = false; + translate_to_redlog(variables, assertion[i]); + } + cout << ")"; + break; + case kind::IMPLIES: + cout << "("; + translate_to_redlog(variables, assertion[0]); + cout << " impl "; + translate_to_redlog(variables, assertion[1]); + cout << ")"; + break; + case kind::IFF: + cout << "("; + translate_to_redlog(variables, assertion[0]); + cout << " equiv "; + translate_to_redlog(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_redlog(variables, assertion[0]); + cout << " " << op << " "; + translate_to_redlog(variables, assertion[1]); + cout << ")"; + } + + if (theory) { + cout << "("; + translate_to_redlog_term(variables, assertion[0]); + cout << " " << op << " "; + translate_to_redlog_term(variables, assertion[1]); + cout << ")"; + } + } +} + +void translate_to_redlog( + string input, + string command, + const vector& info_tags, + const vector& info_data, + const std::map& variables, + const vector& assertions) +{ + bool first; + + // Dump out the information + cout << "load redlog;" << endl; + cout << "rlset ofsf;" << endl; + + // Dump the variables + + cout << "phi := ex({"; + first = true; + for (unsigned i = 0; i < variables.size(); ++ i) { + if (!first) { + cout << ","; + } + cout << " x" << i; + if (first) { + first = false; + } + } + cout << "},"; + + // The assertions + first = true; + for (unsigned i = 0; i < assertions.size(); ++ i) { + if (first == false) { + cout << " and "; + } + first = false; + translate_to_redlog(variables, assertions[i]); + + } + cout << ");" << endl; + + cout << "result := " << command << " phi;" << endl; + cout << "result;" << endl; + cout << "quit;" << endl; + +} + diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp index 819b1fc97..557199e75 100644 --- a/examples/simple_vc_cxx.cpp +++ b/examples/simple_vc_cxx.cpp @@ -37,16 +37,16 @@ int main() { Expr x = em.mkVar("x", integer); Expr y = em.mkVar("y", integer); - Expr zero = em.mkConst(Integer(0)); + Expr zero = em.mkConst(Rational(0)); Expr x_positive = em.mkExpr(kind::GT, x, zero); Expr y_positive = em.mkExpr(kind::GT, y, zero); - Expr two = em.mkConst(Integer(2)); + Expr two = em.mkConst(Rational(2)); Expr twox = em.mkExpr(kind::MULT, two, x); Expr twox_plus_y = em.mkExpr(kind::PLUS, twox, y); - Expr three = em.mkConst(Integer(3)); + Expr three = em.mkConst(Rational(3)); Expr twox_plus_y_geq_3 = em.mkExpr(kind::GEQ, twox_plus_y, three); BoolExpr formula =