* adding as examples the programs i used to translate nonlinear smt2 problems to other formats
+SUBDIRS = nra-translate .
+
AM_CPPFLAGS = \
-I@srcdir@/../src/include -I@srcdir@/../src -I@builddir@/../src $(ANTLR_INCLUDES)
AM_CXXFLAGS = -Wall
--- /dev/null
+topdir = ../..
+srcdir = examples/nra-translate
+
+include $(topdir)/Makefile.subdir
--- /dev/null
+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
--- /dev/null
+#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"
+#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<BoolExpr> assertions;
+
+ Command* cmd;
+ while ((cmd = parser->nextCommand())) {
+
+ AssertCommand* assert = dynamic_cast<AssertCommand*>(cmd);
+ if (assert) {
+ Expr normalized = engine.simplify(assert->getExpr());
+ cout << "(assert " << normalized << ")" << endl;
+ delete cmd;
+ continue;
+ }
+
+ CheckSatCommand* checksat = dynamic_cast<CheckSatCommand*>(cmd);
+ if (checksat) {
+ delete cmd;
+ continue;
+ }
+
+ cout << *cmd << endl;
+ delete cmd;
+ }
+
+ cout << "(check-sat)" << endl;
+
+ // Get rid of the parser
+ delete parser;
+}
+
--- /dev/null
+#include <string>
+#include <iostream>
+#include <typeinfo>
+#include <cassert>
+#include <vector>
+
+
+#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<string> 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) {
+ variables.push_back(declare->getSymbol());
+ delete cmd;
+ continue;
+ }
+
+ AssertCommand* assert = dynamic_cast<AssertCommand*>(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;
+ }
+}
--- /dev/null
+#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"
+#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<Expr, unsigned> variables;
+ vector<string> info_tags;
+ vector<string> info_data;
+ vector<BoolExpr> assertions;
+
+ Command* cmd;
+ while ((cmd = parser->nextCommand())) {
+
+ DeclareFunctionCommand* declare = dynamic_cast<DeclareFunctionCommand*>(cmd);
+ if (declare) {
+ cout << "[-10000, 10000] " << declare->getSymbol() << ";" << endl;
+ }
+
+ AssertCommand* assert = dynamic_cast<AssertCommand*>(cmd);
+ if (assert) {
+ cout << assert->getExpr() << ";" << endl;
+ }
+
+ delete cmd;
+ }
+
+ // Get rid of the parser
+ delete parser;
+}
+
+
--- /dev/null
+#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"
+#include "smt/smt_engine.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::parser;
+
+void translate_to_isat(
+ 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();
+
+ // Smt manager for simplifications
+ SmtEngine engine(&exprManager);
+
+ // 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(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<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_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<Expr, unsigned>& variables, const BoolExpr& assertion) {
+ bool first;
+
+ unsigned n = assertion.getNumChildren();
+
+ if (n == 0) {
+ if (assertion.isConst()) {
+ if (assertion.getConst<bool>()) {
+ 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<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 << 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;
+ }
+
+}
+
--- /dev/null
+#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;
+}
+
--- /dev/null
+#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_qepcad(
+ 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[])
+{
+ std::map<Expr, unsigned> 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<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_qepcad(input, info_tags, info_data, variables, assertions);
+
+ // Get rid of the parser
+ delete parser;
+}
+
+void translate_to_qepcad_term(const std::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_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<Expr, unsigned>& 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<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;
+
+ // 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;
+}
+
--- /dev/null
+#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"
+#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<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]);
+ // 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<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(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<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_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<Expr, unsigned>& variables, const BoolExpr& assertion) {
+ bool first;
+
+ unsigned n = assertion.getNumChildren();
+
+ if (n == 0) {
+ if (assertion.isConst()) {
+ if (assertion.getConst<bool>()) {
+ 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<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 << "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;
+
+}
+
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 =
projects / cvc5.git / commitdiff