From 25ad5cb073ca81fd3b06cad9940c8ab6080c3b9b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 12 Jun 2022 10:45:39 -0700 Subject: [PATCH] prepare ground for drup trim 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. --- src/sat/sat_drat.cpp | 2 +- src/sat/sat_solver.cpp | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index 0731100778f..d5ea181c473 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -802,7 +802,7 @@ namespace sat { // // 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. // svector> drat::trim() { diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 9d84d843936..f8f187fc2d5 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -945,8 +945,8 @@ namespace sat { if (j.level() == 0) { if (m_config.m_drat) drat_log_unit(l, j); - - j = justification(0); // erase justification for level 0 + if (!m_config.m_drup_trim) + j = justification(0); // erase justification for level 0 } else { VERIFY(!at_base_lvl());