work on exprs, driver, util

20 files changed, 518 insertions, 47 deletions

diff --git a/configure.ac b/configure.ac
index 58fcdfac3..77c03ef2c 100644
--- a/configure.ac
+++ b/configure.ac
@@ -12,6 +12,25 @@ LT_INIT
 
 AC_LIBTOOL_WIN32_DLL
 
+# Features requested by the user
+AC_MSG_CHECKING([whether to do a debug build of CVC4])
+AC_ARG_ENABLE([debug],      [AS_HELP_STRING([--enable-debug]      ,[do a debug build of CVC4])])
+if test -z "${enable_debug+set}"; then
+  enable_debug=no
+fi
+AC_MSG_RESULT([$enable_debug])
+
+AC_MSG_CHECKING([whether to include assertions in build])
+AC_ARG_ENABLE([assertions], [AS_HELP_STRING([--disable-assertions],[turn off assertions in build])])
+if test -z "${enable_assertions+set}"; then
+  enable_assertions=yes
+fi
+AC_MSG_RESULT([$enable_assertions])
+
+if test "$enable_assertions" = no -a "$enable_debug" = yes; then
+  AC_MSG_FAILURE([when debugging is on, so must assertions be.])
+fi
+
 # Checks for programs.
 AC_PROG_CC
 AC_PROG_CXX
@@ -20,15 +39,16 @@ AC_PROG_LIBTOOL
 AM_PROG_LEX
 AC_PROG_YACC
 
-AC_CHECK_PROG(DOXYGEN, doxygen, doxygen,)
-if test "$DOXYGEN" = ''; then
-  echo 'WARNING: documentation targets require doxygen.  Set your PATH appropriately or set DOXYGEN to point to a valid doxygen binary.'
+AC_CHECK_PROG(DOXYGEN, doxygen, doxygen, [])
+if test -z "$DOXYGEN"; then
+  AC_MSG_WARN([documentation targets require doxygen.  Set your PATH appropriately or set DOXYGEN to point to a valid doxygen binary.])
 fi
 
 # Checks for libraries.
 AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP not found, see http://gmplib.org/])])
 
 # Checks for header files.
+AC_CHECK_HEADERS([getopt.h unistd.h])
 
 # Checks for typedefs, structures, and compiler characteristics.
 AC_HEADER_STDBOOL
@@ -39,6 +59,17 @@ AC_TYPE_SIZE_T
 
 # Checks for library functions.
 
+# Some definitions for config.h
+if test "$enable_debug" = yes; then
+  AC_DEFINE([CVC4_DEBUG], [], [Whether or not to include debugging code.])
+fi
+
+if test "$enable_assertions" = yes; then
+  AC_DEFINE([CVC4_ASSERTIONS], [], [Whether or not assertions are enabled.])
+fi
+
+# Prepare configure output
+
 AC_CONFIG_FILES([
   Makefile
   contrib/Makefile
@@ -54,4 +85,23 @@ AC_CONFIG_FILES([
   src/parser/Makefile
   src/theory/Makefile
 ])
+
 AC_OUTPUT
+
+# Final information to the user
+debug=debug
+if test "$enable_debug" = no; then
+  debug=non-debug
+fi
+withassertions=with
+if test "$enable_assertions" = no; then
+  withassertions=without
+fi
+
+cat <<EOF
+
+CVC4 $VERSION will be built as a $debug build $withassertions assertions.
+
+Now just type make, followed by make check or make install, as you like.
+
+EOF
diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl
index 96728a1d8..74030e810 100755
--- a/contrib/update-copyright.pl
+++ b/contrib/update-copyright.pl
@@ -4,6 +4,11 @@
 # source files to match a template (inline, below).  For files with no
 # top comment, it adds a fresh one.
 #
+# usage: contrib/update-copyright.pl [dirs...]
+# if dirs... are unspecified, the script scans its own parent directory's
+# "src" directory.  Since it lives in contrib/ in the CVC4 source tree,
+# that means src/ in the CVC4 source tree.
+#
 # It ignores any file/directory not starting with [a-zA-Z]
 # (so, this includes . and .., vi swaps, .svn meta-info,
 # .deps, etc.)
@@ -27,13 +32,15 @@ my $years = '2009';
 use strict;
 use Fcntl ':mode';
 
-my $dir = $0;
-$dir =~ s,/[^/]+/*$,,;
+my @searchdirs = ();
+if($#ARGV == -1) {
+  my $dir = $0;
+  $dir =~ s,/[^/]+/*$,,;
 
-(chdir($dir."/..") && -f "src/include/expr.h") || die "can't find top-level source directory for CVC4";
-my $pwd = `pwd`; chomp $pwd;
+  (chdir($dir."/..") && -f "src/include/cvc4_expr.h") || die "can't find top-level source directory for CVC4";
+  my $pwd = `pwd`; chomp $pwd;
 
-print <<EOF;
+  print <<EOF;
 Warning: this script is dangerous.  It will overwrite the header comments in your
 source files to match the template in the script, attempting to retain file-specific
 comments, but this isn't guaranteed.  You should run this in an svn working directory
@@ -45,15 +52,21 @@ The directory to search for and change sources is:
 Continue? y or n:
 EOF
 
-$_ = <STDIN>; chomp;
-die 'aborting operation' if !( $_ eq 'y' || $_ eq 'yes' || $_ eq 'Y' || $_ eq 'YES' );
+  $_ = <STDIN>; chomp;
+  die 'aborting operation' if !( $_ eq 'y' || $_ eq 'yes' || $_ eq 'Y' || $_ eq 'YES' );
+
+  $searchdirs[0] = 'src';
+} else {
+  @searchdirs = @ARGV;
+}
 
 print "Updating sources...\n";
 
-recurse('src');
+recurse(shift @searchdirs) while $#searchdirs >= 0;
 
 sub recurse {
   my ($srcdir) = @_;
+  print "in dir $srcdir\n";
   opendir(my $DIR, $srcdir);
   while(my $file = readdir $DIR) {
     next if !($file =~ /^[a-zA-Z]/);
diff --git a/src/expr/attr_type.h b/src/expr/attr_type.h
index d76bd742d..d24385f8e 100644
--- a/src/expr/attr_type.h
+++ b/src/expr/attr_type.h
@@ -12,7 +12,7 @@
 #ifndef __CVC4_ATTR_TYPE_H
 #define __CVC4_ATTR_TYPE_H
 
-#include "core/expr_attribute.h"
+#include "expr_attribute.h"
 
 namespace CVC4 {
 
diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
index 5e422f349..b6484ef25 100644
--- a/src/expr/expr.cpp
+++ b/src/expr/expr.cpp
@@ -11,8 +11,8 @@
  **/
 
 #include "cvc4_expr.h"
-#include "core/expr_value.h"
-#include "core/expr_builder.h"
+#include "expr_value.h"
+#include "expr_builder.h"
 
 namespace CVC4 {
 
@@ -44,11 +44,7 @@ Expr& Expr::operator=(const Expr& e) {
   return *this;
 }
 
-ExprValue* Expr::operator->() {
-  return d_ev;
-}
-
-const ExprValue* Expr::operator->() const {
+ExprValue* Expr::operator->() const {
   return d_ev;
 }
 
diff --git a/src/expr/expr_attribute.h b/src/expr/expr_attribute.h
index b00882478..3525a8370 100644
--- a/src/expr/expr_attribute.h
+++ b/src/expr/expr_attribute.h
@@ -15,9 +15,9 @@
 // TODO WARNING this file needs work !
 
 #include <stdint.h>
-#include "core/config.h"
-#include "core/context.h"
-#include "core/cvc4_expr.h"
+#include "config.h"
+#include "context/context.h"
+#include "cvc4_expr.h"
 
 namespace CVC4 {
 
diff --git a/src/expr/expr_builder.cpp b/src/expr/expr_builder.cpp
index 6491b7d44..2f7114a9b 100644
--- a/src/expr/expr_builder.cpp
+++ b/src/expr/expr_builder.cpp
@@ -9,9 +9,10 @@
  **
  **/
 
-#include "core/expr_builder.h"
-#include "core/expr_manager.h"
-#include "core/expr_value.h"
+#include "expr_builder.h"
+#include "expr_manager.h"
+#include "expr_value.h"
+#include "util/assert.h"
 
 using namespace std;
 
@@ -26,6 +27,16 @@ ExprBuilder::ExprBuilder(const Expr& e) : d_em(ExprManager::currentEM()), d_kind
   d_children.u_arr[0] = v;
 }
 
+ExprBuilder& ExprBuilder::reset(const ExprValue* ev) {
+  this->~ExprBuilder();
+  d_kind = Kind(ev->d_kind);
+  d_used = false;
+  d_nchildren = ev->d_nchildren;
+  for(Expr::const_iterator i = ev->begin(); i != ev->end(); ++i)
+    addChild(i->d_ev);
+  return *this;
+}
+
 ExprBuilder::ExprBuilder(const ExprBuilder& eb) : d_em(eb.d_em), d_kind(eb.d_kind), d_used(eb.d_used), d_nchildren(eb.d_nchildren) {
   cvc4assert(!d_used);
 
@@ -34,9 +45,9 @@ ExprBuilder::ExprBuilder(const ExprBuilder& eb) : d_em(eb.d_em), d_kind(eb.d_kin
     d_children.u_vec->reserve(d_nchildren + 5);
     copy(eb.d_children.u_vec->begin(), eb.d_children.u_vec->end(), back_inserter(*d_children.u_vec));
   } else {
-    iterator j = d_children.u_arr;
-    for(iterator i = eb.d_children.u_arr; i != eb.d_children.u_arr + eb.d_nchildren; ++i, ++j)
-      *j = i->inc();
+    ev_iterator j = d_children.u_arr;
+    for(ExprValue* const* i = eb.d_children.u_arr; i != eb.d_children.u_arr + eb.d_nchildren; ++i, ++j)
+      *j = (*i)->inc();
   }
 }
 
@@ -46,7 +57,7 @@ ExprBuilder::ExprBuilder(ExprManager* em) : d_em(em), d_kind(UNDEFINED_KIND), d_
 ExprBuilder::ExprBuilder(ExprManager* em, Kind k) : d_em(em), d_kind(k), d_used(false), d_nchildren(0) {
 }
 
-ExprBuilder::ExprBuilder(ExprManager* em, const Expr&) : d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) {
+ExprBuilder::ExprBuilder(ExprManager* em, const Expr& e) : d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) {
   ExprValue *v = e->inc();
   d_children.u_arr[0] = v;
 }
@@ -55,8 +66,8 @@ ExprBuilder::~ExprBuilder() {
   if(d_nchildren > nchild_thresh) {
     delete d_children.u_vec;
   } else {
-    for(iterator i = d_children.u_arr; i != d_children.u_arr + d_nchildren; ++i) {
-      *i
+    for(ev_iterator i = d_children.u_arr; i != d_children.u_arr + d_nchildren; ++i) {
+      (*i)->dec();
     }
   }
 }
@@ -70,10 +81,20 @@ ExprBuilder& ExprBuilder::eqExpr(const Expr& right) {
 }
 
 ExprBuilder& ExprBuilder::notExpr() {
+  if(d_kind != UNDEFINED_KIND)
+    collapse();
+  d_kind = NOT;
+  return *this;
 }
 
 // avoid double-negatives
 ExprBuilder& ExprBuilder::negate() {
+  if(d_kind == NOT)
+    return reset(d_children.u_arr[0]);
+  if(d_kind != UNDEFINED_KIND)
+    collapse();
+  d_kind = NOT;
+  return *this;
 }
 
 ExprBuilder& ExprBuilder::andExpr(const Expr& right) {
@@ -116,7 +137,43 @@ void ExprBuilder::addChild(const Expr& e) {
   if(d_nchildren == nchild_thresh) {
     vector<Expr>* v = new vector<Expr>();
     v->reserve(nchild_thresh + 5);
-    
+    for(ExprValue** i = d_children.u_arr; i != d_children.u_arr + nchild_thresh; ++i) {
+      v->push_back(Expr(*i));
+      i->dec();
+    }
+    v.push_back(e);
+    d_children.u_vec = v;
+    ++d_nchildren;
+  } else if(d_nchildren > nchild_thresh) {
+    d_children.u_vec.push_back(e);
+    ++d_nchildren;
+  } else {
+    ExprValue *ev = e->d_ev;
+    d_children.u_arr[d_nchildren] = ev;
+    ev->inc();
+    ++d_nchildren;
+  }
+  return *this;
+}
+
+void ExprBuilder::addChild(const ExprValue* ev) {
+  if(d_nchildren == nchild_thresh) {
+    vector<Expr>* v = new vector<Expr>();
+    v->reserve(nchild_thresh + 5);
+    for(ExprValue** i = d_children.u_arr; i != d_children.u_arr + nchild_thresh; ++i) {
+      v->push_back(Expr(*i));
+      i->dec();
+    }
+    v.push_back(Expr(ev));
+    d_children.u_vec = v;
+    ++d_nchildren;
+  } else if(d_nchildren > nchild_thresh) {
+    d_children.u_vec.push_back(Expr(ev));
+    ++d_nchildren;
+  } else {
+    d_children.u_arr[d_nchildren] = ev;
+    ev->inc();
+    ++d_nchildren;
   }
   return *this;
 }
diff --git a/src/expr/expr_builder.h b/src/expr/expr_builder.h
index fa08a3149..1104c17f5 100644
--- a/src/expr/expr_builder.h
+++ b/src/expr/expr_builder.h
@@ -13,8 +13,8 @@
 #define __CVC4_EXPR_BUILDER_H
 
 #include <vector>
-#include "core/expr_manager.h"
-#include "core/kind.h"
+#include "expr_manager.h"
+#include "kind.h"
 
 namespace CVC4 {
 
@@ -41,9 +41,15 @@ class ExprBuilder {
     std::vector<Expr>* u_vec;
   } d_children;
 
-  void addChild();
+  void addChild(const Expr&);
+  void addChild(const ExprValue*);
   void collapse();
 
+  typedef ExprValue** ev_iterator;
+  typedef ExprValue const** const_ev_iterator;
+
+  void reset(const ExprValue*);
+
 public:
 
   ExprBuilder();
diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp
index 90f10d8f7..80091bef6 100644
--- a/src/expr/expr_manager.cpp
+++ b/src/expr/expr_manager.cpp
@@ -10,9 +10,9 @@
  ** Expression manager implementation.
  **/
 
-#include "core/expr_builder.h"
-#include "core/expr_manager.h"
-#include "core/cvc4_expr.h"
+#include "expr_builder.h"
+#include "expr_manager.h"
+#include "cvc4_expr.h"
 
 namespace CVC4 {
 
diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h
index 048250485..7e0da01c6 100644
--- a/src/expr/expr_manager.h
+++ b/src/expr/expr_manager.h
@@ -14,7 +14,7 @@
 
 #include <vector>
 #include "cvc4_expr.h"
-#include "core/kind.h"
+#include "kind.h"
 
 namespace CVC4 {
 
diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp
index ce4177a09..451538f3f 100644
--- a/src/expr/expr_value.cpp
+++ b/src/expr/expr_value.cpp
@@ -14,7 +14,7 @@
  ** reference count on ExprValue instances and
  **/
 
-#include "core/expr_value.h"
+#include "expr_value.h"
 
 namespace CVC4 {
 
diff --git a/src/expr/expr_value.h b/src/expr/expr_value.h
index 5f90533ed..4b4b4f612 100644
--- a/src/expr/expr_value.h
+++ b/src/expr/expr_value.h
@@ -48,6 +48,10 @@ class ExprValue {
   Expr     d_children[0];
 
   friend class Expr;
+  friend class ExprBuilder;
+
+  ExprValue* inc() { /* FIXME thread safety */ ++d_rc; return this; }
+  ExprValue* dec() { /* FIXME thread safety */ --d_rc; return this; }
 
 public:
   /** Hash this expression.
diff --git a/src/include/cvc4_expr.h b/src/include/cvc4_expr.h
index 17e7f4f82..3d7a35fc8 100644
--- a/src/include/cvc4_expr.h
+++ b/src/include/cvc4_expr.h
@@ -38,6 +38,9 @@ class Expr {
    *  Increments the reference count. */
   explicit Expr(ExprValue*);
 
+  typedef Expr* iterator;
+  typedef Expr const* const_iterator;
+
 public:
   Expr(const Expr&);
 
@@ -49,11 +52,7 @@ public:
 
   /** Access to the encapsulated expression.
    *  @return the encapsulated expression. */
-  ExprValue* operator->();
-
-  /** Const access to the encapsulated expression.
-   *  @return the encapsulated expression [const]. */
-  const ExprValue* operator->() const;
+  ExprValue* operator->() const;
 
   uint64_t hash() const;
 
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 */
diff --git a/src/util/options.h b/src/util/options.h
new file mode 100644
index 000000000..f04b06f10
--- /dev/null
+++ b/src/util/options.h
@@ -0,0 +1,31 @@
+#ifndef __CVC4_OPTIONS_H
+#define __CVC4_OPTIONS_H
+
+namespace CVC4 {
+
+struct Options {
+  std::string binary_name;
+
+  bool smtcomp_mode;
+  bool statistics;
+
+  /* -1 means no output */
+  /* 0 is normal (and default) -- warnings only */
+  /* 1 is warnings + notices so the user doesn't get too bored */
+  /* 2 is chatty, giving statistical things etc. */
+  /* with 3, the solver is slowed down by all the scrolling */
+  int verbosity;
+
+  std::string lang;
+
+  Options() : binary_name(),
+              smtcomp_mode(false),
+              statistics(false),
+              verbosity(0),
+              lang()
+  {}
+};/* struct Options */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4_OPTIONS_H */