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