diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2009-12-06 02:21:46 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2009-12-06 02:21:46 +0000 |
commit | c16be5841e613818d5764e4de99e4694a0703685 (patch) | |
tree | 5bf7c07a8f7200c2830d50f5dd83ecbb4f02444d /src/main | |
parent | 200f36785acf7aac3e7e230795ea7ffdb6b1ed64 (diff) |
Big chunk of changes:
* Fixed bugs in option parsing
* Simplified the main.cpp significantly (more c++ like)
* Added the null kind, expr value, and expression, with the default constructor public
* Simplified commands, we need to discuss this in the meeting (what to do with command results?)
* Removed all the lex/yacc files
* Symbol table is now a templated class, as we will have tables for variables, predicates and functions
* The ANTLR parsing infrastructure/makefiles is all in. SMT lib Boolean benchmarks should parse + giving nice error such as
Parse Error: /home/dejan/eclipse-cxx/smtlib-parser/test/test4.smt:3:16: Undeclared variable p
Parse Error: /home/dejan/eclipse-cxx/smtlib-parser/test/test2.smt:2:11: unexpected token: sa
Didn't add any unit tests as the unit testing doesn't work with the updated build system -- it doesn't know how to create directories in the corresponding build directory.
TODO:
* add the PL grammar and unit test when the testing becomes available
* with this build setup my eclipse debugger doesn't work. Might have something to do with the visibility of symbols?
* i'm getting g++ depracated warnings regarding the hash_map from the symbol table, need to figure out how to use it in a standard manner. the new <unordered_map> header is for C++0x, and the <ext/hash_map> is getting deprecation warningns... weird.
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/getopt.cpp | 28 | ||||
-rw-r--r-- | src/main/main.cpp | 115 | ||||
-rw-r--r-- | src/main/main.h | 2 |
3 files changed, 69 insertions, 76 deletions
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index f60dd6e24..2daead11b 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -25,11 +25,9 @@ #include "util/exception.h" #include "usage.h" #include "about.h" -#include "parser/language.h" using namespace std; using namespace CVC4; -using namespace CVC4::parser; namespace CVC4 { namespace main { @@ -58,7 +56,7 @@ static struct option cmdlineOptions[] = { { "stats" , no_argument , NULL, STATS } }; -int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(Exception*) { +int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionException) { const char *progName = argv[0]; int c; @@ -89,19 +87,19 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(Exception*) { break; case 'L': - if(!strcmp(argv[optind], "cvc4") || !strcmp(argv[optind], "pl")) { - opts->lang = PL; + if(!strcmp(optarg, "cvc4") || !strcmp(optarg, "pl")) { + opts->lang = Options::LANG_CVC4; break; - } else if(!strcmp(argv[optind], "smtlib") || !strcmp(argv[optind], "smt")) { - opts->lang = SMTLIB; + } else if(!strcmp(optarg, "smtlib") || !strcmp(optarg, "smt")) { + opts->lang = Options::LANG_SMTLIB; break; - } else if(!strcmp(argv[optind], "auto")) { - opts->lang = AUTO; + } else if(!strcmp(optarg, "auto")) { + opts->lang = Options::LANG_AUTO; break; } - if(strcmp(argv[optind], "help")) - throw new OptionException(string("unknown language for --lang: `") + argv[optind] + "'. Try --lang help."); + if(strcmp(optarg, "help")) + throw OptionException(string("unknown language for --lang: `") + argv[optind] + "'. Try --lang help."); fputs(lang_help, stdout); exit(1); @@ -114,17 +112,17 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(Exception*) { // silences CVC4 (except "sat" or "unsat" or "unknown", forces smtlib input) opts->smtcomp_mode = true; opts->verbosity = -1; - opts->lang = SMTLIB; + opts->lang = Options::LANG_SMTLIB; break; case '?': - throw new OptionException(string("can't understand option: `") + argv[optind] + "'"); + throw OptionException(string("can't understand option: `") + argv[optind] + "'"); case ':': - throw new OptionException(string("option `") + argv[optind] + "' missing its required argument"); + throw OptionException(string("option `") + argv[optind] + "' missing its required argument"); default: - throw new OptionException(string("can't understand option: `") + argv[optind] + "'"); + throw OptionException(string("can't understand option: `") + argv[optind] + "'"); } } diff --git a/src/main/main.cpp b/src/main/main.cpp index 323a989c8..b7833e3ca 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -12,25 +12,15 @@ #include <iostream> #include <fstream> -#include <cstdio> #include <cstdlib> -#include <cerrno> #include <new> -#include <exception> -#include <unistd.h> -#include <string.h> -#include <stdint.h> -#include <time.h> #include "config.h" #include "main.h" #include "usage.h" #include "parser/parser.h" #include "expr/expr_manager.h" -#include "expr/expr.h" -#include "expr/kind.h" #include "smt/smt_engine.h" -#include "parser/language.h" #include "util/command.h" using namespace std; @@ -39,74 +29,79 @@ using namespace CVC4::parser; using namespace CVC4::main; int main(int argc, char *argv[]) { - struct Options opts; + + struct Options options; try { + + // Initialize the signal handlers cvc4_init(); - int firstArgIndex = parseOptions(argc, argv, &opts); + // Parse the options + int firstArgIndex = parseOptions(argc, argv, &options); - istream *in; - ifstream infile; - Language lang = PL; + // If in competition mode, we flush the stdout immediately + if(options.smtcomp_mode) + cout << unitbuf; - if(firstArgIndex >= argc) { - in = &cin; - } else if(argc > firstArgIndex + 1) { + // We only accept one input file + if(argc > firstArgIndex + 1) throw new Exception("Too many input files specified."); - } else { - in = &infile; - if(strlen(argv[firstArgIndex]) >= 4 && - !strcmp(argv[firstArgIndex] + strlen(argv[firstArgIndex]) - 4, ".smt")) - lang = SMTLIB; - infile.open(argv[firstArgIndex], ifstream::in); - - if(!infile) { - throw new Exception(string("Could not open input file `") + - argv[firstArgIndex] + "' for reading: " + - strerror(errno)); - } + + // Create the expression manager + ExprManager exprMgr; + // Create the SmtEngine + SmtEngine smt(&exprMgr, &options); + + // If no file supplied we read from standard input + bool inputFromStdin = firstArgIndex >= argc; + + // Create the parser + Parser* parser; + switch(options.lang) { + case Options::LANG_SMTLIB: + if(inputFromStdin) + parser = new SmtParser(&exprMgr, cin); + else + parser = new SmtParser(&exprMgr, argv[firstArgIndex]); + break; + default: + cerr << "Language" << options.lang << "not supported yet." << endl; + abort(); } - ExprManager *exprMgr = new ExprManager; - SmtEngine smt(exprMgr, &opts); - Parser parser(&smt, exprMgr, lang, *in, &opts); - while(!parser.done()) { - Command *cmd = parser.parseNextCommand(opts.verbosity > 1); - if(opts.verbosity > 0) { - cout << "invoking cmd: "; - cout << cmd << endl; - } + // Parse the and execute commands until we are done + while(!parser->done()) { + // Parse the next command + Command *cmd = parser->parseNextCommand(); if(cmd) { - if(opts.verbosity >= 0) - cout << cmd->invoke(&smt) << endl; + if(options.verbosity > 0) + cout << "Invoking: " << *cmd << endl; + cmd->invoke(&smt); delete cmd; } } - } catch(CVC4::main::OptionException* e) { - if(opts.smtcomp_mode) { - printf("unknown"); - fflush(stdout); - } - fprintf(stderr, "CVC4 Error:\n%s\n\n", e->toString().c_str()); - printf(usage, opts.binary_name.c_str()); + + // Remove the parser + delete parser; + } catch(OptionException& e) { + if(options.smtcomp_mode) + cout << "unknown" << endl; + cerr << "CVC4 Error:" << endl << e << endl; + printf(usage, options.binary_name.c_str()); abort(); - } catch(CVC4::Exception* e) { - if(opts.smtcomp_mode) { - printf("unknown"); - fflush(stdout); - } - fprintf(stderr, "CVC4 Error:\n%s\n", e->toString().c_str()); + } catch(CVC4::Exception& e) { + if(options.smtcomp_mode) + cout << "unknown" << endl; + cerr << "CVC4 Error:" << endl << e << endl; abort(); } catch(bad_alloc) { - if(opts.smtcomp_mode) { - printf("unknown"); - fflush(stdout); - } - fprintf(stderr, "CVC4 ran out of memory.\n"); + if(options.smtcomp_mode) + cout << "unknown" << endl; + cerr << "CVC4 ran out of memory." << endl; abort(); } catch(...) { - fprintf(stderr, "CVC4 threw an exception of unknown type.\n"); + cerr << "CVC4 threw an exception of unknown type." << endl; abort(); } diff --git a/src/main/main.h b/src/main/main.h index 5e0c68053..60817d976 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -28,7 +28,7 @@ public: OptionException(const std::string& s) throw() : CVC4::Exception("Error in option parsing: " + s) {} };/* class OptionException */ -int parseOptions(int argc, char** argv, CVC4::Options*) throw(CVC4::Exception*); +int parseOptions(int argc, char** argv, CVC4::Options*) throw(OptionException); void cvc4_init() throw(); }/* CVC4::main namespace */ |