From: Morgan Deters <mdeters@gmail.com>
Date: Sat, 30 Jan 2010 02:22:25 +0000 (+0000)
Subject: cnf conversion (variable-introducing), cleanups, fixes to minisat calling for multipl... 
X-Git-Tag: cvc5-1.0.0~9322
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=39b707ad22813c184da61c3e2337359ca8061797;p=cvc5.git

cnf conversion (variable-introducing), cleanups, fixes to minisat calling for multiple-query cases
---

diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 7c6405ace..77ff05ab5 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -125,10 +125,21 @@ public:
     return d_ev->ev_end();
   }
 
+  Kind getKind() const {
+    return d_ev->getKind();
+  }
+
   unsigned getNumChildren() const {
     return d_ev->getNumChildren();
   }
 
+  Node operator[](int i) const {
+    Assert(i >= 0 && i < d_ev->getNumChildren());
+    return Node(d_ev->d_children[i]);
+  }
+
+  void clear(Kind k = UNDEFINED_KIND);
+
   // Compound expression constructors
   /*
   NodeBuilder& eqExpr(const Node& right);
@@ -372,6 +383,7 @@ namespace CVC4 {
 template <unsigned nchild_thresh>
 inline NodeBuilder<nchild_thresh>::NodeBuilder() :
   d_size(nchild_thresh),
+  d_hash(0),
   d_nm(NodeManager::currentNM()),
   d_used(false),
   d_ev(&d_inlineEv),
@@ -381,6 +393,7 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder() :
 template <unsigned nchild_thresh>
 inline NodeBuilder<nchild_thresh>::NodeBuilder(Kind k) :
   d_size(nchild_thresh),
+  d_hash(0),
   d_nm(NodeManager::currentNM()),
   d_used(false),
   d_ev(&d_inlineEv),
@@ -394,6 +407,7 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(Kind k) :
 template <unsigned nchild_thresh>
 inline NodeBuilder<nchild_thresh>::NodeBuilder(const NodeBuilder<nchild_thresh>& nb) :
   d_size(nchild_thresh),
+  d_hash(0),
   d_nm(nb.d_nm),
   d_used(nb.d_used),
   d_ev(&d_inlineEv),
@@ -402,16 +416,19 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(const NodeBuilder<nchild_thresh>&
 
   if(evIsAllocated(nb)) {
     realloc(nb.d_size, false);
-    std::copy(nb.d_ev->begin(), nb.d_ev->end(), d_ev->begin());
+    std::copy(nb.d_ev->ev_begin(), nb.d_ev->ev_end(), d_ev->ev_begin());
   } else {
-    std::copy(nb.d_ev->begin(), nb.d_ev->end(), d_inlineEv.begin());
+    std::copy(nb.d_ev->ev_begin(), nb.d_ev->ev_end(), d_inlineEv.ev_begin());
   }
+  d_ev->d_kind = nb.d_ev->d_kind;
+  d_ev->d_nchildren = nb.d_ev->d_nchildren;
 }
 
 template <unsigned nchild_thresh>
 template <unsigned N>
 inline NodeBuilder<nchild_thresh>::NodeBuilder(const NodeBuilder<N>& nb) :
   d_size(nchild_thresh),
+  d_hash(0),
   d_nm(NodeManager::currentNM()),
   d_used(nb.d_used),
   d_ev(&d_inlineEv),
@@ -420,15 +437,18 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(const NodeBuilder<N>& nb) :
 
   if(nb.d_ev->d_nchildren > nchild_thresh) {
     realloc(nb.d_size, false);
-    std::copy(nb.d_ev->begin(), nb.d_ev->end(), d_ev->begin());
+    std::copy(nb.d_ev->ev_begin(), nb.d_ev->end(), d_ev->ev_begin());
   } else {
-    std::copy(nb.d_ev->begin(), nb.d_ev->end(), d_inlineEv.begin());
+    std::copy(nb.d_ev->ev_begin(), nb.d_ev->end(), d_inlineEv.ev_begin());
   }
+  d_ev->d_kind = nb.d_ev->d_kind;
+  d_ev->d_nchildren = nb.d_ev->d_nchildren;
 }
 
 template <unsigned nchild_thresh>
 inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm) :
   d_size(nchild_thresh),
+  d_hash(0),
   d_nm(nm),
   d_used(false),
   d_ev(&d_inlineEv),
@@ -438,6 +458,7 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm) :
 template <unsigned nchild_thresh>
 inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm, Kind k) :
   d_size(nchild_thresh),
+  d_hash(0),
   d_nm(nm),
   d_used(false),
   d_ev(&d_inlineEv),
@@ -450,19 +471,42 @@ 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");
+  if(!d_used) {
+    Warning("NodeBuilder unused at destruction\n");
 
-  return;
-  /*
-  for(iterator i = d_ev->ev_begin();
-      i != d_ev->ev_end();
-      ++i) {
-    (*i)->dec();
+    for(iterator i = d_ev->ev_begin();
+        i != d_ev->ev_end();
+        ++i) {
+      (*i)->dec();
+    }
+    if(evIsAllocated()) {
+      free(d_ev);
+    }
   }
-  if(evIsAllocated()) {
-    free(d_ev);
+}
+
+template <unsigned nchild_thresh>
+void NodeBuilder<nchild_thresh>::clear(Kind k) {
+  if(!d_used) {
+    Warning("NodeBuilder unused at clear\n");
+
+    for(iterator i = d_ev->ev_begin();
+        i != d_ev->ev_end();
+        ++i) {
+      (*i)->dec();
+    }
+    if(evIsAllocated()) {
+      free(d_ev);
+    }
   }
-  */
+
+  d_size = nchild_thresh;
+  d_hash = 0;
+  d_nm = NodeManager::currentNM();
+  d_used = false;
+  d_ev = &d_inlineEv;
+  d_inlineEv.d_kind = k;
+  d_inlineEv.d_nchildren = 0;
 }
 
 template <unsigned nchild_thresh>
diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index dd052ca2e..b7361eb0f 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -47,7 +47,7 @@ unsigned AntlrParser::getPrecedence(Kind kind) {
   case AND:
     return 5;
   default:
-    Unhandled ("Undefined precedence - necessary for proper parsing of CVC files!");
+    Unhandled("Undefined precedence - necessary for proper parsing of CVC files!");
   }
   return 0;
 }
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 16b807904..bc46e39d5 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -30,21 +30,21 @@ using namespace std;
 namespace CVC4 {
 
 PropEngine::PropEngine(DecisionEngine& de, TheoryEngine& te) :
-  d_de(de), d_te(te), d_sat() {
+  d_de(de), d_te(te) {
 }
 
-void PropEngine::addVars(Node e) {
+void PropEngine::addVars(SimpSolver* minisat, map<Node, Var>* vars, map<Var, Node>* varsReverse, Node e) {
   Debug("prop") << "adding vars to " << e << endl;
   for(Node::iterator i = e.begin(); i != e.end(); ++i) {
     Debug("prop") << "expr " << *i << endl;
     if((*i).getKind() == VARIABLE) {
-      if(d_vars.find(*i) == d_vars.end()) {
-        Var v = d_sat.newVar();
+      if(vars->find(*i) == vars->end()) {
+        Var v = minisat->newVar();
         Debug("prop") << "adding var " << *i << " <--> " << v << endl;
-        d_vars.insert(make_pair(*i, v));
-        d_varsReverse.insert(make_pair(v, *i));
-      } else Debug("prop") << "using var " << *i << " <--> " << d_vars[*i] << endl;
-    } else addVars(*i);
+        (*vars).insert(make_pair(*i, v));
+        (*varsReverse).insert(make_pair(v, *i));
+      } else Debug("prop") << "using var " << *i << " <--> " << (*vars)[*i] << endl;
+    } else addVars(minisat, vars, varsReverse, *i);
   }
 }
 
@@ -110,35 +110,41 @@ static void doClause(SimpSolver* minisat, map<Node, Var>* vars, map<Var, Node>*
 }
 
 void PropEngine::solve(Node e) {
+  // FIXME: when context mgr comes online, keep the solver around
+  // between solve() calls if we can
+  CVC4::prop::minisat::SimpSolver sat;
+  std::map<Node, CVC4::prop::minisat::Var> vars;
+  std::map<CVC4::prop::minisat::Var, Node> varsReverse;
+
   Debug("prop") << "SOLVING " << e << endl;
-  addVars(e);
+  addVars(&sat, &vars, &varsReverse, e);
   if(e.getKind() == AND) {
     Debug("prop") << "AND" << endl;
     for(Node::iterator i = e.begin(); i != e.end(); ++i)
-      doClause(&d_sat, &d_vars, &d_varsReverse, *i);
-  } else doClause(&d_sat, &d_vars, &d_varsReverse, e);
+      doClause(&sat, &vars, &varsReverse, *i);
+  } else doClause(&sat, &vars, &varsReverse, e);
 
-  d_sat.verbosity = 1;
-  bool result = d_sat.solve();
+  sat.verbosity = 1;
+  bool result = sat.solve();
 
   Notice() << "result is " << (result ? "sat/invalid" : "unsat/valid") << endl;
   if(result) {
     Notice() << "model:" << endl;
-    for(int i = 0; i < d_sat.model.size(); ++i)
-      Notice() << " " << toInt(d_sat.model[i]);
+    for(int i = 0; i < sat.model.size(); ++i)
+      Notice() << " " << toInt(sat.model[i]);
     Notice() << endl;
-    for(int i = 0; i < d_sat.model.size(); ++i)
-      Notice() << " " << d_varsReverse[i] << " is "
-               << (d_sat.model[i] == l_False ? "FALSE" :
-                   (d_sat.model[i] == l_Undef ? "UNDEF" :
+    for(int i = 0; i < sat.model.size(); ++i)
+      Notice() << " " << varsReverse[i] << " is "
+               << (sat.model[i] == l_False ? "FALSE" :
+                   (sat.model[i] == l_Undef ? "UNDEF" :
                     "TRUE")) << endl;
   } else {
     Notice() << "conflict:" << endl;
-    for(int i = 0; i < d_sat.conflict.size(); ++i)
-      Notice() << " " << (sign(d_sat.conflict[i]) ? "-" : "") << var(d_sat.conflict[i]);
+    for(int i = 0; i < sat.conflict.size(); ++i)
+      Notice() << " " << (sign(sat.conflict[i]) ? "-" : "") << var(sat.conflict[i]);
     Notice() << " [[";
-    for(int i = 0; i < d_sat.conflict.size(); ++i)
-      Notice() << " " << (sign(d_sat.conflict[i]) ? "-" : "") << d_varsReverse[var(d_sat.conflict[i])];
+    for(int i = 0; i < sat.conflict.size(); ++i)
+      Notice() << " " << (sign(sat.conflict[i]) ? "-" : "") << varsReverse[var(sat.conflict[i])];
     Notice() << " ]] " << endl;
   }
 }
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 6cb818d10..6e1f8cb61 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -35,11 +35,11 @@ namespace CVC4 {
 class PropEngine {
   DecisionEngine &d_de;
   TheoryEngine &d_te;
-  CVC4::prop::minisat::SimpSolver d_sat;
-  std::map<Node, CVC4::prop::minisat::Var> d_vars;
-  std::map<CVC4::prop::minisat::Var, Node> d_varsReverse;
+  //CVC4::prop::minisat::SimpSolver d_sat;
+  //std::map<Node, CVC4::prop::minisat::Var> d_vars;
+  //std::map<CVC4::prop::minisat::Var, Node> d_varsReverse;
 
-  void addVars(Node);
+  void addVars(CVC4::prop::minisat::SimpSolver*, std::map<Node, CVC4::prop::minisat::Var>*, std::map<CVC4::prop::minisat::Var, Node>*, Node);
 
 public:
   /**
diff --git a/src/smt/cnf_converter.cpp b/src/smt/cnf_converter.cpp
index c94d62524..7c53e9b04 100644
--- a/src/smt/cnf_converter.cpp
+++ b/src/smt/cnf_converter.cpp
@@ -22,7 +22,6 @@
 namespace CVC4 {
 namespace smt {
 
-
 static void printAST(std::ostream& out, const Node& n, int indent = 0) {
   for(int i = 0; i < indent; ++i) {
     out << "  ";
@@ -46,8 +45,33 @@ static void printAST(std::ostream& out, const Node& n, int indent = 0) {
   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)) {
@@ -55,12 +79,22 @@ Node CnfConverter::convert(const Node& e) {
     n = getConversionMap(e);
   } else {
     switch(d_conversion) {
+
     case CNF_DIRECT_EXPONENTIAL:
-      n = directConvert(e);
+      Debug("cnf") << "direct conversion for " << e << " with id " << e.getId() << " is being computed!" << std::endl;
+      n = directConvert(e, sideConditions);
       break;
-    case CNF_VAR_INTRODUCTION:
-      n = varIntroductionConvert(e);
+
+    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);
     }
@@ -80,153 +114,316 @@ Node CnfConverter::convert(const Node& e) {
   return n;
 }
 
-Node CnfConverter::compressNOT(const Node& e) {
+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(e[0].getKind() == TRUE) {
+  if(f.getKind() == TRUE) {
     return d_nm->mkNode(FALSE);
-  } else if(e[0].getKind() == FALSE) {
+  } else if(f.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);
-        }
+  } 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;
     }
-    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(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;
+    return n;
+  } else {
+    return d_nm->mkNode(NOT, f);
   }
 }
 
 
-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);
+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);
-    directOrHelper(n.begin(), n.end(), m);
+    Debug("dor") << "calling directOrHelper on\n";
+    printAST(Debug("dor"), n);
+    directOrHelper(n.begin(), n.end(), m, sideConditions);
 
     return m;
   }
 
-  return e;
+  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;
+  }
 }
 
-void CnfConverter::directOrHelper(Node::iterator p, Node::iterator end, NodeBuilder<>& result) {
+/**
+ * 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) {
-    if((*p).getKind() == AND) {
-      Debug("cnf") << "orHelper: p      " << *p << std::endl;
-      Debug("cnf") << "          end    " << std::endl;
-      Debug("cnf") << "          result " << result << std::endl;
+    // 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<> resultPrefix = result;
-      result = NodeBuilder<>(AND);
+      NodeBuilder<> prefix = result;
+      result.clear(AND);
 
-      for(Node::iterator i = (*p).begin(); i != (*p).end(); ++i) {
-        NodeBuilder<> r = resultPrefix;
+      for(Node::iterator i = n.begin(); i != n.end(); ++i) {
+        // for each child of the AND
+        NodeBuilder<> r = prefix;
 
-        // is this a double-convert since we did OR flattening before?
-        r << convert(*i);
+        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);
+        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 << r;
+        result << rr;
       }
+
+      Debug("dor") << "end of directOrHelper AND " << ID << "\n";
+      NodeBuilder<> resultnb = result;
+      printAST(Debug("dor"), resultnb);
+
+      return;
     } 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);
+      // if it's not an AND, pass it through, it's fine
+      result << n;
     }
 
     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);
+  Debug("dor") << "end of directOrHelper NO AND " << ID << "\n";
+  NodeBuilder<> resultnb = result;
+  printAST(Debug("dor"), resultnb);
+}
 
-    NodeBuilder<> m(AND);
-    NodeBuilder<> extras(OR);
-    varIntroductionOrHelper(n.begin(), n.end(), m, extras);
+Node CnfConverter::varIntroductionConvert(const Node& e, NodeBuilder<>* sideConditions) {
+  switch(e.getKind()) {
 
-    if(m.getNumChildren() > 0) {
-      return m << extras;
-    } else {
-      return extras;
-    }
+  case NOT: {
+    Node f = compressNOT(e, sideConditions);
+    Debug("stari") << "compressNOT:\n";
+    printAST(Debug("stari"), e);
+    printAST(Debug("stari"), f);
+    return f;
   }
 
-  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;
+  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);
+      }
+    }
 
-      Node var = d_nm->mkVar();
-      extras << var;
+    return var;
+  }
 
-      Debug("cnf") << "  introduced var " << var << "(" << var.getId() << ")" << std::endl;
+  case OR:
+    return flatten<OR>(e, sideConditions);
 
-      Node notVar = d_nm->mkNode(NOT, var);
+  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);
+  }
 
-      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));
-      }
+  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 {
-      // 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);
+      // 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);
     }
 
-    Debug("cnf") << "  ** result now " << result << std::endl;
-    Debug("cnf") << "  ** extras now " << extras << std::endl;
-    ++p;
+  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;
   }
 }
 
diff --git a/src/smt/cnf_converter.h b/src/smt/cnf_converter.h
index d045f4d64..7b7be0480 100644
--- a/src/smt/cnf_converter.h
+++ b/src/smt/cnf_converter.h
@@ -64,9 +64,9 @@ private:
   /**
    * 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.
+   * of ANDs and ORs.  Calls doConvert() on subnodes.
    */
-  Node compressNOT(const Node& e);
+  Node compressNOT(const Node& e, NodeBuilder<>* sideConditions);
 
   /**
    * Flatten a Node of kind K.  K here is going to be AND or OR.
@@ -75,21 +75,22 @@ private:
    * (AND (AND x y) (AND (AND z)) w)  ==>  (AND x y z w).
    */
   template <CVC4::Kind K>
-  Node flatten(const Node& e);
+  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);
+  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<>& result,
+                      NodeBuilder<>* sideConditions);
 
   /**
    * Do a satisfiability-preserving CNF conversion with variable
@@ -97,16 +98,14 @@ private:
    * number of clauses, but new variables are introduced and the
    * output is equisatisfiable (but not equivalent) to the input.
    */
-  Node varIntroductionConvert(const Node& e);
+  Node varIntroductionConvert(const Node& e, NodeBuilder<>* sideConditions);
 
   /**
-   * Helper method for "variable introduction" CNF preprocessing.
-   * CNF-converts an OR.
+   * 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).
    */
-  void varIntroductionOrHelper(Node::iterator p,
-                               Node::iterator end,
-                               NodeBuilder<>& result,
-                               NodeBuilder<>& extras);
+  Node doConvert(const Node& e, NodeBuilder<>* sideconditions);
 
 public:
 
@@ -127,17 +126,36 @@ public:
 };/* class CnfConverter */
 
 template <CVC4::Kind K>
-Node CnfConverter::flatten(const Node& e) {
+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 = convert(*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;
     }
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 65375ab65..b073a68c9 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -96,7 +96,7 @@ public:
   Expr simplify(const Expr& e);
 
   /**
-   * Get a (counter)model (only if preceded by a SAT or INVALID query.
+   * Get a (counter)model (only if preceded by a SAT or INVALID query).
    */
   Model getModel();
 
diff --git a/src/util/options.h b/src/util/options.h
index 57b20c47f..2e696d0db 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -52,7 +52,7 @@ struct Options {
               err(0),
               verbosity(0),
               lang(parser::Parser::LANG_AUTO),
-              d_cnfConversion(CVC4::CNF_DIRECT_EXPONENTIAL)
+              d_cnfConversion(CVC4::CNF_VAR_INTRODUCTION)
   {}
 };/* struct Options */