mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
making simplifier code exception friendlier. Towards getting a handle on #939
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
e47e8c67c0
commit
26ae3a5abb
|
@ -168,14 +168,13 @@ namespace sat {
|
|||
m_need_cleanup = false;
|
||||
m_use_list.init(s.num_vars());
|
||||
init_visited();
|
||||
bool learned_in_use_lists = false;
|
||||
m_learned_in_use_lists = false;
|
||||
if (learned) {
|
||||
register_clauses(s.m_learned);
|
||||
learned_in_use_lists = true;
|
||||
m_learned_in_use_lists = true;
|
||||
}
|
||||
register_clauses(s.m_clauses);
|
||||
|
||||
|
||||
if (!learned && (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls))
|
||||
elim_blocked_clauses();
|
||||
|
||||
|
@ -184,7 +183,9 @@ namespace sat {
|
|||
|
||||
m_sub_counter = m_subsumption_limit;
|
||||
m_elim_counter = m_res_limit;
|
||||
unsigned old_num_elim_vars = m_num_elim_vars;
|
||||
m_old_num_elim_vars = m_num_elim_vars;
|
||||
|
||||
scoped_finalize _scoped_finalize(*this);
|
||||
|
||||
do {
|
||||
if (m_subsumption)
|
||||
|
@ -199,20 +200,22 @@ namespace sat {
|
|||
break;
|
||||
}
|
||||
while (!m_sub_todo.empty());
|
||||
}
|
||||
|
||||
bool vars_eliminated = m_num_elim_vars > old_num_elim_vars;
|
||||
void simplifier::scoped_finalize_fn() {
|
||||
bool vars_eliminated = m_num_elim_vars > m_old_num_elim_vars;
|
||||
|
||||
if (m_need_cleanup) {
|
||||
TRACE("after_simplifier", tout << "cleanning watches...\n";);
|
||||
cleanup_watches();
|
||||
cleanup_clauses(s.m_learned, true, vars_eliminated, learned_in_use_lists);
|
||||
cleanup_clauses(s.m_learned, true, vars_eliminated, m_learned_in_use_lists);
|
||||
cleanup_clauses(s.m_clauses, false, vars_eliminated, true);
|
||||
}
|
||||
else {
|
||||
TRACE("after_simplifier", tout << "skipping cleanup...\n";);
|
||||
if (vars_eliminated) {
|
||||
// must remove learned clauses with eliminated variables
|
||||
cleanup_clauses(s.m_learned, true, true, learned_in_use_lists);
|
||||
cleanup_clauses(s.m_learned, true, true, m_learned_in_use_lists);
|
||||
}
|
||||
}
|
||||
CASSERT("sat_solver", s.check_invariant());
|
||||
|
|
|
@ -91,6 +91,9 @@ namespace sat {
|
|||
unsigned m_num_sub_res;
|
||||
unsigned m_num_elim_lits;
|
||||
|
||||
bool m_learned_in_use_lists;
|
||||
unsigned m_old_num_elim_vars;
|
||||
|
||||
struct size_lt {
|
||||
bool operator()(clause const * c1, clause const * c2) const { return c1->size() > c2->size(); }
|
||||
};
|
||||
|
@ -170,6 +173,14 @@ namespace sat {
|
|||
struct subsumption_report;
|
||||
struct elim_var_report;
|
||||
|
||||
class scoped_finalize {
|
||||
simplifier& s;
|
||||
public:
|
||||
scoped_finalize(simplifier& s) : s(s) {}
|
||||
~scoped_finalize() { s.scoped_finalize_fn(); }
|
||||
};
|
||||
void scoped_finalize_fn();
|
||||
|
||||
public:
|
||||
simplifier(solver & s, params_ref const & p);
|
||||
~simplifier();
|
||||
|
|
Loading…
Reference in a new issue