mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 20:03:38 +00:00
Code Activity

move exchange par

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-02-01 12:12:26 -08:00
parent 40177f7bac
commit 256a0e2d82
2 changed files with 5 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/sat/sat_solver.cpp
View file

@ -84,7 +84,7 @@ namespace sat {
VERIFY(v == mk_var(ext, dvar)); VERIFY(v == mk_var(ext, dvar));
} }
} }
unsigned sz = src.scope_lvl() == 0 ? src.m_trail.size() : src.m_scopes[0].m_trail_lim; unsigned sz = src.init_trail_size();
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
assign(src.m_trail[i], justification()); assign(src.m_trail[i], justification());
} }
@ -774,7 +774,6 @@ namespace sat {
restart(); restart();
simplify_problem(); simplify_problem();
exchange_par();
if (check_inconsistent()) return l_false; if (check_inconsistent()) return l_false;
gc(); gc();
@ -890,9 +889,8 @@ namespace sat {
*/ */
void solver::exchange_par() { void solver::exchange_par() {
if (m_par && scope_lvl() == 0) { if (m_par && scope_lvl() == 0) {
unsigned sz = scope_lvl() == 0 ? m_trail.size() : m_scopes[0].m_trail_lim; unsigned sz = init_trail_size();
unsigned num_in = 0, num_out = 0; unsigned num_in = 0, num_out = 0;
SASSERT(scope_lvl() == 0); // parallel with assumptions is TBD
literal_vector in, out; literal_vector in, out;
for (unsigned i = m_par_limit_out; i < sz; ++i) { for (unsigned i = m_par_limit_out; i < sz; ++i) {
literal lit = m_trail[i]; literal lit = m_trail[i];
@ -2546,6 +2544,7 @@ namespace sat {
void solver::pop_reinit(unsigned num_scopes) { void solver::pop_reinit(unsigned num_scopes) {
pop(num_scopes); pop(num_scopes);
exchange_par();
reinit_assumptions(); reinit_assumptions();
} }
@ -2865,7 +2864,7 @@ namespace sat {
} }
void solver::display_units(std::ostream & out) const { void solver::display_units(std::ostream & out) const {
unsigned end = scope_lvl() == 0 ? m_trail.size() : m_scopes[0].m_trail_lim; unsigned end = init_trail_size();
for (unsigned i = 0; i < end; i++) { for (unsigned i = 0; i < end; i++) {
out << m_trail[i] << " "; out << m_trail[i] << " ";
} }

1
src/sat/sat_solver.h
View file

@ -223,6 +223,7 @@ namespace sat {
lbool value(bool_var v) const { return static_cast<lbool>(m_assignment[literal(v, false).index()]); } lbool value(bool_var v) const { return static_cast<lbool>(m_assignment[literal(v, false).index()]); }
unsigned lvl(bool_var v) const { return m_level[v]; } unsigned lvl(bool_var v) const { return m_level[v]; }
unsigned lvl(literal l) const { return m_level[l.var()]; } unsigned lvl(literal l) const { return m_level[l.var()]; }
unsigned init_trail_size() const { return scope_lvl() == 0 ? m_trail.size() : m_scopes[0].m_trail_lim; }
void assign(literal l, justification j) { void assign(literal l, justification j) {
TRACE("sat_assign", tout << l << " previous value: " << value(l) << "\n";); TRACE("sat_assign", tout << l << " previous value: " << value(l) << "\n";);
switch (value(l)) { switch (value(l)) {