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