diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-11-18 22:02:11 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-11-18 22:02:11 +0000 |
commit | 394791604a62e19763a8a45328bc5177d91fabf9 (patch) | |
tree | 29027c84c0285da33bac6c5d1366635b9e4db1bc /src/main | |
parent | 477e97cd81afe4b86eea47e9abe6311fc22299fc (diff) |
work on exprs, driver, util
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/Makefile.am | 7 | ||||
-rw-r--r-- | src/main/about.h | 17 | ||||
-rw-r--r-- | src/main/getopt.cpp | 128 | ||||
-rw-r--r-- | src/main/main.cpp | 68 | ||||
-rw-r--r-- | src/main/main.h | 26 | ||||
-rw-r--r-- | src/main/usage.h | 29 | ||||
-rw-r--r-- | src/main/util.cpp | 44 |
7 files changed, 317 insertions, 2 deletions
diff --git a/src/main/Makefile.am b/src/main/Makefile.am index e857c8245..3b2ccb05a 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -1,6 +1,9 @@ INCLUDES = -I@srcdir@/../include -I@srcdir@/.. AM_CXXFLAGS = -Wall -bin_BINARIES = cvc4 +bin_PROGRAMS = cvc4 -cvc4_SOURCES = +cvc4_SOURCES = \ + main.cpp \ + getopt.cpp \ + util.cpp diff --git a/src/main/about.h b/src/main/about.h new file mode 100644 index 000000000..f582debf0 --- /dev/null +++ b/src/main/about.h @@ -0,0 +1,17 @@ +#ifndef __CVC4_ABOUT_H +#define __CVC4_ABOUT_H + +namespace CVC4 { +namespace Main { + +const char about[] = "\ +This is a pre-release of CVC4.\n\ +Copyright (C) 2009 The ACSys Group\n\ + Courant Institute of Mathematical Sciences,\n\ + New York University\n\ +"; + +}/* CVC4::Main namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4_MAIN_H */ diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp new file mode 100644 index 000000000..5f32ccd77 --- /dev/null +++ b/src/main/getopt.cpp @@ -0,0 +1,128 @@ +#include <cstdio> +#include <cstdlib> +#include <new> +#include <unistd.h> +#include <string.h> +#include <stdint.h> +#include <time.h> + +#include <getopt.h> + +#include "config.h" +#include "main.h" +#include "util/exception.h" +#include "usage.h" +#include "about.h" + +using namespace std; +using namespace CVC4; + +namespace CVC4 { +namespace Main { + +static const char lang_help[] = "\ +Languages currently supported to the -L / --lang option:\n\ + auto attempt to automatically determine the input language\n\ + pl | cvc4 CVC4 presentation language\n\ + smt | smtlib SMT-LIB format\n\ +"; + +enum Language { + AUTO = 0, + PL, + SMTLIB, +};/* enum Language */ + +enum OptionValue { + SMTCOMP = 256, /* no clash with char options */ + STATS +};/* enum OptionValue */ + +static struct option cmdlineOptions[] = { + // name, has_arg, *flag, val + { "help" , no_argument , NULL, 'h' }, + { "version", no_argument , NULL, 'V' }, + { "verbose", no_argument , NULL, 'v' }, + { "quiet" , no_argument , NULL, 'q' }, + { "lang" , required_argument, NULL, 'L' }, + { "debug" , required_argument, NULL, 'd' }, + { "smtcomp", no_argument , NULL, SMTCOMP }, + { "stats" , no_argument , NULL, STATS } +}; + +int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(Exception*) { + const char *progName = argv[0]; + int c; + + // find the base name of the program + const char *x = strrchr(progName, '/'); + if(x != NULL) + progName = x + 1; + opts->binary_name = string(progName); + + while((c = getopt_long(argc, argv, "+:hVvL:", cmdlineOptions, NULL)) != -1) { + switch(c) { + + case 'h': + printf(usage, opts->binary_name.c_str()); + exit(1); + break; + + case 'V': + fputs(about, stdout); + break; + + case 'v': + ++opts->verbosity; + break; + + case 'q': + --opts->verbosity; + break; + + case 'L': + if(!strcmp(argv[optind], "cvc4") || !strcmp(argv[optind], "pl")) { + opts->lang = PL; + break; + } else if(!strcmp(argv[optind], "smtlib") || !strcmp(argv[optind], "smt")) { + opts->lang = SMTLIB; + break; + } else if(!strcmp(argv[optind], "auto")) { + opts->lang = AUTO; + break; + } + + if(strcmp(argv[optind], "help")) + throw new OptionException(string("unknown language for --lang: `") + argv[optind] + "'. Try --lang help."); + + fputs(lang_help, stdout); + exit(1); + + case STATS: + opts->statistics = true; + break; + + case SMTCOMP: + // silences CVC4 (except "sat" or "unsat" or "unknown", forces smtlib input) + opts->smtcomp_mode = true; + opts->verbosity = -1; + opts->lang = SMTLIB; + break; + + case '?': + throw new OptionException(string("can't understand option: `") + argv[optind] + "'"); + + case ':': + throw new OptionException(string("option `") + argv[optind] + "' missing its required argument"); + + default: + throw new OptionException(string("can't understand option: `") + argv[optind] + "'"); + } + + } + + return optind; +} + +}/* CVC4::Main namespace */ +}/* CVC4 namespace */ diff --git a/src/main/main.cpp b/src/main/main.cpp new file mode 100644 index 000000000..4850d475f --- /dev/null +++ b/src/main/main.cpp @@ -0,0 +1,68 @@ +#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" + +using namespace std; +using namespace CVC4; +using namespace CVC4::Main; + +int main(int argc, char *argv[]) { + struct Options opts; + + try { + cvc4_init(); + + int firstArgIndex = parseOptions(argc, argv, &opts); + + FILE *infile; + + if(firstArgIndex >= argc) { + infile = stdin; + } else if(argc > firstArgIndex + 1) { + throw new Exception("Too many input files specified."); + } else { + infile = fopen(argv[firstArgIndex], "r"); + if(!infile) { + throw new Exception(string("Could not open input file `") + argv[firstArgIndex] + "' for reading: " + strerror(errno)); + exit(1); + } + } + } 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()); + exit(1); + } catch(CVC4::Exception* e) { + if(opts.smtcomp_mode) { + printf("unknown"); + fflush(stdout); + } + fprintf(stderr, "CVC4 Error:\n%s\n", e->toString().c_str()); + exit(1); + } catch(bad_alloc) { + if(opts.smtcomp_mode) { + printf("unknown"); + fflush(stdout); + } + fprintf(stderr, "CVC4 ran out of memory.\n"); + exit(1); + } catch(...) { + fprintf(stderr, "CVC4 threw an exception of unknown type.\n"); + exit(1); + } + + return 0; +} diff --git a/src/main/main.h b/src/main/main.h new file mode 100644 index 000000000..4101f4fe4 --- /dev/null +++ b/src/main/main.h @@ -0,0 +1,26 @@ +#include <iostream> +#include <exception> +#include <string> + +#include "config.h" +#include "util/exception.h" +#include "util/options.h" + +#ifndef __CVC4_MAIN_H +#define __CVC4_MAIN_H + +namespace CVC4 { +namespace Main { + +class OptionException : public CVC4::Exception { +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*); +void cvc4_init() throw(); + +}/* CVC4::Main namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4_MAIN_H */ diff --git a/src/main/usage.h b/src/main/usage.h new file mode 100644 index 000000000..971ba7640 --- /dev/null +++ b/src/main/usage.h @@ -0,0 +1,29 @@ +#ifndef __CVC4_USAGE_H +#define __CVC4_USAGE_H + +namespace CVC4 { +namespace Main { + +// no more % chars in here without being escaped; it's used as a +// printf() format string +const char usage[] = "\ +usage: %s [options] [input-file]\n\ +\n\ +Without an input file, or with `-', CVC4 reads from standard input.\n\ +\n\ +CVC4 options:\n\ + --lang | -L set input language (--lang help gives a list;\n\ + `auto' is default)\n\ + --version | -V identify this CVC4 binary\n\ + --help | -h this command line reference\n\ + --verbose | -v increase verbosity (repeatable)\n\ + --quiet | -q decrease verbosity (repeatable)\n\ + --debug | -d debugging for something (e.g. --debug arith)\n\ + --smtcomp competition mode (very quiet)\n\ + --stats give statistics on exit\n\ +"; + +}/* CVC4::Main namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4_USAGE_H */ diff --git a/src/main/util.cpp b/src/main/util.cpp new file mode 100644 index 000000000..da4d4b0c0 --- /dev/null +++ b/src/main/util.cpp @@ -0,0 +1,44 @@ +#include <string> +#include <cstdio> +#include <cstdlib> +#include <cerrno> +#include <string.h> +#include <signal.h> + +#include "util/exception.h" +#include "config.h" + +using CVC4::Exception; +using namespace std; + +namespace CVC4 { +namespace Main { + +void sigint_handler(int sig, siginfo_t* info, void*) { + fprintf(stderr, "CVC4 interrupted by user.\n"); + exit(info->si_signo + 128); +} + +void segv_handler(int sig, siginfo_t* info, void*) { + fprintf(stderr, "CVC4 suffered a segfault.\n"); + exit(info->si_signo + 128); +} + +void cvc4_init() throw() { + struct sigaction act1; + act1.sa_sigaction = sigint_handler; + act1.sa_flags = SA_SIGINFO; + sigemptyset(&act1.sa_mask); + if(sigaction(SIGINT, &act1, NULL)) + throw new Exception(string("sigaction(SIGINT) failure: ") + strerror(errno)); + + struct sigaction act2; + act2.sa_sigaction = segv_handler; + act2.sa_flags = SA_SIGINFO; + sigemptyset(&act2.sa_mask); + if(sigaction(SIGSEGV, &act2, NULL)) + throw new Exception(string("sigaction(SIGSEGV) failure: ") + strerror(errno)); +} + +}/* CVC4::Main namespace */ +}/* CVC4 namespace */ |