1 /*++ 2 Copyright (c) 2018 Microsoft Corporation 3 4 Module Name: 5 6 recfun_replace.h 7 8 Abstract: 9 10 replace function for recfun. 11 recfun_decl_plugin relies on being able to do expression replacement. 12 It uses expr_safe_replace from ast/rewriter, which depends on ast. 13 To break the dependency cycle we hoist the relevant functionality into 14 an argument to functionality exposed by recfun::set_definition 15 16 Author: 17 18 Nikolaj Bjorner (nbjorner) 2018-11-01 19 20 Revision History: 21 22 23 --*/ 24 25 #pragma once 26 27 #include "ast/recfun_decl_plugin.h" 28 #include "ast/rewriter/expr_safe_replace.h" 29 30 class recfun_replace : public recfun::replace { 31 ast_manager& m; 32 expr_safe_replace m_replace; 33 public: recfun_replace(ast_manager & m)34 recfun_replace(ast_manager& m): m(m), m_replace(m) {} ~recfun_replace()35 ~recfun_replace() override {} reset()36 void reset() override { m_replace.reset(); } insert(expr * s,expr * t)37 void insert(expr* s, expr* t) override { m_replace.insert(s, t); } operator()38 expr_ref operator()(expr* e) override { expr_ref r(m); m_replace(e, r); return r; } 39 }; 40 41