Merging CAV14 paper bit-vector work.

1 files changed, 25 insertions, 32 deletions

diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h
index b34923728..28501ba96 100644
--- a/src/theory/bv/bv_to_bool.h
+++ b/src/theory/bv/bv_to_bool.h
@@ -16,6 +16,7 @@
 
 #include "cvc4_private.h"
 #include "theory/bv/theory_bv_utils.h"
+#include "util/statistics_registry.h"
 
 #ifndef __CVC4__THEORY__BV__BV_TO_BOOL_H
 #define __CVC4__THEORY__BV__BV_TO_BOOL_H
@@ -24,51 +25,43 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; 
-typedef __gnu_cxx::hash_map<Node, Node, TNodeHashFunction> NodeNodeMap; 
+typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap; 
 
-class BvToBoolVisitor {
-  NodeNodeMap d_bvToBoolMap; 
-  NodeNodeMap d_cache;
+class BvToBoolPreprocessor {
+
+  struct Statistics {
+    IntStat d_numTermsLifted;
+    IntStat d_numAtomsLifted;
+    IntStat d_numTermsForcedLifted;
+    Statistics();
+    ~Statistics();
+  };
+  
+  NodeNodeMap d_liftCache;
+  NodeNodeMap d_boolCache;
   Node d_one;
   Node d_zero;
 
-  void addToCache(TNode term, Node new_term);
-  Node getCache(TNode term) const;
-  bool hasCache(TNode term) const; 
+  void addToBoolCache(TNode term, Node new_term);
+  Node getBoolCache(TNode term) const;
+  bool hasBoolCache(TNode term) const; 
+
+  void addToLiftCache(TNode term, Node new_term);
+  Node getLiftCache(TNode term) const;
+  bool hasLiftCache(TNode term) const; 
   
   bool isConvertibleBvTerm(TNode node);
   bool isConvertibleBvAtom(TNode node);
-  Node getBoolForBvTerm(TNode node);
   Node convertBvAtom(TNode node);
   Node convertBvTerm(TNode node);
-  void check(TNode current, TNode parent);
+  Node liftNode(TNode current);
+  Statistics d_statistics;
 public:
-  typedef Node return_type;
-  BvToBoolVisitor()
-    : d_bvToBoolMap(), 
-      d_cache(),
-      d_one(utils::mkConst(BitVector(1, 1u))),
-      d_zero(utils::mkConst(BitVector(1, 0u)))
-  {}
-  void start(TNode node);
-  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); 
+  BvToBoolPreprocessor();
+  void liftBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
 }; 
 
 
-class BvToBoolPreprocessor {
-  bool matchesBooleanPatern(TNode node);
-public:
-  BvToBoolPreprocessor()
-  {}
-  ~BvToBoolPreprocessor() {}
-  void liftBoolToBV(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
-}; 
-
 
 }/* CVC4::theory::bv namespace */
 }/* CVC4::theory namespace */