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