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