fixed CNF conversion, and more modular; CNF conversion command line option; various cleanups; renamed numChildren() to getNumChildren() and added it to NodeBuilder interface; fancier, non-exponential CNF conversion with variable introduction is still buggy (?)

20 files changed, 1086 insertions, 143 deletions

diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
index 6cbb41812..50c9edcd2 100644
--- a/src/expr/expr.cpp
+++ b/src/expr/expr.cpp
@@ -85,9 +85,9 @@ Kind Expr::getKind() const {
   return d_node->getKind();
 }
 
-size_t Expr::numChildren() const {
+size_t Expr::getNumChildren() const {
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
-  return d_node->numChildren();
+  return d_node->getNumChildren();
 }
 
 std::string Expr::toString() const {
diff --git a/src/expr/expr.h b/src/expr/expr.h
index eb4d1ce03..6f7330ed0 100644
--- a/src/expr/expr.h
+++ b/src/expr/expr.h
@@ -104,7 +104,7 @@ public:
    * Returns the number of children of this expression.
    * @return the number of children
    */
-  size_t numChildren() const;
+  size_t getNumChildren() const;
 
   /**
    * Returns the string representation of the expression.
diff --git a/src/expr/kind.h b/src/expr/kind.h
index ea9dbd662..8ba282f0f 100644
--- a/src/expr/kind.h
+++ b/src/expr/kind.h
@@ -88,7 +88,7 @@ inline std::ostream& operator<<(std::ostream& out, CVC4::Kind k) {
   case MINUS:          out << "MINUS";          break;
   case MULT:           out << "MULT";           break;
 
-  default:             out << "UNKNOWNKIND!";   break;
+  default:             out << "UNKNOWNKIND!" << int(k); break;
   }
 
   return out;
diff --git a/src/expr/node.h b/src/expr/node.h
index b40443923..67af6aa18 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -120,6 +120,7 @@ public:
   Node& operator=(const Node&);
 
   uint64_t hash() const;
+  uint64_t getId() const { return d_ev->getId(); }
 
   Node eqExpr(const Node& right) const;
   Node notExpr() const;
@@ -136,7 +137,7 @@ public:
 
   inline Kind getKind() const;
 
-  inline size_t numChildren() const;
+  inline size_t getNumChildren() const;
 
   static Node null();
 
@@ -165,9 +166,7 @@ inline bool Node::operator<(const Node& e) const {
   return d_ev->d_id < e.d_ev->d_id;
 }
 
-inline std::ostream& 
-
-operator<<(std::ostream& out, const Node& e) {
+inline std::ostream& operator<<(std::ostream& out, const Node& e) {
   e.toStream(out);
   return out;
 }
@@ -216,7 +215,7 @@ inline Node::const_iterator Node::end() const {
   return d_ev->end();
 }
 
-inline size_t Node::numChildren() const {
+inline size_t Node::getNumChildren() const {
   return d_ev->d_nchildren;
 }
 
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 13aa0b0ff..7c6405ace 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -36,6 +36,9 @@ namespace CVC4 {
 
 namespace CVC4 {
 
+template <unsigned nchild_thresh>
+inline std::ostream& operator<<(std::ostream&, const NodeBuilder<nchild_thresh>&);
+
 class AndNodeBuilder;
 class OrNodeBuilder;
 class PlusNodeBuilder;
@@ -122,6 +125,10 @@ public:
     return d_ev->ev_end();
   }
 
+  unsigned getNumChildren() const {
+    return d_ev->getNumChildren();
+  }
+
   // Compound expression constructors
   /*
   NodeBuilder& eqExpr(const Node& right);
@@ -189,6 +196,10 @@ public:
   // not const
   operator Node();
 
+  inline void toStream(std::ostream& out) const {
+    d_ev->toStream(out);
+  }
+
   /*
   AndNodeBuilder   operator&&(Node);
   OrNodeBuilder    operator||(Node);
@@ -440,7 +451,7 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm, Kind k) :
 template <unsigned nchild_thresh>
 inline NodeBuilder<nchild_thresh>::~NodeBuilder() {
   Assert(d_used, "NodeBuilder unused at destruction");
-  
+
   return;
   /*
   for(iterator i = d_ev->ev_begin();
@@ -566,7 +577,7 @@ NodeBuilder<nchild_thresh>::operator Node() {// not const
 
   // this inserts into the NodeManager;
   // return the result of lookup() in case another thread beat us to it
-  if(ev->numChildren()) {
+  if(ev->getNumChildren()) {
     Debug("prop") << "ev first child: " << *ev->ev_begin() << std::endl;
   }
   Node n = d_nm->lookup(d_hash, ev);
@@ -574,6 +585,13 @@ NodeBuilder<nchild_thresh>::operator Node() {// not const
   return n;
 }
 
+template <unsigned nchild_thresh>
+inline std::ostream& operator<<(std::ostream& out,
+                                const NodeBuilder<nchild_thresh>& b) {
+  b.toStream(out);
+  return out;
+}
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__NODE_BUILDER_H */
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index a307eb11f..0d3fecac6 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -40,7 +40,7 @@ Node NodeManager::lookup(uint64_t hash, NodeValue* ev) {
         continue;
       }
 
-      if(ev->numChildren() != j->numChildren()) {
+      if(ev->getNumChildren() != j->getNumChildren()) {
         continue;
       }
 
@@ -81,7 +81,7 @@ NodeValue* NodeManager::lookupNoInsert(uint64_t hash, NodeValue* ev) {
         continue;
       }
 
-      if(ev->numChildren() != j->numChildren()) {
+      if(ev->getNumChildren() != j->getNumChildren()) {
         continue;
       }
 
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 84df5957a..847b6b153 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -170,7 +170,8 @@ public:
 
   unsigned getId() const { return d_id; }
   Kind getKind() const { return (Kind) d_kind; }
-  unsigned numChildren() const { return d_nchildren; }
+  unsigned getNumChildren() const { return d_nchildren; }
+
   std::string toString() const;
   void toStream(std::ostream& out) const;
 };
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index 123bc3204..388e58a3b 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -46,9 +46,16 @@ Languages currently supported as arguments to the -L / --lang option:\n\
   smt | smtlib  SMT-LIB format\n\
 ";
 
+static const char cnf_help[] = "\
+CNF conversions currently supported as arguments to the --cnf option:\n\
+  direct  put in equiv. CNF directly (exp. blow up in # clauses, no new vars)\n\
+  var     variable-introduction method (new vars, no exp. blow up in # clauses)\n\
+";
+
 // FIXME add a comment here describing the purpose of this
 enum OptionValue {
-  SMTCOMP = 256, /* no clash with char options */
+  CNF = 256, /* no clash with char options */
+  SMTCOMP,
   STATS
 };/* enum OptionValue */
 
@@ -61,6 +68,7 @@ static struct option cmdlineOptions[] = {
   { "quiet"  , no_argument      , NULL, 'q'     },
   { "lang"   , required_argument, NULL, 'L'     },
   { "debug"  , required_argument, NULL, 'd'     },
+  { "cnf"    , required_argument, NULL, CNF     },
   { "smtcomp", no_argument      , NULL, SMTCOMP },
   { "stats"  , no_argument      , NULL, STATS   }
 };/* if you add things to the above, please remember to update usage.h! */
@@ -117,6 +125,21 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti
       fputs(lang_help, stdout);
       exit(1);
 
+    case CNF:
+      if(!strcmp(optarg, "direct")) {
+        opts->d_cnfConversion = CNF_DIRECT_EXPONENTIAL;
+        break;
+      } else if(!strcmp(optarg, "var")) {
+        opts->d_cnfConversion = CNF_VAR_INTRODUCTION;
+        break;
+      } else if(strcmp(optarg, "help")) {
+        throw OptionException(string("unknown CNF conversion for --cnf: `") +
+                              optarg + "'.  Try --cnf help.");
+      }
+
+      fputs(cnf_help, stdout);
+      exit(1);
+
     case 'd':
       Debug.on(optarg);
       /* fall-through */
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index afc84a5b4..16b807904 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -56,7 +56,7 @@ static void doAtom(SimpSolver* minisat, map<Node, Var>* vars, Node e, vec<Lit>*
     return;
   }
   if(e.getKind() == NOT) {
-    Assert(e.numChildren() == 1);
+    Assert(e.getNumChildren() == 1);
     Node child = *e.begin();
     Assert(child.getKind() == VARIABLE);
     map<Node, Var>::iterator v = vars->find(child);
diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am
index bd75bacab..fa7fed5f1 100644
--- a/src/smt/Makefile.am
+++ b/src/smt/Makefile.am
@@ -7,4 +7,7 @@ noinst_LTLIBRARIES = libsmt.la
 
 libsmt_la_SOURCES = \
 	smt_engine.cpp \
-	smt_engine.h
+	smt_engine.h \
+	cnf_converter.h \
+	cnf_converter.cpp \
+	cnf_conversion.h
diff --git a/src/smt/Makefile.in b/src/smt/Makefile.in
new file mode 100644
index 000000000..3eebba8e1
--- /dev/null
+++ b/src/smt/Makefile.in
@@ -0,0 +1,517 @@
+# Makefile.in generated by automake 1.11 from Makefile.am.
+# @configure_input@
+
+# Copyright (C) 1994, 1995, 1996, 1997, 1998, 1999, 2000, 2001, 2002,
+# 2003, 2004, 2005, 2006, 2007, 2008, 2009  Free Software Foundation,
+# Inc.
+# This Makefile.in is free software; the Free Software Foundation
+# gives unlimited permission to copy and/or distribute it,
+# with or without modifications, as long as this notice is preserved.
+
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY, to the extent permitted by law; without
+# even the implied warranty of MERCHANTABILITY or FITNESS FOR A
+# PARTICULAR PURPOSE.
+
+@SET_MAKE@
+
+VPATH = @srcdir@
+pkgdatadir = $(datadir)/@PACKAGE@
+pkgincludedir = $(includedir)/@PACKAGE@
+pkglibdir = $(libdir)/@PACKAGE@
+pkglibexecdir = $(libexecdir)/@PACKAGE@
+am__cd = CDPATH="$${ZSH_VERSION+.}$(PATH_SEPARATOR)" && cd
+install_sh_DATA = $(install_sh) -c -m 644
+install_sh_PROGRAM = $(install_sh) -c
+install_sh_SCRIPT = $(install_sh) -c
+INSTALL_HEADER = $(INSTALL_DATA)
+transform = $(program_transform_name)
+NORMAL_INSTALL = :
+PRE_INSTALL = :
+POST_INSTALL = :
+NORMAL_UNINSTALL = :
+PRE_UNINSTALL = :
+POST_UNINSTALL = :
+build_triplet = @build@
+host_triplet = @host@
+target_triplet = @target@
+subdir = src/smt
+DIST_COMMON = $(srcdir)/Makefile.am $(srcdir)/Makefile.in
+ACLOCAL_M4 = $(top_srcdir)/aclocal.m4
+am__aclocal_m4_deps = $(top_srcdir)/config/antlr.m4 \
+	$(top_srcdir)/config/cvc4.m4 $(top_srcdir)/config/libtool.m4 \
+	$(top_srcdir)/config/ltoptions.m4 \
+	$(top_srcdir)/config/ltsugar.m4 \
+	$(top_srcdir)/config/ltversion.m4 \
+	$(top_srcdir)/config/lt~obsolete.m4 $(top_srcdir)/configure.ac
+am__configure_deps = $(am__aclocal_m4_deps) $(CONFIGURE_DEPENDENCIES) \
+	$(ACLOCAL_M4)
+mkinstalldirs = $(install_sh) -d
+CONFIG_HEADER = $(top_builddir)/config.h
+CONFIG_CLEAN_FILES =
+CONFIG_CLEAN_VPATH_FILES =
+LTLIBRARIES = $(noinst_LTLIBRARIES)
+libsmt_la_LIBADD =
+am_libsmt_la_OBJECTS = smt_engine.lo cnf_converter.lo
+libsmt_la_OBJECTS = $(am_libsmt_la_OBJECTS)
+DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir)
+depcomp = $(SHELL) $(top_srcdir)/config/depcomp
+am__depfiles_maybe = depfiles
+am__mv = mv -f
+CXXCOMPILE = $(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \
+	$(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS)
+LTCXXCOMPILE = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+	--mode=compile $(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \
+	$(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS)
+CXXLD = $(CXX)
+CXXLINK = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+	--mode=link $(CXXLD) $(AM_CXXFLAGS) $(CXXFLAGS) $(AM_LDFLAGS) \
+	$(LDFLAGS) -o $@
+COMPILE = $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) \
+	$(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+LTCOMPILE = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+	--mode=compile $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \
+	$(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+CCLD = $(CC)
+LINK = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+	--mode=link $(CCLD) $(AM_CFLAGS) $(CFLAGS) $(AM_LDFLAGS) \
+	$(LDFLAGS) -o $@
+SOURCES = $(libsmt_la_SOURCES)
+DIST_SOURCES = $(libsmt_la_SOURCES)
+ETAGS = etags
+CTAGS = ctags
+DISTFILES = $(DIST_COMMON) $(DIST_SOURCES) $(TEXINFOS) $(EXTRA_DIST)
+ACLOCAL = @ACLOCAL@
+AMTAR = @AMTAR@
+ANTLR = @ANTLR@
+ANTLR_INCLUDES = @ANTLR_INCLUDES@
+ANTLR_LDFLAGS = @ANTLR_LDFLAGS@
+AR = @AR@
+AS = @AS@
+AUTOCONF = @AUTOCONF@
+AUTOHEADER = @AUTOHEADER@
+AUTOMAKE = @AUTOMAKE@
+AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
+CC = @CC@
+CCDEPMODE = @CCDEPMODE@
+CFLAGS = @CFLAGS@
+CPP = @CPP@
+CPPFLAGS = @CPPFLAGS@
+CVC4_LIBRARY_RELEASE_CODE = @CVC4_LIBRARY_RELEASE_CODE@
+CVC4_LIBRARY_VERSION = @CVC4_LIBRARY_VERSION@
+CVC4_PARSER_LIBRARY_VERSION = @CVC4_PARSER_LIBRARY_VERSION@
+CXX = @CXX@
+CXXCPP = @CXXCPP@
+CXXDEPMODE = @CXXDEPMODE@
+CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
+CXXTESTGEN = @CXXTESTGEN@
+CYGPATH_W = @CYGPATH_W@
+DEFS = @DEFS@
+DEPDIR = @DEPDIR@
+DLLTOOL = @DLLTOOL@
+DOXYGEN = @DOXYGEN@
+DSYMUTIL = @DSYMUTIL@
+DUMPBIN = @DUMPBIN@
+ECHO_C = @ECHO_C@
+ECHO_N = @ECHO_N@
+ECHO_T = @ECHO_T@
+EGREP = @EGREP@
+EXEEXT = @EXEEXT@
+FGREP = @FGREP@
+GREP = @GREP@
+INSTALL = @INSTALL@
+INSTALL_DATA = @INSTALL_DATA@
+INSTALL_PROGRAM = @INSTALL_PROGRAM@
+INSTALL_SCRIPT = @INSTALL_SCRIPT@
+INSTALL_STRIP_PROGRAM = @INSTALL_STRIP_PROGRAM@
+LD = @LD@
+LDFLAGS = @LDFLAGS@
+LIBOBJS = @LIBOBJS@
+LIBS = @LIBS@
+LIBTOOL = @LIBTOOL@
+LIPO = @LIPO@
+LN_S = @LN_S@
+LTLIBOBJS = @LTLIBOBJS@
+MAKEINFO = @MAKEINFO@
+MKDIR_P = @MKDIR_P@
+NM = @NM@
+NMEDIT = @NMEDIT@
+OBJDUMP = @OBJDUMP@
+OBJEXT = @OBJEXT@
+OTOOL = @OTOOL@
+OTOOL64 = @OTOOL64@
+PACKAGE = @PACKAGE@
+PACKAGE_BUGREPORT = @PACKAGE_BUGREPORT@
+PACKAGE_NAME = @PACKAGE_NAME@
+PACKAGE_STRING = @PACKAGE_STRING@
+PACKAGE_TARNAME = @PACKAGE_TARNAME@
+PACKAGE_URL = @PACKAGE_URL@
+PACKAGE_VERSION = @PACKAGE_VERSION@
+PATH_SEPARATOR = @PATH_SEPARATOR@
+PERL = @PERL@
+RANLIB = @RANLIB@
+SED = @SED@
+SET_MAKE = @SET_MAKE@
+SHELL = @SHELL@
+STRIP = @STRIP@
+TEST_CPPFLAGS = @TEST_CPPFLAGS@
+TEST_CXXFLAGS = @TEST_CXXFLAGS@
+TEST_LDFLAGS = @TEST_LDFLAGS@
+VERSION = @VERSION@
+abs_builddir = @abs_builddir@
+abs_srcdir = @abs_srcdir@
+abs_top_builddir = @abs_top_builddir@
+abs_top_srcdir = @abs_top_srcdir@
+ac_ct_CC = @ac_ct_CC@
+ac_ct_CXX = @ac_ct_CXX@
+ac_ct_DUMPBIN = @ac_ct_DUMPBIN@
+am__include = @am__include@
+am__leading_dot = @am__leading_dot@
+am__quote = @am__quote@
+am__tar = @am__tar@
+am__untar = @am__untar@
+bindir = @bindir@
+build = @build@
+build_alias = @build_alias@
+build_cpu = @build_cpu@
+build_os = @build_os@
+build_vendor = @build_vendor@
+builddir = @builddir@
+datadir = @datadir@
+datarootdir = @datarootdir@
+docdir = @docdir@
+dvidir = @dvidir@
+exec_prefix = @exec_prefix@
+host = @host@
+host_alias = @host_alias@
+host_cpu = @host_cpu@
+host_os = @host_os@
+host_vendor = @host_vendor@
+htmldir = @htmldir@
+includedir = @includedir@
+infodir = @infodir@
+install_sh = @install_sh@
+libdir = @libdir@
+libexecdir = @libexecdir@
+localedir = @localedir@
+localstatedir = @localstatedir@
+lt_ECHO = @lt_ECHO@
+mandir = @mandir@
+mk_include = @mk_include@
+mkdir_p = @mkdir_p@
+oldincludedir = @oldincludedir@
+pdfdir = @pdfdir@
+prefix = @prefix@
+program_transform_name = @program_transform_name@
+psdir = @psdir@
+sbindir = @sbindir@
+sharedstatedir = @sharedstatedir@
+srcdir = @srcdir@
+sysconfdir = @sysconfdir@
+target = @target@
+target_alias = @target_alias@
+target_cpu = @target_cpu@
+target_os = @target_os@
+target_vendor = @target_vendor@
+top_build_prefix = @top_build_prefix@
+top_builddir = @top_builddir@
+top_srcdir = @top_srcdir@
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@srcdir@/../include -I@srcdir@/..
+
+AM_CXXFLAGS = -Wall -fvisibility=hidden
+noinst_LTLIBRARIES = libsmt.la
+libsmt_la_SOURCES = \
+	smt_engine.cpp \
+	smt_engine.h \
+	cnf_converter.h \
+	cnf_converter.cpp \
+	cnf_conversion.h
+
+all: all-am
+
+.SUFFIXES:
+.SUFFIXES: .cpp .lo .o .obj
+$(srcdir)/Makefile.in:  $(srcdir)/Makefile.am  $(am__configure_deps)
+	@for dep in $?; do \
+	  case '$(am__configure_deps)' in \
+	    *$$dep*) \
+	      ( cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh ) \
+	        && { if test -f $@; then exit 0; else break; fi; }; \
+	      exit 1;; \
+	  esac; \
+	done; \
+	echo ' cd $(top_srcdir) && $(AUTOMAKE) --gnu src/smt/Makefile'; \
+	$(am__cd) $(top_srcdir) && \
+	  $(AUTOMAKE) --gnu src/smt/Makefile
+.PRECIOUS: Makefile
+Makefile: $(srcdir)/Makefile.in $(top_builddir)/config.status
+	@case '$?' in \
+	  *config.status*) \
+	    cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh;; \
+	  *) \
+	    echo ' cd $(top_builddir) && $(SHELL) ./config.status $(subdir)/$@ $(am__depfiles_maybe)'; \
+	    cd $(top_builddir) && $(SHELL) ./config.status $(subdir)/$@ $(am__depfiles_maybe);; \
+	esac;
+
+$(top_builddir)/config.status: $(top_srcdir)/configure $(CONFIG_STATUS_DEPENDENCIES)
+	cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh
+
+$(top_srcdir)/configure:  $(am__configure_deps)
+	cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh
+$(ACLOCAL_M4):  $(am__aclocal_m4_deps)
+	cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh
+$(am__aclocal_m4_deps):
+
+clean-noinstLTLIBRARIES:
+	-test -z "$(noinst_LTLIBRARIES)" || rm -f $(noinst_LTLIBRARIES)
+	@list='$(noinst_LTLIBRARIES)'; for p in $$list; do \
+	  dir="`echo $$p | sed -e 's|/[^/]*$$||'`"; \
+	  test "$$dir" != "$$p" || dir=.; \
+	  echo "rm -f \"$${dir}/so_locations\""; \
+	  rm -f "$${dir}/so_locations"; \
+	done
+libsmt.la: $(libsmt_la_OBJECTS) $(libsmt_la_DEPENDENCIES) 
+	$(CXXLINK)  $(libsmt_la_OBJECTS) $(libsmt_la_LIBADD) $(LIBS)
+
+mostlyclean-compile:
+	-rm -f *.$(OBJEXT)
+
+distclean-compile:
+	-rm -f *.tab.c
+
+@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/cnf_converter.Plo@am__quote@
+@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/smt_engine.Plo@am__quote@
+
+.cpp.o:
+@am__fastdepCXX_TRUE@	$(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $<
+@am__fastdepCXX_TRUE@	$(am__mv) $(DEPDIR)/$*.Tpo $(DEPDIR)/$*.Po
+@AMDEP_TRUE@@am__fastdepCXX_FALSE@	source='$<' object='$@' libtool=no @AMDEPBACKSLASH@
+@AMDEP_TRUE@@am__fastdepCXX_FALSE@	DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@
+@am__fastdepCXX_FALSE@	$(CXXCOMPILE) -c -o $@ $<
+
+.cpp.obj:
+@am__fastdepCXX_TRUE@	$(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ `$(CYGPATH_W) '$<'`
+@am__fastdepCXX_TRUE@	$(am__mv) $(DEPDIR)/$*.Tpo $(DEPDIR)/$*.Po
+@AMDEP_TRUE@@am__fastdepCXX_FALSE@	source='$<' object='$@' libtool=no @AMDEPBACKSLASH@
+@AMDEP_TRUE@@am__fastdepCXX_FALSE@	DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@
+@am__fastdepCXX_FALSE@	$(CXXCOMPILE) -c -o $@ `$(CYGPATH_W) '$<'`
+
+.cpp.lo:
+@am__fastdepCXX_TRUE@	$(LTCXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $<
+@am__fastdepCXX_TRUE@	$(am__mv) $(DEPDIR)/$*.Tpo $(DEPDIR)/$*.Plo
+@AMDEP_TRUE@@am__fastdepCXX_FALSE@	source='$<' object='$@' libtool=yes @AMDEPBACKSLASH@
+@AMDEP_TRUE@@am__fastdepCXX_FALSE@	DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@
+@am__fastdepCXX_FALSE@	$(LTCXXCOMPILE) -c -o $@ $<
+
+mostlyclean-libtool:
+	-rm -f *.lo
+
+clean-libtool:
+	-rm -rf .libs _libs
+
+ID: $(HEADERS) $(SOURCES) $(LISP) $(TAGS_FILES)
+	list='$(SOURCES) $(HEADERS) $(LISP) $(TAGS_FILES)'; \
+	unique=`for i in $$list; do \
+	    if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \
+	  done | \
+	  $(AWK) '{ files[$$0] = 1; nonempty = 1; } \
+	      END { if (nonempty) { for (i in files) print i; }; }'`; \
+	mkid -fID $$unique
+tags: TAGS
+
+TAGS:  $(HEADERS) $(SOURCES)  $(TAGS_DEPENDENCIES) \
+		$(TAGS_FILES) $(LISP)
+	set x; \
+	here=`pwd`; \
+	list='$(SOURCES) $(HEADERS)  $(LISP) $(TAGS_FILES)'; \
+	unique=`for i in $$list; do \
+	    if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \
+	  done | \
+	  $(AWK) '{ files[$$0] = 1; nonempty = 1; } \
+	      END { if (nonempty) { for (i in files) print i; }; }'`; \
+	shift; \
+	if test -z "$(ETAGS_ARGS)$$*$$unique"; then :; else \
+	  test -n "$$unique" || unique=$$empty_fix; \
+	  if test $$# -gt 0; then \
+	    $(ETAGS) $(ETAGSFLAGS) $(AM_ETAGSFLAGS) $(ETAGS_ARGS) \
+	      "$$@" $$unique; \
+	  else \
+	    $(ETAGS) $(ETAGSFLAGS) $(AM_ETAGSFLAGS) $(ETAGS_ARGS) \
+	      $$unique; \
+	  fi; \
+	fi
+ctags: CTAGS
+CTAGS:  $(HEADERS) $(SOURCES)  $(TAGS_DEPENDENCIES) \
+		$(TAGS_FILES) $(LISP)
+	list='$(SOURCES) $(HEADERS)  $(LISP) $(TAGS_FILES)'; \
+	unique=`for i in $$list; do \
+	    if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \
+	  done | \
+	  $(AWK) '{ files[$$0] = 1; nonempty = 1; } \
+	      END { if (nonempty) { for (i in files) print i; }; }'`; \
+	test -z "$(CTAGS_ARGS)$$unique" \
+	  || $(CTAGS) $(CTAGSFLAGS) $(AM_CTAGSFLAGS) $(CTAGS_ARGS) \
+	     $$unique
+
+GTAGS:
+	here=`$(am__cd) $(top_builddir) && pwd` \
+	  && $(am__cd) $(top_srcdir) \
+	  && gtags -i $(GTAGS_ARGS) "$$here"
+
+distclean-tags:
+	-rm -f TAGS ID GTAGS GRTAGS GSYMS GPATH tags
+
+distdir: $(DISTFILES)
+	@srcdirstrip=`echo "$(srcdir)" | sed 's/[].[^$$\\*]/\\\\&/g'`; \
+	topsrcdirstrip=`echo "$(top_srcdir)" | sed 's/[].[^$$\\*]/\\\\&/g'`; \
+	list='$(DISTFILES)'; \
+	  dist_files=`for file in $$list; do echo $$file; done | \
+	  sed -e "s|^$$srcdirstrip/||;t" \
+	      -e "s|^$$topsrcdirstrip/|$(top_builddir)/|;t"`; \
+	case $$dist_files in \
+	  */*) $(MKDIR_P) `echo "$$dist_files" | \
+			   sed '/\//!d;s|^|$(distdir)/|;s,/[^/]*$$,,' | \
+			   sort -u` ;; \
+	esac; \
+	for file in $$dist_files; do \
+	  if test -f $$file || test -d $$file; then d=.; else d=$(srcdir); fi; \
+	  if test -d $$d/$$file; then \
+	    dir=`echo "/$$file" | sed -e 's,/[^/]*$$,,'`; \
+	    if test -d "$(distdir)/$$file"; then \
+	      find "$(distdir)/$$file" -type d ! -perm -700 -exec chmod u+rwx {} \;; \
+	    fi; \
+	    if test -d $(srcdir)/$$file && test $$d != $(srcdir); then \
+	      cp -fpR $(srcdir)/$$file "$(distdir)$$dir" || exit 1; \
+	      find "$(distdir)/$$file" -type d ! -perm -700 -exec chmod u+rwx {} \;; \
+	    fi; \
+	    cp -fpR $$d/$$file "$(distdir)$$dir" || exit 1; \
+	  else \
+	    test -f "$(distdir)/$$file" \
+	    || cp -p $$d/$$file "$(distdir)/$$file" \
+	    || exit 1; \
+	  fi; \
+	done
+check-am: all-am
+check: check-am
+all-am: Makefile $(LTLIBRARIES)
+installdirs:
+install: install-am
+install-exec: install-exec-am
+install-data: install-data-am
+uninstall: uninstall-am
+
+install-am: all-am
+	@$(MAKE) $(AM_MAKEFLAGS) install-exec-am install-data-am
+
+installcheck: installcheck-am
+install-strip:
+	$(MAKE) $(AM_MAKEFLAGS) INSTALL_PROGRAM="$(INSTALL_STRIP_PROGRAM)" \
+	  install_sh_PROGRAM="$(INSTALL_STRIP_PROGRAM)" INSTALL_STRIP_FLAG=-s \
+	  `test -z '$(STRIP)' || \
+	    echo "INSTALL_PROGRAM_ENV=STRIPPROG='$(STRIP)'"` install
+mostlyclean-generic:
+
+clean-generic:
+
+distclean-generic:
+	-test -z "$(CONFIG_CLEAN_FILES)" || rm -f $(CONFIG_CLEAN_FILES)
+	-test . = "$(srcdir)" || test -z "$(CONFIG_CLEAN_VPATH_FILES)" || rm -f $(CONFIG_CLEAN_VPATH_FILES)
+
+maintainer-clean-generic:
+	@echo "This command is intended for maintainers to use"
+	@echo "it deletes files that may require special tools to rebuild."
+clean: clean-am
+
+clean-am: clean-generic clean-libtool clean-noinstLTLIBRARIES \
+	mostlyclean-am
+
+distclean: distclean-am
+	-rm -rf ./$(DEPDIR)
+	-rm -f Makefile
+distclean-am: clean-am distclean-compile distclean-generic \
+	distclean-tags
+
+dvi: dvi-am
+
+dvi-am:
+
+html: html-am
+
+html-am:
+
+info: info-am
+
+info-am:
+
+install-data-am:
+
+install-dvi: install-dvi-am
+
+install-dvi-am:
+
+install-exec-am:
+
+install-html: install-html-am
+
+install-html-am:
+
+install-info: install-info-am
+
+install-info-am:
+
+install-man:
+
+install-pdf: install-pdf-am
+
+install-pdf-am:
+
+install-ps: install-ps-am
+
+install-ps-am:
+
+installcheck-am:
+
+maintainer-clean: maintainer-clean-am
+	-rm -rf ./$(DEPDIR)
+	-rm -f Makefile
+maintainer-clean-am: distclean-am maintainer-clean-generic
+
+mostlyclean: mostlyclean-am
+
+mostlyclean-am: mostlyclean-compile mostlyclean-generic \
+	mostlyclean-libtool
+
+pdf: pdf-am
+
+pdf-am:
+
+ps: ps-am
+
+ps-am:
+
+uninstall-am:
+
+.MAKE: install-am install-strip
+
+.PHONY: CTAGS GTAGS all all-am check check-am clean clean-generic \
+	clean-libtool clean-noinstLTLIBRARIES ctags distclean \
+	distclean-compile distclean-generic distclean-libtool \
+	distclean-tags distdir dvi dvi-am html html-am info info-am \
+	install install-am install-data install-data-am install-dvi \
+	install-dvi-am install-exec install-exec-am install-html \
+	install-html-am install-info install-info-am install-man \
+	install-pdf install-pdf-am install-ps install-ps-am \
+	install-strip installcheck installcheck-am installdirs \
+	maintainer-clean maintainer-clean-generic mostlyclean \
+	mostlyclean-compile mostlyclean-generic mostlyclean-libtool \
+	pdf pdf-am ps ps-am tags uninstall uninstall-am
+
+
+# Tell versions [3.59,3.63) of GNU make to not export all variables.
+# Otherwise a system limit (for SysV at least) may be exceeded.
+.NOEXPORT:
diff --git a/src/smt/cnf_conversion.h b/src/smt/cnf_conversion.h
new file mode 100644
index 000000000..924cae063
--- /dev/null
+++ b/src/smt/cnf_conversion.h
@@ -0,0 +1,46 @@
+/*********************                                           -*- C++ -*-  */
+/** cnf_conversion.h
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): none
+ ** 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.
+ **
+ ** A type for describing possible CNF conversions.
+ **/
+
+#ifndef __CVC4__CNF_CONVERSION_H
+#define __CVC4__CNF_CONVERSION_H
+
+namespace CVC4 {
+
+enum CnfConversion {
+  CNF_DIRECT_EXPONENTIAL = 0,
+  CNF_VAR_INTRODUCTION = 1
+};
+
+inline std::ostream& operator<<(std::ostream&, CVC4::CnfConversion) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& out, CVC4::CnfConversion c) {
+  using namespace CVC4;
+
+  switch(c) {
+  case CNF_DIRECT_EXPONENTIAL:
+    out << "CNF_DIRECT_EXPONENTIAL";
+    break;
+  case CNF_VAR_INTRODUCTION:
+    out << "CNF_VAR_INTRODUCTION";
+    break;
+  default:
+    out << "UNKNOWN-CONVERTER!" << int(c);
+  }
+
+  return out;
+}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CNF_CONVERSION_H */
diff --git a/src/smt/cnf_converter.cpp b/src/smt/cnf_converter.cpp
new file mode 100644
index 000000000..c94d62524
--- /dev/null
+++ b/src/smt/cnf_converter.cpp
@@ -0,0 +1,234 @@
+/*********************                                           -*- C++ -*-  */
+/** cnf_converter.cpp
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): none
+ ** 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.
+ **
+ ** A CNF converter for CVC4.
+ **/
+
+#include "smt/cnf_converter.h"
+#include "expr/node_builder.h"
+#include "expr/node.h"
+#include "util/output.h"
+#include "util/Assert.h"
+
+namespace CVC4 {
+namespace smt {
+
+
+static void printAST(std::ostream& out, const Node& n, int indent = 0) {
+  for(int i = 0; i < indent; ++i) {
+    out << "  ";
+  }
+  if(n.getKind() == VARIABLE) {
+    out << "(VARIABLE " << n.getId();
+  } else {
+    out << "(" << n.getKind();
+    if(n.getNumChildren() > 0) {
+      out << std::endl;
+    }
+    for(Node::iterator i = n.begin(); i != n.end(); ++i) {
+      printAST(out, *i, indent + 1);
+    }
+    if(n.getNumChildren() > 0) {
+      for(int i = 0; i < indent; ++i) {
+        out << "  ";
+      }
+    }
+  }
+  out << ")" << std::endl;
+}
+
+
+Node CnfConverter::convert(const Node& e) {
+  Node n;
+
+  if(conversionMapped(e)) {
+    Debug("cnf") << "conversion for " << e << " with id " << e.getId() << " is cached!" << std::endl;
+    n = getConversionMap(e);
+  } else {
+    switch(d_conversion) {
+    case CNF_DIRECT_EXPONENTIAL:
+      n = directConvert(e);
+      break;
+    case CNF_VAR_INTRODUCTION:
+      n = varIntroductionConvert(e);
+      break;
+    default:
+      Unhandled(d_conversion);
+    }
+
+    Debug("cnf") << "mapping conversion " << e << " with id " << e.getId() << " to " << n << " with id " << n.getId() << std::endl;
+    mapConversion(e, n);
+    Assert(conversionMapped(e));
+    Assert(getConversionMap(e) == n);
+  }
+
+  Debug("cnf") << "CONVERTED ================" << std::endl;
+  printAST(Debug("cnf"), e);
+  Debug("cnf") << "TO        ================" << std::endl;
+  printAST(Debug("cnf"), n);
+  Debug("cnf") << "==========================" << std::endl;
+
+  return n;
+}
+
+Node CnfConverter::compressNOT(const Node& e) {
+  Assert(e.getKind() == NOT);
+
+  // short-circuit trivial NOTs
+  if(e[0].getKind() == TRUE) {
+    return d_nm->mkNode(FALSE);
+  } else if(e[0].getKind() == FALSE) {
+    return d_nm->mkNode(TRUE);
+  } else if(e[0].getKind() == NOT) {
+    return convert(e[0][0]);
+  } else {
+    Node f = convert(e[0]);
+    // push NOTs inside of ANDs and ORs
+    if(f.getKind() == AND) {
+      NodeBuilder<> n(OR);
+      for(Node::iterator i = f.begin(); i != f.end(); ++i) {
+        if((*i).getKind() == NOT) {
+          n << (*i)[0];
+        } else {
+          n << d_nm->mkNode(NOT, *i);
+        }
+      }
+      return n;
+    }
+    if(f.getKind() == OR) {
+      NodeBuilder<> n(AND);
+      for(Node::iterator i = f.begin(); i != f.end(); ++i) {
+        if((*i).getKind() == NOT) {
+          n << (*i)[0];
+        } else {
+          n << d_nm->mkNode(NOT, *i);
+        }
+      }
+      return n;
+    }
+    return e;
+  }
+}
+
+
+Node CnfConverter::directConvert(const Node& e) {
+  if(e.getKind() == NOT) {
+    return compressNOT(e);
+  } else if(e.getKind() == AND) {
+    return flatten<AND>(e);
+  } else if(e.getKind() == OR) {
+    Node n = flatten<OR>(e);
+
+    NodeBuilder<> m(OR);
+    directOrHelper(n.begin(), n.end(), m);
+
+    return m;
+  }
+
+  return e;
+}
+
+void CnfConverter::directOrHelper(Node::iterator p, Node::iterator end, NodeBuilder<>& result) {
+  while(p != end) {
+    if((*p).getKind() == AND) {
+      Debug("cnf") << "orHelper: p      " << *p << std::endl;
+      Debug("cnf") << "          end    " << std::endl;
+      Debug("cnf") << "          result " << result << std::endl;
+
+      NodeBuilder<> resultPrefix = result;
+      result = NodeBuilder<>(AND);
+
+      for(Node::iterator i = (*p).begin(); i != (*p).end(); ++i) {
+        NodeBuilder<> r = resultPrefix;
+
+        // is this a double-convert since we did OR flattening before?
+        r << convert(*i);
+        Node::iterator p2 = p;
+        directOrHelper(++p2, end, r);
+
+        result << r;
+      }
+    } else {
+      Debug("cnf") << "orHelper: passing through a conversion of " << *p << std::endl;
+      // is this a double-convert since we did OR flattening before?
+      result << convert(*p);
+    }
+
+    Debug("cnf") << "  ** result now " << result << std::endl;
+
+    ++p;
+  }
+}
+
+Node CnfConverter::varIntroductionConvert(const Node& e) {
+  if(e.getKind() == NOT) {
+    return compressNOT(e);
+  } else if(e.getKind() == AND) {
+    return flatten<AND>(e);
+  } else if(e.getKind() == OR) {
+    Node n = flatten<OR>(e);
+
+    Debug("cnf") << "about to handle an OR:" << std::endl;
+    printAST(Debug("cnf"), n);
+
+    NodeBuilder<> m(AND);
+    NodeBuilder<> extras(OR);
+    varIntroductionOrHelper(n.begin(), n.end(), m, extras);
+
+    if(m.getNumChildren() > 0) {
+      return m << extras;
+    } else {
+      return extras;
+    }
+  }
+
+  return e;
+}
+
+void CnfConverter::varIntroductionOrHelper(Node::iterator p, Node::iterator end, NodeBuilder<>& result, NodeBuilder<>& extras) {
+  while(p != end) {
+    if((*p).getKind() == AND) {
+      Debug("cnf") << "orHelper: p      " << *p << std::endl;
+      printAST(Debug("cnf"), *p);
+      Debug("cnf") << "          end    " << std::endl;
+      Debug("cnf") << "          result " << result << std::endl;
+      Debug("cnf") << "          extras " << extras << std::endl;
+
+      Node var = d_nm->mkVar();
+      extras << var;
+
+      Debug("cnf") << "  introduced var " << var << "(" << var.getId() << ")" << std::endl;
+
+      Node notVar = d_nm->mkNode(NOT, var);
+
+      for(Node::iterator i = (*p).begin(); i != (*p).end(); ++i) {
+        // is this a double-convert since we did OR flattening before?
+        result << d_nm->mkNode(OR, notVar, convert(*i));
+      }
+    } else {
+      // is this a double-convert since we did OR flattening before?
+      Debug("cnf") << "orHelper: p      " << *p << std::endl;
+      Debug("cnf") << "          end    " << std::endl;
+      Debug("cnf") << "          result " << result << std::endl;
+      Debug("cnf") << "          extras " << extras << std::endl;
+      Debug("cnf") << "   passing through" << std::endl;
+      extras << convert(*p);
+    }
+
+    Debug("cnf") << "  ** result now " << result << std::endl;
+    Debug("cnf") << "  ** extras now " << extras << std::endl;
+    ++p;
+  }
+}
+
+}/* CVC4::smt namespace */
+}/* CVC4 namespace */
diff --git a/src/smt/cnf_converter.h b/src/smt/cnf_converter.h
new file mode 100644
index 000000000..d045f4d64
--- /dev/null
+++ b/src/smt/cnf_converter.h
@@ -0,0 +1,152 @@
+/*********************                                           -*- C++ -*-  */
+/** cnf_converter.h
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): none
+ ** 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.
+ **
+ ** A CNF converter for CVC4.
+ **/
+
+#ifndef __CVC4__SMT__CNF_CONVERTER_H
+#define __CVC4__SMT__CNF_CONVERTER_H
+
+#include "expr/node_builder.h"
+#include "expr/node.h"
+#include "smt/cnf_conversion.h"
+
+#include <map>
+
+namespace CVC4 {
+namespace smt {
+
+class CnfConverter {
+
+private:
+
+  /** Our node manager */
+  NodeManager *d_nm;
+
+  /** The type of conversion this converter performs */
+  CVC4::CnfConversion d_conversion;
+
+  /** Map of already-converted Nodes */
+  std::map<Node, Node> d_conversionMap;
+
+  /**
+   * Returns true iff the CNF conversion for the Node was cached
+   * previously.
+   */
+  bool conversionMapped(const Node& n) {
+    return d_conversionMap.find(n) != d_conversionMap.end();
+  }
+
+  /**
+   * Returns true iff the CNF conversion for the Node was cached
+   * previously.
+   */
+  Node getConversionMap(const Node& n) {
+    return d_conversionMap[n];
+  }
+
+  /**
+   * Cache a new CNF conversion.
+   */
+  void mapConversion(const Node& n, const Node& m) {
+    d_conversionMap[n] = m;
+  }
+
+  /**
+   * Compress a NOT: do NNF transformation plus a bit.  Does DNE,
+   * NOT FALSE ==> TRUE, NOT TRUE ==> FALSE, and pushes NOT inside
+   * of ANDs and ORs.  Calls convert() on subnodes.
+   */
+  Node compressNOT(const Node& e);
+
+  /**
+   * Flatten a Node of kind K.  K here is going to be AND or OR.
+   * "Flattening" means to take all children of the Node with the same
+   * kind and hoist their children to the top-level.  So e.g.
+   * (AND (AND x y) (AND (AND z)) w)  ==>  (AND x y z w).
+   */
+  template <CVC4::Kind K>
+  Node flatten(const Node& e);
+
+  /**
+   * Do a direct CNF conversion (with possible exponential blow-up in
+   * the number of clauses).  No new variables are introduced.  The
+   * output is equivalent to the input.
+   */
+  Node directConvert(const Node& e);
+
+  /**
+   * Helper method for "direct" CNF preprocessing.  CNF-converts an OR.
+   */
+  void directOrHelper(Node::iterator p,
+                      Node::iterator end,
+                      NodeBuilder<>& result);
+
+  /**
+   * Do a satisfiability-preserving CNF conversion with variable
+   * introduction.  Doesn't suffer from exponential blow-up in the
+   * number of clauses, but new variables are introduced and the
+   * output is equisatisfiable (but not equivalent) to the input.
+   */
+  Node varIntroductionConvert(const Node& e);
+
+  /**
+   * Helper method for "variable introduction" CNF preprocessing.
+   * CNF-converts an OR.
+   */
+  void varIntroductionOrHelper(Node::iterator p,
+                               Node::iterator end,
+                               NodeBuilder<>& result,
+                               NodeBuilder<>& extras);
+
+public:
+
+  /**
+   * Construct a CnfConverter.
+   */
+  CnfConverter(NodeManager* nm, CVC4::CnfConversion cnv = CNF_VAR_INTRODUCTION) :
+    d_nm(nm),
+    d_conversion(cnv) {}
+
+  /**
+   * Convert an expression into CNF.  If a conversion already exists
+   * for the Node, it is returned.  If a conversion doesn't exist, it
+   * is computed and returned (caching the result).
+   */
+  Node convert(const Node& e);
+
+};/* class CnfConverter */
+
+template <CVC4::Kind K>
+Node CnfConverter::flatten(const Node& e) {
+  Assert(e.getKind() == K);
+
+  NodeBuilder<> n(K);
+
+  for(Node::iterator i = e.begin(); i != e.end(); ++i) {
+    Node f = convert(*i);
+    if(f.getKind() == K) {
+      for(Node::iterator j = f.begin(); j != f.end(); ++j) {
+        n << *j;
+      }
+    } else {
+      n << f;
+    }
+  }
+
+  return n;
+}
+
+}/* CVC4::smt namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__SMT__CNF_CONVERTER_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index db9dc4edf..c0f825462 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -22,12 +22,13 @@ namespace CVC4 {
 
 SmtEngine::SmtEngine(ExprManager* em, Options* opts) throw() :
   d_assertions(),
-  d_public_em(em),
+  d_publicEm(em),
   d_nm(em->getNodeManager()),
   d_opts(opts),
   d_de(),
   d_te(),
-  d_prop(d_de, d_te) {
+  d_prop(d_de, d_te),
+  d_cnfConverter(d_nm, opts->d_cnfConversion) {
 }
 
 SmtEngine::~SmtEngine() {
@@ -38,95 +39,7 @@ void SmtEngine::doCommand(Command* c) {
   c->invoke(this);
 }
 
-void SmtEngine::orHelper(Node::iterator p, Node::iterator end, NodeBuilder<>& result) {
-  if(p == end) {
-    return;
-  } else if((*p).getKind() == AND) {
-    NodeBuilder<> resultPrefix = result;
-    result = NodeBuilder<>(AND);
-
-    for(Node::iterator i = (*p).begin(); i != (*p).end(); ++i) {
-      NodeBuilder<> r = resultPrefix;
-
-      r << preprocess(*i);
-      Node::iterator p2 = p;
-      orHelper(++p2, end, r);
-
-      result << r;
-    }
-  } else {
-    result << preprocess(*p);
-  }
-}
-
 Node SmtEngine::preprocess(const Node& e) {
-  if(e.getKind() == NOT) {
-    // short-circuit trivial NOTs
-    if(e[0].getKind() == TRUE) {
-      return d_nm->mkNode(FALSE);
-    } else if(e[0].getKind() == FALSE) {
-      return d_nm->mkNode(TRUE);
-    } else if(e[0].getKind() == NOT) {
-      return preprocess(e[0][0]);
-    } else {
-      Node f = preprocess(e[0]);
-      // push NOTs inside of ANDs and ORs
-      if(f.getKind() == AND) {
-        NodeBuilder<> n(OR);
-        for(Node::iterator i = f.begin(); i != f.end(); ++i) {
-          if((*i).getKind() == NOT) {
-            n << (*i)[0];
-          } else {
-            n << d_nm->mkNode(NOT, *i);
-          }
-        }
-        return n;
-      }
-      if(f.getKind() == OR) {
-        NodeBuilder<> n(AND);
-        for(Node::iterator i = f.begin(); i != f.end(); ++i) {
-          if((*i).getKind() == NOT) {
-            n << (*i)[0];
-          } else {
-            n << d_nm->mkNode(NOT, *i);
-          }
-        }
-        return n;
-      }
-    }
-  } else if(e.getKind() == AND) {
-    NodeBuilder<> n(AND);
-    // flatten ANDs
-    for(Node::iterator i = e.begin(); i != e.end(); ++i) {
-      Node f = preprocess(*i);
-      if((*i).getKind() == AND) {
-        for(Node::iterator j = f.begin(); j != f.end(); ++j) {
-          n << *j;
-        }
-      } else {
-        n << *i;        
-      }
-    }
-    return n;
-  } else if(e.getKind() == OR) {
-    NodeBuilder<> n(OR);
-    // flatten ORs
-    for(Node::iterator i = e.begin(); i != e.end(); ++i) {
-      if((*i).getKind() == OR) {
-        Node f = preprocess(*i);
-        for(Node::iterator j = f.begin(); j != f.end(); ++j) {
-          n << *j;
-        }
-      }
-    }
-
-    Node nod = n;
-    NodeBuilder<> m(OR);
-    orHelper(nod.begin(), nod.end(), m);
-
-    return m;
-  }
-
   return e;
 }
 
@@ -142,16 +55,55 @@ Node SmtEngine::processAssertionList() {
     asserts << *i;
   }
 
-  return asserts;
+  d_assertions.clear();
+  d_assertions.push_back(asserts);
+  return d_assertions[0];
+}
+
+static void printAST(std::ostream& out, const Node& n, int indent = 0) {
+  for(int i = 0; i < indent; ++i) {
+    out << "  ";
+  }
+  if(n.getKind() == VARIABLE) {
+    out << "(VARIABLE " << n.getId();
+  } else {
+    out << "(" << n.getKind();
+    if(n.getNumChildren() > 0) {
+      out << std::endl;
+    }
+    for(Node::iterator i = n.begin(); i != n.end(); ++i) {
+      printAST(out, *i, indent + 1);
+    }
+    if(n.getNumChildren() > 0) {
+      for(int i = 0; i < indent; ++i) {
+        out << "  ";
+      }
+    }
+  }
+  out << ")" << std::endl;
 }
 
 Result SmtEngine::check() {
+  Debug("smt") << "SMT check()" << std::endl;
   Node asserts = processAssertionList();
-  d_prop.solve(asserts);
+
+  // CNF conversion
+  Debug("cnf") << "preprocessing " << asserts << std::endl;
+  Node assertsOut = d_cnfConverter.convert(asserts);
+  Debug("cnf") << "      and got " << assertsOut << std::endl;
+
+  Debug("smt") << "BEFORE CONVERSION ==" << std::endl;
+  printAST(Debug("smt"), asserts);
+  Debug("smt") << "AFTER CONVERSION ==" << std::endl;
+  printAST(Debug("smt"), assertsOut);
+  Debug("smt") << "===================" << std::endl;
+
+  d_prop.solve(assertsOut);
   return Result(Result::VALIDITY_UNKNOWN);
 }
 
 Result SmtEngine::quickCheck() {
+  Debug("smt") << "SMT quickCheck()" << std::endl;
   processAssertionList();
   return Result(Result::VALIDITY_UNKNOWN);
 }
@@ -162,6 +114,7 @@ void SmtEngine::addFormula(const Node& e) {
 }
 
 Result SmtEngine::checkSat(const BoolExpr& e) {
+  Debug("smt") << "SMT checkSat(" << e << ")" << std::endl;
   NodeManagerScope nms(d_nm);
   Node node_e = preprocess(e.getNode());
   addFormula(node_e);
@@ -169,6 +122,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) {
 }
 
 Result SmtEngine::query(const BoolExpr& e) {
+  Debug("smt") << "SMT query(" << e << ")" << std::endl;
   NodeManagerScope nms(d_nm);
   Node node_e = preprocess(d_nm->mkNode(NOT, e.getNode()));
   addFormula(node_e);
@@ -176,6 +130,7 @@ Result SmtEngine::query(const BoolExpr& e) {
 }
 
 Result SmtEngine::assertFormula(const BoolExpr& e) {
+  Debug("smt") << "SMT assertFormula(" << e << ")" << std::endl;
   NodeManagerScope nms(d_nm);
   Node node_e = preprocess(e.getNode());
   addFormula(node_e);
@@ -183,6 +138,7 @@ Result SmtEngine::assertFormula(const BoolExpr& e) {
 }
 
 Expr SmtEngine::simplify(const Expr& e) {
+  Debug("smt") << "SMT simplify(" << e << ")" << std::endl;
   Expr simplify(const Expr& e);
   Unimplemented();
 }
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index e06a36128..65375ab65 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -29,6 +29,7 @@
 #include "util/options.h"
 #include "prop/prop_engine.h"
 #include "util/decision_engine.h"
+#include "smt/cnf_converter.h"
 
 // In terms of abstraction, this is below (and provides services to)
 // ValidityChecker and above (and requires the services of)
@@ -116,7 +117,7 @@ private:
   std::vector<Node> d_assertions;
 
   /** Our expression manager */
-  ExprManager *d_public_em;
+  ExprManager *d_publicEm;
 
   /** Out internal expression/node manager */
   NodeManager *d_nm;
@@ -133,6 +134,9 @@ private:
   /** The propositional engine */
   PropEngine d_prop;
 
+  /** The CNF converter in use */
+  CVC4::smt::CnfConverter d_cnfConverter;
+
   /**
    * Pre-process an Node.  This is expected to be highly-variable,
    * with a lot of "source-level configurability" to add multiple
@@ -165,11 +169,6 @@ private:
    */
   Node processAssertionList();
 
-  /**
-   * Helper method for CNF preprocessing.  CNF-converts an OR.
-   */
-  void orHelper(Node::iterator p, Node::iterator end, NodeBuilder<>& result);
-
 };/* class SmtEngine */
 
 }/* CVC4 namespace */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 1372616ec..f0db8a7ae 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -62,12 +62,12 @@ public:
   /**
    * Assert a literal in the current context.
    */
-  virtual void assert(Literal) = 0;
+  void assert(Literal);
 
   /**
-   * Check the current assignment's consistency.  Return false iff inconsistent.
+   * Check the current assignment's consistency.
    */
-  virtual bool check(Effort level = FULL_EFFORT) = 0;
+  virtual void check(Effort level = FULL_EFFORT) = 0;
 
   /**
    * T-propagate new literal assignments in the current context.
diff --git a/src/util/options.h b/src/util/options.h
index d6c4e9009..57b20c47f 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -18,6 +18,7 @@
 
 #include <iostream>
 #include "parser/parser.h"
+#include "smt/cnf_conversion.h"
 
 namespace CVC4 {
 
@@ -38,26 +39,20 @@ struct Options {
   /* with 3, the solver is slowed down by all the scrolling */
   int verbosity;
 
-  /** The input language option */
-  enum InputLanguage {
-    /** The SMTLIB input language */
-    LANG_SMTLIB,
-    /** The CVC4 input language */
-    LANG_CVC4,
-    /** Auto-detect the language */
-    LANG_AUTO
-  };
-
   /** The input language */
   parser::Parser::InputLanguage lang;
 
+  /** The CNF conversion */
+  CVC4::CnfConversion d_cnfConversion;
+
   Options() : binary_name(),
               smtcomp_mode(false),
               statistics(false),
               out(0),
               err(0),
               verbosity(0),
-              lang(parser::Parser::LANG_AUTO)
+              lang(parser::Parser::LANG_AUTO),
+              d_cnfConversion(CVC4::CNF_DIRECT_EXPONENTIAL)
   {}
 };/* struct Options */
 
diff --git a/test/regress/simple.cvc b/test/regress/simple.cvc
index c1a5dd840..3566053d9 100644
--- a/test/regress/simple.cvc
+++ b/test/regress/simple.cvc
@@ -2,5 +2,5 @@ x0, x1, x2, x3 : BOOLEAN;
 ASSERT x1 OR NOT x0;
 ASSERT x0 OR NOT x3;
 ASSERT x3 OR x2;
-ASSERT NOT x1;
+ASSERT x1 AND NOT x1;
 QUERY x2;
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 7cb744d02..5e4e1bb34 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -234,7 +234,7 @@ public:
     
 
     TS_ASSERT(EQUAL == eq.getKind());
-    TS_ASSERT(2     == eq.numChildren());
+    TS_ASSERT(2     == eq.getNumChildren());
 
     TS_ASSERT(*(eq.begin()) == left);
     TS_ASSERT(*(++eq.begin()) == right);
@@ -247,7 +247,7 @@ public:
     Node parent = child.notExpr();
 
     TS_ASSERT(NOT == parent.getKind());
-    TS_ASSERT(1   == parent.numChildren());
+    TS_ASSERT(1   == parent.getNumChildren());
 
     TS_ASSERT(*(parent.begin()) == child);
     
@@ -261,7 +261,7 @@ public:
     
 
     TS_ASSERT(AND == eq.getKind());
-    TS_ASSERT(2   == eq.numChildren());
+    TS_ASSERT(2   == eq.getNumChildren());
 
     TS_ASSERT(*(eq.begin()) == left);
     TS_ASSERT(*(++eq.begin()) == right);
@@ -277,7 +277,7 @@ public:
     
 
     TS_ASSERT(OR  == eq.getKind());
-    TS_ASSERT(2   == eq.numChildren());
+    TS_ASSERT(2   == eq.getNumChildren());
 
     TS_ASSERT(*(eq.begin()) == left);
     TS_ASSERT(*(++eq.begin()) == right);
@@ -294,7 +294,7 @@ public:
     
 
     TS_ASSERT(ITE  == ite.getKind());
-    TS_ASSERT(3    == ite.numChildren());
+    TS_ASSERT(3    == ite.getNumChildren());
 
     TS_ASSERT(*(ite.begin()) == cnd);
     TS_ASSERT(*(++ite.begin()) == thenBranch);
@@ -310,7 +310,7 @@ public:
     
 
     TS_ASSERT(IFF == eq.getKind());
-    TS_ASSERT(2   == eq.numChildren());
+    TS_ASSERT(2   == eq.getNumChildren());
 
     TS_ASSERT(*(eq.begin()) == left);
     TS_ASSERT(*(++eq.begin()) == right);
@@ -325,7 +325,7 @@ public:
     
 
     TS_ASSERT(IMPLIES == eq.getKind());
-    TS_ASSERT(2 == eq.numChildren());
+    TS_ASSERT(2 == eq.getNumChildren());
 
     TS_ASSERT(*(eq.begin()) == left);
     TS_ASSERT(*(++eq.begin()) == right);
@@ -339,7 +339,7 @@ public:
     
 
     TS_ASSERT(XOR == eq.getKind());
-    TS_ASSERT(2   == eq.numChildren());
+    TS_ASSERT(2   == eq.getNumChildren());
 
     TS_ASSERT(*(eq.begin()) == left);
     TS_ASSERT(*(++eq.begin()) == right);
@@ -381,22 +381,22 @@ public:
       nbz << Node::null();
     }
     Node result = nbz;
-    TS_ASSERT( N == result.numChildren());
+    TS_ASSERT( N == result.getNumChildren());
   }
 
   void testNumChildren(){
-    /*inline size_t numChildren() const;*/
+    /*inline size_t getNumChildren() const;*/
 
     //test 0
-    TS_ASSERT(0 == (Node::null()).numChildren());
+    TS_ASSERT(0 == (Node::null()).getNumChildren());
 
     //test 1
 
-    TS_ASSERT(1 == (Node::null().notExpr()).numChildren());
+    TS_ASSERT(1 == (Node::null().notExpr()).getNumChildren());
 
     //test 2
 
-    TS_ASSERT(2 == (Node::null().andExpr(Node::null())).numChildren() );
+    TS_ASSERT(2 == (Node::null().andExpr(Node::null())).getNumChildren() );
 
     //Bigger tests