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

Integrate univariate solver in polysat

Browse source
This commit is contained in:
Jakob Rath 2022-03-18 15:43:06 +01:00
parent 9d47d7959d
commit 509a007ed7
9 changed files with 192 additions and 50 deletions
Download patch file Download diff file Expand all files Collapse all files

29
src/math/polysat/constraint.cpp
View file

@ -324,35 +324,6 @@ namespace polysat {
return out.str();
}
bool constraint::propagate(solver& s, bool is_positive, pvar v) {
LOG_H3("Propagate " << s.m_vars[v] << " in " << signed_constraint(this, is_positive));
SASSERT(!vars().empty());
unsigned idx = 0;
if (var(idx) != v)
idx = 1;
SASSERT(v == var(idx));
// find other watch variable.
for (unsigned i = vars().size(); i-- > 2; ) {
unsigned other_v = vars()[i];
if (!s.is_assigned(other_v)) {
s.add_watch({this, is_positive}, other_v);
std::swap(vars()[idx], vars()[i]);
return true;
}
}
// at most one variable remains unassigned.
unsigned other_v = var(idx);
propagate_core(s, is_positive, v, other_v);
return false;
}
void constraint::propagate_core(solver& s, bool is_positive, pvar v, pvar other_v) {
(void)v;
(void)other_v;
narrow(s, is_positive, false);
}
unsigned constraint::level(solver& s) const {
if (s.m_bvars.value(sat::literal(bvar())) != l_undef)
return s.m_bvars.level(bvar());

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

@ -178,8 +178,6 @@ namespace polysat {
virtual std::ostream& display(std::ostream& out, lbool status) const = 0;
virtual std::ostream& display(std::ostream& out) const = 0;
bool propagate(solver& s, bool is_positive, pvar v);
virtual void propagate_core(solver& s, bool is_positive, pvar v, pvar other_v);
virtual bool is_always_false(bool is_positive) const = 0;
virtual bool is_currently_false(solver& s, bool is_positive) const = 0;
virtual bool is_currently_true(solver& s, bool is_positive) const = 0;
@ -248,8 +246,6 @@ namespace polysat {
bool is_positive() const { return m_positive; }
bool is_negative() const { return !is_positive(); }
bool propagate(solver& s, pvar v) { return get()->propagate(s, is_positive(), v); }
void propagate_core(solver& s, pvar v, pvar other_v) { get()->propagate_core(s, is_positive(), v, other_v); }
bool is_always_false() const { return get()->is_always_false(is_positive()); }
bool is_always_true() const { return get()->is_always_false(is_negative()); }
bool is_currently_false(solver& s) const { return get()->is_currently_false(s, is_positive()); }

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

@ -31,6 +31,7 @@ namespace polysat {
solver::solver(reslimit& lim):
m_lim(lim),
m_viable(*this),
m_viable_fallback(*this),
m_linear_solver(*this),
m_conflict(*this),
m_simplify(*this),
@ -105,7 +106,8 @@ namespace polysat {
pvar v = m_value.size();
m_value.push_back(rational::zero());
m_justification.push_back(justification::unassigned());
m_viable.push(sz);
m_viable.push_var(sz);
m_viable_fallback.push_var(sz);
m_pwatch.push_back({});
m_activity.push_back(0);
m_vars.push_back(sz2pdd(sz).mk_var(v));
@ -122,7 +124,8 @@ namespace polysat {
void solver::del_var() {
// TODO also remove v from all learned constraints.
pvar v = m_value.size() - 1;
m_viable.pop();
m_viable.pop_var();
m_viable_fallback.pop_var();
m_value.pop_back();
m_justification.pop_back();
m_pwatch.pop_back();
@ -267,7 +270,7 @@ namespace polysat {
auto& wlist = m_pwatch[v];
unsigned i = 0, j = 0, sz = wlist.size();
for (; i < sz && !is_conflict(); ++i)
if (!wlist[i].propagate(*this, v))
if (propagate(v, wlist[i]))
wlist[j++] = wlist[i];
for (; i < sz; ++i)
wlist[j++] = wlist[i];
@ -275,6 +278,32 @@ namespace polysat {
DEBUG_CODE(m_locked_wlist = std::nullopt;);
}
bool solver::propagate(pvar v, signed_constraint c) {
LOG_H3("Propagate " << m_vars[v] << " in " << c);
SASSERT(!c->vars().empty());
unsigned idx = 0;
if (c->var(idx) != v)
idx = 1;
SASSERT(v == c->var(idx));
// find other watch variable.
for (unsigned i = c->vars().size(); i-- > 2; ) {
unsigned other_v = c->vars()[i];
if (!is_assigned(other_v)) {
add_watch(c, other_v);
std::swap(c->vars()[idx], c->vars()[i]);
SASSERT(!is_assigned(c->var(0)));
SASSERT(!is_assigned(c->var(1)));
return true;
}
}
// at most one variable remains unassigned.
unsigned other_v = c->var(idx);
if (!is_assigned(other_v))
m_viable_fallback.push_constraint(other_v, c);
c.narrow(*this, false);
return false;
}
bool solver::propagate(sat::literal lit, clause& cl) {
SASSERT(cl.size() >= 2);
unsigned idx = cl[0] == ~lit ? 1 : 0;
@ -361,6 +390,10 @@ namespace polysat {
m_viable.push_viable();
break;
}
case trail_instr_t::viable_constraint_i: {
m_viable_fallback.pop_constraint();
break;
}
case trail_instr_t::assign_i: {
auto v = m_search.back().var();
LOG_V("Undo assign_i: v" << v);
@ -451,6 +484,7 @@ namespace polysat {
LOG("Decide v" << v);
IF_LOGGING(m_viable.log(v));
rational val;
justification j;
switch (m_viable.find_viable(v, val)) {
case dd::find_t::empty:
// NOTE: all such cases should be discovered elsewhere (e.g., during propagation/narrowing)
@ -458,16 +492,40 @@ namespace polysat {
DEBUG_CODE( UNREACHABLE(); );
m_free_pvars.unassign_var_eh(v);
set_conflict(v);
break;
return;
case dd::find_t::singleton:
// NOTE: this case may happen legitimately if all other possibilities were excluded by brute force search
assign_core(v, val, justification::propagation(m_level));
j = justification::propagation(m_level);
break;
case dd::find_t::multiple:
push_level();
assign_core(v, val, justification::decision(m_level));
j = justification::decision(m_level + 1);
break;
}
}
// Verify the value we're trying to assign
// TODO: we should add a better way to test constraints under assignments, without modifying the solver state.
m_value[v] = val;
m_search.push_assignment(v, val);
bool is_valid = m_viable_fallback.check_constraints(v);
m_search.pop();
if (!is_valid) {
// Try to find a valid replacement value
switch (m_viable_fallback.find_viable(v, val)) {
case dd::find_t::singleton:
case dd::find_t::multiple:
// NOTE: I don't think this can happen if viable::find_viable returned a singleton. since all values excluded by viable are true negatives.
SASSERT(!j.is_propagation());
j = justification::decision(m_level + 1);
break;
case dd::find_t::empty:
m_free_pvars.unassign_var_eh(v);
// TODO: get unsat core from univariate solver
set_conflict(v);
return;
}
}
if (j.is_decision())
push_level();
assign_core(v, val, j);
}
void solver::bdecide(sat::bool_var b) {
@ -484,11 +542,14 @@ namespace polysat {
++m_stats.m_num_propagations;
LOG(assignment_pp(*this, v, val) << " by " << j);
SASSERT(m_viable.is_viable(v, val));
SASSERT(j.level() == m_level);
SASSERT(!is_assigned(v));
SASSERT(std::all_of(assignment().begin(), assignment().end(), [v](auto p) { return p.first != v; }));
m_value[v] = val;
m_search.push_assignment(v, val);
m_trail.push_back(trail_instr_t::assign_i);
m_justification[v] = j;
SASSERT(m_viable_fallback.check_constraints(v));
#if ENABLE_LINEAR_SOLVER
// TODO: convert justification into a format that can be tracked in a depdendency core.
m_linear_solver.set_value(v, val, UINT_MAX);
@ -818,6 +879,8 @@ namespace polysat {
SASSERT(!c->is_active());
c->set_active(true);
add_watch(c);
if (c->vars().size() == 1)
m_viable_fallback.push_constraint(c->var(0), c);
c.narrow(*this, true);
#if ENABLE_LINEAR_SOLVER
m_linear_solver.activate_constraint(c);

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

@ -69,6 +69,7 @@ namespace polysat {
friend class forbidden_intervals;
friend class linear_solver;
friend class viable;
friend class viable_fallback;
friend class search_state;
friend class assignment_pp;
friend class assignments_pp;
@ -84,6 +85,7 @@ namespace polysat {
mutable scoped_ptr_vector<dd::pdd_manager> m_pdd;
viable m_viable; // viable sets per variable
viable_fallback m_viable_fallback; // fallback for viable, using bitblasting over univariate constraints
linear_solver m_linear_solver;
conflict m_conflict;
simplify m_simplify;
@ -172,6 +174,7 @@ namespace polysat {
void propagate(sat::literal lit);
void propagate(pvar v);
bool propagate(pvar v, signed_constraint c);
void propagate(pvar v, rational const& val, signed_constraint c);
bool propagate(sat::literal lit, clause& cl);
void erase_watch(pvar v, signed_constraint c);

1
src/math/polysat/trail.h
View file

@ -22,6 +22,7 @@ namespace polysat {
inc_level_i,
viable_add_i,
viable_rem_i,
viable_constraint_i,
assign_i,
assign_bool_i
};

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

@ -33,8 +33,20 @@ namespace polysat {
}
viable::~viable() {
for (entry* e : m_alloc)
dealloc(e);
for (entry* e : m_alloc)
dealloc(e);
}
void viable::push_var(unsigned sz) {
m_units.push_back(nullptr);
m_equal_lin.push_back(nullptr);
m_diseq_lin.push_back(nullptr);
}
void viable::pop_var() {
m_units.pop_back();
m_equal_lin.pop_back();
m_diseq_lin.pop_back();
}
viable::entry* viable::alloc_entry() {
@ -58,9 +70,12 @@ namespace polysat {
case entry_kind::equal_e:
e->remove_from(m_equal_lin[v], e);
break;
default:
case entry_kind::diseq_e:
e->remove_from(m_diseq_lin[v], e);
break;
default:
UNREACHABLE();
break;
}
m_alloc.push_back(e);
m_trail.pop_back();
@ -711,6 +726,70 @@ namespace polysat {
return true;
}
//************************************************************************
// viable_fallback
//************************************************************************
viable_fallback::viable_fallback(solver& s):
s(s) {
m_usolver_factory = mk_univariate_bitblast_factory();
}
void viable_fallback::push_var(unsigned sz) {
auto& mk_solver = *m_usolver_factory;
m_usolver.push_back(mk_solver(sz));
}
void viable_fallback::pop_var() {
m_usolver.pop_back();
}
void viable_fallback::push_constraint(pvar v, signed_constraint const& c) {
// v is the only unassigned variable in c.
SASSERT(!s.is_assigned(v));
DEBUG_CODE(for (pvar w : c->vars()) { if (v != w) SASSERT(s.is_assigned(w)); });
auto& us = *m_usolver[v];
// TODO: would be enough to push the solver only for new decision levels
us.push();
unsigned dep = m_constraints[v].size();
c.add_to_univariate_solver(s, us, dep);
m_constraints[v].push_back(c);
m_constraints_trail.push_back(v);
s.m_trail.push_back(trail_instr_t::viable_constraint_i);
}
void viable_fallback::pop_constraint() {
pvar v = m_constraints_trail.back();
m_constraints_trail.pop_back();
m_constraints[v].pop_back();
m_usolver[v]->pop(1);
}
bool viable_fallback::check_constraints(pvar v) {
for (auto const& c : m_constraints[v]) {
// for this check, all variables need to be assigned
DEBUG_CODE(for (pvar w : c->vars()) { SASSERT(s.is_assigned(w)); });
if (c.is_currently_false(s))
return false;
SASSERT(c.is_currently_true(s));
}
return true;
}
dd::find_t viable_fallback::find_viable(pvar v, rational& out_val) {
auto& us = *m_usolver[v];
switch (us.check()) {
case l_true:
out_val = us.model();
// we don't know whether the SMT instance has a unique solution
return dd::find_t::multiple;
case l_false:
return dd::find_t::empty;
default:
// TODO: what should we do here? (SMT solver had resource-out ==> polysat should abort too?)
UNREACHABLE();
return dd::find_t::empty;
}
}
}

36
src/math/polysat/viable.h
View file

@ -69,12 +69,11 @@ namespace polysat {
~viable();
// declare and remove var
void push(unsigned) { m_units.push_back(nullptr); m_equal_lin.push_back(nullptr); m_diseq_lin.push_back(nullptr); }
void pop() { m_units.pop_back(); m_equal_lin.pop_back(); m_diseq_lin.pop_back(); }
void push_var(unsigned sz);
void pop_var();
// undo adding/removing of entries
void pop_viable();
void push_viable();
/**
@ -186,6 +185,35 @@ namespace polysat {
inline std::ostream& operator<<(std::ostream& out, viable::var_pp const& v) {
return v.v.display(out, v.var);
}
class viable_fallback {
solver& s;
scoped_ptr<univariate_solver_factory> m_usolver_factory;
scoped_ptr_vector<univariate_solver> m_usolver;
vector<signed_constraints> m_constraints;
svector<unsigned> m_constraints_trail;
public:
viable_fallback(solver& s);
// declare and remove var
void push_var(unsigned sz);
void pop_var();
// add/remove constraints stored in the fallback solver
void push_constraint(pvar v, signed_constraint const& c);
void pop_constraint();
// Check whether all constraints for 'v' are satisfied.
bool check_constraints(pvar v);
// bool check_value(pvar v, rational const& val);
dd::find_t find_viable(pvar v, rational& out_val);
// TODO: get unsat core
};
}

4
src/test/viable.cpp
View file

@ -33,7 +33,7 @@ namespace polysat {
scoped_solverv s;
auto xv = s.add_var(3);
auto x = s.var(xv);
s.v.push(3);
s.v.push_var(3);
rational val;
auto c = s.ule(x + 3, x + 5);
s.v.intersect(xv, c);
@ -88,7 +88,7 @@ namespace polysat {
scoped_solverv s;
auto xv = s.add_var(3);
auto x = s.var(xv);
s.v.push(3);
s.v.push_var(3);
for (auto const& [lo, len] : intervals)
add_interval(s, xv, x, lo, len);
std::cout << intervals << "\n";

1
src/util/scoped_ptr_vector.h
View file

@ -44,6 +44,7 @@ public:
void reset() { std::for_each(m_vector.begin(), m_vector.end(), delete_proc<T>()); m_vector.reset(); }
void push_back(T * ptr) { m_vector.push_back(ptr); }
void push_back(scoped_ptr<T>&& ptr) { push_back(ptr.detach()); }
void pop_back() { SASSERT(!empty()); set(size()-1, nullptr); m_vector.pop_back(); }
T * back() const { return m_vector.back(); }
T * operator[](unsigned idx) const { return m_vector[idx]; }