mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-23 20:58:54 +00:00
Code Activity

Fix monomials::parity

Browse source
This commit is contained in:
Jakob Rath 2024-03-27 10:49:02 +01:00
parent e22c86acb6
commit a7c84da44d
4 changed files with 45 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

33
src/sat/smt/polysat/constraints.cpp
View file

@ -69,26 +69,33 @@ namespace polysat {
return signed_constraint(ckind_t::op_t, cnstr); return signed_constraint(ckind_t::op_t, cnstr);
} }
// parity p >= k if low order k bits of p are 0 // parity(p) >= k if low order k bits of p are 0.
// Requires 0 <= k <= N.
signed_constraint constraints::parity_at_least(pdd const& p, unsigned k) { signed_constraint constraints::parity_at_least(pdd const& p, unsigned k) {
auto& m = p.manager();
unsigned N = m.power_of_2();
// NOTE: it is ambiguous at this point what we want for k > N:
// - as a condition, parity(p) > N is never true
// - as an implied constraint, we usually want p == 0 instead
VERIFY(k <= N);
if (k == 0) if (k == 0)
return uge(p, 0); // parity(p) >= 0 is a tautology
unsigned N = p.manager().power_of_2(); return eq(m.zero());
if (k == N)
return eq(p);
// parity(p) >= k // parity(p) >= k
// <=> p * 2^(N - k) == 0 // <=> p * 2^(N - k) == 0
if (k > N) return eq(p * rational::power_of_two(N - k));
// parity(p) > N is never true
return ~eq(p.manager().zero());
else if (k == 0)
// parity(p) >= 0 is a tautology
return eq(p.manager().zero());
else if (k == N)
return eq(p);
else
return eq(p * rational::power_of_two(N - k));
} }
// parity(p) <= k.
// Requires 0 <= k <= N.
signed_constraint constraints::parity_at_most(pdd const& p, unsigned k) { signed_constraint constraints::parity_at_most(pdd const& p, unsigned k) {
auto& m = p.manager();
unsigned N = m.power_of_2();
if (k == N)
// parity(p) <= N is a tautology
return eq(m.zero());
return ~parity_at_least(p, k + 1); return ~parity_at_least(p, k + 1);
} }

1
src/sat/smt/polysat/constraints.h
View file

@ -64,6 +64,7 @@ namespace polysat {
signed_constraint() {} signed_constraint() {}
signed_constraint(ckind_t c, constraint* p) : m_op(c), m_constraint(p) {} signed_constraint(ckind_t c, constraint* p) : m_op(c), m_constraint(p) {}
signed_constraint operator~() const { signed_constraint r(*this); r.m_sign = !r.m_sign; return r; } signed_constraint operator~() const { signed_constraint r(*this); r.m_sign = !r.m_sign; return r; }
bool is_null() const { return m_constraint == nullptr; }
bool sign() const { return m_sign; } bool sign() const { return m_sign; }
bool is_positive() const { return !m_sign; } bool is_positive() const { return !m_sign; }
bool is_negative() const { return m_sign; } bool is_negative() const { return m_sign; }

28
src/sat/smt/polysat/monomials.cpp
View file

@ -102,7 +102,7 @@ namespace polysat {
} }
bool monomials::eval_to_false(unsigned i) { bool monomials::eval_to_false(unsigned i) {
rational rhs, lhs; rational rhs;
auto& mon = m_monomials[i]; auto& mon = m_monomials[i];
if (!c.try_eval(mon.var, mon.val)) if (!c.try_eval(mon.var, mon.val))
return false; return false;
@ -198,12 +198,12 @@ namespace polysat {
} }
// parity p * q = min(N, parity(p) + parity(q)) // parity p * q = min(N, parity(p) + parity(q))
bool monomials::parity(monomial const& mon) { bool monomials::parity(monomial const& mon) {
unsigned parity_val = get_parity(mon.val, mon.num_bits()); unsigned N = mon.num_bits();
unsigned parity_val = get_parity(mon.val, N);
unsigned sum_parities = 0; unsigned sum_parities = 0;
unsigned N = mon.var.manager().power_of_2();
for (unsigned j = 0; j < mon.args.size(); ++j) { for (unsigned j = 0; j < mon.args.size(); ++j) {
unsigned k = get_parity(mon.arg_vals[j], mon.num_bits()); unsigned k = get_parity(mon.arg_vals[j], N);
if (k > parity_val) { if (k > parity_val) {
auto const& p = mon.args[j]; auto const& p = mon.args[j];
if (c.add_axiom("parity p >= i => parity p * q >= i", { ~C.parity_at_least(p, k), C.parity_at_least(mon.var, k) }, true)) if (c.add_axiom("parity p >= i => parity p * q >= i", { ~C.parity_at_least(p, k), C.parity_at_least(mon.var, k) }, true))
@ -218,16 +218,18 @@ namespace polysat {
if (sum_parities > parity_val) { if (sum_parities > parity_val) {
constraint_or_dependency_vector clause; constraint_or_dependency_vector clause;
for (unsigned j = 0; j < mon.args.size(); ++j) for (unsigned j = 0; j < mon.args.size(); ++j)
clause.push_back(~C.parity_at_least(mon.args[j], get_parity(mon.arg_vals[j], mon.num_bits()))); clause.push_back(~C.parity_at_least(mon.args[j], get_parity(mon.arg_vals[j], N)));
clause.push_back(C.parity_at_least(mon.var, sum_parities)); unsigned min_var_parity = std::min(N, sum_parities);
clause.push_back(C.parity_at_least(mon.var, min_var_parity));
return c.add_axiom("N >= pp + qp, pp >= parity(p), qq >= parity(q) => parity p * q >= pp + qp)", clause, true); return c.add_axiom("N >= pp + qp, pp >= parity(p), qq >= parity(q) => parity p * q >= pp + qp)", clause, true);
} }
// sum_parities < parity_val // sum_parities < parity_val
SASSERT(sum_parities < N);
constraint_or_dependency_vector clause; constraint_or_dependency_vector clause;
clause.push_back(~C.parity_at_least(mon.var, sum_parities)); clause.push_back(~C.parity_at_least(mon.var, 1 + sum_parities));
for (unsigned j = 0; j < mon.args.size(); ++j) for (unsigned j = 0; j < mon.args.size(); ++j)
clause.push_back(C.parity_at_least(mon.args[j], 1 + get_parity(mon.arg_vals[j], mon.num_bits()))); clause.push_back(C.parity_at_least(mon.args[j], 1 + get_parity(mon.arg_vals[j], N)));
return c.add_axiom("parity(p * q) > pp + qp => pp < parity(p) or qp < parity(q))", clause, true); return c.add_axiom("parity(p * q) > pp + qp => parity(p) > pp or parity(q) > qp", clause, true);
} }
// ~ovfl*(p,q) & q != 0 => p <= p*q // ~ovfl*(p,q) & q != 0 => p <= p*q
@ -374,13 +376,15 @@ namespace polysat {
out << sep << p, sep = " * "; out << sep << p, sep = " * ";
else else
out << sep << "(" << p << ")", sep = " * "; out << sep << "(" << p << ")", sep = " * ";
out << "\n"; // out << " arg_vals " << arg_vals;
// out << " def " << def;
// out << " val " << val;
return out; return out;
} }
std::ostream& monomials::display(std::ostream& out) const { std::ostream& monomials::display(std::ostream& out) const {
for (auto const& mon : m_monomials) for (auto const& mon : m_monomials)
mon.display(out); mon.display(out) << "\n";
return out; return out;
} }
} }

15
src/sat/smt/polysat/monomials.h
View file

@ -29,18 +29,19 @@ namespace polysat {
constraints& C; constraints& C;
struct monomial { struct monomial {
pdd_vector args; pdd_vector args;
pdd var; pdd var;
pdd def; pdd def;
rational_vector arg_vals; rational_vector arg_vals; // values of 'args'
rational val; rational val; // value of 'var'
unsigned size() const { return args.size(); } unsigned size() const { return args.size(); }
unsigned num_bits() const { return args[0].manager().power_of_2(); } unsigned num_bits() const { return var.manager().power_of_2(); }
std::ostream& display(std::ostream& out) const; std::ostream& display(std::ostream& out) const;
}; };
vector<monomial> m_monomials; vector<monomial> m_monomials;
pdd_vector m_tmp; pdd_vector m_tmp;
friend std::ostream& operator<<(std::ostream& out, monomials::monomial const& mon) { return mon.display(out); }
unsigned_vector m_to_refine; unsigned_vector m_to_refine;
void init_to_refine(); void init_to_refine();