Method mk_lambda

src/ast/ast.cpp:2453–2465

}

quantifier * ast_manager::mk_lambda(unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body) {
    SASSERT(body);
    unsigned sz               = quantifier::get_obj_size(num_decls, 0, 0);
    void * mem                = allocate_node(sz);
    array_util autil(*this);
    sort* s = autil.mk_array_sort(num_decls, decl_sorts, body->get_sort());
    quantifier * new_node = new (mem) quantifier(num_decls, decl_sorts, decl_names, body, s);
    quantifier * r = register_node(new_node);
    if (m_trace_stream && r == new_node) {
        trace_quant(*m_trace_stream, r);
    }
    return r;
}


// Return true if the patterns of q are the given ones.