From ea0876b6d6ebe3f97171e88e9d06aaf42bdf5b45 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 21 Feb 2022 18:05:29 -0800 Subject: [PATCH] add lambda definitions during ast translation #5820 Signed-off-by: Nikolaj Bjorner --- src/ast/ast_translation.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/ast/ast_translation.cpp b/src/ast/ast_translation.cpp index c4e32a303..781593b38 100644 --- a/src/ast/ast_translation.cpp +++ b/src/ast/ast_translation.cpp @@ -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_skolem(fi->is_skolem()); 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(), f->get_arity(), new_domain, new_range, 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", tout << f->get_name() << " "; if (fi) tout << *fi; tout << "\n";