Move the translator binary from src/main to examples, no longer built by default.

1 files changed, 176 insertions, 0 deletions

diff --git a/examples/translator.cpp b/examples/translator.cpp
new file mode 100644
index 000000000..67dce699d
--- /dev/null
+++ b/examples/translator.cpp
@@ -0,0 +1,176 @@
+/*********************                                                        */
+/*! \file translator.cpp
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief CVC4 translator
+ **
+ ** The CVC4 translator executable.  This program translates from one of
+ ** CVC4's input languages to one of its output languages.
+ **/
+
+#include <iostream>
+#include <fstream>
+#include <getopt.h>
+#include <cstring>
+#include "util/language.h"
+#include "expr/command.h"
+#include "expr/expr.h"
+#include "parser/parser_builder.h"
+#include "parser/parser.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::language;
+using namespace CVC4::parser;
+
+enum {
+  INPUT_LANG = 'L',
+  OUTPUT_LANG = 'O',
+  OUTPUT_FILE = 'o',
+  HELP = 'h'
+};/* enum */
+
+const struct option longopts[] = {
+  { "output-lang", required_argument, NULL, OUTPUT_LANG },
+  { "output-language", required_argument, NULL, OUTPUT_LANG },
+  { "lang", required_argument, NULL, INPUT_LANG },
+  { "language", required_argument, NULL, INPUT_LANG },
+  { "out", required_argument, NULL, OUTPUT_FILE },
+  { "help", no_argument, NULL, HELP },
+  { NULL, no_argument, NULL, 0 },
+};/* longopts */
+
+static void showHelp() {
+  cerr << "cvc4-translator translation tool" << endl
+       << "  --output-language | -O  set output language (default smt2)" << endl
+       << "  --input-language | -L   set input language (default auto)" << endl
+       << "  --out | -o              set output file (- for stdout)" << endl
+       << "  --help | -h             this help" << endl
+       << "Options and input filenames can be intermixed, and order is important." << endl
+       << "For instance, \"-O smt2 x -O cvc4 y\" reads file x in smt2 format and"
+       << "file y in cvc4 format and writes all output to stdout." << endl
+       << "Some canonicalization may occur." << endl
+       << "Comments and formatting are not preserved." << endl;
+}
+
+static void readFile(const char* filename, InputLanguage fromLang, OutputLanguage toLang, ostream* out) {
+  if(fromLang == input::LANG_AUTO) {
+    unsigned len = strlen(filename);
+    if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
+      fromLang = language::input::LANG_SMTLIB_V2;
+    } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
+      fromLang = language::input::LANG_SMTLIB_V1;
+    } else if(len >= 5 && !strcmp(".smt1", filename + len - 5)) {
+      fromLang = language::input::LANG_SMTLIB_V1;
+    } else if((len >= 2 && !strcmp(".p", filename + len - 2)) ||
+              (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
+      fromLang = language::input::LANG_TPTP;
+    } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) ||
+              ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
+      fromLang = language::input::LANG_CVC4;
+    } else {
+      throw Exception("cannot determine input language to use for `" + string(filename) + "'");
+    }
+  }
+
+  if(toLang == output::LANG_AUTO) {
+    toLang = toOutputLanguage(fromLang);
+  }
+
+  *out << Expr::setlanguage(toLang);
+
+  Options opts;
+  opts.set(options::inputLanguage, fromLang);
+  ExprManager exprMgr(opts);
+  ParserBuilder parserBuilder(&exprMgr, filename, opts);
+  if(!strcmp(filename, "-")) {
+    parserBuilder.withFilename("<stdin>");
+    parserBuilder.withLineBufferedStreamInput(cin);
+  }
+  Parser *parser = parserBuilder.build();
+  while(Command* cmd = parser->nextCommand()) {
+    *out << cmd << endl;
+    if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
+      delete cmd;
+      break;
+    }
+    delete cmd;
+  }
+  *out << flush;
+  delete parser;
+}
+
+/**
+ * Translate from an input language to an output language.
+ */
+int main(int argc, char* argv[]) {
+  ostream* out = &cout;
+  InputLanguage fromLang = input::LANG_AUTO;
+  OutputLanguage toLang = output::LANG_SMTLIB_V2;
+  size_t files = 0;
+
+  try {
+    int c;
+    while((c = getopt_long(argc, argv, "-L:O:o:h", longopts, NULL)) != -1) {
+      switch(c) {
+      case 1:
+        ++files;
+        readFile(optarg, (!strcmp(optarg, "-") && fromLang == input::LANG_AUTO) ? input::LANG_CVC4 : fromLang, toLang, out);
+        break;
+      case INPUT_LANG:
+        if(!strcmp(optarg, "help")) {
+          Options::printLanguageHelp(cerr);
+          exit(1);
+        }
+        fromLang = toInputLanguage(optarg);
+        break;
+      case OUTPUT_LANG:
+        if(!strcmp(optarg, "help")) {
+          Options::printLanguageHelp(cerr);
+          exit(1);
+        }
+        toLang = toOutputLanguage(optarg);
+        break;
+      case OUTPUT_FILE:
+        out->flush();
+        if(out != &cout) {
+          ((ofstream*)out)->close();
+          delete out;
+        }
+        if(strcmp(optarg, "-")) {
+          out = new ofstream(optarg);
+        } else {
+          out = &cout;
+        }
+        break;
+      case 'h':
+        showHelp();
+        exit(0);
+      case '?':
+        showHelp();
+        exit(1);
+      default:
+        cerr << "internal error.  translator failed ("
+             << char(c) << "," << c << ")." << endl;
+        exit(1);
+      }
+    }
+
+    if(files == 0) {
+      readFile("-", fromLang == input::LANG_AUTO ? input::LANG_CVC4 : fromLang, toLang, out);
+      exit(0);
+    }
+  } catch(Exception& e) {
+    cerr << e << endl;
+    exit(1);
+  }
+
+  return 0;
+}