uncompiling new bv to bool lifting

5 files changed, 216 insertions, 161 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f3d5d446e..0f79da82a 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1926,9 +1926,10 @@ bool SmtEnginePrivate::nonClausalSimplify() {
 
 void SmtEnginePrivate::bvToBool() {
   Trace("simplify") << "SmtEnginePrivate::bvToBool()" << endl;
-
+  std::vector<Node> new_assertions;
+  d_smt.d_theoryEngine->ppBvToBool(d_assertionsToCheck, new_assertions); 
   for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
-    d_assertionsToCheck[i] = d_smt.d_theoryEngine->ppBvToBool(d_assertionsToCheck[i]);
+    d_assertionsToCheck[i] = Rewriter::rewrite(new_assertions[i]); 
   }
 }
 
@@ -2481,16 +2482,6 @@ bool SmtEnginePrivate::simplifyAssertions()
     Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
     Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
-    // Lift bit-vectors of size 1 to bool 
-    if(options::bvToBool()) {
-      Chat() << "...doing bvToBool..." << endl;
-      bvToBool();
-    }
-
-    Trace("smt") << "POST bvToBool" << endl;
-    Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
-    Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
-    
     if(options::repeatSimp() && options::simplificationMode() != SIMPLIFICATION_MODE_NONE) {
       Chat() << "...doing another round of nonclausal simplification..." << endl;
       Trace("simplify") << "SmtEnginePrivate::simplify(): "
@@ -2789,6 +2780,17 @@ void SmtEnginePrivate::processAssertions() {
   }
   dumpAssertions("post-static-learning", d_assertionsToCheck);
 
+  // Lift bit-vectors of size 1 to bool 
+  if(options::bvToBool()) {
+    Chat() << "...doing bvToBool..." << endl;
+    bvToBool();
+  }
+
+  Trace("smt") << "POST bvToBool" << endl;
+  Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
+  Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
+
+  
   dumpAssertions("pre-ite-removal", d_assertionsToCheck);
   {
     Chat() << "removing term ITEs..." << endl;
diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp
index 5ab7cf144..7d3f58c8e 100644
--- a/src/theory/bv/bv_to_bool.cpp
+++ b/src/theory/bv/bv_to_bool.cpp
@@ -23,22 +23,6 @@ using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::theory::bv;
 
-void BvToBoolVisitor::storeBvToBool(TNode bv_term, Node bool_term) {
-  Assert (!hasBoolTerm(bv_term));
-  Assert (bool_term.getType().isBoolean()); 
-  d_bvToBoolTerm[bv_term] = bool_term; 
-}
-
-Node BvToBoolVisitor::getBoolTerm(TNode bv_term) const {
-  Assert(hasBoolTerm(bv_term));
-  return d_bvToBoolTerm.find(bv_term)->second; 
-}
-
-bool BvToBoolVisitor::hasBoolTerm(TNode bv_term) const {
-  Assert (bv_term.getType().isBitVector()); 
-  return d_bvToBoolTerm.find(bv_term) != d_bvToBoolTerm.end(); 
-}
-
 void BvToBoolVisitor::addToCache(TNode term, Node new_term) {
   Assert (new_term != Node()); 
   Assert (!hasCache(term));
@@ -56,130 +40,167 @@ bool BvToBoolVisitor::hasCache(TNode term) const {
   return d_cache.find(term) != d_cache.end(); 
 }
 
-
 void BvToBoolVisitor::start(TNode node) {}
 
+void BvToBoolVisitor::storeBvToBool(TNode bv_term, TNode bool_term) {
+  Assert (bv_term.getType().isBitVector() &&
+          bv_term.getType().getBitVectorSize() == 1);
+  Assert (bool_term.getType().isBoolean() &&  d_bvToBoolMap.find(bv_term) == d_bvToBoolMap.end());
+  d_bvToBoolMap[bv_term] = bool_term; 
+}
+
+Node BvToBoolVisitor::getBoolForBvTerm(TNode node) {
+  Assert (d_bvToBoolMap.find(node) != d_bvToBoolMap.end());
+  return d_bvToBoolMap[node]; 
+}
+
 bool BvToBoolVisitor::alreadyVisited(TNode current, TNode parent) {
-  return d_visited.find(current) != d_visited.end(); 
+  return d_cache.find(current) != d_cache.end(); 
+}
+
+bool BvToBoolVisitor::isConvertibleBvAtom(TNode node) {
+  Kind kind = node.getKind();
+  return (kind == kind::BITVECTOR_ULT ||
+          kind == kind::BITVECTOR_ULE ||
+          kind == kind::EQUAL) &&
+    node[0].getType().isBitVector() &&
+    node[0].getType().getBitVectorSize() == 1; 
 }
 
-bool BvToBoolVisitor::isConvertibleToBool(TNode current) {
-  TypeNode type = current.getType(); 
-  if (current.getNumChildren() == 0 && type.isBitVector()) {
-    return type.getBitVectorSize() == 1; 
-  }
-
-  if (current.getKind() == kind::NOT) {
-    current = current[0];
-  }
-  Kind kind = current.getKind();
-  // checking bit-vector kinds 
-  if (kind == kind::BITVECTOR_OR ||
-      kind == kind::BITVECTOR_AND ||
-      kind == kind::BITVECTOR_XOR ||
-      kind == kind::BITVECTOR_NOT ||
-      kind == kind::BITVECTOR_ULT ||
-      kind == kind::BITVECTOR_ULE ||
-      kind == kind::EQUAL) {
-    // we can convert it to bool if all of the children can also be converted
-    // to bool
-    if (! current[0].getType().getBitVectorSize() == 1)
-      return false; 
-    for (unsigned i = 0; i < current.getNumChildren(); ++i) {
-      // we assume that the children have been visited
-      if (!hasBoolTerm(current[i]))
+bool BvToBoolVisitor::isConvertibleBvTerm(TNode node) {
+  // we have already converted it and the result is cached
+  if (d_bvToBoolMap.find(node) != d_bvToBoolMap.end()) {
+    return true;
+  }
+  
+  Kind kind = node.getKind();
+  if (!node.getType().isBitVector() || node.getType().getBitVectorSize() != 1)
+    return false;
+  
+  if (kind == kind::CONST_BITVECTOR) {
+    return true; 
+  }
+
+  if (kind == kind::BITVECTOR_AND || kind == kind::BITVECTOR_OR ||
+      kind == kind::BITVECTOR_NOT || kind == kind::BITVECTOR_XOR) {
+    for (unsigned i = 0; i < node.getNumChildren(); ++i) {
+      if (!isConvertibleBvTerm(node[i]))
         return false; 
     }
     return true; 
   }
-  if (kind == kind::ITE &&
-      type.isBitVector()) {
-    return type.getBitVectorSize() == 1 && hasBoolTerm(current[1]) && hasBoolTerm(current[2]); 
-  }
   return false; 
 }
 
-
-Node BvToBoolVisitor::convertToBool(TNode current) {
-  Debug("bv-to-bool") << "BvToBoolVisitor::convertToBool (" << current << ") "; 
-  Kind kind = current.getKind();
-
-  Node new_current; 
-  if (current.getNumChildren() == 0) {
-    if (current.getKind() == kind::CONST_BITVECTOR) {
-      new_current = current == d_one? utils::mkTrue() : utils::mkFalse(); 
-    } else {
-      new_current = utils::mkNode(kind::EQUAL, current, d_one); 
-    }
-    Debug("bv-to-bool") << "=> " << new_current << "\n"; 
-  } else if (kind == kind::BITVECTOR_ULT) {
-    TNode a = getBoolTerm(current[0]);
-    TNode b = getBoolTerm(current[1]);
-    Node a_eq_0 = utils::mkNode(kind::EQUAL, a, d_zero);
-    Node b_eq_1 = utils::mkNode(kind::EQUAL, b, d_one);
-    new_current = utils::mkNode(kind::AND, a_eq_0, b_eq_1);
-  }  else if (kind == kind::BITVECTOR_ULE) {
-    TNode a = getBoolTerm(current[0]);
-    TNode b = getBoolTerm(current[1]);
+Node BvToBoolVisitor::convertBvAtom(TNode node) {
+  Assert (node.getType().isBoolean());
+  Kind kind = node.getKind();
+  Node result; 
+  switch(kind) {
+  case kind::BITVECTOR_ULT: {
+    TNode a = getBoolForBvTerm(node[0]);
+    TNode b = getBoolForBvTerm(node[1]);
     Node a_eq_0 = utils::mkNode(kind::EQUAL, a, d_zero);
     Node b_eq_1 = utils::mkNode(kind::EQUAL, b, d_one);
-    Node a_lt_b = utils::mkNode(kind::AND, a_eq_0, b_eq_1); 
-    Node a_eq_b = utils::mkNode(kind::EQUAL, a, b);
-    new_current = utils::mkNode(kind::OR, a_lt_b, a_eq_b);
-  } else if (kind == kind::ITE) {
-    TNode cond = current[0];
-    TNode a = getBoolTerm(current[1]);
-    TNode b = getBoolTerm(current[2]);
-    new_current = utils::mkNode(kind::ITE, cond, a, b);
-  } else {
-    Kind new_kind; 
-    switch (kind) {
-    case kind::BITVECTOR_OR :
-      new_kind = kind::OR;
-      break; 
-    case kind::BITVECTOR_AND:
-      new_kind =  kind::AND;
-      break; 
-    case kind::BITVECTOR_XOR:
-      new_kind = kind::XOR;
-      break; 
-    case kind::BITVECTOR_NOT:
-      new_kind =  kind::NOT;
-      break; 
-    case kind::EQUAL:
-      new_kind = kind::IFF;
-      break; 
-    default:
-      Unreachable("Unknown kind ", kind);  
-    }
-    NodeBuilder<> builder(new_kind);
-    if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
-      builder << current.getOperator();
+    result = utils::mkNode(kind::AND, a_eq_0, b_eq_1);
+    break;
+  }
+  case kind::BITVECTOR_ULE: {
+   TNode a = getBoolForBvTerm(node[0]);
+   TNode b = getBoolForBvTerm(node[1]);
+   Node a_eq_0 = utils::mkNode(kind::EQUAL, a, d_zero);
+   Node b_eq_1 = utils::mkNode(kind::EQUAL, b, d_one);
+   Node a_lt_b = utils::mkNode(kind::AND, a_eq_0, b_eq_1); 
+   Node a_eq_b = utils::mkNode(kind::EQUAL, a, b);
+   result = utils::mkNode(kind::OR, a_lt_b, a_eq_b);    
+   break;
+  }
+  case kind::EQUAL: {
+    TNode a = getBoolForBvTerm(node[0]);
+    TNode b = getBoolForBvTerm(node[1]);
+    result = utils::mkNode(kind::IFF, a, b); 
+    break;
+  }
+  default:
+    Unhandled(); 
+  }
+  Assert (result != Node());
+  return result;
+}
+
+Node BvToBoolVisitor::convertBvTerm(TNode node) {
+  Assert (node.getType().isBitVector() &&
+          node.getType().getBitVectorSize() == 1);
+  Kind kind = node.getKind(); 
+
+  if (node.getNumChildren() == 0) {
+    if (node.getKind() == kind::VARIABLE) {
+      return getBoolForBvTerm(node);
     }
-    for (unsigned i = 0; i < current.getNumChildren(); ++i) {
-      builder << getBoolTerm(current[i]); 
+    if (node.getKind() == kind::CONST_BITVECTOR) {
+      return (node == d_one ? utils::mkTrue() : utils::mkFalse());
     }
-    new_current = builder;
   }
   
-  Debug("bv-to-bool") << "=> " << new_current << "\n";
-  if (current.getType().isBitVector()) {
-    storeBvToBool(current, new_current); 
-  } else {
-    addToCache(current, new_current); 
+  if (kind == kind::ITE) {
+    TNode cond = getCache(node[0]);
+    TNode true_branch = getBoolForBvTerm(node[1]);
+    TNode false_branch = getBoolForBvTerm(node[2]);
+    Node result = utils::mkNode(kind::ITE, cond, true_branch, false_branch);
+    storeBvToBool(node, result);
+    return result; 
+  }
+  
+  Kind new_kind; 
+  switch(kind) {
+  case kind::BITVECTOR_OR:
+    new_kind = kind::OR;
+    break;
+  case kind::BITVECTOR_AND:
+    new_kind = kind::AND;
+    break;
+  case kind::BITVECTOR_XOR:
+    new_kind = kind::XOR;
+    break;
+  case kind::BITVECTOR_NOT:
+    new_kind = kind::NOT;
+    break;
+  default:
+    Unhandled(); 
+  }
+
+  NodeBuilder<> builder(new_kind);
+  for (unsigned i = 0; i < node.getNumChildren(); ++i) {
+    builder << getBoolForBvTerm(node[i]); 
+  }
+  Node result = builder;
+  storeBvToBool(node, result);
+  return result; 
+}
+
+void BvToBoolVisitor::check(TNode current, TNode parent) {
+  if (d_bvToBoolMap.find(current) != d_bvToBoolMap.end()) {
+    if (!isConvertibleBvTerm(parent) && !isConvertibleBvAtom(parent)) {
+      Debug("bv-to-bool") << "BvToBoolVisitor::check " << current << " in non boolean context: \n"
+                          << "           " << parent << "\n"; 
+    }
   }
-  return new_current; 
 }
 
 void BvToBoolVisitor::visit(TNode current, TNode parent) {
   Debug("bv-to-bool") << "BvToBoolVisitor visit (" << current << ", " << parent << ")\n"; 
-  Assert (!alreadyVisited(current, parent));
-  d_visited.insert(current);
+  Assert (!alreadyVisited(current, parent) &&
+          !hasCache(current));
+  
+  Node result;
 
-  Node result; 
-  // if it has more than one child
-  if (isConvertibleToBool(current)) {
-    result = convertToBool(current); 
+  // make sure that the bv terms we are replacing to not occur in other contexts
+  check(current, parent); 
+  
+  if (isConvertibleBvAtom(current)) {
+    result = convertBvAtom(current); 
+  } else if (isConvertibleBvTerm(current)) {
+    result = convertBvTerm(current); 
   } else {
     if (current.getNumChildren() == 0) {
       result = current; 
@@ -190,24 +211,60 @@ void BvToBoolVisitor::visit(TNode current, TNode parent) {
       }
       for (unsigned i = 0; i < current.getNumChildren(); ++i) {
         Node converted = getCache(current[i]);
-        if (converted.getType() == current[i].getType()) {
-          builder << converted; 
-        } else {
-          builder << current[i]; 
-        }
+        Assert (converted.getType() == current[i].getType()); 
+        builder << converted; 
       }
       result = builder;
     }
-    addToCache(current, result); 
   }
+  Assert (result != Node()); 
+  addToCache(current, result);
 }
 
+
 BvToBoolVisitor::return_type BvToBoolVisitor::done(TNode node) {
   Assert (hasCache(node)); 
   return getCache(node); 
 }
 
-Node BvToBoolPreprocessor::liftBoolToBV(TNode assertion) {
-  Node result = NodeVisitor<BvToBoolVisitor>::run(d_visitor, assertion);
-  return result; 
+bool BvToBoolPreprocessor::matchesBooleanPatern(TNode current) {
+  // we are looking for something of the type (= (bvvar 1) (some predicate))
+  if (current.getKind() == kind::IFF &&
+      current[0].getKind() == kind::EQUAL &&
+      current[0][0].getType().isBitVector() &&
+      current[0][0].getType().getBitVectorSize() == 1 &&
+      current[0][0].getKind() == kind::VARIABLE &&
+      current[0][1].getKind() == kind::CONST_BITVECTOR) {
+    return true; 
+  }    
+  return false; 
+}
+
+
+void BvToBoolPreprocessor::liftBoolToBV(const std::vector<TNode>& assertions, std::vector<Node>& new_assertions) {
+  TNodeNodeMap candidates;
+  for (unsigned i = 0; i < assertions.size(); ++i) {
+    if (matchesBooleanPatern(assertions[i])) {
+      TNode assertion = assertions[i]; 
+      TNode bv_var = assertion[0][0];
+      Assert (bv_var.getKind() == kind::VARIABLE &&
+              bv_var.getType().isBitVector() &&
+              bv_bar.getType().getBitVectorSize() == 1);
+      TNode bool_cond = assertion[1];
+      Assert (bool_cond.getType().isBoolean());
+      if (candidates.find(bv_var) == candidates.end()) {
+        Debug("bv-to-bool") << "BBvToBoolPreprocessor::liftBvToBoolBV candidate: " << bv_var <<"\n"; 
+        candidates[bv_var] = bool_cond;
+      } else {
+        Debug("bv-to-bool") << "BvToBoolPreprocessor::liftBvToBoolBV multiple def " << bv_var <<"\n"; 
+      }
+    }
+  }
+  
+  BvToBoolVisitor bvToBoolVisitor(candidates); 
+  for (unsigned i = 0; i < assertions.size(); ++i) {
+    Node new_assertion = NodeVisitor<BvToBoolVisitor>::run(bvToBoolVisitor,
+                                              assertions[i]);
+    new_assertions.push_back(new_assertion); 
+  }
 }
diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h
index d5673a295..9b1534b41 100644
--- a/src/theory/bv/bv_to_bool.h
+++ b/src/theory/bv/bv_to_bool.h
@@ -24,33 +24,31 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-class BvToBoolVisitor {
+typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; 
+typedef __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> TNodeNodeMap; 
 
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; 
-  typedef __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> TNodeNodeMap; 
+class BvToBoolVisitor {
+  TNodeNodeMap d_bvToBoolMap; 
   TNodeNodeMap d_cache;
-  TNodeNodeMap d_bvToBoolTerm; 
-  TNodeSet d_visited;
   Node d_one;
   Node d_zero;
 
-  void storeBvToBool(TNode bv_term, Node bool_term);
-  Node getBoolTerm(TNode bv_term) const;
-  bool hasBoolTerm(TNode bv_term) const; 
-
   void addToCache(TNode term, Node new_term);
   Node getCache(TNode term) const;
   bool hasCache(TNode term) const; 
-
   
-  bool isConvertibleToBool(TNode current);
-  Node convertToBool(TNode current);
+  bool isConvertibleBvTerm(TNode node);
+  bool isConvertibleBvAtom(TNode node);
+  Node getBoolForBvTerm(TNode node);
+  void storeBvToBool(TNode bv_term, TNode bool_term);
+  Node convertBvAtom(TNode node);
+  Node convertBvTerm(TNode node);
+  void check(TNode current, TNode parent);
 public:
   typedef Node return_type;
-  BvToBoolVisitor()
-    : d_cache(),
-      d_bvToBoolTerm(),
-      d_visited(),
+  BvToBoolVisitor(TNodeNodeMap& bvToBool)
+    : d_bvToBoolMap(bvToBool), 
+      d_cache(),
       d_one(utils::mkConst(BitVector(1, 1u))),
       d_zero(utils::mkConst(BitVector(1, 0u)))
   {}
@@ -60,14 +58,14 @@ public:
   return_type done(TNode node);
 }; 
 
+
 class BvToBoolPreprocessor {
-  BvToBoolVisitor d_visitor; 
+  bool matchesBooleanPatern(TNode node);
 public:
   BvToBoolPreprocessor()
-    : d_visitor()
   {}
   ~BvToBoolPreprocessor() {}
-  Node liftBoolToBV(TNode assertion);
+  void liftBoolToBV(const std::vector<TNode>& assertions, std::vector<Node>& new_assertions);
 }; 
 
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 6f965879d..8c430d6d4 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1277,10 +1277,8 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
   }
 }
 
-Node TheoryEngine::ppBvToBool(TNode assertion) {
-  Node result = d_bvToBoolPreprocessor.liftBoolToBV(assertion);
-  result = Rewriter::rewrite(result);
-  return result; 
+void TheoryEngine::ppBvToBool(const std::vector<TNode>& assertions, std::vector<Node> new_assertions) {
+  d_bvToBoolPreprocessor.liftBoolToBV(assertions, new_assertions);
 }
 
 Node TheoryEngine::ppSimpITE(TNode assertion)
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 324b952b0..d581aeda2 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -753,7 +753,7 @@ private:
   theory::bv::BvToBoolPreprocessor d_bvToBoolPreprocessor; 
 public:
 
-  Node ppBvToBool(TNode assertion); 
+  void ppBvToBool(const std::vector<TNode>& assertions, std::vector<Node> new_assertions); 
   Node ppSimpITE(TNode assertion);
   void ppUnconstrainedSimp(std::vector<Node>& assertions);