Switched cnf conversion to go through CnfStream.

6 files changed, 8 insertions, 706 deletions

diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am
index fa7fed5f1..a2da2c949 100644
--- a/src/smt/Makefile.am
+++ b/src/smt/Makefile.am
@@ -7,7 +7,4 @@ noinst_LTLIBRARIES = libsmt.la
 
 libsmt_la_SOURCES = \
 	smt_engine.cpp \
-	smt_engine.h \
-	cnf_converter.h \
-	cnf_converter.cpp \
-	cnf_conversion.h
+	smt_engine.h 
diff --git a/src/smt/cnf_conversion.h b/src/smt/cnf_conversion.h
deleted file mode 100644
index 924cae063..000000000
--- a/src/smt/cnf_conversion.h
+++ /dev/null
@@ -1,46 +0,0 @@
-/*********************                                           -*- 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
deleted file mode 100644
index 7c53e9b04..000000000
--- a/src/smt/cnf_converter.cpp
+++ /dev/null
@@ -1,431 +0,0 @@
-/*********************                                           -*- 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) {
-  if(d_conversion == CNF_DIRECT_EXPONENTIAL) {
-    return doConvert(e, NULL);
-  }
-
-  NodeBuilder<> b(AND);
-  Node f = doConvert(e, &b);
-
-  Debug("cnf") << "side conditions are:\n";
-  NodeBuilder<> c = b;
-  printAST(Debug("cnf"), c);
-
-  if(f.getKind() == AND) {
-    for(Node::iterator i = f.begin(); i != f.end(); ++i) {
-      Debug("cnf") << "adding condition:\n";
-      printAST(Debug("cnf"), *i);
-      b << *i;
-    }
-  } else {
-    Debug("cnf") << "adding condition:\n";
-    printAST(Debug("cnf"), f);
-    b << f;
-  }
-  return b;
-}
-
-Node CnfConverter::doConvert(const Node& e, NodeBuilder<>* sideConditions) {
-  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:
-      Debug("cnf") << "direct conversion for " << e << " with id " << e.getId() << " is being computed!" << std::endl;
-      n = directConvert(e, sideConditions);
-      break;
-
-    case CNF_VAR_INTRODUCTION: {
-      Debug("cnf") << "var-intro conversion for " << e << " with id " << e.getId() << " is being computed!" << std::endl;
-      std::vector<Node> v;
-      n = varIntroductionConvert(e, sideConditions);
-      Debug("cnf") << "got" << std::endl;
-      printAST(Debug("cnf"), n);
-
-      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, NodeBuilder<>* sideConditions) {
-  Assert(e.getKind() == NOT);
-
-  Node f = doConvert(e[0], sideConditions);
-
-  Debug("stari") << "compress-not " << e.getId() << "\n";
-
-  // short-circuit trivial NOTs
-  if(f.getKind() == TRUE) {
-    return d_nm->mkNode(FALSE);
-  } else if(f.getKind() == FALSE) {
-    return d_nm->mkNode(TRUE);
-  } else if(f.getKind() == NOT) {
-    return doConvert(f[0], sideConditions);
-  } else if(f.getKind() == AND) {
-    Debug("stari") << "not-converting a NOT AND\nstarted with\n";
-    printAST(Debug("stari"), e[0]);
-    Debug("stari") << "now have\n";
-    printAST(Debug("stari"), f);
-    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;
-  } else 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 {
-    return d_nm->mkNode(NOT, f);
-  }
-}
-
-
-Node CnfConverter::directConvert(const Node& e, NodeBuilder<>* sideConditions) {
-  switch(e.getKind()) {
-
-  case NOT:
-    return compressNOT(e, sideConditions);
-
-  case AND:
-    return flatten<AND>(e, sideConditions);
-
-  case OR: {
-    Node n = flatten<OR>(e, sideConditions);
-
-    NodeBuilder<> m(OR);
-    Debug("dor") << "calling directOrHelper on\n";
-    printAST(Debug("dor"), n);
-    directOrHelper(n.begin(), n.end(), m, sideConditions);
-
-    return m;
-  }
-
-  case IMPLIES: {
-    Assert( e.getNumChildren() == 2 );
-    // just turn  x IMPLIES y  into  (NOT x) OR y
-    Node x = doConvert(e[0], sideConditions);
-    Node y = doConvert(e[1], sideConditions);
-    return doConvert(d_nm->mkNode(OR, doConvert(d_nm->mkNode(NOT, x), sideConditions), y), sideConditions);
-  }
-
-  case IFF:
-    if(e.getNumChildren() == 2) {
-      // common case:
-      // just turn  x IFF y  into  (x AND y) OR ((NOT x) AND (NOT y))
-      Node x = doConvert(e[0], sideConditions);
-      Node y = doConvert(e[1], sideConditions);
-      Node r = d_nm->mkNode(OR,
-                            doConvert(d_nm->mkNode(AND, x, y), sideConditions),
-                            doConvert(d_nm->mkNode(AND,
-                                                 doConvert(d_nm->mkNode(NOT, x), sideConditions),
-                                                 doConvert(d_nm->mkNode(NOT, y), sideConditions)), sideConditions));
-      Debug("cnf") << "working on an IFF\n";
-      printAST(Debug("cnf"), e);
-      Debug("cnf") << "which is\n";
-      printAST(Debug("cnf"), r);
-      return doConvert(r, sideConditions);
-    } else {
-      // more than 2 children:
-      // treat  x IFF y IFF z  as  (x IFF y) AND (y IFF z) ...
-      Node::iterator i = e.begin();
-      Node x = doConvert(*i++, sideConditions);
-      NodeBuilder<> r(AND);
-      while(i != e.end()) {
-        Node y = doConvert(*i++, sideConditions);
-        // now we just have two:
-        // just turn  x IFF y  into  (x AND y) OR ((NOT x) AND (NOT y))
-        r << d_nm->mkNode(OR,
-                          doConvert(d_nm->mkNode(AND, x, y), sideConditions),
-                          doConvert(d_nm->mkNode(AND,
-                                                 doConvert(d_nm->mkNode(NOT, x), sideConditions),
-                                                 doConvert(d_nm->mkNode(NOT, y), sideConditions)), sideConditions));
-        x = y;
-      }
-      return doConvert(r, sideConditions);
-    }
-
-  case XOR:
-    Assert( e.getNumChildren() == 2 );
-    // just turn  x XOR y  into  (x AND (NOT y)) OR ((NOT x) AND y)
-    return doConvert(d_nm->mkNode(OR,
-                                  d_nm->mkNode(AND,
-                                               e[0],
-                                               d_nm->mkNode(NOT, e[1])),
-                                  d_nm->mkNode(AND,
-                                               d_nm->mkNode(NOT, e[0]),
-                                               e[1])), sideConditions);
-
-  default:
-    // variable or theory atom
-    return e;
-  }
-}
-
-/**
- * OR:  all ORs and NOTs
- * -- do nothing
- *
- * find an AND.
- * prefix:   a \/ b \/ c
- * and term: d /\ e
- * rest:     f \/ g \/ h
- * 
- * construct:  prefix \/ child
- * 
- * then, process rest.
- * 
- * if rest has no additional ANDs
- * then I get  prefix \/ child \/ rest
- * and I do same with other children
- * 
- * if rest has additional ANDs
- * then I get  (prefix \/ child \/ rest'1) /\ (prefix \/ child \/ rest'2) /\ ...
- * and I do same with other children
- */
-void CnfConverter::directOrHelper(Node::iterator p, Node::iterator end, NodeBuilder<>& result, NodeBuilder<>* sideConditions) {
-  static int nextID = 0;
-  int ID = ++nextID;
-  Debug("dor") << "beginning of directOrHelper " << ID << "\n";
-
-  while(p != end) {
-    // for each child of the expression:
-
-    Debug("dor") << "CHILD == directOrHelper " << ID << "\n";
-    printAST(Debug("dor"), *p);
-
-    // convert the child first
-    Node n = doConvert(*p, sideConditions);
-
-    Debug("dor") << "CNV CHILD == directOrHelper " << ID << "\n";
-    printAST(Debug("dor"), *p);
-
-    // if the child is an AND
-    if(n.getKind() == AND) {
-      Debug("dor") << "directOrHelper found AND " << ID << "\n";
-
-      NodeBuilder<> prefix = result;
-      result.clear(AND);
-
-      for(Node::iterator i = n.begin(); i != n.end(); ++i) {
-        // for each child of the AND
-        NodeBuilder<> r = prefix;
-
-        Debug("dor") << "directOrHelper AND " << ID << ", converting\n";
-        printAST(Debug("dor"), *i);
-
-        r << doConvert(*i, sideConditions);
-        NodeBuilder<> rx = r;
-        Debug("dor") << "prefix \\/ child is " << ID << "\n";
-        printAST(Debug("dor"), rx);
-        Node::iterator p2 = p;
-        directOrHelper(++p2, end, r, sideConditions);
-
-        Debug("dor") << "directOrHelper recursion done " << ID << "\n";
-        Node rr = r;
-        Debug("dor") << "directOrHelper subterm of AND " << ID << "\n";
-        printAST(Debug("dor"), rr);
-
-        result << rr;
-      }
-
-      Debug("dor") << "end of directOrHelper AND " << ID << "\n";
-      NodeBuilder<> resultnb = result;
-      printAST(Debug("dor"), resultnb);
-
-      return;
-    } else {
-      // if it's not an AND, pass it through, it's fine
-      result << n;
-    }
-
-    Debug("cnf") << "  ** result now " << result << std::endl;
-
-    ++p;
-  }
-
-  Debug("dor") << "end of directOrHelper NO AND " << ID << "\n";
-  NodeBuilder<> resultnb = result;
-  printAST(Debug("dor"), resultnb);
-}
-
-Node CnfConverter::varIntroductionConvert(const Node& e, NodeBuilder<>* sideConditions) {
-  switch(e.getKind()) {
-
-  case NOT: {
-    Node f = compressNOT(e, sideConditions);
-    Debug("stari") << "compressNOT:\n";
-    printAST(Debug("stari"), e);
-    printAST(Debug("stari"), f);
-    return f;
-  }
-
-  case AND: {
-    Node n = flatten<AND>(e, sideConditions);
-    Node var = d_nm->mkVar();
-    Node notVar = d_nm->mkNode(NOT, var);
-    for(Node::iterator i = n.begin(); i != n.end(); ++i) {
-      // *i has already been converted by flatten<>()
-      if((*i).getKind() == OR) {
-        NodeBuilder<> b(OR);
-        b << notVar;
-        for(Node::iterator j = (*i).begin(); j != (*i).end(); ++j) {
-          b << *j;
-        }
-        *sideConditions << b;
-      } else {
-        Debug("stari") << "*i should have been flattened:\n";
-        printAST(Debug("stari"), *i);
-        Node x = convert(*i);
-        printAST(Debug("stari"), x);
-        //Assert(x == *i);
-        *sideConditions << d_nm->mkNode(OR, notVar, *i);
-      }
-    }
-
-    return var;
-  }
-
-  case OR:
-    return flatten<OR>(e, sideConditions);
-
-  case IMPLIES: {
-    Assert( e.getNumChildren() == 2 );
-    // just turn  x IMPLIES y  into  (NOT x) OR y
-    Node x = doConvert(e[0], sideConditions);
-    Node y = doConvert(e[1], sideConditions);
-    return doConvert(d_nm->mkNode(OR, doConvert(d_nm->mkNode(NOT, x), sideConditions), y), sideConditions);
-  }
-
-  case IFF:
-    if(e.getNumChildren() == 2) {
-      // common case:
-      // just turn  x IFF y  into  (x AND y) OR ((NOT x) AND (NOT y))
-      Node x = doConvert(e[0], sideConditions);
-      Node y = doConvert(e[1], sideConditions);
-      Node r = d_nm->mkNode(OR,
-                            doConvert(d_nm->mkNode(AND, x, y), sideConditions),
-                            doConvert(d_nm->mkNode(AND,
-                                                 doConvert(d_nm->mkNode(NOT, x), sideConditions),
-                                                 doConvert(d_nm->mkNode(NOT, y), sideConditions)), sideConditions));
-      Debug("cnf") << "working on an IFF\n";
-      printAST(Debug("cnf"), e);
-      Debug("cnf") << "which is\n";
-      printAST(Debug("cnf"), r);
-      return doConvert(r, sideConditions);
-    } else {
-      // more than 2 children:
-      // treat  x IFF y IFF z  as  (x IFF y) AND (y IFF z) ...
-      Node::iterator i = e.begin();
-      Node x = doConvert(*i++, sideConditions);
-      NodeBuilder<> r(AND);
-      while(i != e.end()) {
-        Node y = doConvert(*i++, sideConditions);
-        // now we just have two:
-        // just turn  x IFF y  into  (x AND y) OR ((NOT x) AND (NOT y))
-        r << d_nm->mkNode(OR,
-                          doConvert(d_nm->mkNode(AND, x, y), sideConditions),
-                          doConvert(d_nm->mkNode(AND,
-                                                 doConvert(d_nm->mkNode(NOT, x), sideConditions),
-                                                 doConvert(d_nm->mkNode(NOT, y), sideConditions)), sideConditions));
-        x = y;
-      }
-      return doConvert(r, sideConditions);
-    }
-
-  case XOR:
-    Assert( e.getNumChildren() == 2 );
-    // just turn  x XOR y  into  (x AND (NOT y)) OR ((NOT x) AND y)
-    return doConvert(d_nm->mkNode(OR,
-                                d_nm->mkNode(AND,
-                                             e[0],
-                                             d_nm->mkNode(NOT, e[1])),
-                                d_nm->mkNode(AND,
-                                             d_nm->mkNode(NOT, e[0]),
-                                             e[1])), sideConditions);
-
-  default:
-    // variable or theory atom
-    return e;
-  }
-}
-
-}/* CVC4::smt namespace */
-}/* CVC4 namespace */
diff --git a/src/smt/cnf_converter.h b/src/smt/cnf_converter.h
deleted file mode 100644
index 7b7be0480..000000000
--- a/src/smt/cnf_converter.h
+++ /dev/null
@@ -1,170 +0,0 @@
-/*********************                                           -*- 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 doConvert() on subnodes.
-   */
-  Node compressNOT(const Node& e, NodeBuilder<>* sideConditions);
-
-  /**
-   * 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, NodeBuilder<>* sideConditions);
-
-  /**
-   * 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, NodeBuilder<>* sideConditions);
-
-  /**
-   * Helper method for "direct" CNF preprocessing.  CNF-converts an OR.
-   */
-  void directOrHelper(Node::iterator p,
-                      Node::iterator end,
-                      NodeBuilder<>& result,
-                      NodeBuilder<>* sideConditions);
-
-  /**
-   * 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, NodeBuilder<>* sideConditions);
-
-  /**
-   * 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 doConvert(const Node& e, NodeBuilder<>* sideconditions);
-
-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>
-struct flatten_traits;
-
-template <>
-struct flatten_traits<AND> {
-  static const CVC4::Kind ignore   = TRUE;  // TRUE  AND x == x
-  static const CVC4::Kind shortout = FALSE; // FALSE AND x == FALSE
-};
-
-template <>
-struct flatten_traits<OR> {
-  static const CVC4::Kind ignore   = FALSE; // FALSE OR x == x
-  static const CVC4::Kind shortout = TRUE;  // TRUE  OR x == TRUE
-};
-
-template <CVC4::Kind K>
-Node CnfConverter::flatten(const Node& e, NodeBuilder<>* sideConditions) {
-  Assert(e.getKind() == K);
-
-  NodeBuilder<> n(K);
-
-  for(Node::iterator i = e.begin(); i != e.end(); ++i) {
-    Node f = doConvert(*i, sideConditions);
-    if(f.getKind() == K) {
-      for(Node::iterator j = f.begin(); j != f.end(); ++j) {
-        n << *j;
-      }
-    } else if(f.getKind() == flatten_traits<K>::ignore) {
-      /* do nothing */
-    } else if(f.getKind() == flatten_traits<K>::shortout) {
-      return f;
-    } 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 c0f825462..7e2b6e24c 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -27,8 +27,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* opts) throw() :
   d_opts(opts),
   d_de(),
   d_te(),
-  d_prop(d_de, d_te),
-  d_cnfConverter(d_nm, opts->d_cnfConversion) {
+  d_prop(d_de, d_te){
 }
 
 SmtEngine::~SmtEngine() {
@@ -43,62 +42,18 @@ Node SmtEngine::preprocess(const Node& e) {
   return e;
 }
 
-Node SmtEngine::processAssertionList() {
-  if(d_assertions.size() == 1) {
-    return d_assertions[0];
+void SmtEngine::processAssertionList() {
+  for(unsigned i = 0; i < d_assertions.size(); ++i) {
+    d_prop.assertFormula(d_assertions[i]);
   }
-
-  NodeBuilder<> asserts(AND);
-  for(std::vector<Node>::iterator i = d_assertions.begin();
-      i != d_assertions.end();
-      ++i) {
-    asserts << *i;
-  }
-
   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();
-
-  // 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);
+  processAssertionList();
+  d_prop.solve();
   return Result(Result::VALIDITY_UNKNOWN);
 }
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index b073a68c9..097500833 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -29,7 +29,6 @@
 #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)
@@ -134,8 +133,6 @@ 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,
@@ -167,7 +164,7 @@ private:
    * Process the assertion list: for literals and conjunctions of
    * literals, assert to T-solver.
    */
-  Node processAssertionList();
+  void processAssertionList();
 
 };/* class SmtEngine */