mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

#5324

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-06-08 12:29:16 -07:00
parent c1ab7987f6
commit c6f0afa008
6 changed files with 34 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/qe/mbp/mbp_arith.cpp
View file

@ -281,9 +281,9 @@ namespace mbp {
obj_map<expr, unsigned> tids;
expr_ref_vector pinned(m);
unsigned j = 0;
TRACE("qe", tout << "vars: " << vars << "\nfmls: " << fmls << "\n";);
for (unsigned i = 0; i < fmls.size(); ++i) {
expr * fml = fmls.get(i);
TRACE("qe", tout << "vars: " << vars << "\nfmls: " << fmls << "\n";
for (expr* f : fmls) tout << mk_pp(f, m) << " := " << model(f) << "\n";);
for (expr* fml : fmls) {
if (!linearize(mbo, eval, fml, fmls, tids)) {
TRACE("qe", tout << "could not linearize: " << mk_pp(fml, m) << "\n";);
fmls[j++] = fml;

2
src/qe/mbp/mbp_plugin.cpp
View file

@ -102,6 +102,8 @@ namespace mbp {
model_evaluator eval(model);
eval.set_expand_array_equalities(true);
TRACE("qe", tout << fmls << "\n";);
DEBUG_CODE(for (expr* fml : fmls) { CTRACE("qe", m.is_false(eval(fml)), tout << mk_pp(fml, m) << " is false\n";); SASSERT(!m.is_false(eval(fml))); });
for (unsigned i = 0; i < fmls.size(); ++i) {
expr* fml = fmls.get(i), * nfml, * f1, * f2, * f3;
SASSERT(m.is_bool(fml));

16
src/sat/smt/euf_model.cpp
View file

@ -229,17 +229,23 @@ namespace euf {
// TODO
}
void solver::model_updated(model_ref& mdl) {
m_values2root.reset();
for (enode* n : m_egraph.nodes())
if (n->is_root() && m_values.get(n->get_expr_id()))
m_values[n->get_expr_id()] = (*mdl)(n->get_expr());
}
obj_map<expr,enode*> const& solver::values2root() {
if (!m_values2root.empty())
return m_values2root;
for (enode* n : m_egraph.nodes())
if (n->is_root() && m_values.get(n->get_expr_id()))
m_values2root.insert(m_values.get(n->get_expr_id()), n);
#if 0
for (auto kv : m_values2root) {
std::cout << mk_pp(kv.m_key, m) << " -> " << bpp(kv.m_value) << "\n";
}
#endif
TRACE("model",
for (auto kv : m_values2root)
tout << mk_pp(kv.m_key, m) << " -> " << bpp(kv.m_value) << "\n";);
return m_values2root;
}

3
src/sat/smt/euf_solver.h
View file

@ -149,7 +149,7 @@ namespace euf {
// model building
expr_ref_vector m_values;
obj_map<expr, enode*> m_values2root;
obj_map<expr, enode*> m_values2root;
bool include_func_interp(func_decl* f);
void register_macros(model& mdl);
void dependencies2values(user_sort& us, deps_t& deps, model_ref& mdl);
@ -370,6 +370,7 @@ namespace euf {
// model construction
void update_model(model_ref& mdl);
obj_map<expr, enode*> const& values2root();
void model_updated(model_ref& mdl);
expr* node2value(enode* n) const;
// diagnostics

12
src/sat/smt/q_mbi.cpp
View file

@ -377,6 +377,7 @@ namespace q {
m_model->reset_eval_cache();
for (app* v : qb.vars)
m_model->register_decl(v->get_decl(), mdl(v));
ctx.model_updated(m_model);
if (qb.var_args.empty())
return;
var_subst subst(m);
@ -416,7 +417,16 @@ namespace q {
expr_ref value = (*m_model)(term);
expr* s = m_model_fixer.invert_app(term, value);
rep.insert(term, s);
eqs.push_back(m.mk_eq(term, s));
expr_ref eq(m.mk_eq(term, s), m);
if (m_model->is_false(eq)) {
IF_VERBOSE(0,
verbose_stream() << mk_pp(s, m) << " := " << (*m_model)(s) << "\n";
verbose_stream() << mk_pp(term, m) << " := " << (*m_model)(term) << "\n";
verbose_stream() << value << " -> " << (*m_model)(ctx.values2root()[value]->get_expr()) << "\n";
verbose_stream() << (*m_model)(s) << " -> " << (*m_model)(ctx.values2root()[(*m_model)(s)]->get_expr()) << "\n";
verbose_stream() << *m_model << "\n";);
}
eqs.push_back(eq);
}
rep(fmls);
fmls.append(eqs);

9
src/sat/smt/q_model_fixer.cpp
View file

@ -218,13 +218,14 @@ namespace q {
expr* model_fixer::invert_app(app* t, expr* value) {
euf::enode* r = nullptr;
auto& v2r = ctx.values2root();
TRACE("q",
tout << "invert-app " << mk_pp(t, m) << " = " << mk_pp(value, m) << "\n";
if (ctx.values2root().find(value, r))
tout << "invert-app " << mk_pp(t, m) << " = " << mk_pp(value, m) << "\n";
if (v2r.find(value, r))
tout << "inverse " << mk_pp(r->get_expr(), m) << "\n";
ctx.display(tout);
ctx.display(tout);
);
if (ctx.values2root().find(value, r))
if (v2r.find(value, r))
return r->get_expr();
return value;
}