mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-16 19:06:17 +00:00
Code Activity

add lambda definitions during ast translation #5820

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-02-21 18:05:29 -08:00
parent d06c51d517
commit ea0876b6d6
1 changed files with 8 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/ast/ast_translation.cpp
View file

@ -170,12 +170,20 @@ void ast_translation::mk_func_decl(func_decl * f, frame & fr) {
new_fi.set_injective(fi->is_injective()); new_fi.set_injective(fi->is_injective());
new_fi.set_skolem(fi->is_skolem()); new_fi.set_skolem(fi->is_skolem());
new_fi.set_idempotent(fi->is_idempotent()); new_fi.set_idempotent(fi->is_idempotent());
new_fi.set_lambda(fi->is_lambda());
new_f = m_to_manager.mk_func_decl(f->get_name(), new_f = m_to_manager.mk_func_decl(f->get_name(),
f->get_arity(), f->get_arity(),
new_domain, new_domain,
new_range, new_range,
new_fi); new_fi);
if (new_fi.is_lambda()) {
quantifier* q = from().is_lambda_def(f);
ast_translation tr(from(), to());
quantifier* new_q = tr(q);
to().add_lambda_def(new_f, new_q);
}
} }
TRACE("ast_translation", TRACE("ast_translation",
tout << f->get_name() << " "; if (fi) tout << *fi; tout << "\n"; tout << f->get_name() << " "; if (fi) tout << *fi; tout << "\n";