Merge remote-tracking branch 'fork/betterSkolems' into cav2019strings

1 files changed, 23 insertions, 14 deletions

diff --git a/src/preprocessing/passes/bool_to_bv.h b/src/preprocessing/passes/bool_to_bv.h
index 49c9dc944..da99d3c84 100644
--- a/src/preprocessing/passes/bool_to_bv.h
+++ b/src/preprocessing/passes/bool_to_bv.h
@@ -2,14 +2,14 @@
 /*! \file bool_to_bv.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Yoni Zohar
+ **   Makai Mann, Yoni Zohar
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief The BoolToBv preprocessing pass
+ ** \brief The BoolToBV preprocessing pass
  **
  **/
 
@@ -18,9 +18,9 @@
 #ifndef __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H
 #define __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H
 
-#include "preprocessing/passes/bv_to_bool.h"
 #include "preprocessing/preprocessing_pass.h"
 #include "preprocessing/preprocessing_pass_context.h"
+#include "theory/bv/theory_bv_utils.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
@@ -39,24 +39,33 @@ class BoolToBV : public PreprocessingPass
  private:
   struct Statistics
   {
+    IntStat d_numIteToBvite;
     IntStat d_numTermsLowered;
-    IntStat d_numAtomsLowered;
     IntStat d_numTermsForcedLowered;
     Statistics();
     ~Statistics();
   };
 
-  void lowerBoolToBv(const std::vector<Node>& assertions,
-                     std::vector<Node>& new_assertions);
-  void addToLowerCache(TNode term, Node new_term);
-  Node getLowerCache(TNode term) const;
-  bool hasLowerCache(TNode term) const;
-  Node lowerNode(TNode current, bool topLevel = false);
-  NodeNodeMap d_lowerCache;
-  Node d_one;
-  Node d_zero;
+  /* Takes an assertion and tries to create more bit-vector structure */
+  Node lowerAssertion(const TNode& a);
+
+  /* Tries to lower one node to a width-one bit-vector */
+  void lowerNode(const TNode& n);
+
+  /* Returns cached node if it exists, otherwise returns the node */
+  Node fromCache(TNode n) const;
+
+  /** Checks if any of the nodes children were rebuilt,
+   *  in which case n needs to be rebuilt as well
+   */
+  bool needToRebuild(TNode n) const;
+
   Statistics d_statistics;
-};  // class
+
+  /* Keeps track of lowered nodes */
+  std::unordered_map<Node, Node, NodeHashFunction> d_lowerCache;
+};  // class BoolToBV
+
 }  // namespace passes
 }  // namespace preprocessing
 }  // namespace CVC4