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

3 files changed, 335 insertions, 120 deletions

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();