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

bug fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-27 11:29:42 -08:00
parent 9cce1ff836
commit 6103c9d718
9 changed files with 124 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

67
src/ast/euf/euf_bv_plugin.cpp
View file

@ -103,7 +103,7 @@ namespace euf {
return mk(e, 0, nullptr);
}
void bv_plugin::merge_eh(enode* x, enode* y) {
void bv_plugin::propagate_merge(enode* x, enode* y) {
if (!bv.is_bv(x->get_expr()))
return;
@ -128,6 +128,35 @@ namespace euf {
propagate_extract(n);
}
void bv_plugin::register_node(enode* n) {
m_queue.push_back(n);
m_trail.push_back(new (get_region()) push_back_vector(m_queue));
push_plugin_undo(bv.get_family_id());
}
void bv_plugin::merge_eh(enode* n1, enode* n2) {
m_queue.push_back(enode_pair(n1, n2));
m_trail.push_back(new (get_region()) push_back_vector(m_queue));
push_plugin_undo(bv.get_family_id());
}
void bv_plugin::propagate() {
if (m_qhead == m_queue.size())
return;
m_trail.push_back(new (get_region()) value_trail(m_qhead));
push_plugin_undo(bv.get_family_id());
for (; m_qhead < m_queue.size(); ++m_qhead) {
if (std::holds_alternative<enode*>(m_queue[m_qhead])) {
auto n = *std::get_if<enode*>(&m_queue[m_qhead]);
propagate_register_node(n);
}
else {
auto [a, b] = *std::get_if<enode_pair>(&m_queue[m_qhead]);
propagate_merge(a, b);
}
}
}
// enforce concat(v1, v2) = v2*2^|v1| + v1
void bv_plugin::propagate_values(enode* x) {
if (!is_value(x))
@ -203,21 +232,32 @@ namespace euf {
}
}
void bv_plugin::push_undo_split(enode* n) {
m_undo_split.push_back(n);
class bv_plugin::undo_split : public trail {
bv_plugin& p;
enode* n;
public:
undo_split(bv_plugin& p, enode* n): p(p), n(n) {}
void undo() override {
auto& i = p.info(n);
i.value = nullptr;
i.lo = nullptr;
i.hi = nullptr;
i.cut = null_cut;
}
};
void bv_plugin::push_undo_split(enode* n) {
m_trail.push_back(new (get_region()) undo_split(*this, n));
push_plugin_undo(bv.get_family_id());
}
void bv_plugin::undo() {
enode* n = m_undo_split.back();
m_undo_split.pop_back();
auto& i = info(n);
i.lo = nullptr;
i.hi = nullptr;
i.cut = null_cut;
m_trail.back()->undo();
m_trail.pop_back();
}
void bv_plugin::register_node(enode* n) {
void bv_plugin::propagate_register_node(enode* n) {
TRACE("bv", tout << "register " << g.bpp(n) << "\n");
auto& i = info(n);
i.value = n;
@ -236,6 +276,7 @@ namespace euf {
push_merge(mk_extract(arg, 0, w - 1), arg);
ensure_slice(arg, lo, hi);
}
TRACE("bv", tout << "done register " << g.bpp(n) << "\n");
}
//
@ -487,10 +528,10 @@ namespace euf {
}
std::ostream& bv_plugin::display(std::ostream& out) const {
out << "bv\n";
out << "bv\n";
for (auto const& i : m_info)
if (i.lo)
out << g.bpp(i.value) << " cut " << i.cut << " lo " << g.bpp(i.lo) << " hi " << g.bpp(i.hi) << "\n";
if (i.lo)
out << g.bpp(i.value) << " cut " << i.cut << " lo " << g.bpp(i.lo) << " hi " << g.bpp(i.hi) << "\n";
return out;
}
}

13
src/ast/euf/euf_bv_plugin.h
View file

@ -19,6 +19,7 @@ Author:
#pragma once
#include "util/trail.h"
#include "ast/bv_decl_plugin.h"
#include "ast/euf/euf_plugin.h"
@ -81,8 +82,16 @@ namespace euf {
svector<std::tuple<enode*, unsigned, unsigned>> m_jtodo;
void clear_offsets();
enode_vector m_undo_split;
ptr_vector<trail> m_trail;
class undo_split;
void push_undo_split(enode* n);
vector<std::variant<enode*, enode_pair>> m_queue;
unsigned m_qhead = 0;
void propagate_register_node(enode* n);
void propagate_merge(enode* a, enode* b);
public:
bv_plugin(egraph& g);
@ -97,7 +106,7 @@ namespace euf {
void diseq_eh(enode* eq) override {}
void propagate() override {}
void propagate() override;
void undo() override;

6
src/ast/euf/euf_egraph.cpp
View file

@ -107,7 +107,10 @@ namespace euf {
void egraph::update_children(enode* n) {
for (enode* child : enode_args(n))
child->get_root()->add_parent(n);
for (enode* child : enode_args(n))
SASSERT(child->get_root()->m_parents.back() == n);
m_updates.push_back(update_record(n, update_record::update_children()));
TRACE("euf", tout << "update children " << bpp(n) << "\n"; display(tout));
}
enode* egraph::mk(expr* f, unsigned generation, unsigned num_args, enode *const* args) {
@ -441,7 +444,10 @@ namespace euf {
p.r1->set_relevant(false);
break;
case update_record::tag_t::is_update_children:
TRACE("euf", tout << "reverse update children " << bpp(p.r1) << "\n"; display(tout));
for (unsigned i = 0; i < p.r1->num_args(); ++i) {
CTRACE("euf", (p.r1->m_args[i]->get_root()->m_parents.back() != p.r1),
display(tout << bpp(p.r1->m_args[i]) << " " << bpp(p.r1->m_args[i]->get_root()) << " "););
SASSERT(p.r1->m_args[i]->get_root()->m_parents.back() == p.r1);
p.r1->m_args[i]->get_root()->m_parents.pop_back();
}

10
src/sat/smt/polysat/core.cpp
View file

@ -320,7 +320,8 @@ namespace polysat {
if (!is_assigned(v0) || is_assigned(v1))
continue;
// detect unitary, add to viable, detect conflict?
m_viable.add_unitary(v1, idx);
if (value != l_undef)
m_viable.add_unitary(v1, idx);
}
SASSERT(m_watch[v].size() == sz && "size of watch list was not changed");
m_watch[v].shrink(j);
@ -347,16 +348,20 @@ namespace polysat {
}
dependency core::get_dependency(constraint_id idx) const {
if (idx.is_null())
return null_dependency;
auto [sc, d, value] = m_constraint_index[idx.id];
return d;
}
#if 0
dependency_vector core::get_dependencies(constraint_id_vector const& ids) const {
dependency_vector result;
for (auto id : ids)
result.push_back(get_dependency(id));
return result;
}
#endif
void core::propagate(constraint_id id, signed_constraint& sc, lbool value, dependency const& d) {
lbool eval_value = eval(sc);
@ -442,8 +447,9 @@ namespace polysat {
out << "polysat:\n";
for (auto const& [sc, d, value] : m_constraint_index)
out << sc << " " << d << " := " << value << "\n";
for (unsigned i = 0; i < m_vars.size(); ++i)
for (unsigned i = 0; i < m_vars.size(); ++i) {
out << m_vars[i] << " := " << m_values[i] << " " << get_dependency(m_justification[i]) << "\n";
}
m_var_queue.display(out << "vars ") << "\n";
return out;
}

2
src/sat/smt/polysat/core.h
View file

@ -155,7 +155,7 @@ namespace polysat {
dependency_vector const& unsat_core() const { return m_unsat_core; }
constraint_id_vector const& assigned_constraints() const { return m_prop_queue; }
dependency get_dependency(constraint_id idx) const;
dependency_vector get_dependencies(constraint_id_vector const& ids) const;
// dependency_vector get_dependencies(constraint_id_vector const& ids) const;
lbool eval(constraint_id id);
dependency propagate(signed_constraint const& sc, dependency_vector const& deps) { return s.propagate(sc, deps); }
lbool eval(signed_constraint const& sc);

4
src/sat/smt/polysat/types.h
View file

@ -110,7 +110,9 @@ namespace polysat {
inline std::ostream& operator<<(std::ostream& out, offset_slice const& js) {
return out << "v" << js.v << "[" << js.offset << "[ @";
if (js.offset == 0)
return out << "v" << js.v;
return out << "v" << js.v << " at offset " << js.offset;
}
using fixed_bits_vector = svector<fixed_slice>;

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

@ -84,6 +84,7 @@ namespace polysat {
}
find_t viable::find_viable(pvar v, rational& lo) {
display(verbose_stream() << "find viable for v" << v << "\n");
rational hi;
switch (find_viable(v, lo, hi)) {
case l_true:
@ -99,7 +100,6 @@ namespace polysat {
m_overlaps.reset();
c.get_bitvector_suffixes(v, m_overlaps);
std::sort(m_overlaps.begin(), m_overlaps.end(), [&](auto const& x, auto const& y) { return c.size(x.v) < c.size(y.v); });
LOG("Overlaps with v" << v << ":" << m_overlaps);
}
lbool viable::find_viable(pvar v, rational& val1, rational& val2) {
@ -217,6 +217,8 @@ namespace polysat {
}
// TODO check if admitted: layer.entries = e;
m_explain.push_back(e);
if (e->interval.is_full())
return l_false;
auto hi = e->interval.hi_val();
if (hi < val1) {
if (is_zero)
@ -868,6 +870,25 @@ namespace polysat {
return out;
}
std::ostream& viable::display(std::ostream& out) const {
for (unsigned v = 0; v < m_units.size(); ++v) {
bool first = true;
for (auto const& layer : m_units[v].get_layers()) {
if (!layer.entries)
continue;
if (first)
out << "v" << v << ": ";
first = false;
if (layer.bit_width != c.size(v))
out << "width[" << layer.bit_width << "] ";
display_all(out, v, layer.entries, " ");
}
if (!first)
out << "\n";
}
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).

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

@ -158,6 +158,9 @@ namespace polysat {
*/
void ensure_var(pvar v);
std::ostream& display(std::ostream& out) const;
};
}

17
src/sat/smt/polysat_solver.cpp
View file

@ -40,7 +40,8 @@ namespace polysat {
m_intblast(ctx),
m_lemma(ctx.get_manager())
{
// ctx.get_egraph().add_plugin(alloc(euf::bv_plugin, ctx.get_egraph()));
m_bv_plugin = alloc(euf::bv_plugin, ctx.get_egraph());
ctx.get_egraph().add_plugin(m_bv_plugin);
}
unsigned solver::get_bv_size(euf::enode* n) {
@ -120,6 +121,20 @@ namespace polysat {
auto lit = sat::literal(bv, s().value(bv) == l_false);
core.push_back(lit);
}
else if (d.is_fixed_claim()) {
auto const& o = d.fixed();
std::function<void(euf::enode*, euf::enode*)> consume = [&](auto* a, auto* b) {
eqs.push_back({ a, b });
};
explain_fixed(o.v, o.lo, o.hi, o.value, consume);
}
else if (d.is_offset_claim()) {
auto const& offs = d.offset();
std::function<void(euf::enode*, euf::enode*)> consume = [&](auto* a, auto* b) {
eqs.push_back({ a, b });
};
explain_slice(offs.v, offs.w, offs.offset, consume);
}
else {
auto const [v1, v2] = d.eq();
euf::enode* const n1 = var2enode(v1);