mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 08:35:31 +00:00
Code Activity

update viable

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-09 09:44:05 -08:00
parent faa6c14610
commit c0a8da34af
2 changed files with 147 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

108
src/sat/smt/polysat/polysat_viable.cpp
View file

@ -45,44 +45,111 @@ 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) {}
pop_viable_trail(viable& s, entry* e, entry_kind k)
: m_s(s), e(e), k(k) {}
void undo() override {
m_s.pop_viable(e, v, k);
m_s.pop_viable(e, 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) {}
push_viable_trail(viable& s, entry* e)
: m_s(s), e(e) {}
void undo() override {
m_s.push_viable(e, v, k);
m_s.push_viable(e);
}
};
viable::entry* viable::alloc_entry(pvar var) {
viable::entry* viable::alloc_entry(pvar var, unsigned constraint_index) {
if (m_alloc.empty())
return alloc(entry);
auto* e = m_alloc.back();
e->reset();
e->var = var;
e->constraint_index = constraint_index;
m_alloc.pop_back();
return e;
}
find_t viable::find_viable(pvar v, rational& out_val) {
find_t viable::find_viable(pvar v, rational& lo) {
rational hi;
ensure_var(v);
throw default_exception("nyi");
switch (find_viable(v, lo, hi)) {
case l_true:
return (lo == hi) ? find_t::singleton : find_t::multiple;
case l_false:
return find_t::empty;
default:
return find_t::resource_out;
}
}
lbool viable::find_viable(pvar v, rational& lo, rational& hi) {
fixed_bits_info fbi;
#if 0
if (!collect_bit_information(v, true, fbi))
return l_false; // conflict already added
#endif
pvar_vector overlaps;
#if 0
// TODO s.m_slicing.collect_simple_overlaps(v, overlaps);
#endif
std::sort(overlaps.begin(), overlaps.end(), [&](pvar x, pvar y) { return c.size(x) > c.size(y); });
uint_set widths_set;
// 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));
#if 0
LOG("Overlaps with v" << v << ":");
for (pvar x : overlaps) {
unsigned hi, lo;
if (s.m_slicing.is_extract(x, v, hi, lo))
LOG(" v" << x << " = v" << v << "[" << hi << ":" << lo << "]");
else
LOG(" v" << x << " not extracted from v" << v << "; size " << s.size(x));
for (layer const& l : m_units[x].get_layers()) {
widths_set.insert(l.bit_width);
}
}
#endif
unsigned_vector widths;
for (unsigned w : widths_set)
widths.push_back(w);
LOG("widths: " << widths);
rational const& max_value = c.var2pdd(v).max_value();
#if 0
lbool result_lo = find_on_layers(v, widths, overlaps, fbi, rational::zero(), max_value, lo);
if (result_lo == l_false)
return l_false; // conflict
if (result_lo == l_undef)
return find_viable_fallback(v, overlaps, lo, hi);
if (lo == max_value) {
hi = lo;
return l_true;
}
lbool result_hi = find_on_layers(v, widths, overlaps, fbi, lo + 1, max_value, hi);
if (result_hi == l_false)
hi = lo; // no other viable value
if (result_hi == l_undef)
return find_viable_fallback(v, overlaps, lo, hi);
#endif
return l_true;
}
/*
* Explain why the current variable is not viable or signleton.
*/
@ -99,7 +166,7 @@ namespace polysat {
return;
auto [sc, d] = c.m_constraint_trail[idx];
entry* ne = alloc_entry(v);
entry* ne = alloc_entry(v, idx);
if (!m_forbidden_intervals.get_interval(sc, v, *ne)) {
m_alloc.push_back(ne);
return;
@ -211,13 +278,13 @@ namespace polysat {
}
auto create_entry = [&]() {
c.trail().push(pop_viable_trail(*this, ne, v, entry_kind::unit_e));
c.trail().push(pop_viable_trail(*this, ne, 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));
c.trail().push(push_viable_trail(*this, e));
e->remove_from(entries, e);
e->active = false;
};
@ -311,7 +378,8 @@ namespace polysat {
return nullptr;
}
void viable::pop_viable(entry* e, pvar v, entry_kind k) {
void viable::pop_viable(entry* e, entry_kind k) {
unsigned v = e->var;
SASSERT(well_formed(m_units[v]));
SASSERT(e->active);
e->active = false;
@ -333,15 +401,15 @@ namespace polysat {
m_alloc.push_back(e);
}
void viable::push_viable(entry* e, pvar v, entry_kind k) {
void viable::push_viable(entry* e) {
// display_one(verbose_stream() << "Push entry: ", v, e) << "\n";
auto v = e->var;
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();
@ -358,7 +426,7 @@ namespace polysat {
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));
c.trail().push(pop_viable_trail(*this, e, k));
e->init(e);
if (!entries[v])

63
src/sat/smt/polysat/polysat_viable.h
View file

@ -50,6 +50,7 @@ namespace polysat {
bool active = true;
bool valid_for_lemma = true;
pvar var = null_var;
unsigned constraint_index = UINT_MAX;
void reset() {
// dll_base<entry>::init(this); // we never did this in alloc_entry either
@ -58,6 +59,7 @@ namespace polysat {
active = true;
valid_for_lemma = true;
var = null_var;
constraint_index = UINT_MAX;
}
};
@ -70,7 +72,7 @@ namespace polysat {
};
class layers final {
svector<layer> m_layers;
svector<layer> m_layers;
public:
svector<layer> const& get_layers() const { return m_layers; }
layer& ensure_layer(unsigned bit_width);
@ -81,6 +83,57 @@ namespace polysat {
entry* get_entries(unsigned bit_width) const { layer const* l = get_layer(bit_width); return l ? l->entries : nullptr; }
};
struct fixed_bits_info {
svector<lbool> fixed;
vector<vector<signed_constraint>> just_src;
vector<vector<signed_constraint>> just_side_cond;
vector<svector<pvar>> just_slicing;
bool is_empty() const {
SASSERT_EQ(fixed.empty(), just_src.empty());
SASSERT_EQ(fixed.empty(), just_side_cond.empty());
return fixed.empty();
}
bool is_empty_at(unsigned i) const {
return fixed[i] == l_undef && just_src[i].empty() && just_side_cond[i].empty();
}
void reset(unsigned num_bits) {
fixed.reset();
fixed.resize(num_bits, l_undef);
just_src.reset();
just_src.resize(num_bits);
just_side_cond.reset();
just_side_cond.resize(num_bits);
just_slicing.reset();
just_slicing.resize(num_bits);
}
void reset_just(unsigned i) {
just_src[i].reset();
just_side_cond[i].reset();
just_slicing[i].reset();
}
void set_just(unsigned i, entry* e) {
reset_just(i);
push_just(i, e);
}
void push_just(unsigned i, entry* e) {
just_src[i].append(e->src);
just_side_cond[i].append(e->side_cond);
}
void push_from_bit(unsigned i, unsigned src) {
just_src[i].append(just_src[src]);
just_side_cond[i].append(just_side_cond[src]);
just_slicing[i].append(just_slicing[src]);
}
};
ptr_vector<entry> m_alloc;
vector<layers> m_units; // set of viable values based on unit multipliers, layered by bit-width in descending order
ptr_vector<entry> m_equal_lin; // entries that have non-unit multipliers, but are equal
@ -89,7 +142,7 @@ namespace polysat {
bool well_formed(entry* e);
bool well_formed(layers const& ls);
entry* alloc_entry(pvar v);
entry* alloc_entry(pvar v, unsigned constraint_index);
std::ostream& display_one(std::ostream& out, pvar v, entry const* e) const;
std::ostream& display_all(std::ostream& out, pvar v, entry const* e, char const* delimiter = "") const;
@ -97,9 +150,9 @@ namespace polysat {
void log(pvar v);
struct pop_viable_trail;
void pop_viable(entry* e, pvar v, entry_kind k);
void pop_viable(entry* e, entry_kind k);
struct push_viable_trail;
void push_viable(entry* e, pvar v, entry_kind k);
void push_viable(entry* e);
void insert(entry* e, pvar v, ptr_vector<entry>& entries, entry_kind k);
@ -107,6 +160,8 @@ namespace polysat {
void ensure_var(pvar v);
lbool find_viable(pvar v, rational& lo, rational& hi);
public:
viable(core& c);