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

make the unsat/sat verdicts from cubing produce empty clause and models respectively

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-10-01 15:52:22 -07:00
parent 75b77979fe
commit 08c58ae614
2 changed files with 28 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/sat_lookahead.cpp
View file

@ -2137,6 +2137,8 @@ namespace sat {
if (lit == null_literal) { if (lit == null_literal) {
vars.reset(); vars.reset();
for (auto v : m_freevars) if (in_reduced_clause(v)) vars.push_back(v); for (auto v : m_freevars) if (in_reduced_clause(v)) vars.push_back(v);
m_model.reset();
init_model();
return l_true; return l_true;
} }
TRACE("sat", tout << "choose: " << lit << " cube: " << m_cube_state.m_cube << "\n";); TRACE("sat", tout << "choose: " << lit << " cube: " << m_cube_state.m_cube << "\n";);

28
src/sat/sat_solver.cpp
View file

@ -1014,14 +1014,38 @@ namespace sat {
} }
lbool solver::cube(bool_var_vector& vars, literal_vector& lits, unsigned backtrack_level) { lbool solver::cube(bool_var_vector& vars, literal_vector& lits, unsigned backtrack_level) {
if (!m_cuber) { bool is_first = !m_cuber;
if (is_first) {
m_cuber = alloc(lookahead, *this); m_cuber = alloc(lookahead, *this);
} }
lbool result = m_cuber->cube(vars, lits, backtrack_level); lbool result = m_cuber->cube(vars, lits, backtrack_level);
m_cuber->update_cube_statistics(m_aux_stats); m_cuber->update_cube_statistics(m_aux_stats);
if (result == l_false) { switch (result) {
case l_false:
dealloc(m_cuber); dealloc(m_cuber);
m_cuber = nullptr; m_cuber = nullptr;
if (is_first) {
pop_to_base_level();
set_conflict(justification());
}
break;
case l_true: {
pop_to_base_level();
model const& mdl = m_cuber->get_model();
for (bool_var v = 0; v < mdl.size(); ++v) {
if (value(v) != l_undef) {
continue;
}
literal l(v, false);
if (mdl[v] != l_true) l.neg();
push();
assign_core(l, justification());
}
mk_model();
break;
}
default:
break;
} }
return result; return result;
} }