innd examples are solved fast, but destruction assertion fail

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f8ec2294320e1d30d5328edea91c57e8d1489ec0..35db0975e918cf0b182f91b767f2129502f5ec67 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1928,11 +1928,11 @@ bool SmtEnginePrivate::nonClausalSimplify() {
 
 
 void SmtEnginePrivate::bvToBool() {
-  Trace("simplify") << "SmtEnginePrivate::bvToBool()" << endl;
+  Trace("bv-to-bool") << "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] = Rewriter::rewrite(new_assertions[i]); 
+    d_assertionsToCheck[i] = Rewriter::rewrite(new_assertions[i]);
   }
 }
 

diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp
index 44c4bd0217e0e48cf9bd0e14b312374fbb534769..8084a728228937eadbcc01f5266cd7e8d54a320c 100644 (file)
--- a/src/theory/bv/bv_to_bool.cpp
+++ b/src/theory/bv/bv_to_bool.cpp
@@ -30,7 +30,7 @@ void BvToBoolVisitor::addToCache(TNode term, Node new_term) {
 }
 
 Node BvToBoolVisitor::getCache(TNode term) const {
-  if (!hasCache(term)) {
+  if (!hasCache(term) || term.getKind() == kind::CONST_BITVECTOR) {
     return term; 
   }
   return d_cache.find(term)->second; 
@@ -62,9 +62,11 @@ bool BvToBoolVisitor::isConvertibleBvAtom(TNode node) {
   Kind kind = node.getKind();
   return (kind == kind::BITVECTOR_ULT ||
           kind == kind::BITVECTOR_ULE ||
+          kind == kind::BITVECTOR_SLT ||
+          kind == kind::BITVECTOR_SLE ||
           kind == kind::EQUAL) &&
-    node[0].getType().isBitVector() &&
-    node[0].getType().getBitVectorSize() == 1; 
+    isConvertibleBvTerm(node[0]) &&
+    isConvertibleBvTerm(node[1]); 
 }
 
 bool BvToBoolVisitor::isConvertibleBvTerm(TNode node) {
@@ -81,6 +83,10 @@ bool BvToBoolVisitor::isConvertibleBvTerm(TNode node) {
     return true; 
   }
 
+  if (kind == kind::ITE) {
+    return isConvertibleBvTerm(node[1]) && isConvertibleBvTerm(node[2]); 
+  }
+
   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) {
@@ -98,32 +104,51 @@ Node BvToBoolVisitor::convertBvAtom(TNode node) {
   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 = getBoolForBvTerm(node[0]);
+    Node b = getBoolForBvTerm(node[1]);
+    Node a_eq_0 = utils::mkNode(kind::IFF, a, utils::mkFalse());
+    Node b_eq_1 = utils::mkNode(kind::IFF, b, utils::mkTrue());
     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 = getBoolForBvTerm(node[0]);
+   Node b = getBoolForBvTerm(node[1]);
+   Node a_eq_0 = utils::mkNode(kind::IFF, a, utils::mkFalse());
+   Node b_eq_1 = utils::mkNode(kind::IFF, b, utils::mkTrue());
    Node a_lt_b = utils::mkNode(kind::AND, a_eq_0, b_eq_1); 
-   Node a_eq_b = utils::mkNode(kind::EQUAL, a, b);
+   Node a_eq_b = utils::mkNode(kind::IFF, a, b);
    result = utils::mkNode(kind::OR, a_lt_b, a_eq_b);    
    break;
   }
+  case kind::BITVECTOR_SLT: {
+    Node a = getBoolForBvTerm(node[0]);
+    Node b = getBoolForBvTerm(node[1]);
+    Node a_eq_1 = utils::mkNode(kind::IFF, a, utils::mkTrue());
+    Node b_eq_0 = utils::mkNode(kind::IFF, b, utils::mkFalse());
+    result = utils::mkNode(kind::AND, a_eq_1, b_eq_0);
+    break; 
+  }
+  case kind::BITVECTOR_SLE: {
+    Node a = getBoolForBvTerm(node[0]);
+    Node b = getBoolForBvTerm(node[1]);
+    Node a_eq_1 = utils::mkNode(kind::IFF, a, utils::mkTrue());
+    Node b_eq_0 = utils::mkNode(kind::IFF, b, utils::mkFalse());
+    Node a_slt_b = utils::mkNode(kind::AND, a_eq_1, b_eq_0);
+    Node a_eq_b = utils::mkNode(kind::IFF, a, b);
+    result = utils::mkNode(kind::OR, a_slt_b, a_eq_b); 
+    break; 
+  }
   case kind::EQUAL: {
-    TNode a = getBoolForBvTerm(node[0]);
-    TNode b = getBoolForBvTerm(node[1]);
+    Node a = getBoolForBvTerm(node[0]);
+    Node b = getBoolForBvTerm(node[1]);
     result = utils::mkNode(kind::IFF, a, b); 
     break;
   }
   default:
     Unhandled(); 
   }
+  Debug("bv-to-bool") << "BvToBoolVisitor::convertBvAtom " << node <<" => " << result << "\n"; 
   Assert (result != Node());
   return result;
 }
@@ -138,16 +163,19 @@ Node BvToBoolVisitor::convertBvTerm(TNode node) {
       return getBoolForBvTerm(node);
     }
     if (node.getKind() == kind::CONST_BITVECTOR) {
-      return (node == d_one ? utils::mkTrue() : utils::mkFalse());
+      Node result = node == d_one ? utils::mkTrue() : utils::mkFalse();
+      storeBvToBool(node, result); 
+      return result; 
     }
   }
   
   if (kind == kind::ITE) {
-    TNode cond = getCache(node[0]);
-    TNode true_branch = getBoolForBvTerm(node[1]);
-    TNode false_branch = getBoolForBvTerm(node[2]);
+    Node cond = getCache(node[0]);
+    Node true_branch = getBoolForBvTerm(node[1]);
+    Node false_branch = getBoolForBvTerm(node[2]);
     Node result = utils::mkNode(kind::ITE, cond, true_branch, false_branch);
     storeBvToBool(node, result);
+    Debug("bv-to-bool") << "BvToBoolVisitor::convertBvTerm " << node <<" => " << result << "\n"; 
     return result; 
   }
   
@@ -175,6 +203,7 @@ Node BvToBoolVisitor::convertBvTerm(TNode node) {
   }
   Node result = builder;
   storeBvToBool(node, result);
+  Debug("bv-to-bool") << "BvToBoolVisitor::convertBvTerm " << node <<" => " << result << "\n"; 
   return result; 
 }
 
@@ -191,9 +220,8 @@ void BvToBoolVisitor::visit(TNode current, TNode parent) {
   Debug("bv-to-bool") << "BvToBoolVisitor visit (" << current << ", " << parent << ")\n"; 
   Assert (!alreadyVisited(current, parent) &&
           !hasCache(current));
-  
-  Node result;
 
+  Node result;
   // make sure that the bv terms we are replacing to not occur in other contexts
   check(current, parent); 
   
@@ -217,14 +245,20 @@ void BvToBoolVisitor::visit(TNode current, TNode parent) {
       result = builder;
     }
   }
-  Assert (result != Node()); 
+  Assert (result != Node());
+  Debug("bv-to-bool") << "    =>" << result <<"\n"; 
   addToCache(current, result);
 }
 
 
 BvToBoolVisitor::return_type BvToBoolVisitor::done(TNode node) {
   Assert (hasCache(node)); 
-  return getCache(node); 
+  Node result = getCache(node);
+  return result; 
+}
+
+bool BvToBoolVisitor::hasBoolTerm(TNode node) {
+  return d_bvToBoolMap.find(node) != d_bvToBoolMap.end(); 
 }
 
 bool BvToBoolPreprocessor::matchesBooleanPatern(TNode current) {
@@ -242,7 +276,8 @@ bool BvToBoolPreprocessor::matchesBooleanPatern(TNode current) {
 
 
 void BvToBoolPreprocessor::liftBoolToBV(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
-  TNodeNodeMap candidates;
+  BvToBoolVisitor bvToBoolVisitor;
+  
   for (unsigned i = 0; i < assertions.size(); ++i) {
     if (matchesBooleanPatern(assertions[i])) {
       TNode assertion = assertions[i]; 
@@ -250,21 +285,21 @@ void BvToBoolPreprocessor::liftBoolToBV(const std::vector<Node>& assertions, std
       Assert (bv_var.getKind() == kind::VARIABLE &&
               bv_var.getType().isBitVector() &&
               bv_var.getType().getBitVectorSize() == 1);
-      TNode bool_cond = assertion[1];
+      Node bool_cond = NodeVisitor<BvToBoolVisitor>::run(bvToBoolVisitor, assertion[1]);
       Assert (bool_cond.getType().isBoolean());
-      if (candidates.find(bv_var) == candidates.end()) {
+      if (!bvToBoolVisitor.hasBoolTerm(bv_var)) {
         Debug("bv-to-bool") << "BBvToBoolPreprocessor::liftBvToBoolBV candidate: " << bv_var <<"\n"; 
-        candidates[bv_var] = bool_cond;
+        bvToBoolVisitor.storeBvToBool(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); 
+    new_assertions.push_back(new_assertion);
+    Trace("bv-to-bool") << "  " << assertions[i] <<" => " << new_assertions[i] <<"\n"; 
   }
 }

diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h
index 39c6b4251bafbbbe7c6639e9020938eeba068c5f..186f2b317971ad51370dbaccc77a66a8e950a83b 100644 (file)
--- a/src/theory/bv/bv_to_bool.h
+++ b/src/theory/bv/bv_to_bool.h
@@ -25,11 +25,11 @@ namespace theory {
 namespace bv {
 
 typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; 
-typedef __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> TNodeNodeMap; 
+typedef __gnu_cxx::hash_map<Node, Node, TNodeHashFunction> NodeNodeMap; 
 
 class BvToBoolVisitor {
-  TNodeNodeMap d_bvToBoolMap; 
-  TNodeNodeMap d_cache;
+  NodeNodeMap d_bvToBoolMap; 
+  NodeNodeMap d_cache;
   Node d_one;
   Node d_zero;
 
@@ -40,14 +40,13 @@ class BvToBoolVisitor {
   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(TNodeNodeMap& bvToBool)
-    : d_bvToBoolMap(bvToBool), 
+  BvToBoolVisitor()
+    : d_bvToBoolMap(), 
       d_cache(),
       d_one(utils::mkConst(BitVector(1, 1u))),
       d_zero(utils::mkConst(BitVector(1, 0u)))
@@ -56,6 +55,8 @@ public:
   bool alreadyVisited(TNode current, TNode parent);
   void visit(TNode current, TNode parent);
   return_type done(TNode node);
+  void storeBvToBool(TNode bv_term, TNode bool_term);
+  bool hasBoolTerm(TNode node); 
 }; 
 
 

diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h
index 768508d2c31ef371cfd14e02750ca3ca81932fb1..5f89af9c6bb339266f9020d3bf8c1a5e67d23718 100644 (file)
--- a/src/theory/term_registration_visitor.h
+++ b/src/theory/term_registration_visitor.h
@@ -95,7 +95,11 @@ public:
    * Notifies the engine of all the theories used.
    */
   bool done(TNode node);
-
+  ~PreRegisterVisitor() {
+    for (TNodeToTheorySetMap::const_iterator it = d_visited.begin(); it != d_visited.end(); ++it) {
+      std::cout << it->first <<"\n"; 
+    }
+  }
 };
 
 

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 22a0b00ed8178e9167dc194246c8c553ae33a229..6c8341345cfb508a90682ada8d8f418adf9550ea 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1277,7 +1277,7 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
   }
 }
 
-void TheoryEngine::ppBvToBool(const std::vector<Node>& assertions, std::vector<Node> new_assertions) {
+void TheoryEngine::ppBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
   d_bvToBoolPreprocessor.liftBoolToBV(assertions, new_assertions);
 }
 

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 6d355ccce4a5e315a91121112b9ddc146e9c7c80..c21819ea1deff2a18418912fcc5a24a5eac94763 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -753,7 +753,7 @@ private:
   theory::bv::BvToBoolPreprocessor d_bvToBoolPreprocessor; 
 public:
 
-  void ppBvToBool(const std::vector<Node>& assertions, std::vector<Node> new_assertions); 
+  void ppBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); 
   Node ppSimpITE(TNode assertion);
   void ppUnconstrainedSimp(std::vector<Node>& assertions);