mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Fix cleanup/initialization of sat::simplifier. Relates to #570.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-11-09 18:00:15 +00:00
parent ca81e803cb
commit 44d05e5375
6 changed files with 119 additions and 96 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/sat/sat_clause.h
View file

@ -102,10 +102,14 @@ namespace sat {
unsigned m_val1;
unsigned m_val2;
public:
bin_clause(literal l1, literal l2, bool learned):m_val1(l1.to_uint()), m_val2((l2.to_uint() << 1) + static_cast<unsigned>(learned)) {}
bin_clause(literal l1, literal l2, bool learned) :m_val1(l1.to_uint()), m_val2((l2.to_uint() << 1) + static_cast<unsigned>(learned)) {}
literal get_literal1() const { return to_literal(m_val1); }
literal get_literal2() const { return to_literal(m_val2 >> 1); }
bool is_learned() const { return (m_val2 & 1) == 1; }
bool operator==(const bin_clause & other) const {
return m_val1 == other.m_val1 && m_val2 == other.m_val2 ||
m_val1 == other.m_val2 && m_val2 == other.m_val1;
}
};
class tmp_clause {

2
src/sat/sat_probing.cpp
View file

@ -256,7 +256,7 @@ namespace sat {
}
void probing::free_memory() {
m_assigned.cleanup();
m_assigned.finalize();
m_to_assert.finalize();
}

32
src/sat/sat_simplifier.cpp
View file

@ -63,6 +63,7 @@ namespace sat {
}
simplifier::~simplifier() {
free_memory();
}
inline watch_list & simplifier::get_wlist(literal l) { return s.get_wlist(l); }
@ -96,7 +97,7 @@ namespace sat {
inline void simplifier::remove_clause_core(clause & c) {
unsigned sz = c.size();
for (unsigned i = 0; i < sz; i++)
insert_todo(c[i].var());
insert_elim_todo(c[i].var());
m_sub_todo.erase(c);
c.set_removed(true);
TRACE("resolution_bug", tout << "del_clause: " << c << "\n";);
@ -116,6 +117,7 @@ namespace sat {
inline void simplifier::remove_bin_clause_half(literal l1, literal l2, bool learned) {
SASSERT(s.get_wlist(~l1).contains(watched(l2, learned)));
s.get_wlist(~l1).erase(watched(l2, learned));
m_sub_bin_todo.erase(bin_clause(l1, l2, learned));
}
void simplifier::init_visited() {
@ -127,27 +129,36 @@ namespace sat {
m_use_list.finalize();
m_sub_todo.finalize();
m_sub_bin_todo.finalize();
m_elim_todo.finalize();
m_visited.finalize();
m_bs_cs.finalize();
m_bs_ls.finalize();
}
void simplifier::initialize() {
m_need_cleanup = false;
s.m_cleaner(true);
m_last_sub_trail_sz = s.m_trail.size();
m_use_list.init(s.num_vars());
m_sub_todo.reset();
m_sub_bin_todo.reset();
m_elim_todo.reset();
init_visited();
TRACE("after_cleanup", s.display(tout););
CASSERT("sat_solver", s.check_invariant());
}
void simplifier::operator()(bool learned) {
if (s.inconsistent())
return;
if (!m_subsumption && !m_elim_blocked_clauses && !m_resolution)
return;
initialize();
CASSERT("sat_solver", s.check_invariant());
TRACE("before_simplifier", s.display(tout););
s.m_cleaner(true);
m_last_sub_trail_sz = s.m_trail.size();
TRACE("after_cleanup", s.display(tout););
CASSERT("sat_solver", s.check_invariant());
m_need_cleanup = false;
m_use_list.init(s.num_vars());
init_visited();
bool learned_in_use_lists = false;
if (learned) {
register_clauses(s.m_learned);
@ -158,7 +169,6 @@ namespace sat {
if (!learned && (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls))
elim_blocked_clauses();
if (!learned)
m_num_calls++;
@ -617,7 +627,7 @@ namespace sat {
TRACE("elim_lit", tout << "processing: " << c << "\n";);
m_need_cleanup = true;
m_num_elim_lits++;
insert_todo(l.var());
insert_elim_todo(l.var());
c.elim(l);
clause_use_list & occurs = m_use_list.get(l);
occurs.erase_not_removed(c);
@ -1235,12 +1245,14 @@ namespace sat {
for (; it2 != end2; ++it2) {
if (it2->is_binary_clause() && it2->get_literal() == l) {
TRACE("bin_clause_bug", tout << "removing: " << l << " " << it2->get_literal() << "\n";);
m_sub_bin_todo.erase(bin_clause(l2, l, it2->is_learned()));
continue;
}
*itprev = *it2;
itprev++;
}
wlist2.set_end(itprev);
m_sub_bin_todo.erase(bin_clause(l, l2, it->is_learned()));
}
}
TRACE("bin_clause_bug", tout << "collapsing watch_list of: " << l << "\n";);

11
src/sat/sat_simplifier.h
View file

@ -97,6 +97,8 @@ namespace sat {
void checkpoint();
void initialize();
void init_visited();
void mark_visited(literal l) { m_visited[l.index()] = true; }
void unmark_visited(literal l) { m_visited[l.index()] = false; }
@ -172,8 +174,13 @@ namespace sat {
simplifier(solver & s, params_ref const & p);
~simplifier();
void insert_todo(bool_var v) { m_elim_todo.insert(v); }
void reset_todo() { m_elim_todo.reset(); }
void insert_elim_todo(bool_var v) { m_elim_todo.insert(v); }
void reset_todos() {
m_elim_todo.reset();
m_sub_todo.reset();
m_sub_bin_todo.reset();
}
void operator()(bool learned);

4
src/sat/sat_solver.cpp
View file

@ -141,7 +141,7 @@ namespace sat {
m_prev_phase.push_back(PHASE_NOT_AVAILABLE);
m_assigned_since_gc.push_back(false);
m_case_split_queue.mk_var_eh(v);
m_simplifier.insert_todo(v);
m_simplifier.insert_elim_todo(v);
SASSERT(!was_eliminated(v));
return v;
}
@ -2674,7 +2674,7 @@ namespace sat {
m_phase.shrink(v);
m_prev_phase.shrink(v);
m_assigned_since_gc.shrink(v);
m_simplifier.reset_todo();
m_simplifier.reset_todos();
}
}

4
src/sat/sat_types.h
View file

@ -200,7 +200,7 @@ namespace sat {
iterator begin() const { return m_set.begin(); }
iterator end() const { return m_set.end(); }
void reset() { m_set.reset(); m_in_set.reset(); }
void cleanup() { m_set.finalize(); m_in_set.finalize(); }
void finalize() { m_set.finalize(); m_in_set.finalize(); }
uint_set& operator&=(uint_set const& other) {
unsigned j = 0;
for (unsigned i = 0; i < m_set.size(); ++i) {
@ -259,7 +259,7 @@ namespace sat {
bool empty() const { return m_set.empty(); }
unsigned size() const { return m_set.size(); }
void reset() { m_set.reset(); }
void cleanup() { m_set.cleanup(); }
void finalize() { m_set.finalize(); }
class iterator {
uint_set::iterator m_it;
public: