mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

tidy

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-12 15:56:09 -07:00
parent f86b85274a
commit 25c1b41c51
1 changed files with 1 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/sat/sat_lookahead.cpp
View file

@ -1078,8 +1078,7 @@ namespace sat {
TRACE("sat", tout << "windfall: " << nlit << " " << l2 << "\n";); TRACE("sat", tout << "windfall: " << nlit << " " << l2 << "\n";);
// if we use try_add_binary, then this may produce new assignments // if we use try_add_binary, then this may produce new assignments
// these assignments get put on m_trail, and they are cleared by // these assignments get put on m_trail, and they are cleared by
// reset_lookahead_reward. We would need to distinguish the trail that comes // lookahead_backtrack.
// from lookahead levels and the main search level for this to work.
add_binary(nlit, l2); add_binary(nlit, l2);
} }
m_stats.m_windfall_binaries += m_wstack.size(); m_stats.m_windfall_binaries += m_wstack.size();
@ -1578,13 +1577,11 @@ namespace sat {
while (!inconsistent() && m_qhead < m_trail.size()) { while (!inconsistent() && m_qhead < m_trail.size()) {
unsigned i = m_qhead; unsigned i = m_qhead;
unsigned sz = m_trail.size(); unsigned sz = m_trail.size();
//for (; i < m_trail.size() && !inconsistent(); ++i) {
for (; i < sz && !inconsistent(); ++i) { for (; i < sz && !inconsistent(); ++i) {
literal l = m_trail[i]; literal l = m_trail[i];
TRACE("sat", tout << "propagate " << l << " @ " << m_level << "\n";); TRACE("sat", tout << "propagate " << l << " @ " << m_level << "\n";);
propagate_binary(l); propagate_binary(l);
} }
//while (m_qhead < m_trail.size() && !inconsistent()) {
while (m_qhead < sz && !inconsistent()) { while (m_qhead < sz && !inconsistent()) {
propagate_clauses(m_trail[m_qhead++]); propagate_clauses(m_trail[m_qhead++]);
} }
@ -1629,7 +1626,6 @@ namespace sat {
pop_lookahead1(lit, num_units); pop_lookahead1(lit, num_units);
if (unsat) { if (unsat) {
TRACE("sat", tout << "backtracking and settting " << ~lit << "\n";); TRACE("sat", tout << "backtracking and settting " << ~lit << "\n";);
//reset_lookahead_reward();
assign(~lit); assign(~lit);
propagate(); propagate();
change = true; change = true;