From a658e46b1f68255d785abed12b7d6bd8b62266f9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 12 Oct 2017 15:46:25 -0700 Subject: [PATCH] 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); ); }