mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-29 01:18:45 +00:00
Code Activity

bugfix

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-12 14:00:33 -08:00
parent abc0cf3775
commit 22103c0322
2 changed files with 15 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/polysat/fixed_bits.cpp
View file

@ -34,11 +34,9 @@ namespace polysat {
bool fixed_bits::check(rational const& val, fi_record& fi) { bool fixed_bits::check(rational const& val, fi_record& fi) {
unsigned sz = c.size(m_var); unsigned sz = c.size(m_var);
rational bw = rational::power_of_two(sz); rational bw = rational::power_of_two(sz);
// verbose_stream() << "check for fixed bits v" << m_var << "[" << sz << "] := " << val << "\n";
for (auto const& s : m_fixed_slices) { for (auto const& s : m_fixed_slices) {
rational sbw = rational::power_of_two(s.length); rational sbw = rational::power_of_two(s.length);
// slice is properly contained in bit-vector variable // slice is properly contained in bit-vector variable
// verbose_stream() << " slice " << s.value << "[" << s.length << "]@" << s.offset << "\n";
if (s.length <= sz && s.value != mod(machine_div2k(val, s.offset), sbw)) { if (s.length <= sz && s.value != mod(machine_div2k(val, s.offset), sbw)) {
SASSERT(s.offset + s.length <= sz); SASSERT(s.offset + s.length <= sz);
rational hi_val = s.value; rational hi_val = s.value;

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

@ -638,20 +638,27 @@ namespace polysat {
if (ebw < bw || aw != bw) { if (ebw < bw || aw != bw) {
auto const& p2b = rational::power_of_two(bw); auto const& p2b = rational::power_of_two(bw);
auto const& p2eb = rational::power_of_two(bw - ebw); auto const& p2eb = rational::power_of_two(bw - ebw);
// let coeff = 2^{bw - ebw}
// let assume coeff * x \not\in [lo, t[
// Then value is chosen, min x . coeff * x >= t.
// In other words:
//
// coeff * (value - 1) <= t < coeff*value + 1
//
auto vlo = c.value(mod((e.value - 1) * p2eb, p2b), bw);
auto vhi = c.value(mod(e.value * p2eb + 1, p2b), bw); auto vhi = c.value(mod(e.value * p2eb + 1, p2b), bw);
auto vlo = c.value(mod((e.value - 1) * p2eb - 1, p2b), bw);
// t in ] (value - 1) * 2^{bw - ebw} ; value * 2^{bw - ebw} ]
// t in [ (value - 1) * 2^{bw - ebw} - 1 ; value * 2^{bw - ebw} + 1 [
#if 0 #if 0
verbose_stream() << e.value << " " << t << "\n"; verbose_stream() << "value " << e.value << "\n";
if (t.is_val()) verbose_stream() << "tval " << t.val() << "\n"; verbose_stream() << "t " << t << "\n";
verbose_stream() << "[" << vlo << " " << vhi << "[\n"; verbose_stream() << "[" << vlo << " " << vhi << "[\n";
verbose_stream() << "bw " << ebw << " " << bw << " " << e.e->interval << " bw " << abw << " " << aw << " " << after.e->coeff << " " << after.e->interval << "\n"; verbose_stream() << "before bw " << ebw << " " << bw << " " << *e.e << "\nafter bw " << abw << " " << aw << " " << *after.e << "\n";
if (!t.is_val()) if (!t.is_val())
IF_VERBOSE(0, verbose_stream() << "symbolic t : " << t << "\n"); IF_VERBOSE(0, verbose_stream() << "symbolic t : " << t << "\n");
#endif #endif
auto sc = cs.ult(t - vlo, vhi - vlo); auto sc = cs.ult(t - vlo, vhi - vlo);
CTRACE("bv", sc.is_always_false(), c.display(tout));
VERIFY(!sc.is_always_false()); VERIFY(!sc.is_always_false());
if (!sc.is_always_true()) if (!sc.is_always_true())
deps.push_back(c.propagate(sc, c.explain_weak_eval(sc))); deps.push_back(c.propagate(sc, c.explain_weak_eval(sc)));
@ -1011,6 +1018,8 @@ namespace polysat {
out << e->coeff << " * v" << v << " " << e->interval << " "; out << e->coeff << " * v" << v << " " << e->interval << " ";
else else
out << e->interval << " "; out << e->interval << " ";
for (auto const& d : e->deps)
out << d << " ";
if (e->side_cond.size() <= 5) if (e->side_cond.size() <= 5)
out << e->side_cond << " "; out << e->side_cond << " ";
else else