mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-25 21:57:00 +00:00
Code Activity

refactor, update comment

Browse source
This commit is contained in:
Jakob Rath 2024-04-15 11:18:42 +02:00
parent 06e5595e87
commit 69ea52407f
2 changed files with 15 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -162,12 +162,12 @@ namespace polysat {
} }
// //
// // find set of layers across all suffixes, sort by bit-width
// from smallest size(w) suffix [w] to largest //
// from smallest bit_width layer [bit_width, entries] to largest // from smallest bit_width layer [bit_width, entries] to largest
// check if val is allowed by entries or advance val to next allowed value // check if val is allowed by entries or advance val to next allowed value
// //
viable::entry* viable::find_overlap(rational& val) { viable::entry* viable::find_overlap(rational& val) {
entry* last = nullptr; entry* last = nullptr;
@ -198,11 +198,7 @@ namespace polysat {
layers.push_back(&layer); layers.push_back(&layer);
std::sort(layers.begin(), layers.end(), [](layer const* l1, layer const* l2) { return l1->bit_width < l2->bit_width; }); std::sort(layers.begin(), layers.end(), [](layer const* l1, layer const* l2) { return l1->bit_width < l2->bit_width; });
next: while (entry* e = find_overlap(layers, val)) {
for (layer const* layer : layers) {
entry* e = find_overlap(*layer, val);
if (!e)
continue;
last = e; last = e;
if (e->interval.is_proper()) if (e->interval.is_proper())
update_value_to_high(val, e); update_value_to_high(val, e);
@ -213,11 +209,17 @@ next:
m_explain_kind = explain_t::conflict; m_explain_kind = explain_t::conflict;
return nullptr; return nullptr;
} }
goto next;
} }
return last; return last;
} }
viable::entry* viable::find_overlap(ptr_vector<layer const> const& layers, rational const& val) {
for (layer const* layer : layers)
if (entry* e = find_overlap(*layer, val))
return e;
return nullptr;
}
viable::entry* viable::find_overlap(layer const& l, rational const& val) { viable::entry* viable::find_overlap(layer const& l, rational const& val) {
if (!l.entries) if (!l.entries)
return nullptr; return nullptr;

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

@ -121,6 +121,7 @@ namespace polysat {
// find the first non-fixed entry that overlaps with val, if any. // find the first non-fixed entry that overlaps with val, if any.
entry* find_overlap(rational& val); entry* find_overlap(rational& val);
entry* find_overlap(ptr_vector<layer const> const& layers, rational const& val);
entry* find_overlap(layer const& l, rational const& val); entry* find_overlap(layer const& l, rational const& val);
void remove_redundant_explanations(); void remove_redundant_explanations();