mirror of
https://github.com/Z3Prover/z3
synced 2025-04-22 08:35:31 +00:00
porting viable
This commit is contained in:
Nikolaj Bjorner
parent
c7d6a8e570
commit
837e111d93
4 changed files with 267 additions and 9 deletions
|
|
@ -308,4 +308,8 @@ namespace polysat {
|
|||
return m_assignment.apply_to(p);
|
||||
}
|
||||
|
||||
trail_stack& core::trail() {
|
||||
return s.get_trail_stack();
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -128,6 +128,7 @@ namespace polysat {
|
|||
unsigned size(pvar v) const { return var2pdd(v).power_of_2(); }
|
||||
|
||||
constraints& cs() { return m_constraints; }
|
||||
trail_stack& trail();
|
||||
|
||||
std::ostream& display(std::ostream& out) const { throw default_exception("nyi"); }
|
||||
};
|
||||
|
|
|
|||
|
|
@ -42,6 +42,32 @@ namespace polysat {
|
|||
}
|
||||
}
|
||||
|
||||
struct viable::pop_viable_trail : public trail {
|
||||
viable& m_s;
|
||||
entry* e;
|
||||
pvar v;
|
||||
entry_kind k;
|
||||
public:
|
||||
pop_viable_trail(viable& s, entry* e, pvar v, entry_kind k)
|
||||
: m_s(s), e(e), v(v), k(k) {}
|
||||
void undo() override {
|
||||
m_s.pop_viable(e, v, k);
|
||||
}
|
||||
};
|
||||
|
||||
struct viable::push_viable_trail : public trail {
|
||||
viable& m_s;
|
||||
entry* e;
|
||||
pvar v;
|
||||
entry_kind k;
|
||||
public:
|
||||
push_viable_trail(viable& s, entry* e, pvar v, entry_kind k)
|
||||
: m_s(s), e(e), v(v), k(k) {}
|
||||
void undo() override {
|
||||
m_s.push_viable(e, v, k);
|
||||
}
|
||||
};
|
||||
|
||||
viable::entry* viable::alloc_entry(pvar var) {
|
||||
if (m_alloc.empty())
|
||||
return alloc(entry);
|
||||
|
|
@ -52,7 +78,10 @@ namespace polysat {
|
|||
return e;
|
||||
}
|
||||
|
||||
find_t viable::find_viable(pvar v, rational& out_val) { throw default_exception("nyi"); }
|
||||
find_t viable::find_viable(pvar v, rational& out_val) {
|
||||
ensure_var(v);
|
||||
throw default_exception("nyi");
|
||||
}
|
||||
|
||||
/*
|
||||
* Explain why the current variable is not viable or signleton.
|
||||
|
|
@ -63,6 +92,9 @@ namespace polysat {
|
|||
* Register constraint at index 'idx' as unitary in v.
|
||||
*/
|
||||
void viable::add_unitary(pvar v, unsigned idx) {
|
||||
|
||||
ensure_var(v);
|
||||
|
||||
if (c.is_assigned(v))
|
||||
return;
|
||||
auto [sc, d] = c.m_constraint_trail[idx];
|
||||
|
|
@ -76,7 +108,7 @@ namespace polysat {
|
|||
if (ne->interval.is_currently_empty()) {
|
||||
m_alloc.push_back(ne);
|
||||
return;
|
||||
}
|
||||
}
|
||||
|
||||
if (ne->coeff == 1) {
|
||||
intersect(v, ne);
|
||||
|
|
@ -144,7 +176,7 @@ namespace polysat {
|
|||
ne->bit_width -= k;
|
||||
display_one(std::cerr << "reduced entry: ", v, ne) << "\n";
|
||||
LOG("reduced entry to unit in bitwidth " << ne->bit_width);
|
||||
return intersect(v, ne);
|
||||
intersect(v, ne);
|
||||
}
|
||||
|
||||
// TODO: later, can reduce according to shared_parity
|
||||
|
|
@ -153,12 +185,92 @@ namespace polysat {
|
|||
insert(ne, v, m_equal_lin, entry_kind::equal_e);
|
||||
return;
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
void viable::intersect(pvar v, entry* e) {
|
||||
void viable::ensure_var(pvar v) {
|
||||
while (v >= m_units.size()) {
|
||||
m_units.push_back(layers());
|
||||
m_equal_lin.push_back(nullptr);
|
||||
m_diseq_lin.push_back(nullptr);
|
||||
}
|
||||
}
|
||||
|
||||
throw default_exception("nyi");
|
||||
bool viable::intersect(pvar v, entry* ne) {
|
||||
SASSERT(!c.is_assigned(v));
|
||||
SASSERT(!ne->src.empty());
|
||||
entry*& entries = m_units[v].ensure_layer(ne->bit_width).entries;
|
||||
entry* e = entries;
|
||||
if (e && e->interval.is_full()) {
|
||||
m_alloc.push_back(ne);
|
||||
return false;
|
||||
}
|
||||
|
||||
if (ne->interval.is_currently_empty()) {
|
||||
m_alloc.push_back(ne);
|
||||
return false;
|
||||
}
|
||||
|
||||
auto create_entry = [&]() {
|
||||
c.trail().push(pop_viable_trail(*this, ne, v, entry_kind::unit_e));
|
||||
ne->init(ne);
|
||||
return ne;
|
||||
};
|
||||
|
||||
auto remove_entry = [&](entry* e) {
|
||||
c.trail().push(push_viable_trail(*this, e, v, entry_kind::unit_e));
|
||||
e->remove_from(entries, e);
|
||||
e->active = false;
|
||||
};
|
||||
|
||||
if (ne->interval.is_full()) {
|
||||
// for (auto const& l : m_units[v].get_layers())
|
||||
// while (l.entries)
|
||||
// remove_entry(l.entries);
|
||||
while (entries)
|
||||
remove_entry(entries);
|
||||
entries = create_entry();
|
||||
return true;
|
||||
}
|
||||
|
||||
if (!e)
|
||||
entries = create_entry();
|
||||
else {
|
||||
entry* first = e;
|
||||
do {
|
||||
if (e->interval.currently_contains(ne->interval)) {
|
||||
m_alloc.push_back(ne);
|
||||
return false;
|
||||
}
|
||||
while (ne->interval.currently_contains(e->interval)) {
|
||||
entry* n = e->next();
|
||||
remove_entry(e);
|
||||
if (!entries) {
|
||||
entries = create_entry();
|
||||
return true;
|
||||
}
|
||||
if (e == first)
|
||||
first = n;
|
||||
e = n;
|
||||
}
|
||||
SASSERT(e->interval.lo_val() != ne->interval.lo_val());
|
||||
if (e->interval.lo_val() > ne->interval.lo_val()) {
|
||||
if (first->prev()->interval.currently_contains(ne->interval)) {
|
||||
m_alloc.push_back(ne);
|
||||
return false;
|
||||
}
|
||||
e->insert_before(create_entry());
|
||||
if (e == first)
|
||||
entries = e->prev();
|
||||
SASSERT(well_formed(m_units[v]));
|
||||
return true;
|
||||
}
|
||||
e = e->next();
|
||||
} while (e != first);
|
||||
// otherwise, append to end of list
|
||||
first->insert_before(create_entry());
|
||||
}
|
||||
SASSERT(well_formed(m_units[v]));
|
||||
return true;
|
||||
}
|
||||
|
||||
void viable::log() {
|
||||
|
|
@ -170,10 +282,94 @@ namespace polysat {
|
|||
throw default_exception("nyi");
|
||||
}
|
||||
|
||||
void viable::insert(entry* e, pvar v, ptr_vector<entry>& entries, entry_kind k) {
|
||||
throw default_exception("nyi");
|
||||
|
||||
viable::layer& viable::layers::ensure_layer(unsigned bit_width) {
|
||||
for (unsigned i = 0; i < m_layers.size(); ++i) {
|
||||
layer& l = m_layers[i];
|
||||
if (l.bit_width == bit_width)
|
||||
return l;
|
||||
else if (l.bit_width < bit_width) {
|
||||
m_layers.push_back(layer(0));
|
||||
for (unsigned j = m_layers.size(); --j > i; )
|
||||
m_layers[j] = m_layers[j - 1];
|
||||
m_layers[i] = layer(bit_width);
|
||||
return m_layers[i];
|
||||
}
|
||||
}
|
||||
m_layers.push_back(layer(bit_width));
|
||||
return m_layers.back();
|
||||
}
|
||||
|
||||
viable::layer* viable::layers::get_layer(unsigned bit_width) {
|
||||
return const_cast<layer*>(std::as_const(*this).get_layer(bit_width));
|
||||
}
|
||||
|
||||
viable::layer const* viable::layers::get_layer(unsigned bit_width) const {
|
||||
for (layer const& l : m_layers)
|
||||
if (l.bit_width == bit_width)
|
||||
return &l;
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
void viable::pop_viable(entry* e, pvar v, entry_kind k) {
|
||||
SASSERT(well_formed(m_units[v]));
|
||||
SASSERT(e->active);
|
||||
e->active = false;
|
||||
switch (k) {
|
||||
case entry_kind::unit_e:
|
||||
entry::remove_from(m_units[v].get_layer(e)->entries, e);
|
||||
SASSERT(well_formed(m_units[v]));
|
||||
break;
|
||||
case entry_kind::equal_e:
|
||||
entry::remove_from(m_equal_lin[v], e);
|
||||
break;
|
||||
case entry_kind::diseq_e:
|
||||
entry::remove_from(m_diseq_lin[v], e);
|
||||
break;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
break;
|
||||
}
|
||||
m_alloc.push_back(e);
|
||||
}
|
||||
|
||||
void viable::push_viable(entry* e, pvar v, entry_kind k) {
|
||||
// display_one(verbose_stream() << "Push entry: ", v, e) << "\n";
|
||||
entry*& entries = m_units[v].get_layer(e)->entries;
|
||||
SASSERT(e->prev() != e || !entries);
|
||||
SASSERT(e->prev() != e || e->next() == e);
|
||||
SASSERT(k == entry_kind::unit_e);
|
||||
SASSERT(!e->active);
|
||||
e->active = true;
|
||||
(void)k;
|
||||
SASSERT(well_formed(m_units[v]));
|
||||
if (e->prev() != e) {
|
||||
entry* pos = e->prev();
|
||||
e->init(e);
|
||||
pos->insert_after(e);
|
||||
if (e->interval.lo_val() < entries->interval.lo_val())
|
||||
entries = e;
|
||||
}
|
||||
else
|
||||
entries = e;
|
||||
SASSERT(well_formed(m_units[v]));
|
||||
}
|
||||
|
||||
void viable::insert(entry* e, pvar v, ptr_vector<entry>& entries, entry_kind k) {
|
||||
SASSERT(well_formed(m_units[v]));
|
||||
|
||||
c.trail().push(pop_viable_trail(*this, e, v, k));
|
||||
|
||||
e->init(e);
|
||||
if (!entries[v])
|
||||
entries[v] = e;
|
||||
else
|
||||
e->insert_after(entries[v]);
|
||||
SASSERT(entries[v]->invariant());
|
||||
SASSERT(well_formed(m_units[v]));
|
||||
}
|
||||
|
||||
|
||||
std::ostream& viable::display_one(std::ostream& out, pvar v, entry const* e) const {
|
||||
auto& m = c.var2pdd(v);
|
||||
if (e->coeff == -1) {
|
||||
|
|
@ -229,4 +425,51 @@ namespace polysat {
|
|||
return out;
|
||||
}
|
||||
|
||||
/*
|
||||
* Lower bounds are strictly ascending.
|
||||
* Intervals don't contain each-other (since lower bounds are ascending, it suffices to check containment in one direction).
|
||||
*/
|
||||
bool viable::well_formed(entry* e) {
|
||||
if (!e)
|
||||
return true;
|
||||
entry* first = e;
|
||||
while (true) {
|
||||
if (!e->active)
|
||||
return false;
|
||||
|
||||
if (e->interval.is_full())
|
||||
return e->next() == e;
|
||||
if (e->interval.is_currently_empty())
|
||||
return false;
|
||||
|
||||
auto* n = e->next();
|
||||
if (n != e && e->interval.currently_contains(n->interval))
|
||||
return false;
|
||||
|
||||
if (n == first)
|
||||
break;
|
||||
if (e->interval.lo_val() >= n->interval.lo_val())
|
||||
return false;
|
||||
e = n;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
/*
|
||||
* Layers are ordered in strictly descending bit-width.
|
||||
* Entries in each layer are well-formed.
|
||||
*/
|
||||
bool viable::well_formed(layers const& ls) {
|
||||
unsigned prev_width = std::numeric_limits<unsigned>::max();
|
||||
for (layer const& l : ls.get_layers()) {
|
||||
if (!well_formed(l.entries))
|
||||
return false;
|
||||
if (!all_of(dll_elements(l.entries), [&l](entry const& e) { return e.bit_width == l.bit_width; }))
|
||||
return false;
|
||||
if (prev_width <= l.bit_width)
|
||||
return false;
|
||||
prev_width = l.bit_width;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -86,6 +86,9 @@ namespace polysat {
|
|||
ptr_vector<entry> m_equal_lin; // entries that have non-unit multipliers, but are equal
|
||||
ptr_vector<entry> m_diseq_lin; // entries that have distinct non-zero multipliers
|
||||
|
||||
bool well_formed(entry* e);
|
||||
bool well_formed(layers const& ls);
|
||||
|
||||
entry* alloc_entry(pvar v);
|
||||
|
||||
std::ostream& display_one(std::ostream& out, pvar v, entry const* e) const;
|
||||
|
|
@ -93,13 +96,20 @@ namespace polysat {
|
|||
void log();
|
||||
void log(pvar v);
|
||||
|
||||
struct pop_viable_trail;
|
||||
void pop_viable(entry* e, pvar v, entry_kind k);
|
||||
struct push_viable_trail;
|
||||
void push_viable(entry* e, pvar v, entry_kind k);
|
||||
|
||||
void insert(entry* e, pvar v, ptr_vector<entry>& entries, entry_kind k);
|
||||
|
||||
void intersect(pvar v, entry* e);
|
||||
bool intersect(pvar v, entry* e);
|
||||
|
||||
void ensure_var(pvar v);
|
||||
|
||||
public:
|
||||
viable(core& c);
|
||||
|
||||
~viable();
|
||||
|
||||
/**
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue