From 4bcfcecbbbfd48720ecb54d68b61155dd0aa8881 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 19 Jun 2021 23:11:06 -0700 Subject: [PATCH] fix initialization/finalization order for bdd Signed-off-by: Nikolaj Bjorner --- src/math/dd/dd_bdd.cpp | 2 +- src/math/polysat/solver.h | 7 ++++--- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/math/dd/dd_bdd.cpp b/src/math/dd/dd_bdd.cpp index 357409877..d3a9e88b4 100644 --- a/src/math/dd/dd_bdd.cpp +++ b/src/math/dd/dd_bdd.cpp @@ -1009,7 +1009,7 @@ namespace dd { bool carry = false; result.push_back(b[0]); for (unsigned i = 1; i < b.size(); ++i) { - carry |= b[i-1]; + carry = carry || b[i-1]; result.push_back(carry ^ b[i]); } return result; diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 2763c1b78..055393b61 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -56,13 +56,13 @@ namespace polysat { typedef ptr_vector constraints; reslimit& m_lim; - linear_solver m_linear_solver; + dd::bdd_manager m_bdd; scoped_ptr_vector m_pdd; scoped_ptr_vector m_bits; - dd::bdd_manager m_bdd; dep_value_manager m_value_manager; small_object_allocator m_alloc; poly_dep_manager m_dm; + linear_solver m_linear_solver; constraints_and_clauses m_conflict; // constraints m_stash_just; var_queue m_free_vars; @@ -204,7 +204,8 @@ namespace polysat { void decide_bool(sat::literal lit, clause& lemma); void propagate_bool(sat::literal lit, clause* reason); - void assign_core(pvar v, rational const& val, justification const& j); + void assign_core(pvar v, rational const& val, justification + const& j); bool is_assigned(pvar v) const { return !m_justification[v].is_unassigned(); }