From ac9808bdc0c6d5619f636691bd737079b50b9ea5 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Sun, 1 Dec 2019 14:57:25 -0800 Subject: [PATCH] Prevent ref count from reaching zero in BV instantiator (#3512) --- src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp | 4 ++-- src/theory/quantifiers/cegqi/ceg_bv_instantiator.h | 2 +- .../quantifiers/cegqi/ceg_bv_instantiator_utils.cpp | 8 ++++---- src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h | 6 +++--- .../theory/theory_quantifiers_bv_instantiator_white.h | 6 +++--- 5 files changed, 13 insertions(+), 13 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 > visited; visited.push(std::unordered_map()); // whether the visited term contains pv - std::unordered_map visited_contains_pv; + std::unordered_map visited_contains_pv; std::unordered_map::iterator it; std::unordered_map curr_subs; std::stack > visit; @@ -534,7 +534,7 @@ Node BvInstantiator::rewriteTermForSolvePv( Node pv, Node n, std::vector& children, - std::unordered_map& contains_pv) + std::unordered_map& 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& children, - std::unordered_map& contains_pv); + std::unordered_map& 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& children, - std::unordered_map& contains_pv) + std::unordered_map& 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& contains_pv) + std::unordered_map& contains_pv) { Node coeff; Assert(n.getAttribute(BvLinearAttribute())); @@ -165,7 +165,7 @@ bool isLinearPlus( Node normalizePvPlus( Node pv, const std::vector& children, - std::unordered_map& contains_pv) + std::unordered_map& contains_pv) { NodeManager* nm; NodeBuilder<> nb_c(BITVECTOR_PLUS); @@ -254,7 +254,7 @@ Node normalizePvPlus( Node normalizePvEqual( Node pv, const std::vector& children, - std::unordered_map& contains_pv) + std::unordered_map& 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& children, - std::unordered_map& contains_pv); + std::unordered_map& 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& children, - std::unordered_map& contains_pv); + std::unordered_map& 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& children, - std::unordered_map& contains_pv); + std::unordered_map& 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 2b61aeb00..0fa7a3f82 100644 --- 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 contains_x; + std::unordered_map 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 contains_x; + std::unordered_map 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 contains_x; + std::unordered_map contains_x; contains_x[x] = true; contains_x[neg_x] = true; -- 2.30.2