1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3 
4 Module Name:
5 
6     num_occurs.cpp
7 
8 Abstract:
9 
10     <abstract>
11 
12 Author:
13 
14     Leonardo de Moura (leonardo) 2008-01-27.
15 
16 Revision History:
17 
18 --*/
19 
20 #include "ast/num_occurs.h"
21 
process(expr * t,expr_fast_mark1 & visited)22 void num_occurs::process(expr * t, expr_fast_mark1 & visited) {
23     ptr_buffer<expr, 128> stack;
24 
25 #define VISIT(ARG) {                                                                                    \
26         if (!m_ignore_ref_count1 || ARG->get_ref_count() > 1) {                                         \
27             m_num_occurs.insert_if_not_there(ARG, 0)++; \
28         }                                                                                               \
29         if (!visited.is_marked(ARG)) {                                                                  \
30             visited.mark(ARG, true);                                                                    \
31             stack.push_back(ARG);                                                                       \
32         }                                                                                               \
33     }
34 
35     VISIT(t);
36 
37     while (!stack.empty()) {
38         expr * t = stack.back();
39         stack.pop_back();
40         unsigned j;
41         switch (t->get_kind()) {
42         case AST_APP:
43             j = to_app(t)->get_num_args();
44             while (j > 0) {
45                 --j;
46                 expr * arg = to_app(t)->get_arg(j);
47                 VISIT(arg);
48             }
49             break;
50         case AST_QUANTIFIER:
51             if (!m_ignore_quantifiers) {
52                 expr * child = to_quantifier(t)->get_expr();
53                 VISIT(child);
54             }
55             break;
56         default:
57             break;
58         }
59     }
60 }
61 
validate()62 void num_occurs::validate() {
63     for (auto & kv : m_num_occurs) {
64         VERIFY(0 < kv.m_key->get_ref_count());
65     }
66 }
67 
operator ()(expr * t)68 void num_occurs::operator()(expr * t) {
69     expr_fast_mark1   visited;
70     process(t, visited);
71 }
72 
operator ()(unsigned num,expr * const * ts)73 void num_occurs::operator()(unsigned num, expr * const * ts) {
74     expr_fast_mark1   visited;
75     for (unsigned i = 0; i < num; i++) {
76         process(ts[i], visited);
77     }
78 }
79 
80