mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

fixing drat proofs

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-01-12 00:30:21 -08:00
parent 836f156d54
commit 0b8dbf2854
3 changed files with 8 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/sat/sat_drat.cpp
View file

@ -68,7 +68,7 @@ namespace sat {
case status::asserted: return; case status::asserted: return;
case status::external: return; // requires extension to drat format. case status::external: return; // requires extension to drat format.
case status::learned: break; case status::learned: break;
case status::deleted: return; (*m_out) << "d "; break; case status::deleted: (*m_out) << "d "; break;
} }
for (unsigned i = 0; i < n; ++i) (*m_out) << c[i] << " "; for (unsigned i = 0; i < n; ++i) (*m_out) << c[i] << " ";
(*m_out) << "0\n"; (*m_out) << "0\n";
@ -220,6 +220,7 @@ namespace sat {
SASSERT(m_assignment[u.var()] != l_undef); SASSERT(m_assignment[u.var()] != l_undef);
}); });
#if 0
if (!m_inconsistent) { if (!m_inconsistent) {
literal_vector lits(n, c); literal_vector lits(n, c);
IF_VERBOSE(0, verbose_stream() << "not drup " << lits << "\n"); IF_VERBOSE(0, verbose_stream() << "not drup " << lits << "\n");
@ -268,6 +269,8 @@ namespace sat {
IF_VERBOSE(0, s.display(verbose_stream())); IF_VERBOSE(0, s.display(verbose_stream()));
exit(0); exit(0);
} }
#endif
for (unsigned i = num_units; i < m_units.size(); ++i) { for (unsigned i = num_units; i < m_units.size(); ++i) {
m_assignment[m_units[i].var()] = l_undef; m_assignment[m_units[i].var()] = l_undef;
} }
@ -568,7 +571,9 @@ namespace sat {
if (m_check) if (m_check)
append(l1, l2, status::deleted); append(l1, l2, status::deleted);
} }
void drat::del(clause& c) { void drat::del(clause& c) {
TRACE("sat", tout << "del: " << c << "\n";); TRACE("sat", tout << "del: " << c << "\n";);
if (m_out) dump(c.size(), c.begin(), status::deleted); if (m_out) dump(c.size(), c.begin(), status::deleted);
if (m_check) { if (m_check) {

9
src/sat/sat_simplifier.cpp
View file

@ -347,22 +347,17 @@ namespace sat {
return; return;
case 1: case 1:
s.assign(c[0], justification()); s.assign(c[0], justification());
c.restore(sz0); s.del_clause(c, false);
s.del_clause(c);
break; break;
case 2: case 2:
s.mk_bin_clause(c[0], c[1], c.is_learned()); s.mk_bin_clause(c[0], c[1], c.is_learned());
c.restore(sz0); s.del_clause(c, false);
s.del_clause(c, true);
break; break;
default: default:
*it2 = *it; *it2 = *it;
it2++; it2++;
if (!c.frozen()) { if (!c.frozen()) {
s.attach_clause(c); s.attach_clause(c);
if (sz != sz0 && s.m_config.m_drat) {
s.m_drat.add(c, true);
}
} }
break; break;
} }

1
src/sat/sat_solver.cpp
View file

@ -2382,7 +2382,6 @@ namespace sat {
while (num_marks > 0); while (num_marks > 0);
m_lemma[0] = ~consequent; m_lemma[0] = ~consequent;
m_drat.verify(m_lemma.size(), m_lemma.c_ptr());
learn_lemma_and_backjump(); learn_lemma_and_backjump();
return true; return true;
} }