mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

add notes about quantifier ordering, bypass

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-21 16:15:02 -08:00
parent edffdf857c
commit 70b344513a
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/tactic/generic_model_converter.cpp
View file

@ -102,9 +102,10 @@ struct min_app_idx_proc {
void generic_model_converter::operator()(expr_ref& fml) { void generic_model_converter::operator()(expr_ref& fml) {
min_app_idx_proc min_proc(m_first_idx); min_app_idx_proc min_proc(m_first_idx);
for_each_expr(min_proc, fml); for_each_expr(min_proc, fml);
unsigned min_idx = min_proc.m_min;
if (min_idx == UINT_MAX) return;
expr_ref_vector fmls(m); expr_ref_vector fmls(m);
fmls.push_back(fml); fmls.push_back(fml);
unsigned min_idx = min_proc.m_min;
for (unsigned i = m_add_entries.size(); i-- > min_idx;) { for (unsigned i = m_add_entries.size(); i-- > min_idx;) {
entry const& e = m_add_entries[i]; entry const& e = m_add_entries[i];
unsigned arity = e.m_f->get_arity(); unsigned arity = e.m_f->get_arity();
@ -120,6 +121,7 @@ void generic_model_converter::operator()(expr_ref& fml) {
names.push_back(symbol(i)); names.push_back(symbol(i));
args.push_back(m.mk_var(i, sorts.back())); args.push_back(m.mk_var(i, sorts.back()));
} }
// TBD: check if order is correct with respect to quantifier binding ordering
expr_ref lhs(m.mk_app(e.m_f, arity, args.c_ptr()), m); expr_ref lhs(m.mk_app(e.m_f, arity, args.c_ptr()), m);
expr_ref body(m.mk_eq(lhs, e.m_def), m); expr_ref body(m.mk_eq(lhs, e.m_def), m);
fmls.push_back(m.mk_forall(arity, sorts.c_ptr(), names.c_ptr(), body)); fmls.push_back(m.mk_forall(arity, sorts.c_ptr(), names.c_ptr(), body));