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

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-02-02 08:24:58 -08:00
commit 4c4f916917
11 changed files with 1151 additions and 1095 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;

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

@ -50,8 +50,11 @@ namespace polysat {
if (!m_vars.empty())
out << " vars";
for (auto v : m_vars)
if (is_pmarked(v))
out << " v" << v;
out << " v" << v;
if (!m_bail_vars.empty())
out << " bail vars";
for (auto v : m_bail_vars)
out << " v" << v;
return out;
}
@ -61,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());
@ -83,7 +87,7 @@ namespace polysat {
else {
SASSERT(c.is_currently_false(s));
// TBD: fails with test_subst SASSERT(c.bvalue(s) == l_true);
c->set_var_dependent();
insert_vars(c);
insert(c);
}
SASSERT(!empty());
@ -140,6 +144,25 @@ 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.
@ -210,7 +233,7 @@ namespace polysat {
SASSERT(std::count(cl.begin(), cl.end(), ~lit) == 0);
remove_literal(lit);
unset_bmark(s.lit2cnstr(lit));
unset_mark(s.lit2cnstr(lit));
for (sat::literal lit2 : cl)
if (lit2 != lit)
insert(s.lit2cnstr(~lit2));
@ -226,14 +249,17 @@ namespace polysat {
SASSERT(contains_literal(lit));
SASSERT(!contains_literal(~lit));
remove_literal(lit);
signed_constraint c = s.lit2cnstr(lit);
unset_mark(c);
for (pvar v : c->vars()) {
if (s.is_assigned(v) && s.get_level(v) <= lvl) {
m_vars.insert(v);
inc_pref(v);
}
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);
}
}
@ -268,8 +294,6 @@ namespace polysat {
lemma.push(~c);
for (unsigned v : m_vars) {
if (!is_pmarked(v))
continue;
auto eq = s.eq(s.var(v), s.get_value(v));
cm().ensure_bvar(eq.get());
if (eq.bvalue(s) == l_undef)
@ -314,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))
@ -366,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;
@ -406,19 +413,12 @@ namespace polysat {
c->set_mark();
if (c->has_bvar())
set_bmark(c->bvar());
if (c->is_var_dependent()) {
for (auto v : c->vars()) {
if (s.is_assigned(v))
m_vars.insert(v);
inc_pref(v);
}
}
}
/**
* unset marking on the constraint, but keep variable dependencies.
*/
void conflict::unset_bmark(signed_constraint c) {
void conflict::unset_mark(signed_constraint c) {
if (!c->is_marked())
return;
c->unset_mark();
@ -426,32 +426,6 @@ namespace polysat {
unset_bmark(c->bvar());
}
void conflict::unset_mark(signed_constraint c) {
if (!c->is_marked())
return;
unset_bmark(c);
if (!c->is_var_dependent())
return;
c->unset_var_dependent();
for (auto v : c->vars())
dec_pref(v);
}
void conflict::inc_pref(pvar v) {
if (v >= m_pvar2count.size())
m_pvar2count.resize(v + 1);
m_pvar2count[v]++;
}
void conflict::dec_pref(pvar v) {
SASSERT(m_pvar2count[v] > 0);
m_pvar2count[v]--;
}
bool conflict::is_pmarked(pvar v) const {
return m_pvar2count.get(v, 0) > 0;
}
void conflict::set_bmark(sat::bool_var b) {
if (b >= m_bvar2mark.size())
m_bvar2mark.resize(b + 1);

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

@ -10,6 +10,64 @@ Author:
Nikolaj Bjorner (nbjorner) 2021-03-19
Jakob Rath 2021-04-6
Notes:
A conflict state is of the form <Vars, Constraints>
Where Vars are shorthand for the constraints v = value(v) for v in Vars and value(v) is the assignent.
The conflict state is unsatisfiable under background clauses F.
Dually, the negation is a consequence of F.
Conflict resolution resolves an assignment in the search stack against the conflict state.
Assignments are of the form:
lit <- D => lit - lit is propagated by the clause D => lit
lit <- ? - lit is a decision literal.
lit <- asserted - lit is asserted
lit <- Vars - lit is propagated from variable evaluation.
v = value <- D - v is assigned value by constraints D
v = value <- ? - v is a decision literal.
- All literals should be assigned in the stack prior to their use.
l <- D => l, < Vars, { l } u C > ===> < Vars, C u D >
l <- ?, < Vars, { l } u C > ===> ~l <- (C & Vars = value(Vars) => ~l)
l <- asserted, < Vars, { l } u C > ===> < Vars, { l } u C >
l <- Vars', < Vars, { l } u C > ===> < Vars u Vars', C > if all Vars' are propagated
l <- Vars', < Vars, { l } u C > ===> Mark < Vars, { l } u C > as bailout
v = value <- D, < Vars u { v }, C > ===> < Vars, D u C >
v = value <- ?, < Vars u { v }, C > ===> v != value <- (C & Vars = value(Vars) => v != value)
Example derivations:
Trail: z <= y <- asserted
xz > xy <- asserted
x = a <- ?
y = b <- ?
z = c <- ?
Conflict: < {x, y, z}, xz > xy > when ~O(a,b) and c <= b
Append x <= a <- { x }
Append y <= b <- { y }
Conflict: < {}, y >= z, xz > xy, x <= a, y <= b >
Based on: z <= y & x <= a & y <= b => xz <= xy
Resolve: y <= b <- { y }, y is a decision variable.
Bailout: lemma ~(y >= z & xz > xy & x <= a & y <= b) at decision level of lemma
With overflow predicate:
Append ~O(x, y) <- { x, y }
Conflict: < {}, y >= z, xz > xy, ~O(x,y) >
Based on z <= y & ~O(x,y) => xz <= xy
Resolve: ~O(x, y) <- { x, y } both x, y are decision variables
Lemma: y < z or xz <= xy or O(x,y)
--*/
#pragma once
#include "math/polysat/constraint.h"
@ -30,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);
@ -77,7 +132,7 @@ namespace polysat {
void reset();
bool is_pmarked(pvar v) const;
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 */
@ -87,7 +142,9 @@ 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);
void remove(signed_constraint c);
void replace(signed_constraint c_old, signed_constraint c_new, vector<signed_constraint> const& c_new_premises);

4
src/math/polysat/constraint.h
View file

@ -146,7 +146,6 @@ namespace polysat {
unsigned_vector m_vars;
lbool m_external_sign = l_undef;
bool m_is_marked = false;
bool m_is_var_dependent = false;
bool m_is_active = false;
/** The boolean variable associated to this constraint, if any.
* If this is not null_bool_var, then the constraint corresponds to a literal on the assignment stack.
@ -207,9 +206,6 @@ namespace polysat {
void unset_mark() { m_is_marked = false; }
bool is_marked() const { return m_is_marked; }
void set_var_dependent() { m_is_var_dependent = true; }
void unset_var_dependent() { m_is_var_dependent = false; }
bool is_var_dependent() const { return m_is_var_dependent; }
bool is_active() const { return m_is_active; }
void set_active(bool f) { m_is_active = f; }

3
src/math/polysat/explain.cpp
View file

@ -165,10 +165,9 @@ namespace polysat {
auto c2 = s.ule(a, b);
if (!c.is_positive())
c2 = ~c2;
LOG("try-reduce is false " << c2.is_currently_false(s));
if (!c2.is_currently_false(s))
continue;
if (c2.bvalue(s) == l_false)
if (c2.is_always_false() || c2.bvalue(s) == l_false)
return false;
if (!c2->has_bvar() || l_undef == c2.bvalue(s)) {
vector<signed_constraint> premises;

8
src/math/polysat/forbidden_intervals.cpp
View file

@ -73,11 +73,9 @@ namespace polysat {
// a*v <= 0, a odd
if (match_zero(c, a1, b1, e1, a2, b2, e2, fi))
return true;
// a*v + b > 0, a odd
if (match_non_zero_linear(c, a1, b1, e1, a2, b2, e2, fi))
return true;
if (match_linear1(c, a1, b1, e1, a2, b2, e2, fi))
return true;
if (match_linear2(c, a1, b1, e1, a2, b2, e2, fi))
@ -349,7 +347,7 @@ namespace polysat {
signed_constraint const& c,
rational const & a1, pdd const& b1, pdd const& e1,
fi_record& fi) {
if (a1.is_odd() && b1.is_zero() && !c.is_positive()) {
if (a1.is_odd() && b1.is_zero() && c.is_negative()) {
auto& m = e1.manager();
rational lo_val(0);
auto lo = m.zero();
@ -361,7 +359,7 @@ namespace polysat {
fi.side_cond.push_back(s.eq(b1, e1));
return true;
}
if (a1.is_odd() && b1.is_val() && !c.is_positive()) {
if (a1.is_odd() && b1.is_val() && c.is_negative()) {
auto& m = e1.manager();
rational const& mod_value = m.two_to_N();
rational a1_inv;
@ -389,7 +387,7 @@ namespace polysat {
signed_constraint const& c,
rational const & a2, pdd const& b2, pdd const& e2,
fi_record& fi) {
if (a2.is_one() && b2.is_val() && !c.is_positive()) {
if (a2.is_one() && b2.is_val() && c.is_negative()) {
auto& m = e2.manager();
rational const& mod_value = m.two_to_N();
rational lo_val(mod(-b2.val() - 1, mod_value));

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

@ -88,7 +88,7 @@ namespace polysat {
for (auto d : m_new_constraints)
core.insert(d);
if (c.bvalue(s) != l_false)
c->set_var_dependent();
core.insert_vars(c);
core.insert(~c);
LOG("Core " << core);
return true;
@ -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;

6
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))
@ -535,7 +535,7 @@ namespace polysat {
// Resolve over variable assignment
pvar v = item.var();
LOG(m_justification[v]);
if (!m_conflict.is_pmarked(v) && !m_conflict.is_bailout()) {
if (!m_conflict.contains_pvar(v) && !m_conflict.is_bailout()) {
m_search.pop_assignment();
continue;
}

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

@ -46,9 +46,11 @@ namespace polysat {
void viable::pop_viable() {
auto& [v, k, e] = m_trail.back();
SASSERT(well_formed(m_units[v]));
switch (k) {
case entry_kind::unit_e:
e->remove_from(m_units[v], e);
SASSERT(well_formed(m_units[v]));
break;
case entry_kind::equal_e:
e->remove_from(m_equal_lin[v], e);
@ -67,13 +69,15 @@ namespace polysat {
SASSERT(e->prev() != e || e->next() == e);
SASSERT(k == entry_kind::unit_e);
(void)k;
SASSERT(well_formed(m_units[v]));
if (e->prev() != e) {
e->prev()->insert_after(e);
if (e->interval.lo_val() < e->next()->interval.lo_val())
if (e->interval.lo_val() < m_units[v]->interval.lo_val())
m_units[v] = e;
}
else
m_units[v] = e;
m_units[v] = e;
SASSERT(well_formed(m_units[v]));
m_trail.pop_back();
}
@ -102,6 +106,7 @@ namespace polysat {
}
void viable::insert(entry* e, pvar v, ptr_vector<entry>& entries, entry_kind k) {
SASSERT(well_formed(m_units[v]));
m_trail.push_back({ v, k, e });
s.m_trail.push_back(trail_instr_t::viable_add_i);
e->init(e);
@ -109,6 +114,7 @@ namespace polysat {
entries[v] = e;
else
e->insert_after(entries[v]);
SASSERT(well_formed(m_units[v]));
}
bool viable::intersect(pvar v, entry* ne) {
@ -122,6 +128,7 @@ namespace polysat {
m_alloc.push_back(ne);
return false;
}
auto create_entry = [&]() {
m_trail.push_back({ v, entry_kind::unit_e, ne });
@ -136,6 +143,13 @@ namespace polysat {
e->remove_from(m_units[v], e);
};
if (ne->interval.is_full()) {
while (m_units[v])
remove_entry(m_units[v]);
m_units[v] = create_entry();
return true;
}
if (!e)
m_units[v] = create_entry();
else {
@ -257,16 +271,21 @@ namespace polysat {
lo = val - lambda_l;
increase_hi(hi);
}
LOG("forbidden interval " << e->coeff << " * " << e->interval << " [" << lo << ", " << hi << "[");
LOG("forbidden interval v" << v << " " << val << " " << e->coeff << " * " << e->interval << " [" << lo << ", " << hi << "[");
SASSERT(hi <= mod_value);
if (hi == mod_value) hi = 0;
bool full = (lo == 0 && hi == mod_value);
if (hi == mod_value)
hi = 0;
pdd lop = s.var2pdd(v).mk_val(lo);
pdd hip = s.var2pdd(v).mk_val(hi);
entry* ne = alloc_entry();
ne->src = e->src;
ne->side_cond = e->side_cond;
ne->coeff = 1;
ne->interval = eval_interval::proper(lop, lo, hip, hi);
if (full)
ne->interval = eval_interval::full();
else
ne->interval = eval_interval::proper(lop, lo, hip, hi);
intersect(v, ne);
return false;
}
@ -371,6 +390,8 @@ namespace polysat {
entry* first = e;
entry* last = e->prev();
if (e->interval.is_full())
return false;
// quick check: last interval doesn't wrap around, so hi_val
// has not been covered
if (last->interval.lo_val() < last->interval.hi_val())
@ -413,6 +434,7 @@ namespace polysat {
return refine_viable(v, val);
}
rational viable::min_viable(pvar v) {
refined:
rational lo(0);
@ -542,18 +564,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);
core.propagate(c);
}
for (auto sc : e->side_cond)
core.insert(sc);
e->src->set_var_dependent();
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();
@ -606,7 +625,7 @@ namespace polysat {
std::ostream& viable::display(std::ostream& out) const {
for (pvar v = 0; v < m_units.size(); ++v)
display(out << "v" << v << ": ", v);
display(out << "v" << v << ": ", v) << "\n";
return out;
}

1967
src/test/polysat.cpp
View file

File diff suppressed because it is too large Load diff