mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-31 16:33:18 +00:00
Code Activity

refactor slicing dep

Browse source
This commit is contained in:
Jakob Rath 2023-07-27 15:34:13 +02:00
parent eb20b8971b
commit 9335b6eed6
3 changed files with 26 additions and 35 deletions
Download patch file Download diff file Expand all files Collapse all files

52
src/math/polysat/slicing.cpp
View file

@ -66,27 +66,31 @@ namespace {
namespace polysat { namespace polysat {
unsigned slicing::dep_t::to_uint() const { void* slicing::dep_t::encode() const {
return std::visit([](auto arg) -> unsigned { void* p = std::visit([](auto arg) -> void* {
using T = std::decay_t<decltype(arg)>; using T = std::decay_t<decltype(arg)>;
if constexpr (std::is_same_v<T, std::monostate>) if constexpr (std::is_same_v<T, std::monostate>)
return UINT_MAX; return nullptr;
else if constexpr (std::is_same_v<T, sat::literal>) else if constexpr (std::is_same_v<T, sat::literal>)
return (arg.to_uint() << 1); return box<void>(arg.to_uint(), 1);
else if constexpr (std::is_same_v<T, unsigned>) else if constexpr (std::is_same_v<T, unsigned>)
return (arg << 1) + 1; return box<void>(arg, 2);
else else
static_assert(always_false_v<T>, "non-exhaustive visitor!"); static_assert(always_false_v<T>, "non-exhaustive visitor!");
}, m_data); }, m_data);
SASSERT(*this == decode(p));
return p;
} }
slicing::dep_t slicing::dep_t::from_uint(unsigned x) { slicing::dep_t slicing::dep_t::decode(void* p) {
if (x == UINT_MAX) if (!p)
return dep_t(); return {};
else if ((x & 1) == 0) unsigned tag = get_tag(p);
return dep_t(sat::to_literal(x >> 1)); SASSERT(tag == 1 || tag == 2);
if (tag == 1)
return dep_t(sat::to_literal(unbox<unsigned>(p)));
else else
return dep_t(static_cast<unsigned>(x >> 1)); return dep_t(unbox<unsigned>(p));
} }
std::ostream& slicing::display(std::ostream& out, dep_t d) { std::ostream& slicing::display(std::ostream& out, dep_t d) {
@ -99,16 +103,6 @@ namespace polysat {
return out; return out;
} }
void* slicing::encode_dep(dep_t d) {
void* p = box<void>(d.to_uint());
SASSERT(d == decode_dep(p));
return p;
}
slicing::dep_t slicing::decode_dep(void* p) {
return dep_t::from_uint(unbox<unsigned>(p));
}
slicing::dep_t slicing::mk_var_dep(pvar v, enode* s) { slicing::dep_t slicing::mk_var_dep(pvar v, enode* s) {
SASSERT_EQ(m_dep_var.size(), m_dep_slice.size()); SASSERT_EQ(m_dep_var.size(), m_dep_slice.size());
unsigned const idx = m_dep_var.size(); unsigned const idx = m_dep_var.size();
@ -123,7 +117,7 @@ namespace polysat {
{ {
reg_decl_plugins(m_ast); reg_decl_plugins(m_ast);
m_bv = alloc(bv_util, m_ast); m_bv = alloc(bv_util, m_ast);
m_egraph.set_display_justification([&](std::ostream& out, void* d) { display(out, decode_dep(d)); }); m_egraph.set_display_justification([&](std::ostream& out, void* dp) { display(out, dep_t::decode(dp)); });
m_egraph.set_on_merge([&](enode* root, enode* other) { egraph_on_merge(root, other); }); m_egraph.set_on_merge([&](enode* root, enode* other) { egraph_on_merge(root, other); });
m_egraph.set_on_propagate([&](enode* lit, enode* ante) { egraph_on_propagate(lit, ante); }); m_egraph.set_on_propagate([&](enode* lit, enode* ante) { egraph_on_propagate(lit, ante); });
} }
@ -271,7 +265,7 @@ namespace polysat {
return eqn; return eqn;
auto args = {x, y}; auto args = {x, y};
eqn = m_egraph.mk(eq, 0, args.size(), args.begin()); eqn = m_egraph.mk(eq, 0, args.size(), args.begin());
auto j = euf::justification::external(encode_dep(lit)); auto j = euf::justification::external(dep_t(lit).encode());
m_egraph.set_value(eqn, l_false, j); m_egraph.set_value(eqn, l_false, j);
SASSERT(eqn->is_equality()); SASSERT(eqn->is_equality());
SASSERT_EQ(eqn->value(), l_false); SASSERT_EQ(eqn->value(), l_false);
@ -317,7 +311,7 @@ namespace polysat {
slice_info& concat_info = m_info[concat->get_id()]; slice_info& concat_info = m_info[concat->get_id()];
SASSERT(!concat_info.slice); // not yet set SASSERT(!concat_info.slice); // not yet set
concat_info.slice = s; concat_info.slice = s;
m_egraph.merge(s, concat, encode_dep(dep_t())); m_egraph.merge(s, concat, dep_t().encode());
} }
void slicing::add_congruence(pvar v) { void slicing::add_congruence(pvar v) {
@ -411,12 +405,12 @@ namespace polysat {
SASSERT(j.is_external()); // cannot be a congruence since the slice wasn't split before. SASSERT(j.is_external()); // cannot be a congruence since the slice wasn't split before.
void* j_hi = j.ext<void>(); void* j_hi = j.ext<void>();
void* j_lo = j.ext<void>(); void* j_lo = j.ext<void>();
dep_t d = decode_dep(j.ext<void>()); dep_t d = dep_t::decode(j.ext<void>());
if (d.is_var_idx()) { if (d.is_var_idx()) {
enode* ds = get_dep_slice(d); enode* ds = get_dep_slice(d);
SASSERT(ds == n || ds == target); SASSERT(ds == n || ds == target);
j_hi = encode_dep(mk_var_dep(get_dep_var(d), sub_hi(ds))); j_hi = mk_var_dep(get_dep_var(d), sub_hi(ds)).encode();
j_lo = encode_dep(mk_var_dep(get_dep_var(d), sub_lo(ds))); j_lo = mk_var_dep(get_dep_var(d), sub_lo(ds)).encode();
} }
m_egraph.merge(sub_hi(n), sub_hi(target), j_hi); m_egraph.merge(sub_hi(n), sub_hi(target), j_hi);
m_egraph.merge(sub_lo(n), sub_lo(target), j_lo); m_egraph.merge(sub_lo(n), sub_lo(target), j_lo);
@ -592,7 +586,7 @@ namespace polysat {
pvar x = null_var; enode* sx = nullptr; pvar x = null_var; enode* sx = nullptr;
pvar y = null_var; enode* sy = nullptr; pvar y = null_var; enode* sy = nullptr;
for (void* dp : m_tmp_deps) { for (void* dp : m_tmp_deps) {
dep_t const d = decode_dep(dp); dep_t const d = dep_t::decode(dp);
if (d.is_null()) if (d.is_null())
continue; continue;
if (d.is_lit()) { if (d.is_lit()) {
@ -756,7 +750,7 @@ namespace polysat {
SASSERT(is_value(s2)); SASSERT(is_value(s2));
dep = mk_var_dep(get_dep_var(dep), s1); dep = mk_var_dep(get_dep_var(dep), s1);
} }
m_egraph.merge(s1, s2, encode_dep(dep)); m_egraph.merge(s1, s2, dep.encode());
return !is_conflict(); return !is_conflict();
} }

7
src/math/polysat/slicing.h
View file

@ -54,8 +54,8 @@ namespace polysat {
unsigned var_idx() const { SASSERT(is_var_idx()); return *std::get_if<unsigned>(&m_data); } unsigned var_idx() const { SASSERT(is_var_idx()); return *std::get_if<unsigned>(&m_data); }
bool operator==(dep_t other) const { return m_data == other.m_data; } bool operator==(dep_t other) const { return m_data == other.m_data; }
bool operator!=(dep_t other) const { return !operator==(other); } bool operator!=(dep_t other) const { return !operator==(other); }
unsigned to_uint() const; void* encode() const;
static dep_t from_uint(unsigned x); static dep_t decode(void* p);
}; };
using dep_vector = svector<dep_t>; using dep_vector = svector<dep_t>;
@ -124,9 +124,6 @@ namespace polysat {
// Add s = concat(s1, ..., sn) // Add s = concat(s1, ..., sn)
void add_concat_node(enode* s, enode* concat); void add_concat_node(enode* s, enode* concat);
static void* encode_dep(dep_t d);
static dep_t decode_dep(void* d);
slice_info& info(euf::enode* n); slice_info& info(euf::enode* n);
slice_info const& info(euf::enode* n) const; slice_info const& info(euf::enode* n) const;

2
src/test/slicing.cpp
View file

@ -37,7 +37,7 @@ namespace polysat {
static std::ostream& display_reason(scoped_solver_slicing& s, std::ostream& out, ptr_vector<void> deps) { static std::ostream& display_reason(scoped_solver_slicing& s, std::ostream& out, ptr_vector<void> deps) {
char const* delim = ""; char const* delim = "";
for (void* dp : deps) { for (void* dp : deps) {
slicing::dep_t d = slicing::decode_dep(dp); slicing::dep_t d = slicing::dep_t::decode(dp);
if (d.is_null()) if (d.is_null())
continue; continue;
s.sl().display(out << delim, d); s.sl().display(out << delim, d);