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