mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

prepare ground for drup trim

Browse source 
By not deleting justifications in base level unit literals it is possible for drup-trim to inspect the trail for dependencies - which clauses were used to derive a literal.
This commit is contained in:
Nikolaj Bjorner 2022-06-12 10:45:39 -07:00
parent 35d4605425
commit 25ad5cb073
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/sat/sat_drat.cpp
View file

@ -802,7 +802,7 @@ namespace sat {
// //
// placeholder for trim function. // placeholder for trim function.
// 1. forward pass replaying propositional proof, populate trail stack. // 1. trail contains justification for the empty clause.
// 2. backward pass to prune. // 2. backward pass to prune.
// //
svector<std::pair<clause&, status>> drat::trim() { svector<std::pair<clause&, status>> drat::trim() {

4
src/sat/sat_solver.cpp
View file

@ -945,8 +945,8 @@ namespace sat {
if (j.level() == 0) { if (j.level() == 0) {
if (m_config.m_drat) if (m_config.m_drat)
drat_log_unit(l, j); drat_log_unit(l, j);
if (!m_config.m_drup_trim)
j = justification(0); // erase justification for level 0 j = justification(0); // erase justification for level 0
} }
else { else {
VERIFY(!at_base_lvl()); VERIFY(!at_base_lvl());