diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-03-15 17:41:27 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-03-19 10:38:05 -0400 |
commit | edd400baac8b4055b9e539a0324e09e07abed02c (patch) | |
tree | e06f2ebcecc3914086184adbc8f682a19003266e /examples/translator.cpp | |
parent | 35fec0bea609697cfa5509e9af9cf2ff356b26ea (diff) |
Move the translator binary from src/main to examples, no longer built by default.
Diffstat (limited to 'examples/translator.cpp')
-rw-r--r-- | examples/translator.cpp | 176 |
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; +} |