Prevent ref count from reaching zero in BV instantiator (#3512)

diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
index eacc3032c7b198d1fa38572cf586677cc72c4f8d..c7aaf572c345335a462a3c523c8a081145a516ac 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
@@ -384,7 +384,7 @@ Node BvInstantiator::rewriteAssertionForSolvePv(CegInstantiator* ci,
   std::stack<std::unordered_map<TNode, Node, TNodeHashFunction> > visited;
   visited.push(std::unordered_map<TNode, Node, TNodeHashFunction>());
   // whether the visited term contains pv
-  std::unordered_map<TNode, bool, TNodeHashFunction> visited_contains_pv;
+  std::unordered_map<Node, bool, NodeHashFunction> visited_contains_pv;
   std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
   std::unordered_map<TNode, Node, TNodeHashFunction> curr_subs;
   std::stack<std::stack<TNode> > visit;
@@ -534,7 +534,7 @@ Node BvInstantiator::rewriteTermForSolvePv(
     Node pv,
     Node n,
     std::vector<Node>& children,
-    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv)
+    std::unordered_map<Node, bool, NodeHashFunction>& contains_pv)
 {
   NodeManager* nm = NodeManager::currentNM();
 

diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
index a548c959eda6046dd6e95e1e840f707266739529..3ad45d5be28512345c45a6c893139b644e02bbc0 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
@@ -140,7 +140,7 @@ class BvInstantiator : public Instantiator
       Node pv,
       Node n,
       std::vector<Node>& children,
-      std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv);
+      std::unordered_map<Node, bool, NodeHashFunction>& contains_pv);
   /** process literal, called from processAssertion
    *
    * lit is the literal to solve for pv that has been rewritten according to

diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp
index b351dc83cd2a1f16af1b13bda214745edff5cfa2..c1ad63fc860e9ccd0cff084704112372e7dcf247 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp
@@ -61,7 +61,7 @@ Node getPvCoeff(TNode pv, TNode n)
 Node normalizePvMult(
     TNode pv,
     const std::vector<Node>& children,
-    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv)
+    std::unordered_map<Node, bool, NodeHashFunction>& contains_pv)
 {
   bool neg, neg_coeff = false;
   bool found_pv = false;
@@ -141,7 +141,7 @@ namespace {
 bool isLinearPlus(
     TNode n,
     TNode pv,
-    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv)
+    std::unordered_map<Node, bool, NodeHashFunction>& contains_pv)
 {
   Node coeff;
   Assert(n.getAttribute(BvLinearAttribute()));
@@ -165,7 +165,7 @@ bool isLinearPlus(
 Node normalizePvPlus(
     Node pv,
     const std::vector<Node>& children,
-    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv)
+    std::unordered_map<Node, bool, NodeHashFunction>& contains_pv)
 {
   NodeManager* nm;
   NodeBuilder<> nb_c(BITVECTOR_PLUS);
@@ -254,7 +254,7 @@ Node normalizePvPlus(
 Node normalizePvEqual(
     Node pv,
     const std::vector<Node>& children,
-    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv)
+    std::unordered_map<Node, bool, NodeHashFunction>& contains_pv)
 {
   Assert(children.size() == 2);
 

diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h
index 7c72a29f202b9955979700004c8d66e2a808843f..8427f3df83d8343a2bbd77269e7c615257808aaa 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h
@@ -63,7 +63,7 @@ Node getPvCoeff(TNode pv, TNode n);
 Node normalizePvMult(
     TNode pv,
     const std::vector<Node>& children,
-    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv);
+    std::unordered_map<Node, bool, NodeHashFunction>& contains_pv);
 
 /**
  * Normalizes the children of a BITVECTOR_PLUS w.r.t. pv. contains_pv marks
@@ -83,7 +83,7 @@ Node normalizePvMult(
 Node normalizePvPlus(
     Node pv,
     const std::vector<Node>& children,
-    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv);
+    std::unordered_map<Node, bool, NodeHashFunction>& contains_pv);
 
 /**
  * Linearize an equality w.r.t. pv such that pv only occurs once. contains_pv
@@ -99,7 +99,7 @@ Node normalizePvPlus(
 Node normalizePvEqual(
     Node pv,
     const std::vector<Node>& children,
-    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv);
+    std::unordered_map<Node, bool, NodeHashFunction>& contains_pv);
 
 }  // namespace utils
 }  // namespace quantifiers

diff --git a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h
index 2b61aeb0022314c6cf7af34abd51fefa5f9e9005..0fa7a3f825a240361e80f652a5062b90b20e2654 100644 (file)
--- a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h
+++ b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h
@@ -153,7 +153,7 @@ void BvInstantiatorWhite::testNormalizePvMult()
   Node zero = mkZero(32);
   Node one = mkOne(32);
   BvLinearAttribute is_linear;
-  std::unordered_map<TNode, bool, TNodeHashFunction> contains_x;
+  std::unordered_map<Node, bool, NodeHashFunction> contains_x;
 
   contains_x[x] = true;
   contains_x[neg_x] = true;
@@ -251,7 +251,7 @@ void BvInstantiatorWhite::testNormalizePvPlus()
   Node c = mkVar(32);
   Node d = mkVar(32);
   BvLinearAttribute is_linear;
-  std::unordered_map<TNode, bool, TNodeHashFunction> contains_x;
+  std::unordered_map<Node, bool, NodeHashFunction> contains_x;
 
   contains_x[x] = true;
   contains_x[neg_x] = true;
@@ -374,7 +374,7 @@ void BvInstantiatorWhite::testNormalizePvEqual()
   Node one = mkOne(32);
   Node ntrue = mkTrue();
   BvLinearAttribute is_linear;
-  std::unordered_map<TNode, bool, TNodeHashFunction> contains_x;
+  std::unordered_map<Node, bool, NodeHashFunction> contains_x;
 
   contains_x[x] = true;
   contains_x[neg_x] = true;