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

updated conflict state

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-02-01 11:47:33 -08:00
parent 486cc632d0
commit c48f14e537
8 changed files with 1085 additions and 1067 deletions
Download patch file Download diff file Expand all files Collapse all files

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

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

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

@ -91,7 +91,7 @@ namespace polysat {
void decide(sat::literal lit, unsigned lvl, clause& lemma);
void decide(sat::literal lit, unsigned lvl);
void eval(sat::literal lit, unsigned lvl);
void asserted(sat::literal lit, unsigned lvl, dependency dep);
void assumption(sat::literal lit, unsigned lvl, dependency dep);
void unassign(sat::literal lit);
std::ostream& display(std::ostream& out) const;

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

@ -51,6 +51,10 @@ namespace polysat {
out << " vars";
for (auto v : m_vars)
out << " v" << v;
if (!m_bail_vars.empty())
out << " bail vars";
for (auto v : m_bail_vars)
out << " v" << v;
return out;
}
@ -60,6 +64,7 @@ namespace polysat {
m_constraints.reset();
m_literals.reset();
m_vars.reset();
m_bail_vars.reset();
m_conflict_var = null_var;
m_bailout = false;
SASSERT(empty());
@ -139,14 +144,26 @@ namespace polysat {
m_constraints.push_back(c);
}
void conflict::propagate(signed_constraint c) {
cm().ensure_bvar(c.get());
switch (c.bvalue(s)) {
case l_undef:
s.assign_eval(c.blit());
break;
case l_true:
break;
case l_false:
break;
}
insert(c);
}
void conflict::insert_vars(signed_constraint c) {
for (pvar v : c->vars())
if (s.is_assigned(v))
m_vars.insert(v);
}
/**
* Premises can either be justified by a Clause or by a value assignment.
* Premises that are justified by value assignments are not assigned (the bvalue is l_undef)
@ -232,10 +249,18 @@ namespace polysat {
SASSERT(contains_literal(lit));
SASSERT(!contains_literal(~lit));
remove_literal(lit);
signed_constraint c = s.lit2cnstr(lit);
unset_mark(c);
insert_vars(c);
bool has_decision = false;
for (pvar v : c->vars())
if (s.is_assigned(v) && s.m_justification[v].is_decision())
m_bail_vars.insert(v), has_decision = true;
if (!has_decision) {
remove(c);
for (pvar v : c->vars())
if (s.is_assigned(v))
m_vars.insert(v);
}
}
/**
@ -313,42 +338,24 @@ namespace polysat {
bool conflict::resolve_value(pvar v) {
// NOTE:
// In the "standard" case where "v = val" is on the stack:
// - core contains both false and true constraints
// (originally only false ones, but additional true ones may come from saturation)
// forbidden interval projection is performed at top level
SASSERT(v != conflict_var());
if (is_bailout()) {
if (!s.m_justification[v].is_decision())
m_vars.remove(v);
return false;
}
SASSERT(v != conflict_var());
auto const& j = s.m_justification[v];
s.inc_activity(v);
#if 0
if (j.is_decision() && m_vars.contains(v)) {
set_bailout();
if (j.is_decision() && m_bail_vars.contains(v))
return false;
}
#endif
s.inc_activity(v);
m_vars.remove(v);
if (j.is_propagation()) {
for (auto const& c : s.m_viable.get_constraints(v)) {
if (!c->has_bvar()) {
// it is a side-condition that was not propagated already.
// it is true in the current variable assignment.
cm().ensure_bvar(c.get());
s.assign_eval(c.blit());
}
insert(c);
}
}
if (is_bailout())
goto bailout;
if (j.is_propagation())
for (auto const& c : s.m_viable.get_constraints(v))
propagate(c);
LOG("try-explain v" << v);
if (try_explain(v))
@ -365,6 +372,7 @@ namespace polysat {
}
LOG("bailout v" << v);
set_bailout();
bailout:
if (s.is_assigned(v) && j.is_decision())
m_vars.insert(v);
return false;

8
src/math/polysat/conflict.h
View file

@ -88,15 +88,12 @@ namespace polysat {
signed_constraints m_constraints; // new constraints used as premises
indexed_uint_set m_literals; // set of boolean literals in the conflict
uint_set m_vars; // variable assignments used as premises
uint_set m_bail_vars;
// If this is not null_var, the conflict was due to empty viable set for this variable.
// Can be treated like "v = x" for any value x.
pvar m_conflict_var = null_var;
unsigned_vector m_pvar2count; // reference count of variables
void inc_pref(pvar v);
void dec_pref(pvar v);
bool_vector m_bvar2mark; // mark of Boolean variables
void set_bmark(sat::bool_var b);
void unset_bmark(sat::bool_var b);
@ -135,7 +132,7 @@ namespace polysat {
void reset();
bool contains_pvar(pvar v) const { return m_vars.contains(v); }
bool contains_pvar(pvar v) const { return m_vars.contains(v) || m_bail_vars.contains(v); }
bool is_bmarked(sat::bool_var b) const;
/** conflict because the constraint c is false under current variable assignment */
@ -145,6 +142,7 @@ namespace polysat {
/** all literals in clause are false */
void set(clause const& cl);
void propagate(signed_constraint c);
void insert(signed_constraint c);
void insert_vars(signed_constraint c);
void insert(signed_constraint c, vector<signed_constraint> const& premises);

16
src/math/polysat/saturation.cpp
View file

@ -423,6 +423,22 @@ namespace polysat {
return false;
if (c.lhs.is_val() || c.rhs.is_val())
return false;
pdd q_l(c.lhs), e_l(c.lhs), q_r(c.rhs), e_r(c.rhs);
bool is_linear = true;
is_linear &= c.lhs.degree(v) <= 1;
is_linear &= c.rhs.degree(v) <= 1;
if (c.lhs.degree(v) == 1) {
c.lhs.factor(v, 1, q_l, e_l);
is_linear &= q_l.is_val();
}
if (c.rhs.degree(v) == 1) {
c.rhs.factor(v, 1, q_r, e_r);
is_linear &= q_r.is_val();
}
if (is_linear)
return false;
if (!c.as_signed_constraint().is_currently_false(s))
return false;
rational l_val, r_val;

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

@ -190,14 +190,14 @@ namespace polysat {
switch (m_bvars.value(lit)) {
case l_false:
set_conflict(c);
SASSERT(dep == null_dependency && "track dependencies is TODO");
break;
case l_true:
// constraint c is already asserted
SASSERT(m_bvars.level(lit) <= m_level);
// TODO: track additional dep?
break;
case l_undef:
m_bvars.asserted(lit, m_level, dep);
m_bvars.assumption(lit, m_level, dep);
m_trail.push_back(trail_instr_t::assign_bool_i);
m_search.push_boolean(lit);
if (c.is_currently_false(*this))

10
src/math/polysat/viable.cpp
View file

@ -555,19 +555,15 @@ namespace polysat {
auto lhs = hi - next_lo;
auto rhs = next_hi - next_lo;
signed_constraint c = s.m_constraints.ult(lhs, rhs);
core.insert(c);
}
for (auto sc : e->side_cond) {
core.insert(sc);
core.insert_vars(sc);
core.propagate(c);
}
for (auto sc : e->side_cond)
core.propagate(sc);
core.insert(e->src);
e = n;
}
while (e != first);
// core.set_bailout();
// TODO - review this; c is true under current assignment?
for (auto c : core) {
if (c.bvalue(s) == l_false) {
core.reset();

2034
src/test/polysat.cpp
View file

File diff suppressed because it is too large Load diff