* 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

9 files changed, 1565 insertions, 0 deletions

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 <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;
+}
+
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 <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;
+  }
+}
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 <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;
+}
+
+
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 <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;
+  }
+
+}
+
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;
+}
+
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 <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;
+}
+
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 <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;
+
+}
+