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

bugfixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-28 17:36:42 -08:00
parent bd93379346
commit 91b9d78cd3
8 changed files with 81 additions and 51 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -74,13 +74,10 @@ then t1 = t2 iff t1 ~ t2 in the E-graph.
TODO: Is saturation for (7) overkill for the purpose of canonization?
TODO: revisit re-entrancy during register_node. It can be called when creating internal extract terms.
Instead of allowing re-entrancy we can accumulate nodes that are registered during recursive calls
and have the main call perform recursive slicing.
--*/
#include "ast/ast_pp.h"
#include "ast/euf/euf_bv_plugin.h"
#include "ast/euf/euf_egraph.h"
@ -91,11 +88,11 @@ namespace euf {
bv(g.get_manager())
{}
enode* bv_plugin::mk_value_concat(enode* a, enode* b) {
auto v1 = get_value(a);
auto v2 = get_value(b);
auto v3 = v1 + v2 * power(rational(2), width(a));
return mk_value(v3, width(a) + width(b));
enode* bv_plugin::mk_value_concat(enode* hi, enode* lo) {
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));
}
enode* bv_plugin::mk_value(rational const& v, unsigned sz) {
@ -157,7 +154,7 @@ namespace euf {
}
}
// enforce concat(v1, v2) = v2*2^|v1| + v1
// enforce concat(v1, v2) = v1*2^|v2| + v2
void bv_plugin::propagate_values(enode* x) {
if (!is_value(x))
return;
@ -171,9 +168,9 @@ namespace euf {
if (is_concat(sib, a, b)) {
if (!is_value(a) || !is_value(b)) {
auto val = get_value(x);
auto v1 = mod2k(val, width(a));
auto v2 = machine_div2k(val, width(a));
push_merge(mk_concat(mk_value(v1, width(a)), mk_value(v2, width(b))), x->get_interpreted());
auto val_a = machine_div2k(val, width(b));
auto val_b = mod2k(val, width(b));
push_merge(mk_concat(mk_value(val_a, width(a)), mk_value(val_b, width(b))), x->get_interpreted());
}
}
}
@ -205,18 +202,18 @@ namespace euf {
if (is_extract(p1, lo_, hi_) && lo_ == lo && hi_ == hi && p1->get_arg(0)->get_root() == arg_r)
return;
// add the axiom instead of merge(p, mk_extract(arg, lo, hi)), which would require tracking justifications
push_merge(mk_concat(mk_extract(arg, lo, mid), mk_extract(arg, mid + 1, hi)), mk_extract(arg, lo, hi));
push_merge(mk_concat(mk_extract(arg, mid + 1, hi), mk_extract(arg, lo, mid)), mk_extract(arg, lo, hi));
};
auto propagate_left = [&](enode* b) {
TRACE("bv", tout << "propagate-left " << g.bpp(b) << "\n");
auto propagate_above = [&](enode* b) {
TRACE("bv", tout << "propagate-above " << g.bpp(b) << "\n");
for (enode* sib : enode_class(b))
if (is_extract(sib, lo2, hi2) && sib->get_arg(0)->get_root() == arg_r && hi1 + 1 == lo2)
ensure_concat(lo1, hi1, hi2);
};
auto propagate_right = [&](enode* a) {
TRACE("bv", tout << "propagate-right " << g.bpp(a) << "\n");
auto propagate_below = [&](enode* a) {
TRACE("bv", tout << "propagate-below " << g.bpp(a) << "\n");
for (enode* sib : enode_class(a))
if (is_extract(sib, lo2, hi2) && sib->get_arg(0)->get_root() == arg_r && hi2 + 1 == lo1)
ensure_concat(lo2, hi2, hi1);
@ -225,9 +222,9 @@ namespace euf {
for (enode* p : enode_parents(n)) {
if (is_concat(p, a, b)) {
if (a->get_root() == n_r)
propagate_left(b);
propagate_below(b);
if (b->get_root() == n_r)
propagate_right(a);
propagate_above(a);
}
}
}
@ -263,9 +260,9 @@ namespace euf {
i.value = n;
enode* a, * b;
if (is_concat(n, a, b)) {
i.lo = a;
i.hi = b;
i.cut = width(a);
i.hi = a;
i.lo = b;
i.cut = width(b);
push_undo_split(n);
}
unsigned lo, hi;
@ -328,12 +325,20 @@ namespace euf {
hi += lo1;
n = n->get_arg(0);
}
if (n->interpreted()) {
auto v = get_value(n);
if (lo > 0)
v = div(v, rational::power_of_two(lo));
if (hi + 1 != width(n))
v = mod(v, rational::power_of_two(hi + 1));
return mk(bv.mk_numeral(v, hi - lo + 1), 0, nullptr);
}
return mk(bv.mk_extract(hi, lo, n->get_expr()), 1, &n);
}
enode* bv_plugin::mk_concat(enode* lo, enode* hi) {
enode* args[2] = { lo, hi };
return mk(bv.mk_concat(lo->get_expr(), hi->get_expr()), 2, args);
enode* bv_plugin::mk_concat(enode* hi, enode* lo) {
enode* args[2] = { hi, lo };
return mk(bv.mk_concat(hi->get_expr(), lo->get_expr()), 2, args);
}
void bv_plugin::merge(enode_vector& xs, enode_vector& ys, justification dep) {
@ -390,7 +395,7 @@ namespace euf {
i.lo = lo;
i.cut = cut;
push_undo_split(n);
push_merge(mk_concat(lo, hi), n);
push_merge(mk_concat(hi, lo), n);
}
void bv_plugin::sub_slices(enode* n, std::function<bool(enode*, unsigned)>& consumer) {

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

@ -53,8 +53,8 @@ namespace euf {
unsigned width(enode* n) const { return bv.get_bv_size(n->get_expr()); }
enode* mk_extract(enode* n, unsigned lo, unsigned hi);
enode* mk_concat(enode* lo, enode* hi);
enode* mk_value_concat(enode* lo, enode* hi);
enode* mk_concat(enode* hi, enode* lo);
enode* mk_value_concat(enode* hi, enode* lo);
enode* mk_value(rational const& v, unsigned sz);
unsigned width(enode* n) { return bv.get_bv_size(n->get_expr()); }
bool is_value(enode* n) { return n->get_root()->interpreted(); }

1
src/ast/euf/euf_plugin.cpp
View file

@ -26,6 +26,7 @@ namespace euf {
}
void plugin::push_merge(enode* a, enode* b, justification j) {
TRACE("euf", tout << "push-merge " << g.bpp(a) << " == " << g.bpp(b) << " " << j << "\n");
g.push_merge(a, b, j);
}

19
src/sat/smt/intblast_solver.cpp
View file

@ -220,7 +220,8 @@ namespace intblast {
m_solver->assert_expr(a.mk_lt(v, a.mk_int(b)));
}
IF_VERBOSE(10, verbose_stream() << "check\n";
IF_VERBOSE(2, verbose_stream() << "check\n" << original_es << "\n");
IF_VERBOSE(3, verbose_stream() << "check\n";
m_solver->display(verbose_stream());
verbose_stream() << es << "\n");
@ -230,14 +231,18 @@ namespace intblast {
IF_VERBOSE(2, verbose_stream() << "(sat.intblast :result " << r << ")\n");
if (r == l_true) {
model_ref mdl;
m_solver->get_model(mdl);
verbose_stream() << original_es << "\n";
verbose_stream() << *mdl << "\n";
verbose_stream() << es << "\n";
m_solver->display(verbose_stream());
IF_VERBOSE(0,
model_ref mdl;
m_solver->get_model(mdl);
verbose_stream() << original_es << "\n";
verbose_stream() << *mdl << "\n";
verbose_stream() << es << "\n";
m_solver->display(verbose_stream()););
SASSERT(false);
}
m_solver = nullptr;
return r;
}

5
src/sat/smt/polysat/constraints.cpp
View file

@ -75,7 +75,10 @@ namespace polysat {
if (!l.hi().is_one())
return false;
v = l.var();
val = -l.lo().val();
if (l.lo().val() == 0)
val = 0;
else
val = l.manager().max_value() + 1 - l.lo().val();
return true;
}

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

@ -172,8 +172,10 @@ namespace polysat {
s.set_conflict(m_viable.explain(), "viable-conflict");
return sat::check_result::CR_CONTINUE;
case find_t::singleton: {
TRACE("bv", tout << "check-propagate v" << m_var << " := " << m_value << "\n");
auto d = s.propagate(m_constraints.eq(var2pdd(m_var), m_value), m_viable.explain(), "viable-propagate");
auto p = var2pdd(m_var).mk_var(m_var);
auto sc = m_constraints.eq(p, m_value);
TRACE("bv", tout << "check-propagate v" << m_var << " := " << m_value << " " << sc << "\n");
auto d = s.propagate(sc, m_viable.explain(), "viable-propagate");
propagate_assignment(m_var, m_value, d);
return sat::check_result::CR_CONTINUE;
}
@ -297,8 +299,6 @@ namespace polysat {
return;
v = w;
}
if (v != null_var)
verbose_stream() << "propagate activation " << v << " " << sc << " " << dep << "\n";
if (v != null_var && !m_viable.add_unitary(v, idx.id))
s.set_conflict(m_viable.explain(), "viable-conflict");
}

33
src/sat/smt/polysat_model.cpp
View file

@ -23,16 +23,29 @@ Author:
namespace polysat {
void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) {
auto p = expr2pdd(n->get_expr());
rational val;
if (!m_core.try_eval(p, val)) {
ctx.s().display(verbose_stream());
verbose_stream() << ctx.bpp(n) << " := " << p << "\n";
UNREACHABLE();
void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) {
expr_ref value(m);
if (n->interpreted())
value = n->get_expr();
else if (n->get_decl() && n->get_decl()->get_family_id() == bv.get_family_id()) {
bv_rewriter rw(m);
expr_ref_vector args(m);
for (auto arg : euf::enode_args(n))
args.push_back(values.get(arg->get_root_id()));
rw.mk_app(n->get_decl(), args.size(), args.data(), value);
}
VERIFY(m_core.try_eval(p, val));
values.set(n->get_root_id(), bv.mk_numeral(val, get_bv_size(n)));
else {
auto p = expr2pdd(n->get_expr());
rational val;
if (!m_core.try_eval(p, val)) {
ctx.s().display(verbose_stream());
verbose_stream() << ctx.bpp(n) << " := " << p << "\n";
UNREACHABLE();
}
VERIFY(m_core.try_eval(p, val));
value = bv.mk_numeral(val, get_bv_size(n));
}
values.set(n->get_root_id(), value);
}
bool solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {
@ -87,12 +100,14 @@ namespace polysat {
auto r = m_intblast.check_propagation(lit, core, eqs);
VERIFY (r != l_true);
}
void solver::validate_conflict(sat::literal_vector const& core, euf::enode_pair_vector const& eqs) {
if (!ctx.get_config().m_core_validate)
return;
auto r = m_intblast.check_core(core, eqs);
VERIFY (r != l_true);
}
void solver::validate_axiom(sat::literal_vector const& clause) {
if (!ctx.get_config().m_core_validate)
return;

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

@ -114,6 +114,7 @@ namespace polysat {
hint = mk_proof_hint(hint_info);
auto ex = euf::th_explain::conflict(*this, lits, eqs, hint);
TRACE("bv", ex->display(tout << "conflict: ") << "\n"; s().display(tout));
validate_conflict(lits, eqs);
ctx.set_conflict(ex);
}
@ -217,7 +218,7 @@ namespace polysat {
auto d = dependency(eq.var());
auto id = eq_constraint(p, q, d);
TRACE("bv", tout << eq << " := " << s().value(eq) << " @" << s().scope_lvl() << "\n");
m_core.assign_eh(id, false, s().lvl(eq));
m_core.assign_eh(id, true, s().lvl(eq));
}
// Core uses the propagate callback to add unit propagations to the trail.