1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6     expr_safe_replace.h
7 
8 Abstract:
9 
10     Version of expr_replace/expr_substitution that is safe for quantifiers.
11 
12 
13 Author:
14 
15     Nikolaj Bjorner (nbjorner) 2012-11-30
16 
17 Revision History:
18 
19 
20 --*/
21 
22 #pragma once
23 
24 #include "ast/ast.h"
25 #include <unordered_map>
26 
27 class expr_safe_replace {
28     ast_manager& m;
29     expr_ref_vector m_src;
30     expr_ref_vector m_dst;
31     ptr_vector<expr> m_todo, m_args;
32     expr_ref_vector m_refs;
33     std::unordered_map<expr*,expr*> m_cache;
34 
35 public:
expr_safe_replace(ast_manager & m)36     expr_safe_replace(ast_manager& m): m(m), m_src(m), m_dst(m), m_refs(m) {}
37 
38     void insert(expr* src, expr* dst);
39 
operator()40     void operator()(expr_ref& e) { (*this)(e.get(), e); }
41 
42     void operator()(expr* src, expr_ref& e);
43 
44     void operator()(expr_ref_vector& es);
45 
46     void apply_substitution(expr* s, expr* def, expr_ref& t);
47 
48     void reset();
49 
empty()50     bool empty() const { return m_src.empty(); }
51 };
52 
53