1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3 
4 Module Name:
5 
6     occurs.cpp
7 
8 Abstract:
9 
10     <abstract>
11 
12 Author:
13 
14     Leonardo de Moura (leonardo) 2007-06-07.
15 
16 Revision History:
17 
18 --*/
19 #include "ast/occurs.h"
20 
21 #include "ast/for_each_expr.h"
22 
23 // -----------------------------------
24 //
25 // Occurs check
26 //
27 // -----------------------------------
28 
29 namespace {
30     struct found {};
31 
32     struct proc {
33         expr * m_n;
34 
35 #define CHECK() { if (n == m_n) throw found(); }
36 
proc__anon3fba2ebc0111::proc37         proc(expr * n):m_n(n) {}
operator ()__anon3fba2ebc0111::proc38         void operator()(var const * n) { CHECK(); }
operator ()__anon3fba2ebc0111::proc39         void operator()(app const * n) { CHECK(); }
operator ()__anon3fba2ebc0111::proc40         void operator()(quantifier const * n) { CHECK(); }
41     };
42 
43     struct decl_proc {
44         func_decl * m_d;
45 
decl_proc__anon3fba2ebc0111::decl_proc46         decl_proc(func_decl * d):m_d(d) {}
operator ()__anon3fba2ebc0111::decl_proc47         void operator()(var const * n) { }
operator ()__anon3fba2ebc0111::decl_proc48         void operator()(app const * n) { if (n->get_decl() == m_d) throw found(); }
operator ()__anon3fba2ebc0111::decl_proc49         void operator()(quantifier const * n) { }
50     };
51 
52 }
53 
54 // Return true if n1 occurs in n2
occurs(expr * n1,expr * n2)55 bool occurs(expr * n1, expr * n2) {
56     proc p(n1);
57     try {
58         quick_for_each_expr(p, n2);
59     }
60     catch (const found &) {
61         return true;
62     }
63     return false;
64 }
65 
occurs(func_decl * d,expr * n)66 bool occurs(func_decl * d, expr * n) {
67     decl_proc p(d);
68     try {
69         quick_for_each_expr(p, n);
70     }
71     catch (const found &) {
72         return true;
73     }
74     return false;
75 }
76 
77