mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

fix bug in consequence extraction: the order of bcp is not fixed between restarts, so the order of unit literals may not be preserved. This is relatively rare, so we optimize for the case where we assume bcp preserves order (and maybe miss some consequences)

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-01-17 13:41:15 -08:00
parent dc543a7ee7
commit 873d975c77
2 changed files with 27 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/sat/sat_solver.cpp
View file

@ -3227,20 +3227,32 @@ namespace sat {
SASSERT(!inconsistent());
unsigned sz = m_trail.size();
for (unsigned i = start; i < sz && lvl(m_trail[i]) <= 1; ++i) {
extract_fixed_consequences(m_trail[i], assumptions, unfixed, conseq);
if (!extract_fixed_consequences(m_trail[i], assumptions, unfixed, conseq)) {
for (i = 0; i < sz && lvl(m_trail[i]) <= 1; ++i) {
VERIFY(extract_fixed_consequences(m_trail[i], assumptions, unfixed, conseq));
}
break;
}
}
start = sz;
}
void solver::extract_assumptions(literal lit, index_set& s) {
bool solver::check_domain(literal lit, literal lit2) {
return m_antecedents.contains(lit2.var());
}
bool solver::extract_assumptions(literal lit, index_set& s) {
justification js = m_justification[lit.var()];
switch (js.get_kind()) {
case justification::NONE:
break;
case justification::BINARY:
if (!check_domain(lit, js.get_literal())) return false;
s |= m_antecedents.find(js.get_literal().var());
break;
case justification::TERNARY:
if (!check_domain(lit, js.get_literal1())) return false;
if (!check_domain(lit, js.get_literal2())) return false;
s |= m_antecedents.find(js.get_literal1().var());
s |= m_antecedents.find(js.get_literal2().var());
break;
@ -3248,6 +3260,7 @@ namespace sat {
clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset()));
for (unsigned i = 0; i < c.size(); ++i) {
if (c[i] != lit) {
if (!check_domain(lit, c[i])) return false;
s |= m_antecedents.find(c[i].var());
}
}
@ -3258,6 +3271,7 @@ namespace sat {
literal_vector::iterator it = m_ext_antecedents.begin();
literal_vector::iterator end = m_ext_antecedents.end();
for (; it != end; ++it) {
if (!check_domain(lit, *it)) return false;
s |= m_antecedents.find(it->var());
}
break;
@ -3267,6 +3281,7 @@ namespace sat {
break;
}
TRACE("sat", display_index_set(tout << lit << ": " , s) << "\n";);
return true;
}
std::ostream& solver::display_index_set(std::ostream& out, index_set const& s) const {
@ -3279,17 +3294,19 @@ namespace sat {
}
void solver::extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq) {
bool solver::extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq) {
index_set s;
if (m_antecedents.contains(lit.var())) {
return;
return true;
}
if (assumptions.contains(lit)) {
s.insert(lit.index());
}
else {
if (!extract_assumptions(lit, s)) {
return false;
}
add_assumption(lit);
extract_assumptions(lit, s);
}
m_antecedents.insert(lit.var(), s);
if (unfixed.contains(lit.var())) {
@ -3302,6 +3319,7 @@ namespace sat {
unfixed.remove(lit.var());
conseq.push_back(cons);
}
return true;
}
void solver::asymmetric_branching() {

6
src/sat/sat_solver.h
View file

@ -439,7 +439,9 @@ namespace sat {
u_map<index_set> m_antecedents;
vector<literal_vector> m_binary_clause_graph;
void extract_assumptions(literal lit, index_set& s);
bool extract_assumptions(literal lit, index_set& s);
bool check_domain(literal lit, literal lit2);
std::ostream& display_index_set(std::ostream& out, index_set const& s) const;
@ -451,7 +453,7 @@ namespace sat {
void extract_fixed_consequences(unsigned& start, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq);
void extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq);
bool extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq);
void update_unfixed_literals(literal_set& unfixed_lits, bool_var_set& unfixed_vars);