1 /*++ 2 Copyright (c) 2012 Microsoft Corporation 3 4 Module Name: 5 6 goal_num_occurs.h 7 8 Abstract: 9 10 11 Author: 12 13 Leonardo de Moura (leonardo) 2012-10-20. 14 15 Revision History: 16 17 --*/ 18 #pragma once 19 20 #include "ast/num_occurs.h" 21 22 class goal; 23 24 class goal_num_occurs : public num_occurs { 25 expr_ref_vector m_pinned; 26 public: 27 goal_num_occurs(ast_manager& m, bool ignore_ref_count1 = false, bool ignore_quantifiers = false): num_occurs(ignore_ref_count1,ignore_quantifiers)28 num_occurs(ignore_ref_count1, ignore_quantifiers), 29 m_pinned(m) { 30 } 31 reset()32 void reset() override { num_occurs::reset(); m_pinned.reset(); } 33 void operator()(goal const & s); 34 }; 35 36 37