mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

Fixed potential SAT solver cleanup problem. Renamed functions for consistency. Relates to #570.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-11-10 17:06:55 +00:00
parent 40d90a951c
commit d66530a112
6 changed files with 13 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/sat/sat_probing.cpp
View file

@ -239,7 +239,7 @@ namespace sat {
m_counter *= 2; m_counter *= 2;
} }
CASSERT("probing", s.check_invariant()); CASSERT("probing", s.check_invariant());
free_memory(); finalize();
return r; return r;
} }
@ -255,9 +255,10 @@ namespace sat {
// TODO // TODO
} }
void probing::free_memory() { void probing::finalize() {
m_assigned.finalize(); m_assigned.finalize();
m_to_assert.finalize(); m_to_assert.finalize();
m_cached_bins.finalize();
} }
void probing::collect_statistics(statistics & st) const { void probing::collect_statistics(statistics & st) const {

2
src/sat/sat_probing.h
View file

@ -69,7 +69,7 @@ namespace sat {
void updt_params(params_ref const & p); void updt_params(params_ref const & p);
static void collect_param_descrs(param_descrs & d); static void collect_param_descrs(param_descrs & d);
void free_memory(); void finalize();
void collect_statistics(statistics & st) const; void collect_statistics(statistics & st) const;
void reset_statistics(); void reset_statistics();

10
src/sat/sat_simplifier.cpp
View file

@ -63,7 +63,7 @@ namespace sat {
} }
simplifier::~simplifier() { simplifier::~simplifier() {
free_memory(); finalize();
} }
inline watch_list & simplifier::get_wlist(literal l) { return s.get_wlist(l); } inline watch_list & simplifier::get_wlist(literal l) { return s.get_wlist(l); }
@ -125,7 +125,7 @@ namespace sat {
m_visited.resize(2*s.num_vars(), false); m_visited.resize(2*s.num_vars(), false);
} }
void simplifier::free_memory() { void simplifier::finalize() {
m_use_list.finalize(); m_use_list.finalize();
m_sub_todo.finalize(); m_sub_todo.finalize();
m_sub_bin_todo.finalize(); m_sub_bin_todo.finalize();
@ -154,6 +154,7 @@ namespace sat {
if (!m_subsumption && !m_elim_blocked_clauses && !m_resolution) if (!m_subsumption && !m_elim_blocked_clauses && !m_resolution)
return; return;
initialize(); initialize();
CASSERT("sat_solver", s.check_invariant()); CASSERT("sat_solver", s.check_invariant());
@ -166,6 +167,7 @@ namespace sat {
} }
register_clauses(s.m_clauses); register_clauses(s.m_clauses);
if (!learned && (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls)) if (!learned && (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls))
elim_blocked_clauses(); elim_blocked_clauses();
@ -207,7 +209,7 @@ namespace sat {
} }
CASSERT("sat_solver", s.check_invariant()); CASSERT("sat_solver", s.check_invariant());
TRACE("after_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout);); TRACE("after_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout););
free_memory(); finalize();
} }
/** /**
@ -932,8 +934,8 @@ namespace sat {
model_converter::entry * new_entry = 0; model_converter::entry * new_entry = 0;
if (s.is_external(l.var()) || s.was_eliminated(l.var())) if (s.is_external(l.var()) || s.was_eliminated(l.var()))
return; return;
{
{
m_to_remove.reset(); m_to_remove.reset();
{ {
clause_use_list & occs = s.m_use_list.get(l); clause_use_list & occs = s.m_use_list.get(l);

2
src/sat/sat_simplifier.h
View file

@ -187,7 +187,7 @@ namespace sat {
void updt_params(params_ref const & p); void updt_params(params_ref const & p);
static void collect_param_descrs(param_descrs & d); static void collect_param_descrs(param_descrs & d);
void free_memory(); void finalize();
void collect_statistics(statistics & st) const; void collect_statistics(statistics & st) const;
void reset_statistics(); void reset_statistics();

2
src/sat/sat_solver.cpp
View file

@ -3042,7 +3042,7 @@ namespace sat {
if (scope_lvl() > 0 || inconsistent()) if (scope_lvl() > 0 || inconsistent())
return; return;
m_simplifier(learned); m_simplifier(learned);
m_simplifier.free_memory(); m_simplifier.finalize();
if (m_ext) if (m_ext)
m_ext->clauses_modifed(); m_ext->clauses_modifed();
} }

1
src/sat/sat_solver.h
View file

@ -239,6 +239,7 @@ namespace sat {
void checkpoint() { void checkpoint() {
if (!m_rlimit.inc()) { if (!m_rlimit.inc()) {
m_mc.reset(); m_mc.reset();
m_model_is_current = false;
throw solver_exception(Z3_CANCELED_MSG); throw solver_exception(Z3_CANCELED_MSG);
} }
++m_num_checkpoints; ++m_num_checkpoints;