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

track empty clause during pop

Browse source 
If a theory solver creates the empty clause it gets dropped during pop.
By maintaining a variable m_empty_clause, the solver ensures that it retains the information that the search state is inconsistent.
This commit is contained in:
Nikolaj Bjorner 2019-12-09 11:10:37 +03:00
parent ebb7d60c75
commit 5cecd986e2
3 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/smt_context.cpp
View file

@ -75,6 +75,7 @@ namespace smt {
m_phase_default(false), m_phase_default(false),
m_conflict(null_b_justification), m_conflict(null_b_justification),
m_not_l(null_literal), m_not_l(null_literal),
m_empty_clause(false),
m_conflict_resolution(mk_conflict_resolution(m, *this, m_dyn_ack_manager, p, m_assigned_literals, m_watches)), m_conflict_resolution(mk_conflict_resolution(m, *this, m_dyn_ack_manager, p, m_assigned_literals, m_watches)),
m_unsat_proof(m), m_unsat_proof(m),
m_dyn_ack_manager(*this, p), m_dyn_ack_manager(*this, p),
@ -2395,9 +2396,10 @@ namespace smt {
m_unsat_proof = nullptr; m_unsat_proof = nullptr;
} }
m_base_scopes.shrink(new_lvl); m_base_scopes.shrink(new_lvl);
m_empty_clause = false;
} }
else { else {
m_conflict = null_b_justification; m_conflict = m_empty_clause ? b_justification::mk_axiom() : null_b_justification;
m_not_l = null_literal; m_not_l = null_literal;
} }
del_clauses(m_aux_clauses, s.m_aux_clauses_lim); del_clauses(m_aux_clauses, s.m_aux_clauses_lim);

5
src/smt/smt_context.h
View file

@ -188,9 +188,12 @@ namespace smt {
// A conflict is usually a single justification. That is, a justification // A conflict is usually a single justification. That is, a justification
// for false. If m_not_l is not null_literal, then m_conflict is a // for false. If m_not_l is not null_literal, then m_conflict is a
// justification for l, and the conflict is union of m_no_l and m_conflict; // justification for l, and the conflict is union of m_not_l and m_conflict;
// m_empty_clause is set to ensure that an empty clause generated in deep scope
// levels survives to the base level.
b_justification m_conflict; b_justification m_conflict;
literal m_not_l; literal m_not_l;
bool m_empty_clause;
scoped_ptr<conflict_resolution> m_conflict_resolution; scoped_ptr<conflict_resolution> m_conflict_resolution;
proof_ref m_unsat_proof; proof_ref m_unsat_proof;

1
src/smt/smt_internalizer.cpp
View file

@ -1351,6 +1351,7 @@ namespace smt {
m_justifications.push_back(j); m_justifications.push_back(j);
TRACE("mk_clause", tout << "empty clause... setting conflict\n";); TRACE("mk_clause", tout << "empty clause... setting conflict\n";);
set_conflict(j == nullptr ? b_justification::mk_axiom() : b_justification(j)); set_conflict(j == nullptr ? b_justification::mk_axiom() : b_justification(j));
m_empty_clause = true;
SASSERT(inconsistent()); SASSERT(inconsistent());
return nullptr; return nullptr;
case 1: case 1: