mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 19:02:02 +00:00
Code Activity

fix initialization/finalization order for bdd

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-06-19 23:11:06 -07:00
parent 947ea66cad
commit 4bcfcecbbb
2 changed files with 5 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/dd/dd_bdd.cpp
View file

@ -1009,7 +1009,7 @@ namespace dd {
bool carry = false; bool carry = false;
result.push_back(b[0]); result.push_back(b[0]);
for (unsigned i = 1; i < b.size(); ++i) { for (unsigned i = 1; i < b.size(); ++i) {
carry |= b[i-1]; carry = carry || b[i-1];
result.push_back(carry ^ b[i]); result.push_back(carry ^ b[i]);
} }
return result; return result;

7
src/math/polysat/solver.h
View file

@ -56,13 +56,13 @@ namespace polysat {
typedef ptr_vector<constraint> constraints; typedef ptr_vector<constraint> constraints;
reslimit& m_lim; reslimit& m_lim;
linear_solver m_linear_solver; dd::bdd_manager m_bdd;
scoped_ptr_vector<dd::pdd_manager> m_pdd; scoped_ptr_vector<dd::pdd_manager> m_pdd;
scoped_ptr_vector<dd::fdd> m_bits; scoped_ptr_vector<dd::fdd> m_bits;
dd::bdd_manager m_bdd;
dep_value_manager m_value_manager; dep_value_manager m_value_manager;
small_object_allocator m_alloc; small_object_allocator m_alloc;
poly_dep_manager m_dm; poly_dep_manager m_dm;
linear_solver m_linear_solver;
constraints_and_clauses m_conflict; constraints_and_clauses m_conflict;
// constraints m_stash_just; // constraints m_stash_just;
var_queue m_free_vars; var_queue m_free_vars;
@ -204,7 +204,8 @@ namespace polysat {
void decide_bool(sat::literal lit, clause& lemma); void decide_bool(sat::literal lit, clause& lemma);
void propagate_bool(sat::literal lit, clause* reason); 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(); } bool is_assigned(pvar v) const { return !m_justification[v].is_unassigned(); }