z3-src 503.2.2

Source distribution of the Z3 SMT solver, for use as a build dependency
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56

/*++
Copyright (c) 2006 Microsoft Corporation

Module Name:

    num_occurs.h

Abstract:

    <abstract>

Author:

    Leonardo de Moura (leonardo) 2008-01-27.

Revision History:

--*/
#pragma once

#include "ast/ast.h"
#include "util/obj_hashtable.h"

/**
   \brief Functor for computing the number of occurrences of each sub-expression in a expression F.
*/
class num_occurs { 
protected:
    bool m_ignore_ref_count1;
    bool m_ignore_quantifiers;
    obj_map<expr, unsigned>        m_num_occurs;

    void process(expr * t, expr_fast_mark1 & visited);
public:
    num_occurs(bool ignore_ref_count1 = false, bool ignore_quantifiers = false):
        m_ignore_ref_count1(ignore_ref_count1), 
        m_ignore_quantifiers(ignore_quantifiers) {
    }

    virtual ~num_occurs() = default;

    void validate();
    virtual void reset() { m_num_occurs.reset(); }
    
    void operator()(expr * t);
    void operator()(unsigned num, expr * const * ts);

    unsigned get_num_occs(expr * n) const { 
        unsigned val;
        if (m_num_occurs.find(n, val))
            return val;
        return 0;
    }
};