configure option adjustments as per 11/24 meeting; various fixes and improvements

23 files changed, 711 insertions, 63 deletions

diff --git a/configure.ac b/configure.ac
index b7e7975f7..0aba48aa3 100644
--- a/configure.ac
+++ b/configure.ac
@@ -8,29 +8,142 @@ AC_CONFIG_AUX_DIR([config])
 AC_CONFIG_MACRO_DIR([config])
 AM_INIT_AUTOMAKE(cvc4, prerelease)
 AC_CONFIG_HEADERS([config.h])
+
+# keep track of whether the user set these (check here, because
+# autoconf might set a default later)
+if test -z "${CPPFLAGS+set}"; then user_cppflags=no; else user_cppflags=yes; fi
+if test -z "${CXXFLAGS+set}"; then user_cxxflags=no; else user_cxxflags=yes; fi
+if test -z "${LDFLAGS+set}" ; then user_ldflags=no ; else user_ldflags=yes ; fi
+
 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
+AC_MSG_CHECKING([for requested build profile])
+AC_ARG_WITH([build],             [AS_HELP_STRING([--with-build=profile],     [for profile in {production,debug,default,competition}])])
+if test -z "${with_build+set}" -o "$with_build" = default; then
+  with_build=default
+fi
+if test "$user_cppflags" = no -a "$user_cxxflags" = no -a "$user_ldflags" = no -a -z "${enable_optimized+set}" -a -z "${enable_debug_symbols+set}" -a -z "${enable_assertions+set}" -a -z "${enable_tracing+set}" -a -z "${enable_muzzle+set}" -a -z "${enable_coverage+set}" -a -z "${enable_profiling+set}"; then
+  non_standard_build_profile=no
+else
+  non_standard_build_profile=yes
+fi
+case "$with_build" in
+  production)
+    CVC4CPPFLAGS=
+    CVC4CXXFLAGS=-O3
+    CVC4LDFLAGS=
+    if test -z "${enable_assertions+set}"; then enable_assertions=no             ; fi
+    if test -z "${enable_tracing+set}"   ; then enable_tracing=no                ; fi
+    if test -z "${enable_muzzle+set}"    ; then enable_muzzle=no                 ; fi
+    ;;
+  debug)
+    CVC4CPPFLAGS=-DCVC4_DEBUG
+    CVC4CXXFLAGS='-O0 -fno-inline -ggdb3'
+    CVC4LDFLAGS=
+    if test -z "${enable_assertions+set}"; then enable_assertions=yes            ; fi
+    if test -z "${enable_tracing+set}"   ; then enable_tracing=yes               ; fi
+    if test -z "${enable_muzzle+set}"    ; then enable_muzzle=no                 ; fi
+    ;;
+  default)
+    CVC4CPPFLAGS=
+    CVC4CXXFLAGS=-O2
+    CVC4LDFLAGS=
+    if test -z "${enable_assertions+set}"; then enable_assertions=yes            ; fi
+    if test -z "${enable_tracing+set}"   ; then enable_tracing=yes               ; fi
+    if test -z "${enable_muzzle+set}"    ; then enable_muzzle=no                 ; fi
+    ;;
+  competition)
+    CVC4CPPFLAGS=
+    CVC4CXXFLAGS='-O9 -funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs'
+    CVC4LDFLAGS=
+    if test -z "${enable_assertions+set}"; then enable_assertions=no             ; fi
+    if test -z "${enable_tracing+set}"   ; then enable_tracing=no                ; fi
+    if test -z "${enable_muzzle+set}"    ; then enable_muzzle=yes                ; fi
+    ;;
+  *)
+    AC_MSG_FAILURE([unknown build profile: $with_build])
+    ;;
+esac
+AC_MSG_RESULT([$with_build])
+
+AC_MSG_CHECKING([whether to optimize libcvc4])
+AC_ARG_ENABLE([optimized],       [AS_HELP_STRING([--enable-optimized],       [optimize the build])])
+if test -z "${enable_optimized+set}"; then
+  enable_optimized=no
+fi
+AC_MSG_RESULT([$enable_optimized])
+if test "$enable_optimized" = yes; then
+  CVC4CXXFLAGS="$CVC4CXXFLAGS -O3"
+fi
+
+AC_MSG_CHECKING([whether to include debugging symbols in libcvc4])
+AC_ARG_ENABLE([debug-symbols],   [AS_HELP_STRING([--disable-debug-symbols],  [do not include debug symbols in libcvc4])])
+if test -z "${enable_debug_symbols+set}"; then
+  enable_debug_symbols=yes
+fi
+AC_MSG_RESULT([$enable_debug_symbols])
+if test "$enable_debug_symbols" = yes; then
+  CVC4CXXFLAGS="$CVC4CXXFLAGS -ggdb3"
 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])])
+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" = yes; then
+  CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_ASSERTIONS"
+fi
 
-if test "$enable_assertions" = no -a "$enable_debug" = yes; then
-  AC_MSG_FAILURE([when debugging is on, so must assertions be.])
+AC_MSG_CHECKING([whether to do a traceable build of CVC4])
+AC_ARG_ENABLE([tracing],         [AS_HELP_STRING([--disable-tracing],        [remove all tracing code from CVC4])])
+if test -z "${enable_tracing+set}"; then
+  enable_tracing=yes
+fi
+AC_MSG_RESULT([$enable_tracing])
+if test "$enable_tracing" = yes; then
+  CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_TRACING"
+fi
+
+AC_MSG_CHECKING([whether to do a muzzled build of CVC4])
+AC_ARG_ENABLE([muzzle],          [AS_HELP_STRING([--enable-muzzle],          [completely silence CVC4; remove ALL non-result output from build])])
+if test -z "${enable_muzzle+set}"; then
+  enable_muzzle=no
+fi
+AC_MSG_RESULT([$enable_muzzle])
+if test "$enable_muzzle" = yes; then
+  CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_MUZZLE"
+fi
+
+AC_MSG_CHECKING([whether to do a gcov-enabled build of CVC4])
+AC_ARG_ENABLE([coverage],        [AS_HELP_STRING([--enable-coverage],        [build with support for gcov coverage testing])])
+if test -z "${enable_coverage+set}"; then
+  enable_coverage=no
+fi
+AC_MSG_RESULT([$enable_coverage])
+if test "$enable_coverage" = yes; then
+  CVC4CXXFLAGS="$CVC4CXXFLAGS --coverage"
+  CVC4LDFLAGS="$CVC4LDFLAGS --coverage"
+fi
+
+AC_MSG_CHECKING([whether to do a profiling-enabled build of CVC4])
+AC_ARG_ENABLE([profiling],       [AS_HELP_STRING([--enable-profiling],       [build with support for gprof profiling])])
+if test -z "${enable_profiling+set}"; then
+  enable_profiling=no
+fi
+AC_MSG_RESULT([$enable_profiling])
+if test "$enable_profiling" = yes; then
+  CVC4CXXFLAGS="$CVC4CXXFLAGS -pg"
+  CVC4LDFLAGS="$CVC4LDFLAGS -pg"
 fi
 
+
+
+
 # Checks for programs.
 AC_PROG_CC
 AC_PROG_CXX
@@ -93,13 +206,6 @@ 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
 
@@ -125,19 +231,67 @@ AC_CONFIG_FILES([
 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.
+CVC4 $VERSION
+
+Build profile: $with_build$non_standard
+Optimized    : $enable_optimized
+Debug symbols: $enable_debug_symbols
+Assertions   : $enable_assertions
+Tracing      : $enable_tracing
+Muzzle       : $enable_muzzle
+gcov support : $enable_coverage
+gprof support: $enable_profiling
+
+CPPFLAGS     : $CPPFLAGS
+CXXFLAGS     : $CXXFLAGS
+LDFLAGS      : $LDFLAGS
 
 Now just type make, followed by make check or make install, as you like.
 
+You can also use 'make build_profile' to reconfigure for a different profile.
+Build profiles: production optimized default competition
+
 EOF
+
+if test "$user_cppflags" = yes; then
+  AC_MSG_WARN([])
+  AC_MSG_WARN([I won't override your CPPFLAGS setting.  But some of your build options to configure may not be honored.])
+  AC_MSG_WARN([To support your options to configure, I would like to set CPPFLAGS to:])
+  AC_MSG_WARN([    $CVC4CPPFLAGS])
+  AC_MSG_WARN([])
+else
+  CPPFLAGS="$CVC4CPPFLAGS"
+fi
+if test "$user_cxxflags" = yes; then
+  AC_MSG_WARN([])
+  AC_MSG_WARN([I won't override your CXXFLAGS setting.  But some of your build options to configure may not be honored.])
+  AC_MSG_WARN([To support your options to configure, I would like to set CXXFLAGS to:])
+  AC_MSG_WARN([    $CVC4CXXFLAGS])
+  AC_MSG_WARN([])
+else
+  CXXFLAGS="$CVC4CXXFLAGS"
+fi
+if test "$user_ldflags" = yes; then
+  AC_MSG_WARN([])
+  AC_MSG_WARN([I won't override your LDFLAGS setting.  But some of your build options to configure may not be honored.])
+  AC_MSG_WARN([To support your options to configure, I would like to set LDFLAGS to:])
+  AC_MSG_WARN([    $CVC4LDFLAGS])
+  AC_MSG_WARN([])
+else
+  LDFLAGS="$CVC4LDFLAGS"
+fi
+
+non_standard=
+if test "$non_standard_build_profile" = yes; then
+  if test "$with_build" = default; then
+    with_build=custom
+  else
+    AC_MSG_WARN([])
+    AC_MSG_WARN([This is a non-standard $with_build build profile.])
+    AC_MSG_WARN([])
+    non_standard=-custom
+  fi
+fi
diff --git a/contrib/editing-with-emacs b/contrib/editing-with-emacs
index 277424230..66ee555a9 100644
--- a/contrib/editing-with-emacs
+++ b/contrib/editing-with-emacs
@@ -12,7 +12,7 @@ describing your usual cvc4 editing location(s):
   (setq c-basic-offset 2)
   (c-set-offset 'innamespace 0)
   (setq indent-tabs-mode nil))
-(setq auto-mode-alist (cons '("/home/mdeters/cvc4.*/.*\\.\\(cc\\|cpp\\|h\\|hh\\|hpp\\)$" . cvc4-c++-editing-mode) auto-mode-alist))
+(setq auto-mode-alist (cons '("/home/mdeters/cvc4.*/.*\\.\\(cc\\|cpp\\|h\\|hh\\|hpp\\|y\\|yy\\|ypp\\|lex\\|l\\|ll\\|lpp\\)$" . cvc4-c++-editing-mode) auto-mode-alist))
 
 
 -- Morgan Deters <mdeters@cs.nyu.edu>  Mon, 02 Nov 2009 18:19:22 -0500
diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl
index 74030e810..a270e7362 100755
--- a/contrib/update-copyright.pl
+++ b/contrib/update-copyright.pl
@@ -103,6 +103,7 @@ sub recurse {
           last if $line =~ /^ \*\*\s*$/;
         }
       } else {
+        my $line = $_;
         print "adding\n";
         if($file =~ /\.(y|yy|ypp|Y)$/) {
           print $OUT "%{/*******************                                           -*- C++ -*-  */\n";
@@ -119,6 +120,7 @@ sub recurse {
         print $OUT " **\n";
         print $OUT " ** [[ Add file-specific comments here ]]\n";
         print $OUT " **/\n\n";
+        print $OUT $line;
         if($file =~ /\.(y|yy|ypp|Y)$/) {
           while(my $line = <$IN>) {
             chomp $line;
diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
index f1b334ff8..e25cf8595 100644
--- a/src/expr/expr.cpp
+++ b/src/expr/expr.cpp
@@ -10,7 +10,7 @@
  ** Reference-counted encapsulation of a pointer to an expression.
  **/
 
-#include "cvc4_expr.h"
+#include "expr/expr.h"
 #include "expr_value.h"
 #include "expr_builder.h"
 
diff --git a/src/expr/expr.h b/src/expr/expr.h
new file mode 100644
index 000000000..d99708991
--- /dev/null
+++ b/src/expr/expr.h
@@ -0,0 +1,103 @@
+/*********************                                           -*- C++ -*-  */
+/** cvc4_expr.h
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Reference-counted encapsulation of a pointer to an expression.
+ **/
+
+#ifndef __CVC4_EXPR_H
+#define __CVC4_EXPR_H
+
+#include <vector>
+#include <stdint.h>
+
+#include "cvc4_config.h"
+#include "expr/kind.h"
+
+namespace CVC4 {
+
+namespace expr {
+  class ExprValue;
+}/* CVC4::expr namespace */
+
+using CVC4::expr::ExprValue;
+
+/**
+ * Encapsulation of an ExprValue pointer.  The reference count is
+ * maintained in the ExprValue.
+ */
+class CVC4_PUBLIC Expr {
+  /** A convenient null-valued encapsulated pointer */
+  static Expr s_null;
+
+  /** The referenced ExprValue */
+  ExprValue* d_ev;
+
+  /** This constructor is reserved for use by the Expr package; one
+   *  must construct an Expr using one of the build mechanisms of the
+   *  Expr package.
+   *
+   *  Increments the reference count. */
+  explicit Expr(ExprValue*);
+
+  typedef Expr* iterator;
+  typedef Expr const* const_iterator;
+
+  friend class ExprBuilder;
+
+public:
+  CVC4_PUBLIC Expr(const Expr&);
+
+  /** Destructor.  Decrements the reference count and, if zero,
+   *  collects the ExprValue. */
+  CVC4_PUBLIC ~Expr();
+
+  Expr& operator=(const Expr&) CVC4_PUBLIC;
+
+  /** Access to the encapsulated expression.
+   *  @return the encapsulated expression. */
+  ExprValue* operator->() const CVC4_PUBLIC;
+
+  uint64_t hash() const;
+
+  Expr eqExpr(const Expr& right) const;
+  Expr notExpr() const;
+  Expr negate() const; // avoid double-negatives
+  Expr andExpr(const Expr& right) const;
+  Expr orExpr(const Expr& right) const;
+  Expr iteExpr(const Expr& thenpart, const Expr& elsepart) const;
+  Expr iffExpr(const Expr& right) const;
+  Expr impExpr(const Expr& right) const;
+  Expr xorExpr(const Expr& right) const;
+  Expr skolemExpr(int i) const;
+  Expr substExpr(const std::vector<Expr>& oldTerms,
+                 const std::vector<Expr>& newTerms) const;
+
+  Expr plusExpr(const Expr& right) const;
+  Expr uMinusExpr() const;
+  Expr multExpr(const Expr& right) const;
+
+  inline Kind getKind() const;
+
+  static Expr null() { return s_null; }
+
+};/* class Expr */
+
+}/* CVC4 namespace */
+
+#include "expr/expr_value.h"
+
+namespace CVC4 {
+
+inline Kind Expr::getKind() const {
+  return Kind(d_ev->d_kind);
+}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4_EXPR_H */
diff --git a/src/expr/expr_attribute.h b/src/expr/expr_attribute.h
index b44c9af6f..03140c4eb 100644
--- a/src/expr/expr_attribute.h
+++ b/src/expr/expr_attribute.h
@@ -17,7 +17,7 @@
 #include <stdint.h>
 #include "config.h"
 #include "context/context.h"
-#include "cvc4_expr.h"
+#include "expr/expr.h"
 
 namespace CVC4 {
 namespace expr {
diff --git a/src/expr/expr_builder.cpp b/src/expr/expr_builder.cpp
index c5f366654..bf572cfbc 100644
--- a/src/expr/expr_builder.cpp
+++ b/src/expr/expr_builder.cpp
@@ -38,7 +38,7 @@ ExprBuilder& ExprBuilder::reset(const ExprValue* ev) {
 }
 
 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);
+  Assert( !d_used );
 
   if(d_nchildren > nchild_thresh) {
     d_children.u_vec = new vector<Expr>();
@@ -74,59 +74,104 @@ ExprBuilder::~ExprBuilder() {
 
 // Compound expression constructors
 ExprBuilder& ExprBuilder::eqExpr(const Expr& right) {
-  if(d_kind != UNDEFINED_KIND && d_kind != EQUAL)
+  Assert( d_kind != UNDEFINED_KIND );
+  if(EXPECT_TRUE( d_kind != EQUAL )) {
     collapse();
-  d_kind = EQUAL;
+    d_kind = EQUAL;
+  }
+  addChild(right);
   return *this;
 }
 
 ExprBuilder& ExprBuilder::notExpr() {
-  if(d_kind != UNDEFINED_KIND)
-    collapse();
+  Assert( d_kind != UNDEFINED_KIND );
+  collapse();
   d_kind = NOT;
   return *this;
 }
 
 // avoid double-negatives
 ExprBuilder& ExprBuilder::negate() {
-  if(d_kind == NOT)
+  if(EXPECT_FALSE( d_kind == NOT ))
     return reset(d_children.u_arr[0]);
-  if(d_kind != UNDEFINED_KIND)
-    collapse();
+  Assert( d_kind != UNDEFINED_KIND );
+  collapse();
   d_kind = NOT;
   return *this;
 }
 
 ExprBuilder& ExprBuilder::andExpr(const Expr& right) {
+  Assert( d_kind != UNDEFINED_KIND );
+  if(d_kind != AND) {
+    collapse();
+    d_kind = AND;
+  }
+  addChild(right);
+  return *this;
 }
 
 ExprBuilder& ExprBuilder::orExpr(const Expr& right) {
+  Assert( d_kind != UNDEFINED_KIND );
+  if(EXPECT_TRUE( d_kind != OR )) {
+    collapse();
+    d_kind = OR;
+  }
+  addChild(right);
+  return *this;
 }
 
 ExprBuilder& ExprBuilder::iteExpr(const Expr& thenpart, const Expr& elsepart) {
+  Assert( d_kind != UNDEFINED_KIND );
+  collapse();
+  d_kind = ITE;
+  addChild(thenpart);
+  addChild(elsepart);
+  return *this;
 }
 
 ExprBuilder& ExprBuilder::iffExpr(const Expr& right) {
+  Assert( d_kind != UNDEFINED_KIND );
+  if(EXPECT_TRUE( d_kind != IFF )) {
+    collapse();
+    d_kind = IFF;
+  }
+  addChild(right);
+  return *this;
 }
 
 ExprBuilder& ExprBuilder::impExpr(const Expr& right) {
+  Assert( d_kind != UNDEFINED_KIND );
+  collapse();
+  d_kind = IMPLIES;
+  addChild(right);
+  return *this;
 }
 
 ExprBuilder& ExprBuilder::xorExpr(const Expr& right) {
+  Assert( d_kind != UNDEFINED_KIND );
+  if(EXPECT_TRUE( d_kind != XOR )) {
+    collapse();
+    d_kind = XOR;
+  }
+  addChild(right);
+  return *this;
 }
 
 ExprBuilder& ExprBuilder::skolemExpr(int i) {
-}
-
-ExprBuilder& ExprBuilder::substExpr(const std::vector<Expr>& oldTerms,
-                                    const std::vector<Expr>& newTerms) {
+  Assert( d_kind != UNDEFINED_KIND );
+  collapse();
+  d_kind = SKOLEM;
+  //addChild(i);//FIXME: int constant
+  return *this;
 }
 
 // "Stream" expression constructor syntax
 ExprBuilder& ExprBuilder::operator<<(const Kind& op) {
+  return *this;
 }
 
 ExprBuilder& ExprBuilder::operator<<(const Expr& child) {
+  return *this;
 }
 
 void ExprBuilder::addChild(const Expr& e) {
@@ -182,21 +227,27 @@ void ExprBuilder::collapse() {
 
 // not const
 ExprBuilder::operator Expr() {
+  // FIXME
 }
 
-AndExprBuilder   ExprBuilder::operator&&(Expr) {
+AndExprBuilder   ExprBuilder::operator&&(Expr e) {
+  return AndExprBuilder(*this) && e;
 }
 
-OrExprBuilder    ExprBuilder::operator||(Expr) {
+OrExprBuilder    ExprBuilder::operator||(Expr e) {
+  return OrExprBuilder(*this) || e;
 }
 
-PlusExprBuilder  ExprBuilder::operator+ (Expr) {
+PlusExprBuilder  ExprBuilder::operator+ (Expr e) {
+  return PlusExprBuilder(*this) + e;
 }
 
-PlusExprBuilder  ExprBuilder::operator- (Expr) {
+PlusExprBuilder  ExprBuilder::operator- (Expr e) {
+  return PlusExprBuilder(*this) - e;
 }
 
-MultExprBuilder  ExprBuilder::operator* (Expr) {
+MultExprBuilder  ExprBuilder::operator* (Expr e) {
+  return MultExprBuilder(*this) * e;
 }
 
 }/* CVC4 namespace */
diff --git a/src/expr/expr_builder.h b/src/expr/expr_builder.h
index 07d069a9e..97f18ca6d 100644
--- a/src/expr/expr_builder.h
+++ b/src/expr/expr_builder.h
@@ -109,6 +109,8 @@ class AndExprBuilder {
 
 public:
 
+  AndExprBuilder(const ExprBuilder&);
+
   AndExprBuilder&   operator&&(Expr);
   OrExprBuilder     operator||(Expr);
 
@@ -121,6 +123,8 @@ class OrExprBuilder {
 
 public:
 
+  OrExprBuilder(const ExprBuilder&);
+
   AndExprBuilder    operator&&(Expr);
   OrExprBuilder&    operator||(Expr);
 
@@ -133,6 +137,8 @@ class PlusExprBuilder {
 
 public:
 
+  PlusExprBuilder(const ExprBuilder&);
+
   PlusExprBuilder&  operator+(Expr);
   PlusExprBuilder&  operator-(Expr);
   MultExprBuilder   operator*(Expr);
@@ -146,6 +152,8 @@ class MultExprBuilder {
 
 public:
 
+  MultExprBuilder(const ExprBuilder&);
+
   PlusExprBuilder   operator+(Expr);
   PlusExprBuilder   operator-(Expr);
   MultExprBuilder&  operator*(Expr);
diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h
index 802cfe9c0..e3fbd91bf 100644
--- a/src/expr/expr_manager.h
+++ b/src/expr/expr_manager.h
@@ -13,7 +13,7 @@
 #define __CVC4__EXPR_MANAGER_H
 
 #include <vector>
-#include "cvc4_expr.h"
+#include "expr/expr.h"
 #include "kind.h"
 
 namespace CVC4 {
diff --git a/src/expr/expr_value.h b/src/expr/expr_value.h
index e0451f7a6..0b97dfdae 100644
--- a/src/expr/expr_value.h
+++ b/src/expr/expr_value.h
@@ -16,7 +16,7 @@
 
 /* this must be above the check for __CVC4__EXPR__EXPR_VALUE_H */
 /* to resolve a circular dependency */
-#include "cvc4_expr.h"
+#include "expr/expr.h"
 
 #ifndef __CVC4__EXPR__EXPR_VALUE_H
 #define __CVC4__EXPR__EXPR_VALUE_H
diff --git a/src/expr/kind.h b/src/expr/kind.h
index 98cc7e2e3..db25d914e 100644
--- a/src/expr/kind.h
+++ b/src/expr/kind.h
@@ -36,12 +36,14 @@ enum Kind {
 
   AND,
   IFF,
+  IMPLIES,
   OR,
   XOR,
 
   /* from arith */
   PLUS,
-  MINUS
+  MINUS,
+  MULT
 
 };/* enum Kind */
 
diff --git a/src/include/cvc4_config.h b/src/include/cvc4_config.h
index e571f5969..ccc07b40a 100644
--- a/src/include/cvc4_config.h
+++ b/src/include/cvc4_config.h
@@ -39,3 +39,6 @@
 #  define CVC4_PUBLIC
 
 #endif /* __BUILDING_CVC4LIB */
+
+#define EXPECT_TRUE(x) __builtin_expect( (x), true)
+#define EXPECT_FALSE(x) __builtin_expect( (x), false)
diff --git a/src/include/cvc4_expr.h b/src/include/cvc4_expr.h
index 36d771647..d99708991 100644
--- a/src/include/cvc4_expr.h
+++ b/src/include/cvc4_expr.h
@@ -78,6 +78,10 @@ public:
   Expr substExpr(const std::vector<Expr>& oldTerms,
                  const std::vector<Expr>& newTerms) const;
 
+  Expr plusExpr(const Expr& right) const;
+  Expr uMinusExpr() const;
+  Expr multExpr(const Expr& right) const;
+
   inline Kind getKind() const;
 
   static Expr null() { return s_null; }
diff --git a/src/main/about.h b/src/main/about.h
index 458716842..e81e04288 100644
--- a/src/main/about.h
+++ b/src/main/about.h
@@ -10,6 +10,7 @@
  ** [[ Add file-specific comments here ]]
  **/
 
+#ifndef __CVC4__MAIN__ABOUT_H
 #define __CVC4__MAIN__ABOUT_H
 
 namespace CVC4 {
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index f1fe375b6..dcb23c303 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -10,6 +10,7 @@
  ** [[ Add file-specific comments here ]]
  **/
 
+#include <cstdio>
 #include <cstdlib>
 #include <new>
 #include <unistd.h>
@@ -29,7 +30,7 @@ using namespace std;
 using namespace CVC4;
 
 namespace CVC4 {
-namespace Main {
+namespace main {
 
 static const char lang_help[] = "\
 Languages currently supported to the -L / --lang option:\n\
@@ -135,5 +136,5 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(Exception*) {
   return optind;
 }
 
-}/* CVC4::Main namespace */
+}/* CVC4::main namespace */
 }/* CVC4 namespace */
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 44543a75f..8529f2ca2 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -10,6 +10,7 @@
  ** [[ Add file-specific comments here ]]
  **/
 
+#include <cstdio>
 #include <cstdlib>
 #include <cerrno>
 #include <new>
@@ -25,7 +26,7 @@
 
 using namespace std;
 using namespace CVC4;
-using namespace CVC4::Main;
+using namespace CVC4::main;
 
 int main(int argc, char *argv[]) {
   struct Options opts;
@@ -57,7 +58,7 @@ int main(int argc, char *argv[]) {
       //   delete cmd;
       // }
     }
-  } catch(CVC4::Main::OptionException* e) {
+  } catch(CVC4::main::OptionException* e) {
     if(opts.smtcomp_mode) {
       printf("unknown");
       fflush(stdout);
diff --git a/src/main/usage.h b/src/main/usage.h
index 3326108ac..0b503cdb2 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -10,6 +10,7 @@
  ** [[ Add file-specific comments here ]]
  **/
 
+#ifndef __CVC4__MAIN__USAGE_H
 #define __CVC4__MAIN__USAGE_H
 
 namespace CVC4 {
diff --git a/src/main/util.cpp b/src/main/util.cpp
index 572aea00f..e2333b417 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -23,7 +23,7 @@ using CVC4::Exception;
 using namespace std;
 
 namespace CVC4 {
-namespace Main {
+namespace main {
 
 void sigint_handler(int sig, siginfo_t* info, void*) {
   fprintf(stderr, "CVC4 interrupted by user.\n");
@@ -51,5 +51,5 @@ void cvc4_init() throw() {
     throw new Exception(string("sigaction(SIGSEGV) failure: ") + strerror(errno));
 }
 
-}/* CVC4::Main namespace */
+}/* CVC4::main namespace */
 }/* CVC4 namespace */
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
new file mode 100644
index 000000000..078bf9cde
--- /dev/null
+++ b/src/smt/smt_engine.h
@@ -0,0 +1,116 @@
+/*********************                                           -*- C++ -*-  */
+/** prover.h
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ **/
+
+#ifndef __CVC4__SMT__SMT_ENGINE_H
+#define __CVC4__SMT__SMT_ENGINE_H
+
+#include <vector>
+#include "core/cvc4_expr.h"
+#include "core/result.h"
+#include "core/model.h"
+
+// In terms of abstraction, this is below (and provides services to)
+// ValidityChecker and above (and requires the services of)
+// PropEngine.
+
+namespace CVC4 {
+namespace smt {
+
+// TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
+// hood): use a type parameter and have check() delegate, or subclass
+// SmtEngine and override check()?
+//
+// Probably better than that is to have a configuration object that
+// indicates which passes are desired.  The configuration occurs
+// elsewhere (and can even occur at runtime).  A simple "pass manager"
+// of sorts determines check()'s behavior.
+//
+// The CNF conversion can go on in PropEngine.
+
+class SmtEngine {
+  /** Current set of assertions. */
+  // TODO: make context-aware to handle user-level push/pop.
+  std::vector<Expr> d_assertList;
+
+private:
+  /**
+   * Pre-process an Expr.  This is expected to be highly-variable,
+   * with a lot of "source-level configurability" to add multiple
+   * passes over the Expr.  TODO: may need to specify a LEVEL of
+   * preprocessing (certain contexts need more/less ?).
+   */
+  void preprocess(Expr);
+
+  /**
+   * Adds a formula to the current context.
+   */
+  void addFormula(Expr);
+
+  /**
+   * Full check of consistency in current context.  Returns true iff
+   * consistent.
+   */
+  Result check();
+
+  /**
+   * Quick check of consistency in current context: calls
+   * processAssertionList() then look for inconsistency (based only on
+   * that).
+   */
+  Result quickCheck();
+
+  /**
+   * Process the assertion list: for literals and conjunctions of
+   * literals, assert to T-solver.
+   */
+  void processAssertionList();
+
+public:
+  /**
+   * Add a formula to the current context: preprocess, do per-theory
+   * setup, use processAssertionList(), asserting to T-solver for
+   * literals and conjunction of literals.  Returns false iff
+   * inconsistent.
+   */
+  Result assert(Expr);
+
+  /**
+   * Add a formula to the current context and call check().  Returns
+   * true iff consistent.
+   */
+  Result query(Expr);
+
+  /**
+   * Simplify a formula without doing "much" work.  Requires assist
+   * from the SAT Engine.
+   */
+  Expr simplify(Expr);
+
+  /**
+   * Get a (counter)model (only if preceded by a SAT or INVALID query.
+   */
+  Model getModel();
+
+  /**
+   * Push a user-level context.
+   */
+  void push();
+
+  /**
+   * Pop a user-level context.  Throws an exception if nothing to pop.
+   */
+  void pop();
+};/* class SmtEngine */
+
+}/* CVC4::smt namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__SMT__SMT_ENGINE_H */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 1369d5f0b..5e5f053a6 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -12,7 +12,7 @@
 #ifndef __CVC4__THEORY__THEORY_H
 #define __CVC4__THEORY__THEORY_H
 
-#include "cvc4_expr.h"
+#include "expr/expr.h"
 #include "util/literal.h"
 
 namespace CVC4 {
diff --git a/src/util/assert.h b/src/util/assert.h
index 24e3a4cdf..6691c1b04 100644
--- a/src/util/assert.h
+++ b/src/util/assert.h
@@ -7,20 +7,78 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** Assertion utility classes, functions, and exceptions.
  **/
 
 #ifndef __CVC4__ASSERT_H
 #define __CVC4__ASSERT_H
 
-#include <cassert>
+#include <string>
+#include "util/exception.h"
+#include "cvc4_config.h"
+#include "config.h"
 
-#ifdef DEBUG
-// the __builtin_expect() helps us if assert is built-in or a macro
-# define cvc4assert(x) assert(__builtin_expect((x), 1))
-#else
-// TODO: use a compiler annotation when assertions are off ?
-// (to improve optimization)
-# define cvc4assert(x)
-#endif /* DEBUG */
+namespace CVC4 {
+
+class AssertionException : public Exception {
+public:
+  AssertionException() : Exception() {}
+  AssertionException(std::string msg) : Exception(msg) {}
+  AssertionException(const char* msg) : Exception(msg) {}
+};/* class AssertionException */
+
+class UnreachableCodeException : public AssertionException {
+public:
+  UnreachableCodeException() : AssertionException() {}
+  UnreachableCodeException(std::string msg) : AssertionException(msg) {}
+  UnreachableCodeException(const char* msg) : AssertionException(msg) {}
+};/* class UnreachableCodeException */
+
+#ifdef CVC4_ASSERTIONS
+#  define Assert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ":  " #cond, __builtin_expect((cond), 1), ## msg)
+#else /* ! CVC4_ASSERTIONS */
+#  define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/
+#endif /* CVC4_ASSERTIONS */
+
+#define AlwaysAssert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ":  " #cond, __builtin_expect((cond), 1), ## msg)
+#define Unreachable(cond, msg...) __CVC4_UNREACHABLEGLUE("Hit a section of unreachable code at " __FILE__ ":", __LINE__, __builtin_expect((cond), 1), ## msg)
+
+#define __CVC4_ASSERTGLUE(str1, line, str2, cond, msg...) AssertImpl(str1 #line str2, cond, ## msg)
+#define __CVC4_UNREACHABLEGLUE(str, line, cond, msg...) AssertImpl(str #line, cond, ## msg)
+
+inline void AssertImpl(const char* info, bool cond, std::string msg) {
+  if(EXPECT_FALSE( ! cond ))
+    throw new AssertionException(std::string(info) + "\n" + msg);
+}
+
+inline void AssertImpl(const char* info, bool cond, const char* msg) {
+  if(EXPECT_FALSE( ! cond ))
+    throw new AssertionException(std::string(info) + "\n" + msg);
+}
+
+inline void AssertImpl(const char* info, bool cond) {
+  if(EXPECT_FALSE( ! cond ))
+    throw new AssertionException(info);
+}
+
+#ifdef __GNUC__
+inline void UnreachableImpl(const char* info, std::string msg) __attribute__ ((noreturn));
+inline void UnreachableImpl(const char* info, const char* msg) __attribute__ ((noreturn));
+inline void UnreachableImpl(const char* info) __attribute__ ((noreturn));
+#endif /* __GNUC__ */
+
+inline void UnreachableImpl(const char* info, std::string msg) {
+  throw new UnreachableCodeException(std::string(info) + "\n" + msg);
+}
+
+inline void UnreachableImpl(const char* info, const char* msg) {
+  throw new UnreachableCodeException(std::string(info) + "\n" + msg);
+}
+
+inline void UnreachableImpl(const char* info) {
+  throw new UnreachableCodeException(info);
+}
+
+}/* CVC4 namespace */
 
 #endif /* __CVC4__ASSERT_H */
diff --git a/src/util/options.h b/src/util/options.h
index 490cd607b..54b4e2f9b 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -10,6 +10,9 @@
  ** [[ Add file-specific comments here ]]
  **/
 
+#include <iostream>
+
+#ifndef __CVC4__OPTIONS_H
 #define __CVC4__OPTIONS_H
 
 namespace CVC4 {
@@ -20,6 +23,9 @@ struct Options {
   bool smtcomp_mode;
   bool statistics;
 
+  std::ostream *out;
+  std::ostream *err;
+
   /* -1 means no output */
   /* 0 is normal (and default) -- warnings only */
   /* 1 is warnings + notices so the user doesn't get too bored */
@@ -32,6 +38,8 @@ struct Options {
   Options() : binary_name(),
               smtcomp_mode(false),
               statistics(false),
+              out(0),
+              err(0),
               verbosity(0),
               lang()
   {}
diff --git a/src/util/output.h b/src/util/output.h
new file mode 100644
index 000000000..4d3752849
--- /dev/null
+++ b/src/util/output.h
@@ -0,0 +1,135 @@
+/*********************                                           -*- C++ -*-  */
+/** output.h
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Output utility classes and functions.
+ **/
+
+#ifndef __CVC4__OUTPUT_H
+#define __CVC4__OUTPUT_H
+
+#include <iostream>
+#include <string>
+#include <set>
+#include "util/exception.h"
+
+namespace CVC4 {
+
+
+class Debug {
+  std::set<std::string> d_tags;
+  std::ostream &d_out;
+
+public:
+  static void operator()(const char* tag, const char*);
+  static void operator()(const char* tag, std::string);
+  static void operator()(string tag, const char*);
+  static void operator()(string tag, std::string);
+
+  static void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
+  static void printf(const char* tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3)));
+  static void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
+  static void printf(std::string tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3)));
+
+  static std::ostream& operator()(const char* tag);
+  static std::ostream& operator()(std::string tag);
+
+  static void on (const char* tag) { d_tags.insert(std::string(tag)); };
+  static void on (std::string tag) { d_tags.insert(tag);              };
+  static void off(const char* tag) { d_tags.erase (std::string(tag)); };
+  static void off(std::string tag) { d_tags.erase (tag);              };
+
+  static void setStream(std::ostream& os) { d_out = os; }
+};/* class Debug */
+
+
+class Warning {
+  std::ostream &d_out;
+
+public:
+  static void operator()(const char*);
+  static void operator()(std::string);
+
+  static void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
+  static void printf(std::string fmt, ...) __attribute__ ((format(printf, 2, 3)));
+
+  static std::ostream& operator()();
+
+  static void setStream(std::ostream& os) { d_out = os; }
+};/* class Warning */
+
+
+class Notice {
+  std::ostream &d_os;
+
+public:
+  static void operator()(const char*);
+  static void operator()(std::string);
+
+  static void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
+  static void printf(std::string fmt, ...) __attribute__ ((format(printf, 2, 3)));
+
+  static std::ostream& operator()();
+
+  static void setStream(std::ostream& os) { d_out = os; }
+};/* class Notice */
+
+
+class Chat {
+  std::ostream &d_os;
+
+public:
+  static void operator()(const char*);
+  static void operator()(std::string);
+
+  static void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
+  static void printf(std::string fmt, ...) __attribute__ ((format(printf, 2, 3)));
+
+  static std::ostream& operator()();
+
+  static void setStream(std::ostream& os) { d_out = os; }
+};/* class Chat */
+
+
+class Trace {
+  std::ostream &d_os;
+
+public:
+  static void operator()(const char* tag, const char*);
+  static void operator()(const char* tag, std::string);
+  static void operator()(string tag, const char*);
+  static void operator()(string tag, std::string);
+
+  static void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3))) {
+    va_list vl;
+    va_start(vl, fmt);
+    vfprintf(buf, 1024, fmt, vl);
+    va_end(vl);
+  }
+  static void printf(const char* tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3))) {
+  }
+  static void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3))) {
+  }
+  static void printf(std::string tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3))) {
+  }
+
+  static std::ostream& operator()(const char* tag);
+  static std::ostream& operator()(std::string tag);
+
+  static void on (const char* tag) { d_tags.insert(std::string(tag)); };
+  static void on (std::string tag) { d_tags.insert(tag);              };
+  static void off(const char* tag) { d_tags.erase (std::string(tag)); };
+  static void off(std::string tag) { d_tags.erase (tag);              };
+
+  static void setStream(std::ostream& os) { d_out = os; }
+};/* class Trace */
+
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__OUTPUT_H */