mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-06 19:21:22 +00:00
Code Activity

separate scope

Browse source
This commit is contained in:
Jakob Rath 2024-05-15 11:36:06 +02:00
parent 865822651c
commit 16fb86b636
1 changed files with 17 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -974,23 +974,25 @@ v0[19] := 0 v0 [-131062 ; 0[ := [-131062;0[ src ~4 <= 43691*v0;
#endif
// for simplicity, we fix the evaluation of the stored upper bits
// (alternative would be to track sub-ranges of extracted symbolic bounds)
pdd const t_val = c.subst(t); // we have to take the actual value of 't', because e.value is computed after bit-width-reduction, which may include a wrap-around
VERIFY(t_val.is_val());
unsigned const k = bw - ebw;
rational const t_fixed = machine_div2k(t_val.val(), abw + k);
auto const sc = cs.fixed(t, ebw - 1 + k, abw + k, t_fixed);
{
pdd const t_val = c.subst(t); // we have to take the actual value of 't', because e.value is computed after bit-width-reduction, which may include a wrap-around
VERIFY(t_val.is_val());
unsigned const k = bw - ebw;
rational const t_fixed = machine_div2k(t_val.val(), abw + k);
auto const sc = cs.fixed(t, ebw - 1 + k, abw + k, t_fixed);
#if DEBUG_EXPLAIN
verbose_stream() << " t " << t << "\n";
verbose_stream() << " eval(t) " << c.subst(t) << " val " << c.subst(t).val() << "\n";
verbose_stream() << " t[" << (ebw - 1 + k) << ":" << (abw + k) << "] = " << store_val << "\n";
verbose_stream() << " fixed prefix constraint " << sc << "\n";
verbose_stream() << " eval " << sc.eval() << "\n";
verbose_stream() << " weval " << sc.weak_eval(c.get_assignment()) << "\n";
verbose_stream() << " seval " << sc.strong_eval(c.get_assignment()) << "\n";
verbose_stream() << " t " << t << "\n";
verbose_stream() << " eval(t) " << c.subst(t) << " val " << c.subst(t).val() << "\n";
verbose_stream() << " t[" << (ebw - 1 + k) << ":" << (abw + k) << "] = " << store_val << "\n";
verbose_stream() << " fixed prefix constraint " << sc << "\n";
verbose_stream() << " eval " << sc.eval() << "\n";
verbose_stream() << " weval " << sc.weak_eval(c.get_assignment()) << "\n";
verbose_stream() << " seval " << sc.strong_eval(c.get_assignment()) << "\n";
#endif
VERIFY(!sc.is_always_false());
if (!sc.is_always_true())
deps.push_back(c.propagate(sc, c.explain_weak_eval(sc), "explain_overlap prefix evaluation"));
VERIFY(!sc.is_always_false());
if (!sc.is_always_true())
deps.push_back(c.propagate(sc, c.explain_weak_eval(sc), "explain_overlap prefix evaluation"));
}
/*
from smtlib-2023-ni/QF_BV/sage/app5/bench_1002.smt2
v2[16] := 0 v2 [256 ; 0[ := [256;0[ src ~256 <= v2;