mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

produce binary clauses for DRAT for units produced by probing

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-01-14 10:56:10 -08:00
parent 0b84c60886
commit a686aa7f56
2 changed files with 10 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/sat/sat_drat.cpp
View file

@ -483,10 +483,6 @@ namespace sat {
literal lit = c[i]; literal lit = c[i];
if (lit != wc.m_l1 && lit != wc.m_l2 && value(lit) != l_false) { if (lit != wc.m_l1 && lit != wc.m_l2 && value(lit) != l_false) {
wc.m_l2 = lit; 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); m_watches[(~lit).index()].push_back(idx);
done = true; done = true;
} }

12
src/sat/sat_probing.cpp
View file

@ -65,6 +65,10 @@ namespace sat {
if (implied_lits) { if (implied_lits) {
for (literal lit : *implied_lits) { for (literal lit : *implied_lits) {
if (m_assigned.contains(lit)) { 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()); s.assign(lit, justification());
m_num_assigned++; m_num_assigned++;
} }
@ -95,8 +99,12 @@ namespace sat {
cache_bins(l, old_tr_sz); cache_bins(l, old_tr_sz);
s.pop(1); s.pop(1);
for (literal l : m_to_assert) { for (literal lit : m_to_assert) {
s.assign(l, justification()); 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++; m_num_assigned++;
} }
} }