Prevent ref count from reaching zero in BV instantiator

The `normalize*` methods in `ceg_bv_instantiator_utils.{h,cpp}` each modify a
map that marks terms in which `pv` occurs. The map was mapping `TNode`s to
`bool`s. The problem was that the keys in the map could be new terms that
needed to be kept alive for the map to remain valid. When compiling CVC4 with
Clang under macOS, `theory_quantifiers_bv_instantiator_white` and
`theory_quantifiers_bv_inverter_white` were failing because the reference count
of keys in the map reached zero. Generally, the critical keys are contained in
the result of the functions and kept alive by the `visited` stack in
`rewriteAssertionForSolvePv()`. The unit test
`theory_quantifiers_bv_instantiator_white` did not keep the results alive,
resulting in reference counts reaching zero. However, the failure of
`theory_quantifiers_bv_inverter_white` shows that the issue is not limited to
the unit tests of the `normalize*` methods. To avoid this issue, this commit
changes the map to use `Node` keys instead (so the map itself keeps the keys
alive).

4 files changed, 10 insertions, 10 deletions

diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
index eacc3032c..c7aaf572c 100644
--- 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 a548c959e..3ad45d5be 100644
--- 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 b351dc83c..c1ad63fc8 100644
--- 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 7c72a29f2..8427f3df8 100644
--- 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