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

missing disequality parity constraint

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-12-25 16:13:26 -08:00
parent 4c6499f28b
commit 67b9ecbd97
1 changed files with 33 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -379,6 +379,8 @@ namespace polysat {
if (!i.is_strict())
return false;
y = i.lhs();
if (i.rhs().is_val() && i.rhs().val() == 1)
return false;
rational y_val;
if (!s.try_eval(y, y_val) || y_val != 0)
return false;
@ -991,12 +993,14 @@ namespace polysat {
}
/**
* 2^{K-1}*x*y != 0 => odd(x) & odd(y)
* 2^k*x != 0 => parity(x) < K - k
* 2^k*x*y != 0 => parity(x) + parity(y) < K - k
* 2^{N-1}*x*y != 0 => odd(x) & odd(y)
* 2^k*x != 0 => parity(x) < N - k
* 2^k*x*y != 0 => parity(x) + parity(y) < N - k
*
* 2^k*x + b != 0 & parity(x) < N - k => b != 0
*/
bool saturation::try_parity_diseq(pvar x, conflict& core, inequality const& axb_l_y) {
set_rule("[x] 2^k*x*y != 0 => parity(x) + parity(y) < K - k");
set_rule("[x] p(x,y) != 0 => constraints on parity(x), parity(y)");
auto& m = s.var2pdd(x);
unsigned N = m.power_of_2();
pdd y = m.zero();
@ -1004,18 +1008,31 @@ namespace polysat {
pdd X = s.var(x);
if (!is_AxB_diseq_0(x, axb_l_y, a, b, y))
return false;
if (!is_forced_eq(b, 0))
return false;
auto coeff = a.leading_coefficient();
if (coeff.is_odd())
return false;
SASSERT(coeff != 0);
unsigned k = coeff.trailing_zeros();
m_lemma.reset();
m_lemma.insert_eval(~s.eq(y));
m_lemma.insert_eval(~s.eq(b));
if (propagate(x, core, axb_l_y, ~s.parity(X, N - k)))
return true;
if (is_forced_eq(b, 0)) {
auto coeff = a.leading_coefficient();
if (coeff.is_odd())
return false;
SASSERT(coeff != 0);
unsigned k = coeff.trailing_zeros();
m_lemma.reset();
m_lemma.insert_eval(~s.eq(y));
m_lemma.insert_eval(~s.eq(b));
if (propagate(x, core, axb_l_y, ~s.parity(X, N - k)))
return true;
// TODO parity on a (without leading coefficient?)
}
if (a.is_val()) {
auto coeff = a.val();
unsigned k = coeff.trailing_zeros();
unsigned p_x = max_parity(X);
if (k + p_x < N) {
m_lemma.reset();
m_lemma.insert_eval(~s.eq(y));
m_lemma.insert_eval(~s.parity_at_most(X, p_x));
if (propagate(x, core, axb_l_y, ~s.eq(b)))
return true;
}
}
return false;
}