mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 12:51:22 +00:00
Code Activity

test mbi

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-10-30 17:03:04 -07:00
parent a764d528a1
commit fb6e7e146b
3 changed files with 22 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/sat/smt/arith_internalize.cpp
View file

@ -119,7 +119,6 @@ namespace arith {
literal lit = eq_internalize(n, e); literal lit = eq_internalize(n, e);
add_unit(lit); add_unit(lit);
} }
} }
lpvar solver::add_const(int c, lpvar& var, bool is_int) { lpvar solver::add_const(int c, lpvar& var, bool is_int) {
@ -299,6 +298,11 @@ namespace arith {
st.to_ensure_var().reset(); st.to_ensure_var().reset();
} }
void solver::eq_internalized(enode* n) {
internalize_term(n->get_arg(0)->get_expr());
internalize_term(n->get_arg(1)->get_expr());
}
bool solver::internalize_atom(expr* atom) { bool solver::internalize_atom(expr* atom) {
TRACE("arith", tout << mk_pp(atom, m) << "\n";); TRACE("arith", tout << mk_pp(atom, m) << "\n";);
SASSERT(!ctx.get_enode(atom)); SASSERT(!ctx.get_enode(atom));

1
src/sat/smt/arith_solver.h
View file

@ -432,6 +432,7 @@ namespace arith {
void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override; void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
sat::literal internalize(expr* e, bool sign, bool root, bool learned) override; sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
void internalize(expr* e, bool redundant) override; void internalize(expr* e, bool redundant) override;
void eq_internalized(euf::enode* n) override;
void apply_sort_cnstr(euf::enode* n, sort* s) override {} void apply_sort_cnstr(euf::enode* n, sort* s) override {}
bool is_shared(theory_var v) const override; bool is_shared(theory_var v) const override;
lbool get_phase(bool_var v) override; lbool get_phase(bool_var v) override;

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

@ -203,14 +203,25 @@ namespace q {
expr_ref mbqi::solver_project(model& mdl, q_body& qb) { expr_ref mbqi::solver_project(model& mdl, q_body& qb) {
for (app* v : qb.vars) for (app* v : qb.vars)
m_model->register_decl(v->get_decl(), mdl(v)); m_model->register_decl(v->get_decl(), mdl(v));
TRACE("q",
tout << "Project\n";
tout << *m_model << "\n";
tout << qb.vbody << "\n";
tout << "model of projection\n" << mdl << "\n";);
expr_ref_vector fmls(qb.vbody); expr_ref_vector fmls(qb.vbody);
app_ref_vector vars(qb.vars); app_ref_vector vars(qb.vars);
fmls.append(qb.domain_eqs); fmls.append(qb.domain_eqs);
TRACE("q",
tout << "Project\n";
tout << *m_model << "\n";
tout << fmls << "\n";
tout << "model of projection\n" << mdl << "\n";
tout << "var args: " << qb.var_args.size() << "\n";
for (expr* f : fmls)
if (m_model->is_false(f))
tout << mk_pp(f, m) << " := false\n";
);
//
// TBD: need to compute projection based on eliminate_nested_vars,
// but apply it based on original formulas, or add constraints that
// nested variable occurrences are equal to their subsitutions.
// The result may not be a proper projection.
//
eliminate_nested_vars(fmls, qb); eliminate_nested_vars(fmls, qb);
mbp::project_plugin proj(m); mbp::project_plugin proj(m);
proj.extract_literals(*m_model, vars, fmls); proj.extract_literals(*m_model, vars, fmls);
@ -220,17 +231,6 @@ namespace q {
if (p) if (p)
(*p)(*m_model, vars, fmls); (*p)(*m_model, vars, fmls);
} }
#if 0
// should be redundant
expr_safe_replace esubst(m);
for (app* v : qb.vars) {
expr_ref val = assign_value(*m_model, v);
if (!val)
return expr_ref(m);
esubst.insert(v, val);
}
esubst(fmls);
#endif
return mk_and(fmls); return mk_and(fmls);
} }