z3-src 503.3.0

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
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81

/*++
Copyright (c) 2006 Microsoft Corporation

Module Name:

    fingerprints.h

Abstract:

    <abstract>

Author:

    Leonardo de Moura (leonardo) 2007-02-24.

Revision History:

--*/
#pragma once

#include "smt/smt_enode.h"
#include "util/util.h"

namespace smt {

    class fingerprint {
    protected:
        void*         m_data = nullptr;
        unsigned      m_data_hash = 0;
        unsigned      m_num_args = 0;
        enode**       m_args = nullptr;

        friend class fingerprint_set;
        fingerprint() = default;
    public:
        fingerprint(region & r, void * d, unsigned d_hash, unsigned n, enode * const * args);
        void * get_data() const { return m_data; }
        unsigned get_data_hash() const { return m_data_hash; }
        unsigned get_num_args() const { return m_num_args;  }
        enode * const * get_args() const { return m_args; }
        enode * get_arg(unsigned idx) const { SASSERT(idx < m_num_args); return m_args[idx]; }
        enode * const * begin() const { return m_args; }
        enode * const * end() const { return begin() + get_num_args(); }
        friend std::ostream& operator<<(std::ostream& out, fingerprint const& f);
    };
    
    class fingerprint_set {
        
        struct fingerprint_hash_proc {
            unsigned operator()(fingerprint const * f) const {
                return f->get_data_hash();
            }
        };
        struct fingerprint_eq_proc { bool operator()(fingerprint const * f1, fingerprint const * f2) const; };
        typedef ptr_hashtable<fingerprint, fingerprint_hash_proc, fingerprint_eq_proc> set;

        region &                 m_region;
        set                      m_set;
        ptr_vector<fingerprint>  m_fingerprints;
        unsigned_vector          m_scopes;
        ptr_vector<enode>        m_tmp;
        fingerprint              m_dummy;

        fingerprint * mk_dummy(void * data, unsigned data_hash, unsigned num_args, enode * const * args);

    public:
        fingerprint_set(ast_manager& m, region & r): m_region(r) {}
        fingerprint * insert(void * data, unsigned data_hash, unsigned num_args, enode * const * args);
        unsigned size() const { return m_fingerprints.size(); }
        bool contains(void * data, unsigned data_hash, unsigned num_args, enode * const * args);
        void reset();
        void push_scope();
        void pop_scope(unsigned num_scopes);
        void display(std::ostream & out) const;
#ifdef Z3DEBUG
        bool slow_contains(void const * data, unsigned data_hash, unsigned num_args, enode * const * args) const;
#endif
    };
}