mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

add variable minimization

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-09-22 14:27:05 -07:00
parent c82bbaad7d
commit e6c413b249
6 changed files with 85 additions and 51 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -22,6 +22,7 @@ Notes:
It should apply saturation rules currently only available for propagated values.
TODO: dependency tracking for constraints evaluating to false should be minimized.
--*/
#include "math/polysat/conflict.h"
@ -39,9 +40,7 @@ namespace polysat {
conflict::conflict(solver& s):s(s) {
ex_engines.push_back(alloc(ex_polynomial_superposition, s));
ve_engines.push_back(alloc(ve_reduction));
inf_engines.push_back(alloc(inf_saturate));
for (auto* engine : inf_engines)
engine->set_solver(s);
inf_engines.push_back(alloc(inf_saturate, s));
}
conflict::~conflict() {}
@ -218,6 +217,9 @@ namespace polysat {
while (!m_constraints.empty())
keep(m_constraints.back());
for (auto c : *this)
minimize_vars(c);
for (auto c : *this)
lemma.push(~c);
@ -232,6 +234,34 @@ namespace polysat {
return lemma;
}
void conflict::minimize_vars(signed_constraint c) {
if (m_vars.empty())
return;
if (!c.is_currently_false(s))
return;
assignment_t a;
for (auto v : m_vars)
a.push_back(std::make_pair(v, s.get_value(v)));
for (unsigned i = 0; i < a.size(); ++i) {
auto save = a[i];
auto last = a.back();
a[i] = last;
a.pop_back();
if (c.is_currently_false(a))
--i;
else {
a.push_back(last);
a[i] = save;
}
}
if (a.size() == m_vars.num_elems())
return;
m_vars.reset();
for (auto [v, val] : a)
m_vars.insert(v);
LOG("reduced " << m_vars);
}
bool conflict::resolve_value(pvar v, vector<signed_constraint> const& cjust_v) {
// NOTE:

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

@ -50,6 +50,8 @@ namespace polysat {
void insert_literal(sat::literal lit);
void remove_literal(sat::literal lit);
void minimize_vars(signed_constraint c);
/** Whether we are in a bailout state. We enter a bailout state when we give up on proper conflict resolution. */
bool m_bailout = false;
@ -65,6 +67,7 @@ namespace polysat {
pvar conflict_var() const { return m_conflict_var; }
bool is_bailout() const { return m_bailout; }
void set_bailout();
bool empty() const {

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

@ -122,11 +122,11 @@ namespace polysat {
}
bool signed_constraint::is_currently_false(solver& s) const {
return get()->is_currently_false(s.assignment(), is_positive());
return is_currently_false(s.assignment());
}
bool signed_constraint::is_currently_true(solver& s) const {
return get()->is_currently_true(s.assignment(), is_positive());
return is_currently_true(s.assignment());
}
/** Look up constraint among stored constraints. */
@ -182,20 +182,20 @@ namespace polysat {
return m_constraints.size() > m_num_external + 100;
}
signed_constraint constraint_manager::eq(pdd const& p) {
pdd z = p.manager().zero();
return {dedup(alloc(ule_constraint, *this, p, z)), true};
}
signed_constraint constraint_manager::ule(pdd const& a, pdd const& b) {
return {dedup(alloc(ule_constraint, *this, a, b)), true};
return { dedup(alloc(ule_constraint, *this, a, b)), true };
}
signed_constraint constraint_manager::ult(pdd const& a, pdd const& b) {
// a < b <=> !(b <= a)
return ~ule(b, a);
signed_constraint constraint_manager::eq(pdd const& p) {
return ule(p, p.manager().zero());
}
signed_constraint constraint_manager::ult(pdd const& a, pdd const& b) {
return ~ule(b, a);
}
// To do signed comparison of bitvectors, flip the msb and do unsigned comparison:
//
// x <=s y <=> x + 2^(w-1) <=u y + 2^(w-1)

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

@ -90,7 +90,7 @@ namespace polysat {
signed_constraint eq(pdd const& p);
signed_constraint ule(pdd const& a, pdd const& b);
signed_constraint ult(pdd const& a, pdd const& b);
signed_constraint ult(pdd const& a, pdd const& b);
signed_constraint sle(pdd const& a, pdd const& b);
signed_constraint slt(pdd const& a, pdd const& b);
@ -224,6 +224,8 @@ namespace polysat {
bool is_always_true() const { return get()->is_always_false(is_negative()); }
bool is_currently_false(solver& s) const;
bool is_currently_true(solver& s) const;
bool is_currently_false(assignment_t const& a) const { return get()->is_currently_false(a, is_positive()); }
bool is_currently_true(assignment_t const& a) const { return get()->is_currently_true(a, is_positive()); }
lbool bvalue(solver& s) const;
unsigned level(solver& s) const { return get()->level(s); }
void narrow(solver& s) { get()->narrow(s, is_positive()); }

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

@ -50,9 +50,9 @@ namespace polysat {
signed_constraint inf_saturate::ineq(bool is_strict, pdd const& lhs, pdd const& rhs) {
if (is_strict)
return s().ult(lhs, rhs);
return s.ult(lhs, rhs);
else
return s().ule(lhs, rhs);
return s.ule(lhs, rhs);
}
/**
@ -60,12 +60,12 @@ namespace polysat {
* The lemmas outlined in the rules are valid and therefore c is implied.
*/
bool inf_saturate::propagate(conflict& core, inequality const& crit1, inequality const& crit2, signed_constraint& c, vector<signed_constraint>& new_constraints) {
bool crit1_false = crit1.as_signed_constraint().is_currently_false(s());
bool crit2_false = crit2.as_signed_constraint().is_currently_false(s());
bool crit1_false = crit1.as_signed_constraint().is_currently_false(s);
bool crit2_false = crit2.as_signed_constraint().is_currently_false(s);
if (!crit1_false && !crit2_false)
return false;
bool is_bool_false = c.bvalue(s()) == l_false;
bool is_model_false = c.is_currently_false(s());
bool is_bool_false = c.bvalue(s) == l_false;
bool is_model_false = c.is_currently_false(s);
if (!is_bool_false && !is_model_false)
return false;
@ -95,8 +95,8 @@ namespace polysat {
rational x_val, y_val;
auto& pddm = x.manager();
rational bound = pddm.max_value();
VERIFY(s().try_eval(x, x_val));
VERIFY(s().try_eval(y, y_val));
VERIFY(s.try_eval(x, x_val));
VERIFY(s.try_eval(y, y_val));
SASSERT(x_val * y_val <= bound);
rational x_lo = x_val, x_hi = x_max, y_lo = y_val, y_hi = y_max;
@ -140,8 +140,8 @@ namespace polysat {
// conflict resolution should be able to pick up this as a valid justification.
// or we resort to the same extension as in the original mul_overflow code
// where we add explicit equality propagations from the current assignment.
auto c1 = s().ule(x, pddm.mk_val(x_lo));
auto c2 = s().ule(y, pddm.mk_val(y_lo));
auto c1 = s.ule(x, pddm.mk_val(x_lo));
auto c2 = s.ule(y, pddm.mk_val(y_lo));
new_constraints.insert(c1);
new_constraints.insert(c2);
}
@ -154,16 +154,16 @@ namespace polysat {
rational y_max = pddm.max_value();
if (x.is_var())
x_max = s().m_viable.max_viable(x.var());
x_max = s.m_viable.max_viable(x.var());
if (y.is_var())
y_max = s().m_viable.max_viable(y.var());
y_max = s.m_viable.max_viable(y.var());
if (x_max * y_max > pddm.max_value())
push_omega_bisect(new_constraints, x, x_max, y, y_max);
else {
for (auto c : s().m_cjust[y.var()])
for (auto c : s.m_cjust[y.var()])
new_constraints.insert(c);
for (auto c : s().m_cjust[x.var()])
for (auto c : s.m_cjust[x.var()])
new_constraints.insert(c);
}
}
@ -172,14 +172,14 @@ namespace polysat {
* Match [v] .. <= v
*/
bool inf_saturate::is_l_v(pvar v, inequality const& i) {
return i.rhs == s().var(v);
return i.rhs == s.var(v);
}
/*
* Match [v] v <= ...
*/
bool inf_saturate::is_g_v(pvar v, inequality const& i) {
return i.lhs == s().var(v);
return i.lhs == s.var(v);
}
/*
@ -199,7 +199,7 @@ namespace polysat {
}
bool inf_saturate::verify_Y_l_Ax(pvar x, inequality const& d, pdd const& a, pdd const& y) {
return d.lhs == y && d.rhs == a * s().var(x);
return d.lhs == y && d.rhs == a * s.var(x);
}
/**
@ -218,7 +218,7 @@ namespace polysat {
rational x_val, y_val;
auto& pddm = x.manager();
rational bound = rational::power_of_two(pddm.power_of_2());
return s().try_eval(x, x_val) && s().try_eval(y, y_val) && x_val * y_val < bound;
return s.try_eval(x, x_val) && s.try_eval(y, y_val) && x_val * y_val < bound;
}
/**
@ -229,7 +229,7 @@ namespace polysat {
}
bool inf_saturate::verify_Xy_l_XZ(pvar v, inequality const& c, pdd const& x, pdd const& z) {
return c.lhs == s().var(v) * x && c.rhs == z * x;
return c.lhs == s.var(v) * x && c.rhs == z * x;
}
/**
@ -240,7 +240,7 @@ namespace polysat {
}
bool inf_saturate::verify_YX_l_zX(pvar z, inequality const& c, pdd const& x, pdd const& y) {
return c.lhs == y * x && c.rhs == s().var(z) * x;
return c.lhs == y * x && c.rhs == s.var(z) * x;
}
/**
@ -263,19 +263,19 @@ namespace polysat {
* [x] yx <= zx ==> Ω*(x,y) \/ y <= z \/ x = 0
*/
bool inf_saturate::try_ugt_x(pvar v, conflict& core, inequality const& c) {
pdd x = s().var(v);
pdd x = s.var(v);
pdd y = x;
pdd z = x;
if (!is_xY_l_xZ(v, c, y, z))
return false;
if (!is_non_overflow(x, y))
return false;
if (!c.is_strict && s().get_value(v).is_zero())
if (!c.is_strict && s.get_value(v).is_zero())
return false;
vector<signed_constraint> new_constraints;
if (!c.is_strict)
new_constraints.push_back(~s().eq(x));
new_constraints.push_back(~s.eq(x));
push_omega(new_constraints, x, y);
return propagate(core, c, c, c.is_strict, y, z, new_constraints);
}
@ -283,7 +283,7 @@ namespace polysat {
/// [y] z' <= y /\ zx > yx ==> Ω*(x,y) \/ zx > z'x
/// [y] z' <= y /\ yx <= zx ==> Ω*(x,y) \/ z'x <= zx
bool inf_saturate::try_ugt_y(pvar v, conflict& core, inequality const& le_y, inequality const& yx_l_zx, pdd const& x, pdd const& z) {
pdd const y = s().var(v);
pdd const y = s.var(v);
SASSERT(is_l_v(v, le_y));
SASSERT(verify_Xy_l_XZ(v, yx_l_zx, x, z));
@ -303,7 +303,7 @@ namespace polysat {
bool inf_saturate::try_ugt_y(pvar v, conflict& core, inequality const& c) {
if (!is_l_v(v, c))
return false;
pdd x = s().var(v);
pdd x = s.var(v);
pdd z = x;
for (auto dd : core) {
if (!dd->is_ule())
@ -321,7 +321,7 @@ namespace polysat {
bool inf_saturate::try_y_l_ax_and_x_l_z(pvar x, conflict& core, inequality const& c) {
if (!is_g_v(x, c))
return false;
pdd y = s().var(x);
pdd y = s.var(x);
pdd a = y;
for (auto dd : core) {
if (!dd->is_ule())
@ -353,7 +353,7 @@ namespace polysat {
bool inf_saturate::try_ugt_z(pvar z, conflict& core, inequality const& c) {
if (!is_g_v(z, c))
return false;
pdd y = s().var(z);
pdd y = s.var(z);
pdd x = y;
for (auto dd : core) {
if (!dd->is_ule())
@ -387,19 +387,19 @@ namespace polysat {
return false;
if (c.lhs.is_val() || c.rhs.is_val())
return false;
if (!c.as_signed_constraint().is_currently_false(s()))
if (!c.as_signed_constraint().is_currently_false(s))
return false;
rational l_val, r_val;
if (!s().try_eval(c.lhs, l_val))
if (!s.try_eval(c.lhs, l_val))
return false;
if (!s().try_eval(c.rhs, r_val))
if (!s.try_eval(c.rhs, r_val))
return false;
SASSERT(c.is_strict || l_val > r_val);
SASSERT(!c.is_strict || l_val >= r_val);
vector<signed_constraint> new_constraints;
new_constraints.push_back(c.as_signed_constraint());
new_constraints.push_back(s().ule(c.rhs, r_val));
return propagate(core, c, c, c.is_strict ? s().ult(c.lhs, r_val) : s().ule(c.lhs, r_val), new_constraints);
new_constraints.push_back(s.ule(c.rhs, r_val));
return propagate(core, c, c, c.is_strict ? s.ult(c.lhs, r_val) : s.ule(c.lhs, r_val), new_constraints);
}
}

7
src/math/polysat/saturation.h
View file

@ -21,11 +21,10 @@ namespace polysat {
class inference_engine {
friend class conflict;
solver* m_solver = nullptr;
void set_solver(solver& s) { m_solver = &s; }
protected:
solver& s() { return *m_solver; }
solver& s;
public:
inference_engine(solver& s) :s(s) {}
virtual ~inference_engine() {}
/** Try to apply an inference rule.
* Derive new constraints from constraints containing the variable v (i.e., at least one premise must contain v).
@ -91,7 +90,7 @@ namespace polysat {
bool is_coeffxY(pdd const& coeff_x, pdd const& p, pdd& y);
public:
inf_saturate(solver& s) : inference_engine(s) {}
bool perform(pvar v, conflict& core) override;
};