mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 16:38:45 +00:00
Code Activity

expose missed propagations

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-18 08:57:32 -07:00
parent e0e7836c12
commit edea879864
3 changed files with 6 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/ba_solver.cpp
View file

@ -1556,7 +1556,7 @@ namespace sat {
m_learned.push_back(c); m_learned.push_back(c);
} }
else { else {
SASSERT(s().at_base_lvl()); SASSERT(!m_solver || s().at_base_lvl());
m_constraints.push_back(c); m_constraints.push_back(c);
} }
literal lit = c->lit(); literal lit = c->lit();

4
src/sat/ba_solver.h
View file

@ -362,8 +362,8 @@ namespace sat {
// access solver // access solver
inline lbool value(bool_var v) const { return value(literal(v, false)); } inline lbool value(bool_var v) const { return value(literal(v, false)); }
inline lbool value(literal lit) const { return m_lookahead ? m_lookahead->value(lit) : m_solver->value(lit); } inline lbool value(literal lit) const { return m_lookahead ? m_lookahead->value(lit) : m_solver->value(lit); }
inline unsigned lvl(literal lit) const { return m_solver->lvl(lit); } inline unsigned lvl(literal lit) const { return m_lookahead ? 0 : m_solver->lvl(lit); }
inline unsigned lvl(bool_var v) const { return m_solver->lvl(v); } inline unsigned lvl(bool_var v) const { return m_lookahead ? 0 : m_solver->lvl(v); }
inline bool inconsistent() const { return m_lookahead ? m_lookahead->inconsistent() : m_solver->inconsistent(); } inline bool inconsistent() const { return m_lookahead ? m_lookahead->inconsistent() : m_solver->inconsistent(); }
inline watch_list& get_wlist(literal l) { return m_lookahead ? m_lookahead->get_wlist(l) : m_solver->get_wlist(l); } inline watch_list& get_wlist(literal l) { return m_lookahead ? m_lookahead->get_wlist(l) : m_solver->get_wlist(l); }
inline watch_list const& get_wlist(literal l) const { return m_lookahead ? m_lookahead->get_wlist(l) : m_solver->get_wlist(l); } inline watch_list const& get_wlist(literal l) const { return m_lookahead ? m_lookahead->get_wlist(l) : m_solver->get_wlist(l); }

4
src/sat/sat_lookahead.cpp
View file

@ -408,6 +408,7 @@ namespace sat {
} }
bool lookahead::missed_propagation() const { bool lookahead::missed_propagation() const {
if (inconsistent()) return false;
for (literal l1 : m_trail) { for (literal l1 : m_trail) {
SASSERT(is_true(l1)); SASSERT(is_true(l1));
for (literal l2 : m_binary[l1.index()]) { for (literal l2 : m_binary[l1.index()]) {
@ -1614,7 +1615,7 @@ namespace sat {
} }
SASSERT(m_qhead == m_trail.size() || (inconsistent() && m_qhead < m_trail.size())); SASSERT(m_qhead == m_trail.size() || (inconsistent() && m_qhead < m_trail.size()));
//SASSERT(!missed_conflict()); //SASSERT(!missed_conflict());
//SASSERT(inconsistent() || !missed_propagation()); VERIFY(!missed_propagation());
TRACE("sat_verbose", display(tout << scope_lvl() << " " << (inconsistent()?"unsat":"sat") << "\n");); TRACE("sat_verbose", display(tout << scope_lvl() << " " << (inconsistent()?"unsat":"sat") << "\n"););
} }
@ -1656,6 +1657,7 @@ namespace sat {
unsat = inconsistent(); unsat = inconsistent();
pop_lookahead1(lit, num_units); pop_lookahead1(lit, num_units);
} }
// VERIFY(!missed_propagation());
if (unsat) { if (unsat) {
TRACE("sat", tout << "backtracking and settting " << ~lit << "\n";); TRACE("sat", tout << "backtracking and settting " << ~lit << "\n";);
lookahead_backtrack(); lookahead_backtrack();