mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-14 14:55:25 +00:00
Code Activity

propagate during asymmetric branching

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-03-26 15:17:41 -07:00
parent 7063ad81cc
commit 96b717f494
2 changed files with 4 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/sat/sat_asymm_branch.cpp
View file

@ -108,7 +108,6 @@ namespace sat {
int64 limit = -m_asymm_branch_limit; int64 limit = -m_asymm_branch_limit;
std::stable_sort(clauses.begin(), clauses.end(), clause_size_lt()); std::stable_sort(clauses.begin(), clauses.end(), clause_size_lt());
m_counter -= clauses.size(); m_counter -= clauses.size();
SASSERT(s.m_qhead == s.m_trail.size());
clause_vector::iterator it = clauses.begin(); clause_vector::iterator it = clauses.begin();
clause_vector::iterator it2 = it; clause_vector::iterator it2 = it;
clause_vector::iterator end = clauses.end(); clause_vector::iterator end = clauses.end();
@ -120,7 +119,6 @@ namespace sat {
} }
break; break;
} }
SASSERT(s.m_qhead == s.m_trail.size());
clause & c = *(*it); clause & c = *(*it);
if (m_counter < limit || s.inconsistent() || c.was_removed()) { if (m_counter < limit || s.inconsistent() || c.was_removed()) {
*it2 = *it; *it2 = *it;
@ -414,19 +412,16 @@ namespace sat {
s.assign(c[0], justification()); s.assign(c[0], justification());
s.propagate_core(false); s.propagate_core(false);
scoped_d.del_clause(); scoped_d.del_clause();
SASSERT(s.inconsistent() || s.m_qhead == s.m_trail.size());
return false; // check_missed_propagation() may fail, since m_clauses is not in a consistent state. return false; // check_missed_propagation() may fail, since m_clauses is not in a consistent state.
case 2: case 2:
SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef); SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef);
s.mk_bin_clause(c[0], c[1], c.is_learned()); s.mk_bin_clause(c[0], c[1], c.is_learned());
scoped_d.del_clause(); scoped_d.del_clause();
SASSERT(s.m_qhead == s.m_trail.size());
return false; return false;
default: default:
c.shrink(new_sz); c.shrink(new_sz);
if (s.m_config.m_drat) s.m_drat.add(c, true); if (s.m_config.m_drat) s.m_drat.add(c, true);
// if (s.m_config.m_drat) s.m_drat.del(c0); // TBD // if (s.m_config.m_drat) s.m_drat.del(c0); // TBD
SASSERT(s.m_qhead == s.m_trail.size());
return true; return true;
} }
} }
@ -445,12 +440,8 @@ namespace sat {
bool asymm_branch::process(clause & c) { bool asymm_branch::process(clause & c) {
TRACE("asymm_branch_detail", tout << "processing: " << c << "\n";); TRACE("asymm_branch_detail", tout << "processing: " << c << "\n";);
SASSERT(s.scope_lvl() == 0); SASSERT(s.scope_lvl() == 0);
SASSERT(s.m_qhead == s.m_trail.size());
SASSERT(!s.inconsistent()); SASSERT(!s.inconsistent());
#ifdef Z3DEBUG
unsigned trail_sz = s.m_trail.size();
#endif
unsigned sz = c.size(); unsigned sz = c.size();
SASSERT(sz > 0); SASSERT(sz > 0);
unsigned i; unsigned i;
@ -468,14 +459,15 @@ namespace sat {
// try asymmetric branching // try asymmetric branching
// clause must not be used for propagation // clause must not be used for propagation
s.propagate(false);
if (s.inconsistent())
return true;
scoped_detach scoped_d(s, c); scoped_detach scoped_d(s, c);
unsigned new_sz = c.size(); unsigned new_sz = c.size();
unsigned flip_position = m_rand(c.size()); unsigned flip_position = m_rand(c.size());
bool found_conflict = flip_literal_at(c, flip_position, new_sz); bool found_conflict = flip_literal_at(c, flip_position, new_sz);
SASSERT(!s.inconsistent()); SASSERT(!s.inconsistent());
SASSERT(s.scope_lvl() == 0); SASSERT(s.scope_lvl() == 0);
SASSERT(trail_sz == s.m_trail.size());
SASSERT(s.m_qhead == s.m_trail.size());
if (!found_conflict) { if (!found_conflict) {
// clause size can't be reduced. // clause size can't be reduced.
return true; return true;

2
src/sat/sat_solver.cpp
View file

@ -324,7 +324,7 @@ namespace sat {
case 2: case 2:
mk_bin_clause(lits[0], lits[1], learned); mk_bin_clause(lits[0], lits[1], learned);
if (learned && m_par) m_par->share_clause(*this, lits[0], lits[1]); if (learned && m_par) m_par->share_clause(*this, lits[0], lits[1]);
return 0; return nullptr;
case 3: case 3:
return mk_ter_clause(lits, learned); return mk_ter_clause(lits, learned);
default: default: