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

full interval case

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-11 08:44:16 -08:00
parent 86de8bd5b1
commit 9fb9e659b0
2 changed files with 26 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/polysat/op_constraint.h
View file

@ -9,7 +9,7 @@ Module Name:
ashr: r == p >>a q
lshl: r == p << q
and: r == p & q
not: r == ~p
or: r == p | q
Author:

30
src/sat/smt/polysat/viable.cpp
View file

@ -744,18 +744,38 @@ namespace polysat {
ne->side_cond.push_back(~cs.eq(hi_eq));
}
//
// If new_lo = new_hi it means that
// mod(ceil (lo / 2^k), 2^w) = mod(ceil (hi / 2^k), 2^w)
// or
// div (mod(lo + 2^k -1, 2^w), 2^k) = div (mod(hi + 2^k - 1, 2^w), 2^k)
// but we also have lo != hi.
// Assume lo < hi
// - it means 2^k does not divide any of [lo, hi[
// so x*2^k cannot be in [lo, hi[
// Assume lo > hi
// - then the constraint is x*2^k not in [lo, 0[, [0, hi[
// - then new_lo = new_hi = 0
// - it means 2^k does not divide any of [hi, lo[
// - therefore the interval [lo, hi[ contains all the divisors of 2^k
//
if (new_lo == new_hi) {
if (lo < hi) {
m_alloc.push_back(ne);
return find_t::multiple;
}
else {
IF_VERBOSE(0, display_one(verbose_stream() << "full: ", v, ne) << "\n");
SASSERT(hi < lo);
// exclude 0
IF_VERBOSE(0, display_one(verbose_stream() << "Exclude 0: ", v, ne) << "\n");
SASSERT(new_lo == 0);
new_hi = 1;
ne->interval = eval_interval::full();
ne->coeff = 1;
m_explain.reset();
m_explain.push_back({ ne, rational::zero() });
m_fixed_bits.reset();
m_var = v;
return find_t::empty;
}
}