examples/nra-translate/normalize.cpp

   1 #include <string>
   2 #include <iostream>
   3 #include <typeinfo>
   4 #include <cassert>
   5 #include <vector>
   6 #include <map>
   7
   8
   9 #include "options/options.h"
  10 #include "expr/expr.h"
  11 #include "expr/command.h"
  12 #include "parser/parser.h"
  13 #include "parser/parser_builder.h"
  14 #include "smt/smt_engine.h"
  15
  16 using namespace std;
  17 using namespace CVC4;
  18 using namespace CVC4::parser;
  19 using namespace CVC4::options;
  20 using namespace CVC4::theory;
  21
  22 int main(int argc, char* argv[])
  23 {
  24
  25   // Get the filename
  26   string input(argv[1]);
  27
  28   // Create the expression manager
  29   Options options;
  30   options.set(inputLanguage, language::input::LANG_SMTLIB_V2);
  31   ExprManager exprManager(options);
  32
  33   cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2) << Expr::setdepth(-1);
  34
  35   // Create the parser
  36   ParserBuilder parserBuilder(&exprManager, input, options);
  37   Parser* parser = parserBuilder.build();
  38
  39   // Smt manager for simplifications
  40   SmtEngine engine(&exprManager);
  41
  42   // Variables and assertions
  43   vector<BoolExpr> assertions;
  44
  45   Command* cmd;
  46   while ((cmd = parser->nextCommand())) {
  47
  48     AssertCommand* assert = dynamic_cast<AssertCommand*>(cmd);
  49     if (assert) {
  50       Expr normalized = engine.simplify(assert->getExpr());
  51       cout << "(assert " << normalized << ")" << endl;
  52       delete cmd;
  53       continue;
  54     }
  55
  56     CheckSatCommand* checksat = dynamic_cast<CheckSatCommand*>(cmd);
  57     if (checksat) {
  58       delete cmd;
  59       continue;
  60     }
  61
  62     cout << *cmd << endl;
  63     delete cmd;
  64   }
  65
  66   cout << "(check-sat)" << endl;
  67
  68   // Get rid of the parser
  69   delete parser;
  70 }
  71