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)55bool 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)66bool 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