1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3 
4 Module Name:
5 
6     goal_shared_occs.h
7 
8 Abstract:
9 
10     Functor for computing the set of shared occurrences in a goal.
11 
12 Author:
13 
14     Leonardo de Moura (leonardo) 2011-12-28
15 
16 Revision History:
17 
18 --*/
19 #pragma once
20 
21 #include "tactic/goal.h"
22 #include "ast/shared_occs.h"
23 
24 /**
25    \brief Functor for computing the set of shared occurrences in a goal.
26 
27    It is essentially a wrapper for shared_occs functor.
28 */
29 class goal_shared_occs {
30     shared_occs m_occs;
31 public:
32     goal_shared_occs(ast_manager & m, bool track_atomic = false, bool visit_quantifiers = true, bool visit_patterns = false):
m_occs(m,track_atomic,visit_quantifiers,visit_patterns)33         m_occs(m, track_atomic, visit_quantifiers, visit_patterns) {
34     }
35     void operator()(goal const & s);
is_shared(expr * t)36     bool is_shared(expr * t) { return m_occs.is_shared(t); }
num_shared()37     unsigned num_shared() const { return m_occs.num_shared(); }
reset()38     void reset() { return m_occs.reset(); }
cleanup()39     void cleanup() { return m_occs.cleanup(); }
display(std::ostream & out,ast_manager & m)40     void display(std::ostream & out, ast_manager & m) const { m_occs.display(out, m); }
41 };
42 
43 
44