From a686aa7f5628248eb8819dfc96845c25b73c5e19 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 14 Jan 2019 10:56:10 -0800 Subject: [PATCH] produce binary clauses for DRAT for units produced by probing Signed-off-by: Nikolaj Bjorner --- src/sat/sat_drat.cpp | 4 ---- src/sat/sat_probing.cpp | 12 ++++++++++-- 2 files changed, 10 insertions(+), 6 deletions(-) diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index 110ad3b8a..e7b9088d5 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -483,10 +483,6 @@ namespace sat { literal lit = c[i]; if (lit != wc.m_l1 && lit != wc.m_l2 && value(lit) != l_false) { wc.m_l2 = lit; - if (m_watches.size() <= (~lit).index()) - { - IF_VERBOSE(0, verbose_stream() << m_watches.size() << " " << lit << " " << (~lit).index() << "\n"); - } m_watches[(~lit).index()].push_back(idx); done = true; } diff --git a/src/sat/sat_probing.cpp b/src/sat/sat_probing.cpp index 52ab9f9f7..e76a3f7c4 100644 --- a/src/sat/sat_probing.cpp +++ b/src/sat/sat_probing.cpp @@ -65,6 +65,10 @@ namespace sat { if (implied_lits) { for (literal lit : *implied_lits) { if (m_assigned.contains(lit)) { + if (s.m_config.m_drat) { + s.m_drat.add(l, lit, true); + s.m_drat.add(~l, lit, true); + } s.assign(lit, justification()); m_num_assigned++; } @@ -95,8 +99,12 @@ namespace sat { cache_bins(l, old_tr_sz); s.pop(1); - for (literal l : m_to_assert) { - s.assign(l, justification()); + for (literal lit : m_to_assert) { + if (s.m_config.m_drat) { + s.m_drat.add(l, lit, true); + s.m_drat.add(~l, lit, true); + } + s.assign(lit, justification()); m_num_assigned++; } }