mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

use lazy explanation function for slices, use euf-bv-plugin to extract slices

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-12-23 11:10:18 -08:00
parent 5bbec43235
commit fbbad72c29
11 changed files with 243 additions and 197 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -389,11 +389,11 @@ namespace polysat {
}
}
void core::get_bitvector_suffixes(pvar v, justified_slices& out) {
void core::get_bitvector_suffixes(pvar v, offset_slices& out) {
s.get_bitvector_suffixes(v, out);
}
void core::get_fixed_bits(pvar v, justified_fixed_bits& fixed_bits) {
void core::get_fixed_bits(pvar v, fixed_bits_vector& fixed_bits) {
s.get_fixed_bits(v, fixed_bits);
}

4
src/sat/smt/polysat/core.h
View file

@ -83,8 +83,8 @@ namespace polysat {
void propagate_unsat_core();
void propagate(constraint_id id, signed_constraint& sc, lbool value, dependency const& d);
void get_bitvector_suffixes(pvar v, justified_slices& out);
void get_fixed_bits(pvar v, justified_fixed_bits& fixed_bits);
void get_bitvector_suffixes(pvar v, offset_slices& out);
void get_fixed_bits(pvar v, fixed_bits_vector& fixed_bits);
bool inconsistent() const;
void add_watch(unsigned idx, unsigned var);

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

@ -17,8 +17,6 @@ Author:
namespace polysat {
using fixed_bits_vector = vector<fixed_bits>;
bool get_eq_fixed_lsb(pdd const& p, fixed_bits& out);
bool get_eq_fixed_bits(pdd const& p, fixed_bits& out);

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

@ -29,7 +29,7 @@ namespace polysat {
using pvar_vector = unsigned_vector;
using theory_var_pair = std::pair<theory_var, theory_var>;
using theory_var_pairs = svector<theory_var_pair>;
using offset_claim = std::tuple<pvar, pvar, unsigned>;
inline const pvar null_var = UINT_MAX;
class signed_constraint;
@ -37,22 +37,22 @@ namespace polysat {
class dependency {
struct axiom_t {};
std::variant<axiom_t, sat::literal, theory_var_pair, theory_var_pairs> m_data;
std::variant<axiom_t, sat::literal, theory_var_pair, offset_claim> m_data;
unsigned m_level;
dependency(): m_data(axiom_t()), m_level(0) {}
public:
dependency(sat::literal lit, unsigned level) : m_data(lit), m_level(level) {}
dependency(theory_var v1, theory_var v2, unsigned level) : m_data(std::make_pair(v1, v2)), m_level(level) {}
dependency(theory_var_pairs& j, unsigned level) : m_data(j), m_level(level) {}
dependency(offset_claim const& c, unsigned level) : m_data(c), m_level(level) {}
static dependency axiom() { return dependency(); }
bool is_null() const { return is_literal() && *std::get_if<sat::literal>(&m_data) == sat::null_literal; }
bool is_axiom() const { return std::holds_alternative<axiom_t>(m_data); }
bool is_eqs() const { return std::holds_alternative<theory_var_pairs>(m_data); }
bool is_eq() const { return std::holds_alternative<theory_var_pair>(m_data); }
bool is_literal() const { return std::holds_alternative<sat::literal>(m_data); }
bool is_offset_claim() const { return std::holds_alternative<offset_claim>(m_data); }
sat::literal literal() const { SASSERT(is_literal()); return *std::get_if<sat::literal>(&m_data); }
theory_var_pair eq() const { SASSERT(!is_literal()); return *std::get_if<theory_var_pair>(&m_data); }
theory_var_pairs const& eqs() const { SASSERT(!is_literal()); return *std::get_if<theory_var_pairs>(&m_data); }
offset_claim offset() const { return *std::get_if<offset_claim>(&m_data); }
unsigned level() const { return m_level; }
void set_level(unsigned level) { m_level = level; }
dependency operator~() const { SASSERT(is_literal()); return dependency(~literal(), level()); }
@ -70,10 +70,8 @@ namespace polysat {
else if (d.is_eq())
return out << "v" << d.eq().first << " == v" << d.eq().second << "@" << d.level();
else {
char const* sep = "";
for (auto [v1, v2] : d.eqs())
out << sep << "v" << d.eq().first << " == v" << d.eq().second, sep = ", ";
return out << " @" << d.level();
auto [v1, v2, offset] = d.offset();
return out << "v" << v1 << " == v" << v2 << " offset " << offset << "@" << d.level();
}
}
@ -90,17 +88,16 @@ namespace polysat {
fixed_bits(unsigned hi, unsigned lo, rational value) : hi(hi), lo(lo), value(value) {}
};
struct justified_slice {
struct offset_slice {
pvar v;
unsigned offset;
dependency dep;
};
inline std::ostream& operator<<(std::ostream& out, justified_slice const& js) {
return out << "v" << js.v << "[" << js.offset << "[ @" << js.dep;
inline std::ostream& operator<<(std::ostream& out, offset_slice const& js) {
return out << "v" << js.v << "[" << js.offset << "[ @";
}
using justified_fixed_bits = vector<std::pair<fixed_bits, dependency>>;
using fixed_bits_vector = svector<fixed_bits>;
using dependency_vector = vector<dependency>;
using constraint_or_dependency = std::variant<signed_constraint, dependency>;
@ -110,7 +107,7 @@ namespace polysat {
using core_vector = std::initializer_list<constraint_or_dependency>;
using constraint_id_vector = svector<constraint_id>;
using constraint_id_list = std::initializer_list<constraint_id>;
using justified_slices = vector<justified_slice>;
using offset_slices = vector<offset_slice>;
using eq_justification = svector<std::pair<theory_var, theory_var>>;
//
@ -127,10 +124,10 @@ namespace polysat {
virtual void propagate(dependency const& d, bool sign, constraint_id_vector const& deps) = 0;
virtual trail_stack& trail() = 0;
virtual bool inconsistent() const = 0;
virtual void get_bitvector_suffixes(pvar v, justified_slices& out) = 0;
virtual void get_bitvector_sub_slices(pvar v, justified_slices& out) = 0;
virtual void get_bitvector_super_slices(pvar v, justified_slices& out) = 0;
virtual void get_fixed_bits(pvar v, justified_fixed_bits& fixed_bits) = 0;
virtual void get_bitvector_suffixes(pvar v, offset_slices& out) = 0;
virtual void get_bitvector_sub_slices(pvar v, offset_slices& out) = 0;
virtual void get_bitvector_super_slices(pvar v, offset_slices& out) = 0;
virtual void get_fixed_bits(pvar v, fixed_bits_vector& fixed_bits) = 0;
};
}

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

@ -103,7 +103,7 @@ namespace polysat {
return l_false; // conflict already added
#endif
justified_slices overlaps;
offset_slices overlaps;
c.get_bitvector_suffixes(v, overlaps);
std::sort(overlaps.begin(), overlaps.end(), [&](auto const& x, auto const& y) { return c.size(x.v) > c.size(y.v); });
@ -111,7 +111,7 @@ namespace polysat {
// max size should always be present, regardless of whether we have intervals there (to make sure all fixed bits are considered)
widths_set.insert(c.size(v));
for (auto const& [v, offset, j] : overlaps)
for (auto const& [v, offset] : overlaps)
for (layer const& l : m_units[v].get_layers())
widths_set.insert(l.bit_width);
@ -147,7 +147,7 @@ namespace polysat {
lbool viable::find_on_layers(
pvar const v,
unsigned_vector const& widths,
justified_slices const& overlaps,
offset_slices const& overlaps,
fixed_bits_info const& fbi,
rational const& to_cover_lo,
rational const& to_cover_hi,
@ -201,7 +201,7 @@ namespace polysat {
pvar const v,
unsigned const w_idx,
unsigned_vector const& widths,
justified_slices const& overlaps,
offset_slices const& overlaps,
fixed_bits_info const& fbi,
rational const& to_cover_lo,
rational const& to_cover_hi,
@ -240,7 +240,7 @@ namespace polysat {
// find relevant interval lists
svector<entry_cursor> ecs;
for (auto const& [x, offset, j] : overlaps) {
for (auto const& [x, offset] : overlaps) {
if (c.size(x) < w) // note that overlaps are sorted by variable size descending
break;
if (entry* e = m_units[x].get_entries(w)) {
@ -614,17 +614,17 @@ namespace polysat {
out_fbi.reset(v_sz);
auto& [fixed, just_src, just_side_cond, just_slice] = out_fbi;
justified_fixed_bits fbs;
fixed_bits_vector fbs;
c.get_fixed_bits(v, fbs);
for (auto const& [fb, d] : fbs) {
for (auto const& fb : fbs) {
LOG("slicing fixed bits: v" << v << "[" << fb.hi << ":" << fb.lo << "] = " << fb.value);
for (unsigned i = fb.lo; i <= fb.hi; ++i) {
SASSERT(out_fbi.just_src[i].empty()); // since we don't get overlapping ranges from collect_fixed.
SASSERT(out_fbi.just_side_cond[i].empty());
SASSERT(out_fbi.just_slicing[i].empty());
out_fbi.fixed[i] = to_lbool(fb.value.get_bit(i - fb.lo));
out_fbi.just_slicing[i].push_back({ fb, d });
out_fbi.just_slicing[i].push_back(fb);
}
}

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

@ -107,7 +107,7 @@ namespace polysat {
svector<lbool> fixed;
vector<vector<signed_constraint>> just_src;
vector<vector<signed_constraint>> just_side_cond;
vector<justified_fixed_bits> just_slicing;
vector<fixed_bits_vector> just_slicing;
bool is_empty() const {
SASSERT_EQ(fixed.empty(), just_src.empty());
@ -186,7 +186,7 @@ namespace polysat {
lbool find_on_layers(
pvar v,
unsigned_vector const& widths,
justified_slices const& overlaps,
offset_slices const& overlaps,
fixed_bits_info const& fbi,
rational const& to_cover_lo,
rational const& to_cover_hi,
@ -196,7 +196,7 @@ namespace polysat {
pvar v,
unsigned w_idx,
unsigned_vector const& widths,
justified_slices const& overlaps,
offset_slices const& overlaps,
fixed_bits_info const& fbi,
rational const& to_cover_lo,
rational const& to_cover_hi,

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

@ -20,110 +20,15 @@ Author:
#include "sat/smt/polysat_solver.h"
#include "sat/smt/euf_solver.h"
namespace polysat {
struct solver::scoped_eq_justification {
eq_justification& j;
euf::enode* a, * b;
scoped_eq_justification(solver& s, eq_justification& j, euf::enode* a, euf::enode* b) :
j(j), a(a), b(b) {
if (a != b)
j.push_back({ s.get_th_var(a), s.get_th_var(b) });
}
~scoped_eq_justification() {
if (a != b)
j.pop_back();
}
};
void solver::get_sub_slices(pvar pv, slice_infos& slices) {
theory_var v = m_pddvar2var[pv];
unsigned lo, hi;
expr* e = nullptr;
euf::enode* n = var2enode(v);
slices.push_back({ n, 0, {} });
for (unsigned i = 0; i < slices.size(); ++i) {
auto [n, offset, just] = slices[i];
if (n->get_root()->is_marked1())
continue;
n->get_root()->mark1();
for (auto sib : euf::enode_class(n)) {
if (bv.is_concat(sib->get_expr())) {
unsigned delta = 0;
scoped_eq_justification sp(*this, just, n, sib);
for (unsigned j = sib->num_args(); j-- > 0; ) {
auto arg = sib->get_arg(j);
slices.push_back({ arg, offset + delta, just });
delta += bv.get_bv_size(arg->get_expr());
}
}
}
for (auto p : euf::enode_parents(n->get_root())) {
if (p->get_root()->is_marked1())
continue;
if (bv.is_extract(p->get_expr(), lo, hi, e)) {
auto child = expr2enode(e);
SASSERT(n->get_root() == child->get_root());
scoped_eq_justification sp(*this, just, child, n);
slices.push_back({ p, offset + lo, just });
}
}
}
for (auto const& [n,offset,d] : slices)
n->get_root()->unmark1();
}
void solver::get_super_slices(pvar pv, slice_infos& slices) {
theory_var v = m_pddvar2var[pv];
unsigned lo, hi;
expr* e = nullptr;
euf::enode* n = var2enode(v);
slices.push_back({ n, 0, {} });
for (unsigned i = 0; i < slices.size(); ++i) {
auto [n, offset, just] = slices[i];
if (n->get_root()->is_marked1())
continue;
n->get_root()->mark1();
for (auto sib : euf::enode_class(n)) {
if (bv.is_extract(sib->get_expr(), lo, hi, e)) {
auto child = expr2enode(e);
SASSERT(n->get_root() == child->get_root());
scoped_eq_justification sp(*this, just, child, n);
slices.push_back({ sib, offset + lo, just });
}
}
for (auto p : euf::enode_parents(n->get_root())) {
if (p->get_root()->is_marked1())
continue;
if (bv.is_concat(p->get_expr())) {
unsigned delta = 0;
for (unsigned j = p->num_args(); j-- > 0; ) {
auto arg = p->get_arg(j);
if (arg->get_root() == n->get_root()) {
scoped_eq_justification sp(*this, just, arg, n);
slices.push_back({ p, offset + delta, just });
}
delta += bv.get_bv_size(arg->get_expr());
}
}
}
}
for (auto const& [n, offset, d] : slices)
n->get_root()->unmark1();
}
// walk the egraph starting with pvar for suffix overlaps.
void solver::get_bitvector_suffixes(pvar pv, justified_slices& out) {
slice_infos slices;
get_sub_slices(pv, slices);
void solver::get_bitvector_suffixes(pvar pv, offset_slices& out) {
uint_set seen;
for (auto& [n, offset, just] : slices) {
std::function<bool(euf::enode*, unsigned)> consume_slice = [&](euf::enode* n, unsigned offset) {
if (offset != 0)
continue;
return false;
for (auto sib : euf::enode_class(n)) {
auto w = sib->get_th_var(get_id());
if (w == euf::null_theory_var)
@ -134,19 +39,18 @@ namespace polysat {
auto const& p = m_var2pdd[w];
if (!p.is_var())
continue;
scoped_eq_justification sp(*this, just, sib, n);
out.push_back({ p.var(), offset, dependency(just, s().scope_lvl()) }); // approximate to current scope
out.push_back({ p.var(), offset });
}
}
return true;
};
theory_var v = m_pddvar2var[pv];
m_bv_plugin->sub_slices(var2enode(v), consume_slice);
}
// walk the egraph starting with pvar for any overlaps.
void solver::get_bitvector_sub_slices(pvar pv, justified_slices& out) {
slice_infos slices;
get_sub_slices(pv, slices);
void solver::get_bitvector_sub_slices(pvar pv, offset_slices& out) {
uint_set seen;
for (auto& [n, offset, just] : slices) {
std::function<bool(euf::enode*, unsigned)> consume_slice = [&](euf::enode* n, unsigned offset) {
for (auto sib : euf::enode_class(n)) {
auto w = sib->get_th_var(get_id());
if (w == euf::null_theory_var)
@ -157,19 +61,18 @@ namespace polysat {
auto const& p = m_var2pdd[w];
if (!p.is_var())
continue;
scoped_eq_justification sp(*this, just, sib, n);
out.push_back({ p.var(), offset, dependency(just, s().scope_lvl()) }); // approximate to current scope
out.push_back({ p.var(), offset });
}
}
return true;
};
theory_var v = m_pddvar2var[pv];
m_bv_plugin->sub_slices(var2enode(v), consume_slice);
}
// walk the egraph for bit-vectors that contain pv.
void solver::get_bitvector_super_slices(pvar pv, justified_slices& out) {
slice_infos slices;
get_super_slices(pv, slices);
void solver::get_bitvector_super_slices(pvar pv, offset_slices& out) {
uint_set seen;
for (auto& [n, offset, just] : slices) {
std::function<bool(euf::enode*, unsigned)> consume_slice = [&](euf::enode* n, unsigned offset) {
for (auto sib : euf::enode_class(n)) {
auto w = sib->get_th_var(get_id());
if (w == euf::null_theory_var)
@ -180,35 +83,49 @@ namespace polysat {
auto const& p = m_var2pdd[w];
if (!p.is_var())
continue;
scoped_eq_justification sp(*this, just, sib, n);
out.push_back({ p.var(), offset, dependency(just, s().scope_lvl()) }); // approximate to current scope
out.push_back({ p.var(), offset });
}
}
return true;
};
theory_var v = m_pddvar2var[pv];
m_bv_plugin->super_slices(var2enode(v), consume_slice);
}
// walk the e-graph to retrieve fixed overlaps
void solver::get_fixed_bits(pvar pv, justified_fixed_bits& out) {
slice_infos slices;
get_sub_slices(pv, slices);
void solver::get_fixed_bits(pvar pv, fixed_bits_vector& out) {
for (auto& [n, offset, just] : slices) {
if (offset != 0)
continue;
if (!n->get_root()->interpreted())
continue;
std::function<bool(euf::enode*, unsigned)> consume_slice = [&](euf::enode* n, unsigned offset) {
if (!n->interpreted())
return true;
auto w = n->get_root()->get_th_var(get_id());
if (w == euf::null_theory_var)
continue;
return true;
auto const& p = m_var2pdd[w];
if (!p.is_var())
continue;
scoped_eq_justification sp(*this, just, n, n->get_root());
return true;
unsigned lo = offset, hi = bv.get_bv_size(n->get_expr());
rational value;
VERIFY(bv.is_numeral(n->get_expr(), value));
out.push_back({ fixed_bits(lo, hi, value), dependency(just, s().scope_lvl()) }); // approximate level
}
out.push_back({ fixed_bits(lo, hi, value) });
return false;
};
theory_var v = m_pddvar2var[pv];
m_bv_plugin->sub_slices(var2enode(v), consume_slice);
}
void solver::explain_slice(pvar pv, pvar pw, unsigned offset, std::function<void(euf::enode*, euf::enode*)>& consume_eq) {
euf::theory_var v = m_pddvar2var[pv];
euf::theory_var w = m_pddvar2var[pw];
m_bv_plugin->explain_slice(var2enode(v), offset, var2enode(w), consume_eq);
}
void solver::explain_fixed(pvar pv, unsigned lo, unsigned hi, rational const& value, std::function<void(euf::enode*, euf::enode*)>& consume_eq) {
euf::theory_var v = m_pddvar2var[pv];
expr_ref val(bv.mk_numeral(value, hi - lo + 1), m);
euf::enode* b = ctx.get_egraph().find(val);
SASSERT(b);
m_bv_plugin->explain_slice(var2enode(v), lo, b, consume_eq);
}
}

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

@ -24,7 +24,7 @@ The result of polysat::core::check is one of:
--*/
#include "ast/euf/euf_bv_plugin.h"
#include "sat/smt/polysat_solver.h"
#include "sat/smt/euf_solver.h"
#include "sat/smt/polysat/ule_constraint.h"
@ -144,26 +144,6 @@ namespace polysat {
return { core, eqs };
}
// If an MCSat lemma is added, then backjump based on the lemma level and
// add the lemma to the solver with potentially fresh literals.
// return l_false to signal sat::solver that backjumping has been taken care of internally.
lbool solver::resolve_conflict() {
if (!m_has_lemma)
return l_undef;
SASSERT(m_lemma_level > 0);
unsigned num_scopes = s().scope_lvl() - m_lemma_level - 1;
NOT_IMPLEMENTED_YET();
// s().pop_reinit(num_scopes);
sat::literal_vector lits;
for (auto* e : m_lemma)
lits.push_back(~ctx.mk_literal(e));
s().add_clause(lits.size(), lits.data(), sat::status::th(true, get_id(), nullptr));
return l_false;
}
// Create an equality literal that represents the value assignment
// Prefer case split to true.
// The equality gets added in a callback using asserted().
@ -269,9 +249,12 @@ namespace polysat {
auto [v1, v2] = d.eq();
lits.push_back(~eq_internalize(var2enode(v1), var2enode(v2)));
}
else if (d.is_eqs()) {
for (auto [v1, v2] : d.eqs())
lits.push_back(~eq_internalize(var2enode(v1), var2enode(v2)));
else if (d.is_offset_claim()) {
auto [v, w, offset] = d.offset();
std::function<void(euf::enode*, euf::enode*)> consume = [&](auto* a, auto* b) {
lits.push_back(~eq_internalize(a, b));
};
explain_slice(v, w, offset, consume);
}
else {
SASSERT(d.is_axiom());

14
src/sat/smt/polysat_solver.h
View file

@ -20,6 +20,7 @@ Author:
#include "math/dd/dd_pdd.h"
#include "sat/smt/polysat/core.h"
#include "sat/smt/intblast_solver.h"
#include "ast/euf/euf_bv_plugin.h"
namespace euf {
class solver;
@ -65,6 +66,7 @@ namespace polysat {
bool_vector m_var2pdd_valid; // valid flag
unsigned_vector m_pddvar2var; // pvar -> theory_var
ptr_vector<atom> m_bool_var2atom; // bool_var -> atom
euf::bv_plugin* m_bv_plugin = nullptr;
svector<std::pair<euf::theory_var, euf::theory_var>> m_var_eqs;
unsigned m_var_eqs_head = 0;
@ -77,6 +79,8 @@ namespace polysat {
void get_sub_slices(pvar v, slice_infos& slices);
void get_super_slices(pvar v, slice_infos& slices);
void explain_slice(pvar v, pvar w, unsigned offset, std::function<void(euf::enode*, euf::enode*)>& consume);
void explain_fixed(pvar v, unsigned lo, unsigned hi, rational const& value, std::function<void(euf::enode*, euf::enode*)>& consume_eq);
// internalize
bool visit(expr* e) override;
@ -170,10 +174,11 @@ namespace polysat {
void propagate(dependency const& d, bool sign, constraint_id_vector const& deps) override;
trail_stack& trail() override;
bool inconsistent() const override;
void get_bitvector_sub_slices(pvar v, justified_slices& out) override;
void get_bitvector_super_slices(pvar v, justified_slices& out) override;
void get_bitvector_suffixes(pvar v, justified_slices& out) override;
void get_fixed_bits(pvar v, justified_fixed_bits& fixed_bits) override;
void get_bitvector_sub_slices(pvar v, offset_slices& out) override;
void get_bitvector_super_slices(pvar v, offset_slices& out) override;
void get_bitvector_suffixes(pvar v, offset_slices& out) override;
void get_fixed_bits(pvar v, fixed_bits_vector& fixed_bits) override;
dependency explain_slice(pvar v, pvar w, unsigned offset);
bool add_axiom(char const* name, core_vector const& clause, bool redundant) {
return add_axiom(name, clause.begin(), clause.end(), redundant);
@ -209,7 +214,6 @@ namespace polysat {
void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) override {}
void gc() override {}
void pop_reinit() override {}
lbool resolve_conflict() override;
bool validate() override { return true; }
void init_use_list(sat::ext_use_list& ul) override {}
bool is_blocked(literal l, sat::ext_constraint_idx) override { return false; }