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

bugbash

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-01-04 10:54:02 -08:00
parent f71219a9d0
commit 7b0c04a3e8
8 changed files with 67 additions and 48 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/sat/smt/polysat/core.cpp
View file

@ -216,17 +216,6 @@ namespace polysat {
// break;
}
switch (m_monomials.refine()) {
case l_true:
break;
case l_false:
TRACE("bv", tout << "refine\n");
return sat::check_result::CR_CONTINUE;
case l_undef:
r = l_undef;
break;
}
saturation saturate(*this);
switch (saturate()) {
case l_true:
@ -239,6 +228,17 @@ namespace polysat {
break;
}
switch (m_monomials.refine()) {
case l_true:
break;
case l_false:
TRACE("bv", tout << "refine\n");
return sat::check_result::CR_CONTINUE;
case l_undef:
r = l_undef;
break;
}
switch (m_monomials.bit_blast()) {
case l_true:
break;

18
src/sat/smt/polysat/monomials.cpp
View file

@ -59,19 +59,21 @@ namespace polysat {
if (m_to_refine.empty())
return l_true;
shuffle(m_to_refine.size(), m_to_refine.data(), c.rand());
if (any_of(m_to_refine, [&](auto i) { return prefix_overflow(m_monomials[i]); }))
return l_false;
if (any_of(m_to_refine, [&](auto i) { return mul0(m_monomials[i]); }))
return l_false;
if (any_of(m_to_refine, [&](auto i) { return mul1(m_monomials[i]); }))
return l_false;
if (any_of(m_to_refine, [&](auto i) { return non_overflow_unit(m_monomials[i]); }))
return l_false;
if (any_of(m_to_refine, [&](auto i) { return non_overflow_zero(m_monomials[i]); }))
return l_false;
if (any_of(m_to_refine, [&](auto i) { return parity0(m_monomials[i]); }))
if (false && any_of(m_to_refine, [&](auto i) { return parity0(m_monomials[i]); }))
return l_false;
if (any_of(m_to_refine, [&](auto i) { return parity(m_monomials[i]); }))
return l_false;
if (any_of(m_to_refine, [&](auto i) { return prefix_overflow(m_monomials[i]); }))
if (false && any_of(m_to_refine, [&](auto i) { return parity(m_monomials[i]); }))
return l_false;
if (any_of(m_to_refine, [&](auto i) { return non_overflow_monotone(m_monomials[i]); }))
return l_false;
@ -153,16 +155,16 @@ namespace polysat {
}
constraint_or_dependency_vector cs;
pdd offset = c.value(rational(1), mon.num_bits());
if (free_index == UINT_MAX)
free_index = c.rand()() % mon.size();
for (unsigned j = mon.size(); j-- > 0; ) {
if (j != free_index) {
cs.push_back(~C.eq(mon.args[j], mon.arg_vals[j]));
offset *= mon.arg_vals[j];
}
}
if (free_index == UINT_MAX)
cs.push_back(C.eq(mon.var, offset));
else
cs.push_back(C.eq(mon.var, offset * mon.args[free_index]));
cs.push_back(C.eq(mon.var, offset * mon.args[free_index]));
return c.add_axiom("p = k => p * q = k * q", cs, true);
}

8
src/sat/smt/polysat/saturation.cpp
View file

@ -58,13 +58,13 @@ namespace polysat {
void saturation::resolve(pvar v, inequality const& i) {
if (c.size(v) != i.lhs().power_of_2())
return;
if (!c.inconsistent())
if (false && !c.inconsistent())
try_ugt_x(v, i);
if (!c.inconsistent())
if (false && !c.inconsistent())
try_ugt_y(v, i);
if (!c.inconsistent())
if (false && !c.inconsistent())
try_ugt_z(v, i);
if (!c.inconsistent())
if (false && !c.inconsistent())
try_eq_resolve(v, i);
}

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

@ -358,7 +358,7 @@ namespace polysat {
auto p = c.subst(lhs());
auto q = c.subst(rhs());
auto& C = c.cs();
if (sign && !lhs().is_val() && !rhs().is_val()) {
if (false && sign && !lhs().is_val() && !rhs().is_val()) {
c.add_axiom("lhs > rhs ==> -1 > rhs", { d, C.ult(rhs(), -1) }, false);
c.add_axiom("lhs > rhs ==> lhs > 0", { d, C.ult(0, lhs()) }, false);
}

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

@ -89,7 +89,7 @@ namespace polysat {
m_num_bits = c.size(v);
m_fixed_bits.reset(v);
init_overlaps(v);
m_start = lo;
m_conflict = false;
// verbose_stream() << "find viable v" << v << " starting with " << lo << "\n";
@ -97,18 +97,15 @@ namespace polysat {
auto n = find_overlap(lo);
if (m_conflict)
return find_t::empty;
if (!n) {
if (refine_disequal_lin(v, lo) &&
refine_equal_lin(v, lo))
return find_t::multiple;
++rounds;
continue;
}
update_value_to_high(lo, n);
m_explain.push_back({ n, lo });
if (is_conflict())
return find_t::empty;
}
}
return find_t::resource_out;
@ -137,14 +134,22 @@ namespace polysat {
VERIFY(m_fixed_bits.next(val));
}
entry* last = nullptr;
for (auto const& [w, offset] : m_overlaps) {
for (auto& layer : m_units[w].get_layers()) {
entry* e = find_overlap(w, layer, val);
if (e)
return e;
if (!e)
continue;
last = e;
update_value_to_high(val, e);
m_explain.push_back({ e, val });
if (is_conflict()) {
m_conflict = true;
return nullptr;
}
}
}
return nullptr;
return last;
}
viable::entry* viable::find_overlap(pvar w, layer& l, rational& val) {
@ -521,34 +526,43 @@ namespace polysat {
*
* - 2^kx \not\in [lo, hi[,
* - 2^k'y \not\in [lo', hi'[
* - a value v such that
* - 2^kv \not\in [lo, hi[
* - 2^k'v \in [lo', hi'[
* - hi \in ] (v - 1) * 2^{bw - ebw} ; v * 2^{bw - ebw} ]
*
* Where:
* - w is the width of x, w' the width of y
* - bw is the bit-width of x, bw' the bit-width of y
* - k = w - bwx, k' = w' - bw'
* - bw is the width of x, aw the width of y
* - ebw is the bit-width of x, abw the bit-width of y
* - k = bw - ebw, k' = aw - abw
*
* We want to encode the constraint that (2^k' hi)[w'] in [lo', hi'[
*
* Note that x in [lo, hi[ <=> x - lo < hi - lo
* If k' = 0, w' = w, there is nothing to do.
* If bw = aw, ebw = abw there is nothing else to do.
* - hi \in [lo', hi'[
*
* TODO - describe.
* If bw != aw or aw < bw:
* - hi \in ] (v - 1) * 2^{bw - ebw} ; v * 2^{bw - ebw} ]
* - hi := v mod aw
*
* - 2^k'hi \in [lo', hi'[
*
*/
void viable::explain_overlap(explanation const& e, explanation const& after, dependency_vector& deps) {
auto bw = c.size(e.e->var);
auto ebw = e.e->bit_width;
auto bw_after = c.size(after.e->var);
auto aw = c.size(after.e->var);
auto abw = after.e->bit_width;
auto t = e.e->interval.hi();
auto lo = after.e->interval.lo();
auto hi = after.e->interval.hi();
SASSERT(abw <= bw_after);
SASSERT(abw <= aw);
SASSERT(ebw <= bw);
if (ebw < bw || bw_after != bw) {
if (ebw < bw || aw != bw) {
auto const& p2b = rational::power_of_two(bw);
auto const& p2eb = rational::power_of_two(bw - ebw);
auto vhi = c.value(mod(e.value * p2eb + 1, p2b), bw);
@ -563,11 +577,11 @@ namespace polysat {
if (!sc.is_always_true())
deps.push_back(c.propagate(sc, c.explain_eval(sc)));
t.reset(lo.manager());
t = c.value(mod(e.value, rational::power_of_two(bw_after)), bw_after);
t = c.value(mod(e.value, rational::power_of_two(aw)), aw);
}
if (abw < bw_after)
t *= rational::power_of_two(bw_after - abw);
if (abw < aw)
t *= rational::power_of_two(aw - abw);
auto sc = cs.ult(t - lo, hi - lo);
SASSERT(!sc.is_always_false());

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

@ -135,7 +135,7 @@ namespace polysat {
pvar m_var = null_var;
rational m_start;
bool m_conflict = false;
unsigned m_num_bits = 0;
fixed_bits m_fixed_bits;
offset_slices m_overlaps;

1
src/sat/smt/polysat_internalize.cpp
View file

@ -658,6 +658,7 @@ namespace polysat {
auto eq0 = eq_internalize(e, bv.mk_numeral(0, sz_e));
auto gelo = mk_literal(bv.mk_ule(bv.mk_numeral(rational::power_of_two(lo), sz_x), x));
auto name = "extract";
verbose_stream() << "extract axiom " << mk_pp(e, m) << " " << eq0 << " " << s().value(eq0) << " " << gelo << " " << s().value(gelo) << "\n";
add_axiom(name, { eq0, gelo });
if (hi + 1 == sz_e)
add_axiom(name, { ~eq0, ~gelo });

4
src/sat/smt/polysat_solver.cpp
View file

@ -346,6 +346,7 @@ namespace polysat {
return false;
}
TRACE("bv", tout << name << ": "; for (auto lit : lits) tout << ctx.literal2expr(lit) << " "; tout << "\n");
IF_VERBOSE(1, verbose_stream() << name << ": "; for (auto lit : lits) verbose_stream() << ctx.literal2expr(lit) << " "; verbose_stream() << "\n");
validate_axiom(lits);
s().add_clause(lits.size(), lits.data(), sat::status::th(is_redundant, get_id(), hint));
return true;
@ -366,7 +367,8 @@ namespace polysat {
for (auto lit : clause)
lits.push_back(lit);
}
validate_axiom(lits);
validate_axiom(lits);
IF_VERBOSE(1, verbose_stream() << name << ": "; for (auto lit : lits) verbose_stream() << ctx.literal2expr(lit) << " "; verbose_stream() << "\n");
s().add_clause(lits.size(), lits.data(), sat::status::th(is_redundant, get_id(), hint));
}