1 /*++ 2 Copyright (c) 2011 Microsoft Corporation 3 4 Module Name: 5 6 shared_occs.h 7 8 Abstract: 9 10 Functor for computing the shared subterms in a given 11 term. 12 13 Author: 14 15 Leonardo de Moura (leonardo) 2011-04-01. 16 17 Revision History: 18 --*/ 19 #pragma once 20 21 #include "ast/ast.h" 22 #include "util/obj_hashtable.h" 23 24 class shared_occs_mark { 25 ptr_buffer<ast> m_to_unmark; 26 public: shared_occs_mark()27 shared_occs_mark() {} 28 ~shared_occs_mark()29 ~shared_occs_mark() { 30 reset(); 31 } 32 is_marked(ast * n)33 bool is_marked(ast * n) { return n->is_marked_so(); } reset_mark(ast * n)34 void reset_mark(ast * n) { n->reset_mark_so(); } mark(ast * n)35 void mark(ast * n) { if (is_marked(n)) return; n->mark_so(true); m_to_unmark.push_back(n); } reset()36 void reset() { 37 ptr_buffer<ast>::iterator it = m_to_unmark.begin(); 38 ptr_buffer<ast>::iterator end = m_to_unmark.end(); 39 for (; it != end; ++it) { 40 reset_mark(*it); 41 } 42 m_to_unmark.reset(); 43 } mark(ast * n,bool flag)44 void mark(ast * n, bool flag) { if (flag) mark(n); else reset_mark(n); } 45 }; 46 47 /** 48 \brief Functor for computing the shared subterms in a given term. 49 */ 50 class shared_occs { 51 ast_manager & m; 52 bool m_track_atomic; 53 bool m_visit_quantifiers; 54 bool m_visit_patterns; 55 expr_ref_vector m_shared; 56 typedef std::pair<expr*, unsigned> frame; 57 svector<frame> m_stack; 58 bool process(expr * t, shared_occs_mark & visited); 59 void insert(expr * t); 60 public: 61 typedef obj_hashtable<expr>::iterator iterator; 62 shared_occs(ast_manager & _m, bool track_atomic = false, bool visit_quantifiers = true, bool visit_patterns = false): m(_m)63 m(_m), 64 m_track_atomic(track_atomic), 65 m_visit_quantifiers(visit_quantifiers), 66 m_visit_patterns(visit_patterns), 67 m_shared(m) { 68 } 69 ~shared_occs(); 70 void operator()(expr * t); 71 void operator()(expr * t, shared_occs_mark & visited); is_shared(expr * t)72 bool is_shared(expr * t) const { return m_shared.get(t->get_id(), nullptr) != nullptr; } 73 unsigned num_shared() const; 74 void reset(); 75 void cleanup(); 76 void display(std::ostream & out, ast_manager & mgr) const; 77 }; 78 79