From a658e46b1f68255d785abed12b7d6bd8b62266f9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 12 Oct 2017 15:46:25 -0700 Subject: [PATCH 1/2] removing failed literal macro Signed-off-by: Nikolaj Bjorner --- src/sat/sat_lookahead.cpp | 15 --------------- 1 file changed, 15 deletions(-) diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index ed5976838..00a469a0a 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -1576,7 +1576,6 @@ namespace sat { TRACE("sat_verbose", display(tout << scope_lvl() << " " << (inconsistent()?"unsat":"sat") << "\n");); } -#define CHECK_FAILED_LITERAL 0 void lookahead::compute_lookahead_reward() { init_lookahead_reward(); @@ -1585,10 +1584,6 @@ namespace sat { unsigned base = 2; bool change = true; literal last_changed = null_literal; -#if CHECK_FAILED_LITERAL - unsigned_vector assigns; - literal_vector assigns_lits; -#endif while (change && !inconsistent()) { change = false; for (unsigned i = 0; !inconsistent() && i < m_lookahead.size(); ++i) { @@ -1616,10 +1611,6 @@ namespace sat { if (unsat) { TRACE("sat", tout << "backtracking and settting " << ~lit << "\n";); reset_lookahead_reward(); -#if CHECK_FAILED_LITERAL - assigns.push_back(m_trail.size()); - assigns_lits.push_back(~lit); -#endif assign(~lit); propagate(); init_lookahead_reward(); @@ -1639,12 +1630,6 @@ namespace sat { base += 2 * m_lookahead.size(); } reset_lookahead_reward(); -#if CHECK_FAILED_LITERAL - for (unsigned i = 0; i < assigns.size(); ++i) { - std::cout << "check trail: " << m_trail[assigns[i]] << " " << assigns_lits[i] << "\n"; - VERIFY(m_trail[assigns[i]] == assigns_lits[i]); - } -#endif TRACE("sat", display_lookahead(tout); ); } From 25c1b41c516ceb886ece86e726e8268d442ad9b9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 12 Oct 2017 15:56:09 -0700 Subject: [PATCH 2/2] tidy Signed-off-by: Nikolaj Bjorner --- src/sat/sat_lookahead.cpp | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index c468ebbc1..9a0740cb5 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -1078,8 +1078,7 @@ namespace sat { TRACE("sat", tout << "windfall: " << nlit << " " << l2 << "\n";); // if we use try_add_binary, then this may produce new assignments // these assignments get put on m_trail, and they are cleared by - // reset_lookahead_reward. We would need to distinguish the trail that comes - // from lookahead levels and the main search level for this to work. + // lookahead_backtrack. add_binary(nlit, l2); } m_stats.m_windfall_binaries += m_wstack.size(); @@ -1578,13 +1577,11 @@ namespace sat { while (!inconsistent() && m_qhead < m_trail.size()) { unsigned i = m_qhead; unsigned sz = m_trail.size(); - //for (; i < m_trail.size() && !inconsistent(); ++i) { for (; i < sz && !inconsistent(); ++i) { literal l = m_trail[i]; TRACE("sat", tout << "propagate " << l << " @ " << m_level << "\n";); propagate_binary(l); } - //while (m_qhead < m_trail.size() && !inconsistent()) { while (m_qhead < sz && !inconsistent()) { propagate_clauses(m_trail[m_qhead++]); } @@ -1629,7 +1626,6 @@ namespace sat { pop_lookahead1(lit, num_units); if (unsat) { TRACE("sat", tout << "backtracking and settting " << ~lit << "\n";); - //reset_lookahead_reward(); assign(~lit); propagate(); change = true;