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

Sharon & Neta notes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-08-03 16:45:25 -07:00
parent da60abd84b
commit 7ae4e93e86
2 changed files with 20 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -169,10 +169,9 @@ namespace q {
return l_false; return l_false;
if (check_forall_default(q, *qb, *mdl)) if (check_forall_default(q, *qb, *mdl))
return l_false; return l_false;
else { else
return l_undef; return l_undef;
} }
}
if (m_generation_bound >= m_generation_max) if (m_generation_bound >= m_generation_max)
return l_true; return l_true;
m_generation_bound += inc; m_generation_bound += inc;
@ -337,8 +336,8 @@ namespace q {
qb.domain_eqs.reset(); qb.domain_eqs.reset();
var_subst subst(m); var_subst subst(m);
for (auto p : qb.var_args) { for (auto [t, idx] : qb.var_args) {
expr_ref bounds = m_model_fixer.restrict_arg(p.first, p.second); expr_ref bounds = m_model_fixer.restrict_arg(t, idx);
if (m.is_true(bounds)) if (m.is_true(bounds))
continue; continue;
expr_ref vbounds = subst(bounds, qb.vars); expr_ref vbounds = subst(bounds, qb.vars);
@ -393,11 +392,11 @@ namespace q {
if (qb.var_args.empty()) if (qb.var_args.empty())
return; return;
var_subst subst(m); var_subst subst(m);
for (auto p : qb.var_args) { for (auto [t, idx] : qb.var_args) {
expr_ref _term = subst(p.first, qb.vars); expr_ref _term = subst(t, qb.vars);
app_ref term(to_app(_term), m); app_ref term(to_app(_term), m);
expr_ref value = (*m_model)(term->get_arg(p.second)); expr_ref value = (*m_model)(term->get_arg(idx));
m_model_fixer.invert_arg(term, p.second, value, qb.domain_eqs); m_model_fixer.invert_arg(term, idx, value, qb.domain_eqs);
} }
} }

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

@ -111,6 +111,18 @@ namespace q {
add_projection_functions(mdl, f); add_projection_functions(mdl, f);
} }
/**
* we are given f with interpretation:
* if x = v0 and y = w0 then f0
* else if x = v1 and y = w1 then f1
* ...
* Create a new interpretation for f as follows:
* f := f_aux(project1(x), project2(y))
* f_aux uses the original interpretation of f
* project1 sorts the values of v0, v1, ..., and maps arguments below v0 to v0, between v0, v1 to v1 etc.
* project2 sorts values of w0, w1, ... and maps argument y to values w0, w1, ..
*
*/
void model_fixer::add_projection_functions(model& mdl, func_decl* f) { void model_fixer::add_projection_functions(model& mdl, func_decl* f) {
// update interpretation of f so that the graph of f is fully determined by the // update interpretation of f so that the graph of f is fully determined by the
// ground values of its arguments. // ground values of its arguments.