From: Morgan Deters Date: Sat, 15 Mar 2014 21:41:27 +0000 (-0400) Subject: Move the translator binary from src/main to examples, no longer built by default. X-Git-Tag: cvc5-1.0.0~7008 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=edd400baac8b4055b9e539a0324e09e07abed02c;p=cvc5.git Move the translator binary from src/main to examples, no longer built by default. --- 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 +#include +#include +#include +#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(""); + parserBuilder.withLineBufferedStreamInput(cin); + } + Parser *parser = parserBuilder.build(); + while(Command* cmd = parser->nextCommand()) { + *out << cmd << endl; + if(dynamic_cast(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; +} diff --git a/src/main/Makefile.am b/src/main/Makefile.am index 042b7cf45..7e87fa59a 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -3,7 +3,7 @@ AM_CPPFLAGS = \ -I@builddir@/.. $(ANTLR_INCLUDES) -I@srcdir@/../include -I@srcdir@/.. AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -bin_PROGRAMS = cvc4 cvc4-translator +bin_PROGRAMS = cvc4 noinst_LIBRARIES = libmain.a @@ -62,12 +62,6 @@ cvc4_LDADD += \ @builddir@/../lib/libreplacements.la endif -cvc4_translator_SOURCES = \ - translator.cpp -cvc4_translator_LDADD = \ - @builddir@/../parser/libcvc4parser.la \ - @builddir@/../libcvc4.la - BUILT_SOURCES = \ $(TOKENS_FILES) diff --git a/src/main/translator.cpp b/src/main/translator.cpp deleted file mode 100644 index 7cc90bbd1..000000000 --- a/src/main/translator.cpp +++ /dev/null @@ -1,175 +0,0 @@ -/********************* */ -/*! \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 Main driver for CVC4 translator executable - ** - ** Main driver for CVC4 translator executable. - **/ - -#include -#include -#include -#include -#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(""); - parserBuilder.withLineBufferedStreamInput(cin); - } - Parser *parser = parserBuilder.build(); - while(Command* cmd = parser->nextCommand()) { - *out << cmd << endl; - if(dynamic_cast(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; -}