1 /*++ 2 Copyright (c) 2010 Microsoft Corporation 3 4 Module Name: 5 6 expr_functors.h 7 8 Abstract: 9 10 Functors on expressions. 11 12 Author: 13 14 Nikolaj Bjorner (nbjorner) 2010-02-19 15 16 Revision History: 17 18 Hoisted from quant_elim. 19 20 --*/ 21 22 #pragma once 23 24 #include "ast/ast.h" 25 #include "ast/expr_map.h" 26 27 class i_expr_pred { 28 public: 29 virtual bool operator()(expr* e) = 0; ~i_expr_pred()30 virtual ~i_expr_pred() {} 31 }; 32 33 34 class i_sort_pred { 35 public: 36 virtual bool operator()(sort* s) = 0; ~i_sort_pred()37 virtual ~i_sort_pred() {} 38 }; 39 40 41 /** 42 \brief Memoizing predicate functor on sub-expressions. 43 44 The class is initialized with a predicate 'p' on expressions. 45 46 The class is memoizing. 47 48 */ 49 50 class check_pred { 51 i_expr_pred& m_pred; 52 ast_mark m_pred_holds; 53 ast_mark m_visited; 54 expr_ref_vector m_refs; 55 bool m_check_quantifiers; 56 public: 57 check_pred(i_expr_pred& p, ast_manager& m, bool check_quantifiers = true) : m_pred(p)58 m_pred(p), m_refs(m), m_check_quantifiers(check_quantifiers) {} 59 60 bool operator()(expr* e); 61 reset()62 void reset() { m_pred_holds.reset(); m_visited.reset(); m_refs.reset(); } 63 64 private: 65 void visit(expr* e); 66 }; 67 68 /** 69 \brief Determine if expression 'e' or vector of expressions 'v' contains the app x 70 */ 71 72 class contains_app { 73 class pred : public i_expr_pred { 74 app* m_x; 75 public: pred(app * x)76 pred(app* x) : m_x(x) {} operator()77 bool operator()(expr* e) override { 78 return m_x == e; 79 } 80 }; 81 app_ref m_x; 82 pred m_pred; 83 check_pred m_check; 84 85 public: contains_app(ast_manager & m,app * x)86 contains_app(ast_manager& m, app* x) : 87 m_x(x, m), m_pred(x), m_check(m_pred, m) {} 88 operator()89 bool operator()(expr* e) { 90 return m_check(e); 91 } 92 operator()93 bool operator()(expr_ref_vector const& v) { 94 return (*this)(v.size(), v.c_ptr()); 95 } 96 97 bool operator()(unsigned size, expr* const* es); 98 x()99 app* x() const { return m_x; } 100 101 }; 102 103 /** 104 \brief Base class of functor that applies map to expressions. 105 */ 106 class map_proc { 107 protected: 108 ast_manager& m; 109 expr_map m_map; 110 ptr_vector<expr> m_args; 111 public: map_proc(ast_manager & m)112 map_proc(ast_manager& m): 113 m(m), 114 m_map(m) 115 {} 116 reset()117 void reset() { m_map.reset(); } 118 visit(var * e)119 void visit(var* e) { m_map.insert(e, e, nullptr); } 120 121 void visit(quantifier* e); 122 123 void reconstruct(app* a); 124 125 expr* get_expr(expr* e); 126 127 }; 128 129 130