mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

tweak control flow for empty clauses

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-07-23 18:16:00 -07:00
parent 48deb4d3e0
commit 6c8b8609ee
2 changed files with 7 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/sat/sat_proof_trim.cpp
View file

@ -40,7 +40,6 @@ namespace sat {
conflict_analysis_core(m_conflict, m_conflict_clause);
m_trail.pop_back();
for (unsigned i = m_trail.size(); i-- > 0; ) {
auto const& [id, cl, clp, is_add, is_initial] = m_trail[i];
if (!is_add) {
@ -384,13 +383,17 @@ namespace sat {
return false;
};
if (all_of(m_clause, [&](sat::literal lit) { return s.value(lit) == l_false; }))
return;
if (m_clause.size() == 2 && is_unit2())
s.propagate_bin_clause(m_clause[0], m_clause[1]);
else if (m_clause.size() > 2 && is_unit())
s.propagate_clause(*cl, true, 0, s.cls_allocator().get_offset(cl));
s.propagate(false);
if (s.inconsistent() || all_of(m_clause, [&](sat::literal lit) { return s.value(lit) == l_false; }))
set_conflict(m_clause, cl);
if (s.inconsistent() || all_of(m_clause, [&](sat::literal lit) { return s.value(lit) == l_false; })) {
IF_VERBOSE(3, verbose_stream() << "conflict " << m_clause << "\n");
set_conflict(m_clause, cl);
}
}
/**

2
src/sat/smt/euf_solver.cpp
View file

@ -272,7 +272,7 @@ namespace euf {
if (create_hint) {
log_justifications(l, ez, is_euf);
if (reduced || multiple_theories)
if (l != sat::null_literal && (reduced || multiple_theories))
log_rup(l, r);
}
}