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