mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

removing failed literal macro

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-12 15:46:25 -07:00
parent 4adf4d4ac2
commit a658e46b1f
1 changed files with 0 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/sat/sat_lookahead.cpp
View file

@ -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); );
}