mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 09:26:15 +00:00
Code Activity

minor

Browse source
This commit is contained in:
Jakob Rath 2023-07-17 19:04:17 +02:00
parent d1cb02b735
commit 11d9e5c862
3 changed files with 44 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -153,8 +153,8 @@ namespace polysat {
m_scopes.shrink(target_lvl); m_scopes.shrink(target_lvl);
while (m_trail.size() > target_size) { while (m_trail.size() > target_size) {
switch (m_trail.back()) { switch (m_trail.back()) {
case trail_item::add_var: undo_add_var(); break; case trail_item::add_var: undo_add_var(); break;
case trail_item::split_core: undo_split_core(); break; case trail_item::split_core: undo_split_core(); break;
default: UNREACHABLE(); default: UNREACHABLE();
} }
m_trail.pop_back(); m_trail.pop_back();
@ -203,6 +203,7 @@ namespace polysat {
// split a single slice without updating any equivalences // split a single slice without updating any equivalences
void slicing::split_core(enode* s, unsigned cut) { void slicing::split_core(enode* s, unsigned cut) {
SASSERT(!has_sub(s)); SASSERT(!has_sub(s));
SASSERT(info(s).sub_hi == nullptr && info(s).sub_lo == nullptr);
SASSERT(width(s) > cut + 1); SASSERT(width(s) > cut + 1);
unsigned const width_hi = width(s) - cut - 1; unsigned const width_hi = width(s) - cut - 1;
unsigned const width_lo = cut + 1; unsigned const width_lo = cut + 1;
@ -216,6 +217,8 @@ namespace polysat {
else { else {
sub_hi = alloc_slice(width_hi); sub_hi = alloc_slice(width_hi);
sub_lo = alloc_slice(width_lo); sub_lo = alloc_slice(width_lo);
// info(sub_hi).parent = s;
// info(sub_lo).parent = s;
} }
info(s).set_cut(cut, sub_hi, sub_lo); info(s).set_cut(cut, sub_hi, sub_lo);
m_trail.push_back(trail_item::split_core); m_trail.push_back(trail_item::split_core);
@ -361,7 +364,6 @@ namespace polysat {
} }
bool slicing::merge(enode_vector& xs, enode_vector& ys, dep_t dep) { bool slicing::merge(enode_vector& xs, enode_vector& ys, dep_t dep) {
// LOG_H2("Merging " << xs << " with " << ys);
while (!xs.empty()) { while (!xs.empty()) {
SASSERT(!ys.empty()); SASSERT(!ys.empty());
enode* x = xs.back(); enode* x = xs.back();
@ -381,20 +383,17 @@ namespace polysat {
SASSERT(!has_sub(x)); SASSERT(!has_sub(x));
SASSERT(!has_sub(y)); SASSERT(!has_sub(y));
if (width(x) == width(y)) { if (width(x) == width(y)) {
// LOG("Match " << x << " and " << y);
if (!merge_base(x, y, dep)) if (!merge_base(x, y, dep))
return false; return false;
} }
else if (width(x) > width(y)) { else if (width(x) > width(y)) {
// need to split x according to y // need to split x according to y
// LOG("Splitting " << x << " to fit " << y);
mk_slice(x, width(y) - 1, 0, xs, true); mk_slice(x, width(y) - 1, 0, xs, true);
ys.push_back(y); ys.push_back(y);
} }
else { else {
SASSERT(width(y) > width(x)); SASSERT(width(y) > width(x));
// need to split y according to x // need to split y according to x
// LOG("Splitting " << y << " to fit " << x);
mk_slice(y, width(x) - 1, 0, ys, true); mk_slice(y, width(x) - 1, 0, ys, true);
xs.push_back(x); xs.push_back(x);
} }
@ -442,6 +441,8 @@ namespace polysat {
ys.clear(); ys.clear();
if (result) { if (result) {
// TODO: merge equivalence class of x, y (on upper level)? but can we always combine the sub-trees? // TODO: merge equivalence class of x, y (on upper level)? but can we always combine the sub-trees?
// need to add a congruence to track justification.
// adding virtual concat terms for x,y will do that automatically.
} }
return result; return result;
} }
@ -605,6 +606,7 @@ namespace polysat {
// TODO: evaluate under current assignment? // TODO: evaluate under current assignment?
if (!c->is_eq()) if (!c->is_eq())
return; return;
dep_t const d = c.blit();
pdd const& p = c->to_eq(); pdd const& p = c->to_eq();
auto& m = p.manager(); auto& m = p.manager();
for (auto& [a, x] : p.linear_monomials()) { for (auto& [a, x] : p.linear_monomials()) {
@ -616,7 +618,12 @@ namespace polysat {
enode* const sx = var2slice(x); enode* const sx = var2slice(x);
if (body.is_val()) { if (body.is_val()) {
// Simple assignment x = value // Simple assignment x = value
// TODO: set fixed bits enode* const sval = mk_value_slice(body.val(), body.power_of_2());
if (!merge(sx, sval, d)) {
// TODO: conflict
NOT_IMPLEMENTED_YET();
return;
}
continue; continue;
} }
pvar const y = m_solver.m_names.get_name(body); pvar const y = m_solver.m_names.get_name(body);
@ -626,8 +633,11 @@ namespace polysat {
} }
enode* const sy = var2slice(y); enode* const sy = var2slice(y);
if (c.is_positive()) { if (c.is_positive()) {
if (!merge(sx, sy, c.blit())) if (!merge(sx, sy, d)) {
// TODO: conflict
NOT_IMPLEMENTED_YET();
return; return;
}
} }
else { else {
SASSERT(c.is_negative()); SASSERT(c.is_negative());
@ -654,9 +664,8 @@ namespace polysat {
get_root_base(vs, base); get_root_base(vs, base);
for (enode* s : base) for (enode* s : base)
display(out << " ", s); display(out << " ", s);
// if (has_value(vs)) { if (has_value(vs->get_root()))
// out << " -- (val:" << get_value(vs) << ")"; out << " [root_value: " << get_value(vs->get_root()) << "]";
// }
out << "\n"; out << "\n";
} }
return out; return out;
@ -690,10 +699,7 @@ namespace polysat {
} }
std::ostream& slicing::display(std::ostream& out, enode* s) const { std::ostream& slicing::display(std::ostream& out, enode* s) const {
out << "{id:" << s->get_id() << ",w:" << width(s); out << "{id:" << s->get_id() << ",w:" << width(s) << "}";
// if (has_value(s))
// out << ",val:" << get_value(s);
out << "}";
return out; return out;
} }
@ -704,7 +710,17 @@ namespace polysat {
for (enode* s : m_egraph.nodes()) { for (enode* s : m_egraph.nodes()) {
// if the slice is equivalent to a variable, then the variable's slice is in the equivalence class // if the slice is equivalent to a variable, then the variable's slice is in the equivalence class
pvar const v = slice2var(s); pvar const v = slice2var(s);
VERIFY_EQ(v != null_var, var2slice(v)->get_root() == s->get_root()); if (v != null_var) {
VERIFY_EQ(var2slice(v)->get_root(), s->get_root());
}
// if slice has a value, it should be propagated to its sub-slices
if (has_value(s)) {
VERIFY(s->is_root());
if (has_sub(s)) {
VERIFY(has_value(sub_hi(s)));
VERIFY(has_value(sub_lo(s)));
}
}
// properties below only matter for representatives // properties below only matter for representatives
if (!s->is_root()) if (!s->is_root())
continue; continue;
@ -712,11 +728,6 @@ namespace polysat {
// equivalence class only contains slices of equal length // equivalence class only contains slices of equal length
VERIFY_EQ(width(s), width(n)); VERIFY_EQ(width(s), width(n));
} }
// if slice has a value, it should be propagated to its sub-slices
// if (has_value(s)) {
// VERIFY(has_value(sub_hi(s)->get_root()));
// VERIFY(has_value(sub_lo(s)->get_root()));
// }
} }
return true; return true;
} }

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

@ -47,12 +47,17 @@ namespace polysat {
static constexpr unsigned null_cut = std::numeric_limits<unsigned>::max(); static constexpr unsigned null_cut = std::numeric_limits<unsigned>::max();
// Kinds of slices:
// - proper (from variables)
// - values
// - virtual concat(...) expressions
struct slice_info { struct slice_info {
unsigned width = 0; // number of bits in the slice unsigned width = 0; // number of bits in the slice
// Cut point: if not null_cut, the slice s has been subdivided into s[|s|-1:cut+1] and s[cut:0]. // Cut point: if not null_cut, the slice s has been subdivided into s[|s|-1:cut+1] and s[cut:0].
// The cut point is relative to the parent slice (rather than a root variable, which might not be unique) // The cut point is relative to the parent slice (rather than a root variable, which might not be unique)
unsigned cut = null_cut; // cut point, or null_cut if no subslices unsigned cut = null_cut; // cut point, or null_cut if no subslices
pvar var = null_var; // slice is equivalent to this variable, if any (without dependencies) pvar var = null_var; // slice is equivalent to this variable, if any (without dependencies)
// enode* parent = nullptr; // parent slice, only for proper slices (if not null: s == sub_hi(parent(s)) || s == sub_lo(parent(s)))
enode* slice = nullptr; // if enode corresponds to a concat(...) expression, this field links to the represented slice. enode* slice = nullptr; // if enode corresponds to a concat(...) expression, this field links to the represented slice.
enode* sub_hi = nullptr; // upper subslice s[|s|-1:cut+1] enode* sub_hi = nullptr; // upper subslice s[|s|-1:cut+1]
enode* sub_lo = nullptr; // lower subslice s[cut:0] enode* sub_lo = nullptr; // lower subslice s[cut:0]

7
src/test/slicing.cpp
View file

@ -51,6 +51,7 @@ namespace polysat {
std::cout << sl << "\n"; std::cout << sl << "\n";
sl.display_tree(std::cout); sl.display_tree(std::cout);
VERIFY(sl.invariant());
} }
// x[7:3] = a // x[7:3] = a
@ -73,6 +74,7 @@ namespace polysat {
std::cout << sl << "\n"; std::cout << sl << "\n";
sl.display_tree(std::cout); sl.display_tree(std::cout);
VERIFY(sl.invariant());
(void)a; (void)a;
(void)b; (void)b;
@ -123,6 +125,8 @@ namespace polysat {
reason.reset(); reason.reset();
sl.explain_equal(sl.var2slice(b), sl.pdd2slice(d), reason); sl.explain_equal(sl.var2slice(b), sl.pdd2slice(d), reason);
std::cout << " Reason: " << reason << "\n\n"; std::cout << " Reason: " << reason << "\n\n";
VERIFY(sl.invariant());
} }
// 1. a = b // 1. a = b
@ -155,7 +159,9 @@ namespace polysat {
sat::literal_vector reason; sat::literal_vector reason;
sl.explain_equal(sl.var2slice(d), sl.var2slice(e), reason); sl.explain_equal(sl.var2slice(d), sl.var2slice(e), reason);
std::cout << " Reason: " << reason << "\n"; std::cout << " Reason: " << reason << "\n";
sl.display_tree(std::cout); sl.display_tree(std::cout);
VERIFY(sl.invariant());
} }
// x[5:2] = y // x[5:2] = y
@ -183,6 +189,7 @@ namespace polysat {
std::cout << "v" << z << " = 7\n" << sl << "\n"; std::cout << "v" << z << " = 7\n" << sl << "\n";
sl.display_tree(std::cout); sl.display_tree(std::cout);
VERIFY(sl.invariant());
} }
}; };