work on exprs, driver, util

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 */