mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

introducing scoped detacth/attach of clauses to enforce basic sat solver invariants. Part of investigating #939:

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-03-22 14:12:47 -07:00
parent 25d839ed10
commit e47e8c67c0
5 changed files with 42 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/sat/sat_asymm_branch.cpp
View file

@ -96,7 +96,6 @@ namespace sat {
if (!process(c)) if (!process(c))
continue; // clause was removed continue; // clause was removed
*it2 = *it; *it2 = *it;
// throw exception to test bug fix: if (it2 != it) throw solver_exception("trigger bug");
++it2; ++it2;
} }
s.m_clauses.set_end(it2); s.m_clauses.set_end(it2);
@ -129,14 +128,14 @@ namespace sat {
// check if the clause is already satisfied // check if the clause is already satisfied
for (i = 0; i < sz; i++) { for (i = 0; i < sz; i++) {
if (s.value(c[i]) == l_true) { if (s.value(c[i]) == l_true) {
s.dettach_clause(c); s.detach_clause(c);
s.del_clause(c); s.del_clause(c);
return false; return false;
} }
} }
// try asymmetric branching // try asymmetric branching
// clause must not be used for propagation // clause must not be used for propagation
s.dettach_clause(c); solver::scoped_detach scoped_d(s, c);
s.push(); s.push();
for (i = 0; i < sz - 1; i++) { for (i = 0; i < sz - 1; i++) {
literal l = c[i]; literal l = c[i];
@ -154,7 +153,6 @@ namespace sat {
SASSERT(s.m_qhead == s.m_trail.size()); SASSERT(s.m_qhead == s.m_trail.size());
if (i == sz - 1) { if (i == sz - 1) {
// clause size can't be reduced. // clause size can't be reduced.
s.attach_clause(c);
return true; return true;
} }
// clause can be reduced // clause can be reduced
@ -189,18 +187,17 @@ namespace sat {
TRACE("asymm_branch", tout << "produced unit clause: " << c[0] << "\n";); TRACE("asymm_branch", tout << "produced unit clause: " << c[0] << "\n";);
s.assign(c[0], justification()); s.assign(c[0], justification());
s.propagate_core(false); s.propagate_core(false);
s.del_clause(c); scoped_d.del_clause();
SASSERT(s.inconsistent() || s.m_qhead == s.m_trail.size()); 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], false); s.mk_bin_clause(c[0], c[1], false);
s.del_clause(c); scoped_d.del_clause();
SASSERT(s.m_qhead == s.m_trail.size()); SASSERT(s.m_qhead == s.m_trail.size());
return false; return false;
default: default:
c.shrink(new_sz); c.shrink(new_sz);
s.attach_clause(c);
SASSERT(s.m_qhead == s.m_trail.size()); SASSERT(s.m_qhead == s.m_trail.size());
return true; return true;
} }

2
src/sat/sat_elim_eqs.cpp
View file

@ -94,7 +94,7 @@ namespace sat {
continue; continue;
} }
if (!c.frozen()) if (!c.frozen())
m_solver.dettach_clause(c); m_solver.detach_clause(c);
// apply substitution // apply substitution
for (i = 0; i < sz; i++) { for (i = 0; i < sz; i++) {
SASSERT(!m_solver.was_eliminated(c[i].var())); SASSERT(!m_solver.was_eliminated(c[i].var()));

24
src/sat/sat_solver.cpp
View file

@ -462,25 +462,25 @@ namespace sat {
return simplify_clause_core<false>(num_lits, lits); return simplify_clause_core<false>(num_lits, lits);
} }
void solver::dettach_bin_clause(literal l1, literal l2, bool learned) { void solver::detach_bin_clause(literal l1, literal l2, bool learned) {
get_wlist(~l1).erase(watched(l2, learned)); get_wlist(~l1).erase(watched(l2, learned));
get_wlist(~l2).erase(watched(l1, learned)); get_wlist(~l2).erase(watched(l1, learned));
} }
void solver::dettach_clause(clause & c) { void solver::detach_clause(clause & c) {
if (c.size() == 3) if (c.size() == 3)
dettach_ter_clause(c); detach_ter_clause(c);
else else
dettach_nary_clause(c); detach_nary_clause(c);
} }
void solver::dettach_nary_clause(clause & c) { void solver::detach_nary_clause(clause & c) {
clause_offset cls_off = get_offset(c); clause_offset cls_off = get_offset(c);
erase_clause_watch(get_wlist(~c[0]), cls_off); erase_clause_watch(get_wlist(~c[0]), cls_off);
erase_clause_watch(get_wlist(~c[1]), cls_off); erase_clause_watch(get_wlist(~c[1]), cls_off);
} }
void solver::dettach_ter_clause(clause & c) { void solver::detach_ter_clause(clause & c) {
erase_ternary_watch(get_wlist(~c[0]), c[1], c[2]); erase_ternary_watch(get_wlist(~c[0]), c[1], c[2]);
erase_ternary_watch(get_wlist(~c[1]), c[0], c[2]); erase_ternary_watch(get_wlist(~c[1]), c[0], c[2]);
erase_ternary_watch(get_wlist(~c[2]), c[0], c[1]); erase_ternary_watch(get_wlist(~c[2]), c[0], c[1]);
@ -1493,7 +1493,7 @@ namespace sat {
for (unsigned i = new_sz; i < sz; i++) { for (unsigned i = new_sz; i < sz; i++) {
clause & c = *(m_learned[i]); clause & c = *(m_learned[i]);
if (can_delete(c)) { if (can_delete(c)) {
dettach_clause(c); detach_clause(c);
del_clause(c); del_clause(c);
} }
else { else {
@ -1551,7 +1551,7 @@ namespace sat {
else { else {
c.inc_inact_rounds(); c.inc_inact_rounds();
if (c.inact_rounds() > m_config.m_gc_k) { if (c.inact_rounds() > m_config.m_gc_k) {
dettach_clause(c); detach_clause(c);
del_clause(c); del_clause(c);
m_stats.m_gc_clause++; m_stats.m_gc_clause++;
deleted++; deleted++;
@ -1562,7 +1562,7 @@ namespace sat {
if (psm(c) > static_cast<unsigned>(c.size() * m_min_d_tk)) { if (psm(c) > static_cast<unsigned>(c.size() * m_min_d_tk)) {
// move to frozen; // move to frozen;
TRACE("sat_frozen", tout << "freezing size: " << c.size() << " psm: " << psm(c) << " " << c << "\n";); TRACE("sat_frozen", tout << "freezing size: " << c.size() << " psm: " << psm(c) << " " << c << "\n";);
dettach_clause(c); detach_clause(c);
c.reset_inact_rounds(); c.reset_inact_rounds();
c.freeze(); c.freeze();
m_num_frozen++; m_num_frozen++;
@ -2595,7 +2595,7 @@ namespace sat {
} }
else { else {
clause & c = *(cw.get_clause()); clause & c = *(cw.get_clause());
dettach_clause(c); detach_clause(c);
attach_clause(c, reinit); attach_clause(c, reinit);
if (scope_lvl() > 0 && reinit) { if (scope_lvl() > 0 && reinit) {
// clause propagated literal, must keep it in the reinit stack. // clause propagated literal, must keep it in the reinit stack.
@ -2628,7 +2628,7 @@ namespace sat {
for (unsigned i = 0; i < clauses.size(); ++i) { for (unsigned i = 0; i < clauses.size(); ++i) {
clause & c = *(clauses[i]); clause & c = *(clauses[i]);
if (c.contains(lit)) { if (c.contains(lit)) {
dettach_clause(c); detach_clause(c);
del_clause(c); del_clause(c);
} }
else { else {
@ -2646,7 +2646,7 @@ namespace sat {
literal l1 = m_user_bin_clauses[i].first; literal l1 = m_user_bin_clauses[i].first;
literal l2 = m_user_bin_clauses[i].second; literal l2 = m_user_bin_clauses[i].second;
if (nlit == l1 || nlit == l2) { if (nlit == l1 || nlit == l2) {
dettach_bin_clause(l1, l2, learned); detach_bin_clause(l1, l2, learned);
} }
} }
} }

27
src/sat/sat_solver.h
View file

@ -195,15 +195,34 @@ namespace sat {
bool attach_nary_clause(clause & c); bool attach_nary_clause(clause & c);
void attach_clause(clause & c, bool & reinit); void attach_clause(clause & c, bool & reinit);
void attach_clause(clause & c) { bool reinit; attach_clause(c, reinit); } void attach_clause(clause & c) { bool reinit; attach_clause(c, reinit); }
class scoped_detach {
solver& s;
clause& c;
bool m_deleted;
public:
scoped_detach(solver& s, clause& c): s(s), c(c), m_deleted(false) {
s.detach_clause(c);
}
~scoped_detach() {
if (!m_deleted) s.attach_clause(c);
}
void del_clause() {
if (!m_deleted) {
s.del_clause(c);
m_deleted = true;
}
}
};
unsigned select_watch_lit(clause const & cls, unsigned starting_at) const; unsigned select_watch_lit(clause const & cls, unsigned starting_at) const;
unsigned select_learned_watch_lit(clause const & cls) const; unsigned select_learned_watch_lit(clause const & cls) const;
bool simplify_clause(unsigned & num_lits, literal * lits) const; bool simplify_clause(unsigned & num_lits, literal * lits) const;
template<bool lvl0> template<bool lvl0>
bool simplify_clause_core(unsigned & num_lits, literal * lits) const; bool simplify_clause_core(unsigned & num_lits, literal * lits) const;
void dettach_bin_clause(literal l1, literal l2, bool learned); void detach_bin_clause(literal l1, literal l2, bool learned);
void dettach_clause(clause & c); void detach_clause(clause & c);
void dettach_nary_clause(clause & c); void detach_nary_clause(clause & c);
void dettach_ter_clause(clause & c); void detach_ter_clause(clause & c);
void push_reinit_stack(clause & c); void push_reinit_stack(clause & c);
// ----------------------- // -----------------------

2
src/util/small_object_allocator.cpp
View file

@ -70,6 +70,7 @@ void small_object_allocator::reset() {
void small_object_allocator::deallocate(size_t size, void * p) { void small_object_allocator::deallocate(size_t size, void * p) {
if (size == 0) return; if (size == 0) return;
#if defined(Z3DEBUG) && !defined(_WINDOWS) #if defined(Z3DEBUG) && !defined(_WINDOWS)
// Valgrind friendly // Valgrind friendly
memory::deallocate(p); memory::deallocate(p);
@ -93,6 +94,7 @@ void small_object_allocator::deallocate(size_t size, void * p) {
void * small_object_allocator::allocate(size_t size) { void * small_object_allocator::allocate(size_t size) {
if (size == 0) return 0; if (size == 0) return 0;
#if defined(Z3DEBUG) && !defined(_WINDOWS) #if defined(Z3DEBUG) && !defined(_WINDOWS)
// Valgrind friendly // Valgrind friendly
return memory::allocate(size); return memory::allocate(size);