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

update slice/offset claim structures to allow for equal variable.

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-03-13 11:48:09 -07:00
parent 5d1602b6c7
commit 1e9381c2f6
5 changed files with 43 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -324,27 +324,27 @@ namespace polysat {
c.get_bitvector_suffixes(x, x_suffixes);
rational x_val, y_val;
for (auto const& xslice : x_suffixes) {
if (c.size(xslice.v) == mon.num_bits())
if (c.size(xslice.child) == mon.num_bits())
continue;
auto const& xmax_value = c.var(xslice.v).manager().max_value();
auto const& xmax_value = c.var(xslice.child).manager().max_value();
if (mon.val <= xmax_value)
continue;
if (!c.try_eval(c.var(xslice.v), x_val) || x_val != mon.arg_vals[0])
if (!c.try_eval(c.var(xslice.child), x_val) || x_val != mon.arg_vals[0])
continue;
if (!y_computed)
c.get_bitvector_suffixes(y, y_suffixes);
y_computed = true;
for (auto const& yslice : y_suffixes) {
if (c.size(yslice.v) != c.size(xslice.v))
if (c.size(yslice.child) != c.size(xslice.child))
continue;
if (!c.try_eval(c.var(yslice.v), y_val) || y_val != mon.arg_vals[1])
if (!c.try_eval(c.var(yslice.child), y_val) || y_val != mon.arg_vals[1])
continue;
bool added = c.add_axiom("0p * 0q >= 2^k => ovfl(p,q), where |p| = |q| = k",
{ dependency({x, xslice}), dependency({y, yslice}),
~C.ule(mon.args[0], xmax_value),
~C.ule(mon.args[1], xmax_value),
~C.ugt(mon.var, xmax_value),
C.umul_ovfl(c.var(xslice.v), c.var(yslice.v)) },
C.umul_ovfl(c.var(xslice.child), c.var(yslice.child)) },
true);
if (added)
return true;

32
src/sat/smt/polysat/types.h
View file

@ -36,34 +36,37 @@ namespace polysat {
class signed_constraint;
struct fixed_slice {
pvar child;
unsigned offset = 0;
unsigned length = 0;
rational value;
fixed_slice() = default;
fixed_slice(rational value, unsigned offset, unsigned length) : offset(offset), length(length), value(std::move(value)) {}
fixed_slice(pvar child, rational value, unsigned offset, unsigned length) :
child(child), offset(offset), length(length), value(std::move(value)) {}
unsigned end() const { return offset + length; }
};
struct fixed_claim : public fixed_slice {
pvar v;
pvar parent;
fixed_claim() = default;
fixed_claim(pvar v, rational value, unsigned offset, unsigned length) : fixed_slice(std::move(value), offset, length), v(v) {}
fixed_claim(pvar v, fixed_slice const& s) : fixed_slice(s), v(v) {}
fixed_claim(pvar v, rational value, unsigned offset, unsigned length) : fixed_slice(child, std::move(value), offset, length), parent(v) {}
fixed_claim(pvar v, fixed_slice const& s) : fixed_slice(s), parent(v) {}
};
struct offset_slice {
pvar v;
pvar child;
unsigned offset;
offset_slice() = default;
offset_slice(pvar v, unsigned offset) : v(v), offset(offset) {}
offset_slice(pvar v, unsigned offset) : child(v), offset(offset) {}
};
struct offset_claim : public offset_slice {
pvar w;
pvar parent;
offset_claim() = default;
offset_claim(pvar w, offset_slice const& s) : offset_slice(s), w(w) {}
offset_claim(pvar w, offset_slice const& s) : offset_slice(s), parent(w) {}
};
class dependency {
struct axiom_t {};
std::variant<axiom_t, sat::bool_var, theory_var_pair, offset_claim, fixed_claim> m_data;
@ -99,11 +102,11 @@ namespace polysat {
return out << "tv" << d.eq().first << " == tv" << d.eq().second;
else if (d.is_offset_claim()) {
auto offs = d.offset();
return out << "v" << offs.v << " == v" << offs.w << " offset " << offs.offset;
return out << "v" << offs.child << " == v" << offs.parent << " offset " << offs.offset;
}
else if (d.is_fixed_claim()) {
auto fixed = d.fixed();
return out << fixed.value << " == v" << fixed.v << " [" << fixed.length << "]@" << fixed.offset;
return out << fixed.value << " == v" << fixed.parent << " [" << fixed.length << "]@" << fixed.offset;
}
else {
UNREACHABLE();
@ -115,8 +118,8 @@ namespace polysat {
inline std::ostream& operator<<(std::ostream& out, offset_slice const& js) {
if (js.offset == 0)
return out << "v" << js.v;
return out << "v" << js.v << " at offset " << js.offset;
return out << "v" << js.child;
return out << "v" << js.child << " at offset " << js.offset;
}
using fixed_bits_vector = vector<fixed_slice>;
@ -125,8 +128,8 @@ namespace polysat {
unsigned level = 0; // level when sub-slice was fixed to value
dependency dep = null_dependency;
fixed_slice_extra() = default;
fixed_slice_extra(rational value, unsigned offset, unsigned length, unsigned level, dependency dep):
fixed_slice(std::move(value), offset, length), level(level), dep(std::move(dep)) {}
fixed_slice_extra(rational value, unsigned offset, unsigned length, unsigned level, dependency dep) :
fixed_slice(child, std::move(value), offset, length), level(level), dep(std::move(dep)) {}
};
using fixed_slice_extra_vector = vector<fixed_slice_extra>;
@ -137,6 +140,7 @@ namespace polysat {
};
using offset_slice_extra_vector = vector<offset_slice_extra>;
using dependency_vector = vector<dependency>;
using constraint_or_dependency = std::variant<signed_constraint, dependency>;
using constraint_id_or_constraint = std::variant<constraint_id, signed_constraint>;

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

@ -154,7 +154,7 @@ namespace polysat {
void viable::init_overlaps(pvar v) {
m_overlaps.reset();
c.get_bitvector_suffixes(v, m_overlaps);
std::sort(m_overlaps.begin(), m_overlaps.end(), [&](auto const& x, auto const& y) { return c.size(x.v) < c.size(y.v); });
std::sort(m_overlaps.begin(), m_overlaps.end(), [&](auto const& x, auto const& y) { return c.size(x.child) < c.size(y.child); });
}
@ -683,7 +683,7 @@ namespace polysat {
// e.g., prefers constant 'c' if we have pvars for both 'c' and 'concat(c,...)'
std::sort(subslices.begin(), subslices.end(), [&](auto const& a, auto const& b) -> bool {
return a.level > b.level
|| (a.level == b.level && c.size(a.v) < c.size(b.v));
|| (a.level == b.level && c.size(a.child) < c.size(b.child));
});
for (auto const& slice : subslices)
@ -693,7 +693,7 @@ namespace polysat {
}
dependency viable::propagate_from_containing_slice(entry* e, rational const& value, dependency_vector const& e_deps, fixed_slice_extra_vector const& fixed, offset_slice_extra const& slice) {
pvar w = slice.v;
pvar w = slice.child;
unsigned offset = slice.offset;
unsigned w_level = slice.level; // level where value of w was fixed
if (w == m_var)
@ -1496,9 +1496,9 @@ namespace polysat {
std::ostream& viable::display_state(std::ostream& out) const {
out << "v" << m_var << ":";
for (auto const& slice : m_overlaps) {
out << " v" << slice.v << ":" << c.size(slice.v) << "@" << slice.offset;
if (c.is_assigned(slice.v))
out << " value=" << c.get_assignment().value(slice.v);
out << " v" << slice.child << ":" << c.size(slice.child) << "@" << slice.offset;
if (c.is_assigned(slice.child))
out << " value=" << c.get_assignment().value(slice.child);
}
out << "\n";
return out;

12
src/sat/smt/polysat_egraph.cpp
View file

@ -115,7 +115,7 @@ namespace polysat {
unsigned length = bv.get_bv_size(r->get_expr());
rational value;
VERIFY(bv.is_numeral(r->get_expr(), value));
out.push_back({ fixed_slice(value, offset, length) });
out.push_back({ fixed_slice(null_var, value, offset, length) });
return false;
};
@ -186,6 +186,10 @@ namespace polysat {
m_bv_plugin->explain_slice(var2enode(v), offset, var2enode(w), consume_eq);
}
//
// explain that pv contains a fixed sub-slice at offset/length
// in addition, if slice.child is not null_var, then explain that
//
void solver::explain_fixed(pvar pv, fixed_slice const& slice, std::function<void(euf::enode*, euf::enode*)> const& consume_eq) {
euf::theory_var v = m_pddvar2var[pv];
expr_ref val(bv.mk_numeral(slice.value, slice.length), m);
@ -197,6 +201,12 @@ namespace polysat {
SASSERT(b);
m_bv_plugin->explain_slice(var2enode(v), slice.offset, b, consume_eq);
if (slice.child != null_var) {
auto c = var2enode(m_pddvar2var[slice.child]);
if (b != c)
m_bv_plugin->explain_slice(b, 0, c, consume_eq);
}
}
}

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

@ -148,11 +148,11 @@ namespace polysat {
}
else if (d.is_fixed_claim()) {
auto const& o = d.fixed();
explain_fixed(o.v, o, consume);
explain_fixed(o.parent, o, consume);
}
else if (d.is_offset_claim()) {
auto const& offs = d.offset();
explain_slice(offs.v, offs.w, offs.offset, consume);
explain_slice(offs.child, offs.parent, offs.offset, consume);
}
else {
auto const [v1, v2] = d.eq();