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

bugbash

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-09 14:15:25 -08:00
parent f34e55e86e
commit 21711a14f5
7 changed files with 56 additions and 42 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -92,7 +92,7 @@ namespace euf {
auto v1 = get_value(hi);
auto v2 = get_value(lo);
auto v3 = v2 + v1 * rational::power_of_two(width(lo));
return mk_value(v3, width(lo) + width(lo));
return mk_value(v3, width(lo) + width(hi));
}
enode* bv_plugin::mk_value(rational const& v, unsigned sz) {
@ -261,6 +261,8 @@ namespace euf {
TRACE("bv", tout << "register " << g.bpp(n) << "\n");
auto& i = info(n);
i.value = n;
if (n->get_expr_id() == 255 && false)
verbose_stream() << g.bpp(n) << "\n";
enode* a, * b;
if (is_concat(n, a, b)) {
i.hi = a;
@ -291,7 +293,8 @@ namespace euf {
SASSERT(ub - lb + 1 == width(r));
if (lb == lo && ub == hi)
return;
slice_info& i = info(r);
slice_info const& i = info(r);
if (!i.lo) {
if (lo > lb) {
split(r, lo - lb);
@ -349,6 +352,7 @@ namespace euf {
SASSERT(!ys.empty());
auto x = xs.back();
auto y = ys.back();
TRACE("bv", tout << "merge " << g.bpp(x) << " " << g.bpp(y) << "\n");
if (unfold_sub(x, xs))
continue;
else if (unfold_sub(y, ys))
@ -391,9 +395,8 @@ namespace euf {
SASSERT(0 < cut && cut < w);
enode* hi = mk_extract(n, cut, w - 1);
enode* lo = mk_extract(n, 0, cut - 1);
auto& i = info(n);
if (!i.value)
i.value = n;
auto& i = info(n);
i.value = n;
i.hi = hi;
i.lo = lo;
i.cut = cut;
@ -542,8 +545,7 @@ namespace euf {
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";
out << g.bpp(i.value) << " cut " << i.cut << " lo " << g.bpp(i.lo) << " hi " << g.bpp(i.hi) << "\n";
return out;
}
}

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

@ -46,7 +46,7 @@ namespace euf {
std::function<void(enode*)> m_ensure_th_var;
bool is_concat(enode* n) const { return bv.is_concat(n->get_expr()); }
bool is_concat(enode* n, enode*& a, enode*& b) { return is_concat(n) && (a = n->get_arg(0), b = n->get_arg(1), true); }
bool is_concat(enode* n, enode*& a, enode*& b) { return is_concat(n) && n->num_args() == 2 && (a = n->get_arg(0), b = n->get_arg(1), true); }
bool is_extract(enode* n, unsigned& lo, unsigned& hi) { expr* body; return bv.is_extract(n->get_expr(), lo, hi, body); }
bool is_extract(enode* n) const { return bv.is_extract(n->get_expr()); }
unsigned width(enode* n) const { return bv.get_bv_size(n->get_expr()); }
@ -59,7 +59,6 @@ namespace euf {
bool is_value(enode* n) { return n->get_root()->interpreted(); }
rational get_value(enode* n) { rational val; VERIFY(bv.is_numeral(n->get_interpreted()->get_expr(), val)); return val; }
slice_info& info(enode* n) { unsigned id = n->get_id(); m_info.reserve(id + 1); return m_info[id]; }
slice_info& root_info(enode* n) { unsigned id = n->get_root_id(); m_info.reserve(id + 1); return m_info[id]; }
bool has_sub(enode* n) { return !!info(n).lo; }
enode* sub_lo(enode* n) { return info(n).lo; }
enode* sub_hi(enode* n) { return info(n).hi; }

2
src/ast/euf/euf_egraph.h
View file

@ -218,7 +218,7 @@ namespace euf {
// plugin related methods
void push_plugin_undo(unsigned th_id) { m_updates.push_back(update_record(th_id, update_record::plugin_undo())); }
void push_merge(enode* a, enode* b, justification j) { m_to_merge.push_back({ a, b, j }); }
void push_merge(enode* a, enode* b, justification j) { SASSERT(a->get_sort() == b->get_sort()); m_to_merge.push_back({ a, b, j }); }
void push_merge(enode* a, enode* b, bool comm) { m_to_merge.push_back({ a, b, comm }); }
void propagate_plugins();

2
src/sat/smt/polysat/ule_constraint.cpp
View file

@ -228,7 +228,7 @@ namespace polysat {
lhs *= x;
SASSERT(lhs.leading_coefficient().is_power_of_two());
}
TRACE("bv", tout << "simplified " << lhs << " <= " << rhs << "\n");
TRACE("bv_verbose", tout << "simplified " << lhs << " <= " << rhs << "\n");
} // simplify_impl
}

31
src/sat/smt/polysat_internalize.cpp
View file

@ -666,19 +666,28 @@ namespace polysat {
// e = hi lo
// hi = 0 <=> e < 2^|lo|
void solver::axioms_for_concat(app* e) {
if (bv.is_concat(e) && e->get_num_args() == 2) {
expr* hi = e->get_arg(0);
expr* lo = e->get_arg(1);
auto sz_e = bv.get_bv_size(e);
SASSERT(bv.is_concat(e));
SASSERT(e->get_num_args() > 0);
sat::literal_vector neqs;
verbose_stream() << mk_pp(e, m) << "\n";
expr* hi = e->get_arg(e->get_num_args() - 1);
auto sz_e = bv.get_bv_size(e);
auto sz_h = bv.get_bv_size(hi);
auto eq0 = eq_internalize(hi, bv.mk_numeral(0, sz_h));
auto sz_eqs = sz_h;
neqs.push_back(~eq0);
for (unsigned i = e->get_num_args() - 1; i-- > 0; ) {
auto gtlo = ~mk_literal(bv.mk_ule(bv.mk_numeral(rational::power_of_two(sz_e - sz_eqs), sz_e), e));
neqs.push_back(gtlo);
add_axiom("hi = 0 => concat(hi, lo) < 2^|lo|", neqs, false);
neqs.pop_back();
for (auto neq : neqs)
add_axiom("concat(hi,lo) < 2^|lo| => hi = 0", {~neq, ~gtlo}); // hi = 0 or e >= 2^|lo|
expr* lo = e->get_arg(i);
auto sz_l = bv.get_bv_size(lo);
auto sz_h = bv.get_bv_size(hi);
auto name = "concat";
auto eq0 = eq_internalize(hi, bv.mk_numeral(0, sz_h));
auto gtlo = ~mk_literal(bv.mk_ule(bv.mk_numeral(rational::power_of_two(sz_l), sz_e), e));
equiv_axiom(name, eq0, gtlo);
neqs.push_back(~eq_internalize(lo, bv.mk_numeral(0, sz_l)));
sz_eqs += sz_l;
}
else
NOT_IMPLEMENTED_YET();
}
void solver::internalize_concat(app* e) {

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

@ -359,37 +359,39 @@ namespace polysat {
return true;
}
void solver::add_axiom(char const* name, std::initializer_list<sat::literal> const& clause) {
void solver::add_axiom(char const* name, sat::literal const* begin, sat::literal const* end, bool is_redundant) {
++m_stats.m_num_axioms;
bool is_redundant = false;
sat::literal_vector lits;
proof_hint* hint = nullptr;
if (ctx.use_drat()) {
for (auto lit : clause)
lits.push_back(~lit);
hint = mk_proof_hint(name, lits, {});
for (auto& lit : lits)
lit.neg();
}
else {
for (auto lit : clause)
lits.push_back(lit);
}
validate_axiom(lits);
unsigned j = 0;
for (auto lit : lits) {
validate_axiom(sat::literal_vector(static_cast<unsigned>(end - begin), begin));
for (auto it = begin; it != end; ++it) {
auto lit = *it;
if (s().value(lit) == l_true && s().lvl(lit) == 0)
return;
if (s().value(lit) == l_false && s().lvl(lit) == 0)
continue;
lits[j++] = lit;
lits.push_back(lit);
}
lits.shrink(j);
proof_hint* hint = nullptr;
if (ctx.use_drat()) {
sat::literal_vector core;
for (auto lit : lits)
core.push_back(~lit);
hint = mk_proof_hint(name, core, {});
}
IF_VERBOSE(1, display_clause(name, verbose_stream(), lits));
s().add_clause(lits.size(), lits.data(), sat::status::th(is_redundant, get_id(), hint));
}
void solver::add_axiom(char const* name, sat::literal_vector const& clause, bool is_redundant) {
add_axiom(name, clause.begin(), clause.end(), is_redundant);
}
void solver::add_axiom(char const* name, std::initializer_list<sat::literal> const& clause) {
add_axiom(name, clause.begin(), clause.end(), false);
}
void solver::equiv_axiom(char const* name, sat::literal a, sat::literal b) {
add_axiom(name, { a, ~b });
add_axiom(name, { ~a, b });

2
src/sat/smt/polysat_solver.h
View file

@ -227,6 +227,8 @@ namespace polysat {
}
void add_axiom(char const* name, std::initializer_list<sat::literal> const& clause);
void add_axiom(char const* name, sat::literal_vector const& clause, bool is_redundant);
void add_axiom(char const* name, sat::literal const* begin, sat::literal const* end, bool is_redundant);
void equiv_axiom(char const* name, sat::literal a, sat::literal b);
void validate_propagate(sat::literal lit, sat::literal_vector const& core, euf::enode_pair_vector const& eqs);