1 /*++
2 Copyright (c) 2019 Microsoft Corporation
3 
4 Module Name:
5 
6     func_decl_replace.h
7 
8 Abstract:
9 
10     Replace functions in expressions.
11 
12 Author:
13 
14     Nikolaj Bjorner (nbjorner) 2019-03-28
15 
16 Revision History:
17 
18 
19 --*/
20 
21 #pragma once
22 
23 #include "ast/ast.h"
24 
25 class func_decl_replace {
26     ast_manager& m;
27     obj_map<func_decl, func_decl*> m_subst;
28     obj_map<expr, expr*> m_cache;
29     ptr_vector<expr>     m_todo, m_args;
30     expr_ref_vector      m_refs;
31     func_decl_ref_vector m_funs;
32 
33 public:
func_decl_replace(ast_manager & m)34     func_decl_replace(ast_manager& m): m(m), m_refs(m), m_funs(m) {}
35 
insert(func_decl * src,func_decl * dst)36     void insert(func_decl* src, func_decl* dst) { m_subst.insert(src, dst); m_funs.push_back(src), m_funs.push_back(dst); }
37 
38     expr_ref operator()(expr* e);
39 
40     void reset();
41 
empty()42     bool empty() const { return m_subst.empty(); }
43 };
44 
45