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

resolution is still wrong

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-01-29 09:32:14 -08:00
parent 0eb0306ae2
commit 60248d0981
4 changed files with 30 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/polysat/boolean.cpp
View file

@ -85,8 +85,8 @@ namespace polysat {
void bool_var_manager::asserted(sat::literal lit, unsigned lvl, dependency dep) {
LOG("Asserted " << lit << " @ " << lvl);
assign(kind_t::decision, lit, lvl, nullptr, dep);
SASSERT(is_decision(lit));
assign(dep == null_dependency ? kind_t::decision : kind_t::assumption, lit, lvl, nullptr, dep);
SASSERT(is_decision(lit) || is_assumption(lit));
}
void bool_var_manager::assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, dependency dep) {

3
src/math/polysat/boolean.h
View file

@ -24,6 +24,7 @@ namespace polysat {
unassigned,
bool_propagation,
value_propagation,
assumption,
decision,
};
@ -57,6 +58,8 @@ namespace polysat {
bool is_assigned(sat::literal lit) const { return value(lit) != l_undef; }
bool is_decision(sat::bool_var var) const { return is_assigned(var) && m_kind[var] == kind_t::decision; }
bool is_decision(sat::literal lit) const { return is_decision(lit.var()); }
bool is_assumption(sat::bool_var var) const { return is_assigned(var) && m_kind[var] == kind_t::assumption; }
bool is_assumption(sat::literal lit) const { return is_assumption(lit.var()); }
bool is_bool_propagation(sat::bool_var var) const { return is_assigned(var) && m_kind[var] == kind_t::bool_propagation; }
bool is_bool_propagation(sat::literal lit) const { return is_bool_propagation(lit.var()); }
bool is_value_propagation(sat::bool_var var) const { return is_assigned(var) && m_kind[var] == kind_t::value_propagation; }

26
src/math/polysat/conflict.cpp
View file

@ -50,7 +50,8 @@ namespace polysat {
if (!m_vars.empty())
out << " vars";
for (auto v : m_vars)
out << " v" << v;
if (is_pmarked(v))
out << " v" << v;
return out;
}
@ -328,7 +329,14 @@ namespace polysat {
auto const& j = s.m_justification[v];
s.inc_activity(v);
#if 0
if (j.is_decision() && m_vars.contains(v)) {
set_bailout();
return false;
}
#endif
m_vars.remove(v);
if (j.is_propagation()) {
@ -343,32 +351,38 @@ namespace polysat {
}
}
LOG("try-explain v" << v);
if (try_explain(v))
return true;
// No value resolution method was successful => fall back to saturation and variable elimination
while (s.inc()) {
LOG("try-eliminate v" << v);
// TODO: as a last resort, substitute v by m_value[v]?
if (try_eliminate(v))
return true;
if (!try_saturate(v))
break;
}
LOG("bailout v" << v);
set_bailout();
if (s.is_assigned(v) && j.is_decision())
m_vars.insert(v);
return false;
}
bool conflict::try_eliminate(pvar v) {
bool conflict::try_eliminate(pvar v) {
LOG("try v" << v << " contains " << m_vars.contains(v));
if (m_vars.contains(v))
return false;
bool has_v = false;
for (auto c : *this)
has_v |= c->is_var_dependent() && c->contains_var(v);
has_v |= c->contains_var(v);
if (!has_v)
return true;
for (auto* engine : ve_engines)
if (engine->perform(s, v, *this))
return true;
if (engine->perform(s, v, *this))
return true;
return false;
}

23
src/math/polysat/solver.cpp
View file

@ -554,14 +554,14 @@ namespace polysat {
sat::bool_var const var = lit.var();
if (!m_conflict.is_bmarked(var))
continue;
if (m_bvars.level(var) <= base_level())
continue;
LOG("Conflict: " << m_conflict);
if (m_bvars.is_decision(var)) {
if (m_bvars.is_assumption(var))
continue;
else if (m_bvars.is_decision(var)) {
revert_bool_decision(lit);
return;
}
if (m_bvars.is_bool_propagation(var))
else if (m_bvars.is_bool_propagation(var))
m_conflict.resolve(lit, *m_bvars.reason(lit));
else
m_conflict.resolve_with_assignment(lit, m_bvars.level(lit));
@ -600,19 +600,6 @@ namespace polysat {
}
m_activity_inc >>= 14;
}
#if 0
/** Conflict resolution case where boolean literal 'lit' is on top of the stack
* NOTE: boolean resolution should work normally even in bailout mode.
*/
void solver::resolve_bool(sat::literal lit) {
SASSERT(m_bvars.is_bool_propagation(lit));
clause const& other = *m_bvars.reason(lit);
LOG_H3("resolve_bool: " << lit << " " << show_deref(&other));
m_conflict.resolve(lit, *other);
}
#endif
void solver::report_unsat() {
backjump(base_level());
@ -782,7 +769,7 @@ namespace polysat {
}
unsigned solver::level(sat::literal lit0, clause const& cl) {
unsigned lvl = base_level();
unsigned lvl = 0;
for (auto lit : cl) {
if (lit == lit0)
continue;