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

Commit

Browse source
This commit is contained in:
Miguel Neves 2017-10-12 16:14:56 -07:00
parent bdce957ac8
commit 56496ead2f
2 changed files with 11 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/sat/sat_lookahead.cpp
View file

@ -1672,6 +1672,17 @@ namespace sat {
change = true; change = true;
last_changed = lit; last_changed = lit;
} }
{
// if l was derived from lit and ~lit -> l, then l is a necessary assignment
scoped_level _sl(*this, dl_lvl);
literal_vector const& lits = m_binary[(~l).index()];
for (literal l : lits) {
if (inconsistent()) break;
if (is_true(l) && !is_fixed_at(l, cl_fixed_truth)) {
assign(l);
}
}
}
SASSERT(inconsistent() || !is_unsat()); SASSERT(inconsistent() || !is_unsat());
} }
if (c_fixed_truth - 2 * m_lookahead.size() < base) { if (c_fixed_truth - 2 * m_lookahead.size() < base) {

1
src/sat/sat_lookahead.h
View file

@ -501,7 +501,6 @@ namespace sat {
unsigned do_double(literal l, unsigned& base); unsigned do_double(literal l, unsigned& base);
unsigned double_look(literal l, unsigned& base); unsigned double_look(literal l, unsigned& base);
void set_conflict() { TRACE("sat", tout << "conflict\n";); m_inconsistent = true; } void set_conflict() { TRACE("sat", tout << "conflict\n";); m_inconsistent = true; }
//void set_conflict() { TRACE("sat", tout << "conflict\n";); printf("CONFLICT\n"); m_inconsistent = true; }
bool inconsistent() { return m_inconsistent; } bool inconsistent() { return m_inconsistent; }
unsigned scope_lvl() const { return m_trail_lim.size(); } unsigned scope_lvl() const { return m_trail_lim.size(); }