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

Simplify equations into canonical form

Browse source 
Also simplify constraints that are always false due to parity
This commit is contained in:
Jakob Rath 2022-09-28 13:17:14 +02:00
parent 480ba01cb0
commit 6715058876
4 changed files with 105 additions and 69 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -203,7 +203,11 @@ namespace polysat {
}
signed_constraint constraint_manager::ule(pdd const& a, pdd const& b) {
return { dedup(alloc(ule_constraint, *this, a, b)), true };
bool is_positive = true;
pdd lhs = a;
pdd rhs = b;
ule_constraint::simplify(is_positive, lhs, rhs);
return { dedup(alloc(ule_constraint, *this, lhs, rhs)), is_positive };
}
signed_constraint constraint_manager::eq(pdd const& p) {
@ -215,18 +219,12 @@ namespace polysat {
}
bool signed_constraint::is_eq() const {
if (is_positive())
return m_constraint->is_eq();
else
return m_constraint->is_diseq();
return is_positive() && m_constraint->is_eq();
}
pdd const& signed_constraint::eq() const {
SASSERT(is_eq());
if (is_positive())
return m_constraint->to_ule().lhs();
else
return m_constraint->to_ule().rhs();
return m_constraint->to_ule().lhs();
}
/**

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

@ -106,8 +106,8 @@ namespace polysat {
signed_constraint lshr(pdd const& p, pdd const& q, pdd const& r);
signed_constraint band(pdd const& p, pdd const& q, pdd const& r);
constraint *const* begin() const { return m_constraints.data(); }
constraint *const* end() const { return m_constraints.data() + m_constraints.size(); }
constraint* const* begin() const { return m_constraints.data(); }
constraint* const* end() const { return m_constraints.data() + m_constraints.size(); }
using clause_iterator = decltype(m_clauses)::const_iterator;
clause_iterator clauses_begin() const { return m_clauses.begin(); }
@ -167,7 +167,6 @@ namespace polysat {
bool operator!=(constraint const& other) const { return !operator==(other); }
virtual bool is_eq() const { return false; }
virtual bool is_diseq() const { return false; }
bool is_ule() const { return m_kind == ckind_t::ule_t; }
bool is_umul_ovfl() const { return m_kind == ckind_t::umul_ovfl_t; }
bool is_smul_fl() const { return m_kind == ckind_t::smul_fl_t; }

150
src/math/polysat/ule_constraint.cpp
View file

@ -12,15 +12,30 @@ Author:
Notes:
Canonical representation of equation p == 0 is the constraint p <= 0.
The alternatives p < 1, -1 <= q, q > -2 are eliminated.
Rewrite rules to simplify expressions.
In the following let k, k1, k2 be values.
- k1 <= k2 ==> 0 <= 0 if k1 <= k2
- k1 <= k2 ==> 1 <= 0 if k1 > k2
- 0 <= p ==> 0 <= 0
- p <= -1 ==> 0 <= 0
- k*2^n*p <= 0 ==> 2^n*p <= 0 if k is odd, leading coeffient is always a power of 2.
- k <= p ==> p - k <= - k - 1
- k1 <= k2 ==> 0 <= 0 if k1 <= k2
- k1 <= k2 ==> 1 <= 0 if k1 > k2
- 0 <= p ==> 0 <= 0
- p <= 0 ==> 1 <= 0 if p is never zero due to parity
- p <= -1 ==> 0 <= 0
- k <= p ==> p - k <= - k - 1
- k*2^n*p <= 0 ==> 2^n*p <= 0 if k is odd, leading coeffient is always a power of 2.
Note: the rules will rewrite alternative formulations of equations:
- -1 <= p ==> p + 1 <= 0
- 1 <= p ==> p - 1 <= -2
Rewrite rules on signed constraints:
- p > -2 ==> p + 1 <= 0
- p <= -2 ==> p + 1 > 0
At this point, all equations are in canonical form.
TODO: clause simplifications:
@ -44,72 +59,97 @@ Note:
#include "math/polysat/solver.h"
#include "math/polysat/log.h"
namespace {
using namespace polysat;
// Simplify lhs <= rhs
void simplify_impl(bool& is_positive, pdd& lhs, pdd& rhs) {
// 0 <= p --> 0 <= 0
if (lhs.is_zero()) {
rhs = 0;
return;
}
// p <= -1 --> 0 <= 0
if (rhs.is_val() && rhs.val() == rhs.manager().max_value()) {
lhs = 0, rhs = 0;
return;
}
// p <= p --> 0 <= 0
if (lhs == rhs) {
lhs = 0, rhs = 0;
return;
}
// Evaluate constants
if (lhs.is_val() && rhs.is_val()) {
if (lhs.val() <= rhs.val())
lhs = 0, rhs = 0;
else
lhs = 1, rhs = 0;
return;
}
// k <= p --> p - k <= - k - 1
if (lhs.is_val()) {
pdd k = lhs;
lhs = rhs - k;
rhs = - k - 1;
}
// p > -2 --> p + 1 <= 0
// p <= -2 --> p + 1 > 0
if (rhs.is_val() && (rhs + 2).is_zero()) {
lhs = lhs + 1;
rhs = 0;
is_positive = !is_positive;
}
// 2p + 1 <= 0 --> 1 <= 0
if (rhs.is_zero() && lhs.is_never_zero()) {
lhs = 1;
return;
}
// a*p + q <= 0 --> p + a^-1*q <= 0 for a odd
if (rhs.is_zero() && !lhs.leading_coefficient().is_power_of_two()) {
rational lc = lhs.leading_coefficient();
rational x, y;
gcd(lc, lhs.manager().two_to_N(), x, y);
if (x.is_neg())
x = mod(x, lhs.manager().two_to_N());
lhs *= x;
SASSERT(lhs.leading_coefficient().is_power_of_two());
}
} // simplify_impl
}
namespace polysat {
ule_constraint::ule_constraint(constraint_manager& m, pdd const& l, pdd const& r) :
constraint(m, ckind_t::ule_t), m_lhs(l), m_rhs(r) {
#ifndef NDEBUG
pdd const old_lhs = m_lhs;
pdd const old_rhs = m_rhs;
#endif
simplify();
#ifndef NDEBUG
if (old_lhs != m_lhs || old_rhs != m_rhs)
LOG("Simplify: " << ule_pp(l_true, old_lhs, old_rhs) << " --> " << ule_pp(l_true, m_lhs, m_rhs));
#endif
m_vars.append(m_lhs.free_vars());
for (auto v : m_rhs.free_vars())
if (!m_vars.contains(v))
m_vars.push_back(v);
}
void ule_constraint::simplify() {
if (m_lhs.is_zero()) {
m_rhs = 0;
return;
}
if (m_rhs.is_val() && m_rhs.val() == m_rhs.manager().max_value()) {
m_lhs = 0, m_rhs = 0;
return;
}
if (m_lhs == m_rhs) {
m_lhs = m_rhs = 0;
return;
}
if (m_lhs.is_val() && m_rhs.is_val()) {
if (m_lhs.val() <= m_rhs.val())
m_lhs = m_rhs = 0;
else
m_lhs = 1, m_rhs = 0;
return;
}
// k <= p --> p - k <= - k - 1
if (m_lhs.is_val()) {
pdd k = m_lhs;
m_lhs = m_rhs - k;
m_rhs = - k - 1;
}
// a*p + q <= 0 <=> p + a^-1*q <= 0 for a odd
if (m_rhs.is_zero() && !m_lhs.leading_coefficient().is_power_of_two()) {
rational lc = m_lhs.leading_coefficient();
rational x, y;
gcd(lc, m_lhs.manager().two_to_N(), x, y);
if (x.is_neg())
x = mod(x, m_lhs.manager().two_to_N());
m_lhs *= x;
SASSERT(m_lhs.leading_coefficient().is_power_of_two());
void ule_constraint::simplify(bool& is_positive, pdd& lhs, pdd& rhs) {
#ifndef NDEBUG
bool const old_is_positive = is_positive;
pdd const old_lhs = lhs;
pdd const old_rhs = rhs;
#endif
simplify_impl(is_positive, lhs, rhs);
#ifndef NDEBUG
if (old_is_positive != is_positive || old_lhs != lhs || old_rhs != rhs) {
ule_pp const old_ule(to_lbool(old_is_positive), old_lhs, old_rhs);
ule_pp const new_ule(to_lbool(is_positive), lhs, rhs);
LOG("Simplify: " << old_ule << " --> " << new_ule);
}
#endif
}
std::ostream& ule_constraint::display(std::ostream& out, lbool status, pdd const& lhs, pdd const& rhs) {
out << lhs;
if (rhs.is_zero() && status == l_true) out << " == ";
else if (rhs.is_zero() && status == l_false) out << " != ";
// else if (lhs.is_one() && status == l_true) out << " != ";
// else if (lhs.is_one() && status == l_false) out << " == ";
else if (status == l_true) out << " <= ";
else if (status == l_false) out << " > ";
else out << " <=/> ";
@ -149,6 +189,7 @@ namespace polysat {
}
bool ule_constraint::is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs) {
// NOTE: don't assume simplifications here because we also call this on partially substituted constraints
if (is_positive) {
// lhs <= rhs
if (rhs.is_zero())
@ -199,7 +240,6 @@ namespace polysat {
return p.is_val() && q.is_val() && p.val() > q.val();
}
inequality ule_constraint::as_inequality(bool is_positive) const {
if (is_positive)
return inequality(lhs(), rhs(), false, this);

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

@ -26,7 +26,7 @@ namespace polysat {
pdd m_rhs;
ule_constraint(constraint_manager& m, pdd const& l, pdd const& r);
void simplify();
static void simplify(bool& is_positive, pdd& lhs, pdd& rhs);
public:
~ule_constraint() override {}
@ -46,7 +46,6 @@ namespace polysat {
unsigned hash() const override;
bool operator==(constraint const& other) const override;
bool is_eq() const override { return m_rhs.is_zero(); }
bool is_diseq() const override { return m_lhs.is_one(); }
void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override;
};