mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

sketch parity generalization

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-12-07 20:04:58 -08:00
parent 55d691e16e
commit 437f826e8b
4 changed files with 118 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

41
src/math/dd/dd_pdd.cpp
View file

@ -165,6 +165,47 @@ namespace dd {
return true;
}
unsigned pdd_manager::min_parity(PDD p) {
if (m_semantics != mod2N_e)
return 0;
if (is_val(p)) {
rational v = val(p);
if (v.is_zero())
return m_power_of_2 + 1;
unsigned r = 0;
while (v.is_even() && v > 0)
r++, v /= 2;
return r;
}
PDD q = p;
while (!is_val(q))
q = lo(q);
unsigned p2 = val(q).trailing_zeros();
init_mark();
if (p2 == 0)
return 0;
init_mark();
m_todo.push_back(hi(p));
while (!m_todo.empty() && p2 != 0) {
PDD r = m_todo.back();
m_todo.pop_back();
if (is_marked(r))
continue;
set_mark(r);
if (!is_val(r)) {
m_todo.push_back(lo(r));
m_todo.push_back(hi(r));
}
else if (val(r).is_zero())
continue;
else if (val(r).trailing_zeros() < p2)
p2 = val(r).trailing_zeros();
}
m_todo.reset();
return p2;
}
pdd pdd_manager::subst_val(pdd const& p, pdd const& s) {
return pdd(apply(p.root, s.root, pdd_subst_val_op), this);
}

2
src/math/dd/dd_pdd.h
View file

@ -255,6 +255,7 @@ namespace dd {
inline bool is_var(PDD p) const { return !is_val(p) && is_zero(lo(p)) && is_one(hi(p)); }
inline bool is_max(PDD p) const { SASSERT(m_semantics == mod2_e || m_semantics == mod2N_e); return is_val(p) && val(p) == max_value(); }
bool is_never_zero(PDD p);
unsigned min_parity(PDD p);
inline unsigned level(PDD p) const { return m_nodes[p].m_level; }
inline unsigned var(PDD p) const { return m_level2var[level(p)]; }
inline PDD lo(PDD p) const { return m_nodes[p].m_lo; }
@ -432,6 +433,7 @@ namespace dd {
void get_univariate_coefficients(vector<rational>& coeff) const { m.get_univariate_coefficients(root, coeff); }
vector<rational> get_univariate_coefficients() const { vector<rational> coeff; m.get_univariate_coefficients(root, coeff); return coeff; }
bool is_never_zero() const { return m.is_never_zero(root); }
unsigned min_parity() const { return m.min_parity(root); }
bool var_is_leaf(unsigned v) const { return m.var_is_leaf(root, v); }
pdd operator-() const { return m.minus(*this); }

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

@ -633,6 +633,7 @@ namespace polysat {
bool saturation::try_parity(pvar x, conflict& core, inequality const& axb_l_y) {
set_rule("[x] a*x + b = 0 => (odd(a) & odd(x) <=> odd(b))");
auto& m = s.var2pdd(x);
unsigned N = m.power_of_2();
pdd y = m.zero();
pdd a = m.zero();
pdd b = m.zero();
@ -653,29 +654,78 @@ namespace polysat {
LOG("a_is_odd: " << lit_pp(s, a_is_odd));
LOG("x_is_odd: " << lit_pp(s, x_is_odd));
#endif
if (!b_is_odd.is_currently_true(s)) {
if (!a_is_odd.is_currently_true(s))
return false;
if (!x_is_odd.is_currently_true(s))
return false;
if (a_is_odd.is_currently_true(s) &&
x_is_odd.is_currently_true(s)) {
m_lemma.reset();
m_lemma.insert_eval(~s.eq(y));
m_lemma.insert_eval(~a_is_odd);
m_lemma.insert_eval(~x_is_odd);
if (propagate(core, axb_l_y, b_is_odd))
return true;
return false;
}
m_lemma.reset();
m_lemma.insert_eval(~s.eq(y));
m_lemma.insert_eval(~b_is_odd);
if (propagate(core, axb_l_y, a_is_odd))
return true;
m_lemma.reset();
m_lemma.insert_eval(~s.eq(y));
m_lemma.insert_eval(~b_is_odd);
if (propagate(core, axb_l_y, x_is_odd))
return true;
#if 0
// TODO - enable this code and test
// a is divisibly by 4,
// max divisor of x is k
// -> b has parity k + 4
if ((~a_is_odd).is_currently_true(s) ||
(~x_is_odd).is_currently_true(s)) {
unsigned a_parity = 0;
unsigned x_parity = 0;
while (a_parity <= N && s.parity(a, a_parity+1).is_currently_true(s))
++a_parity;
while (x_parity <= N && s.parity(X, x_parity+1).is_currently_true(s))
++x_parity;
SASSERT(a_parity > 0 || x_parity > 0);
unsigned b_parity = std::min(N + 1, a_parity + x_parity);
if (a_parity > 0)
m_lemma.insert_eval(~s.parity(a, a_parity));
if (x_parity > 0)
m_lemma.insert_eval(~s.parity(X, x_parity));
if (propagate(core, axb_l_y, s.parity(b, b_parity)))
return true;
}
#endif
if (b_is_odd.is_currently_true(s)) {
m_lemma.reset();
m_lemma.insert_eval(~s.eq(y));
m_lemma.insert_eval(~b_is_odd);
if (propagate(core, axb_l_y, a_is_odd))
return true;
m_lemma.reset();
m_lemma.insert_eval(~s.eq(y));
m_lemma.insert_eval(~b_is_odd);
if (propagate(core, axb_l_y, x_is_odd))
return true;
}
#if 0
//
// if b has at least b_parity, then a*x has at least b_parity
// establish lower bound on parity of b
//
if ((~b_is_odd).is_currently_true(s) && !is_forced_eq(b, 0)) {
unsigned b_parity = 1;
while (b_parity <= N && s.parity(b, b_parity+1).is_currently_true(s))
++b_parity;
SASSERT(b_parity <= N);
// TODO:
// something like this (but fixed)
for (unsigned i = 0; i <= b_parity; ++i) {
if (s.parity(a, b_parity - i).is_currently_false(s)) {
m_lemma.reset();
m_lemma.insert_eval(~s.eq(y));
m_lemma.insert_eval(~s.parity(b, b_parity));
m_lemma.insert_eval(s.parity(a, b_parity - i));
if (propagate(core, axb_l_y, s.parity(x, i)))
return true;
}
}
}
#endif
return false;
}

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

@ -413,7 +413,15 @@ namespace polysat {
signed_constraint odd(pdd const& p) { return ~even(p); }
signed_constraint even(pdd const& p) { return parity(p, 1); }
/** parity(p) >= k (<=> p * 2^(K-k) == 0) */
signed_constraint parity(pdd const& p, unsigned k) { return eq(p*rational::power_of_two(p.manager().power_of_2() - k)); }
signed_constraint parity(pdd const& p, unsigned k) {
unsigned N = p.manager().power_of_2();
if (k > N)
return eq(p);
else if (k == 0)
return odd(p);
else
return eq(p*rational::power_of_two(N - k));
}
signed_constraint diseq(pdd const& p, rational const& q) { return diseq(p - q); }
signed_constraint diseq(pdd const& p, unsigned q) { return diseq(p - q); }
signed_constraint ule(pdd const& p, pdd const& q) { return m_constraints.ule(p, q); }