z3-src 415.4.4

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
82
83
84
85
86
87
88
89
90
91
92

/*++
Copyright (c) 2006 Microsoft Corporation

Module Name:

    expr_offset_map.h

Abstract:

    A generic mapping from (expression, offset) to a value T.

Author:

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

Revision History:

--*/
#pragma once

#include "ast/substitution/expr_offset.h"
#include "util/vector.h"

/**
   \brief A mapping from expr_offset to some value of type T.
*/
template<typename T>
class expr_offset_map {
    struct data {
        T        m_data;
        unsigned m_timestamp;
        data():m_timestamp(0) {}
    };
    vector<svector<data> > m_map;
    unsigned               m_timestamp;
public:
    expr_offset_map():
        m_timestamp(1) {}
    
    bool contains(expr_offset const & n) const {
        unsigned off = n.get_offset();
        if (off < m_map.size()) {
            svector<data> const & v = m_map[off];
            unsigned id             = n.get_expr()->get_id();
            if (id < v.size()) 
                return v[id].m_timestamp == m_timestamp;
        }
        return false;
    }

    bool find(expr_offset const & n, T & r) const {
        unsigned off = n.get_offset();
        if (off < m_map.size()) {
            svector<data> const & v = m_map[off];
            unsigned id             = n.get_expr()->get_id();
            if (id < v.size() && v[id].m_timestamp == m_timestamp) {
                r = v[id].m_data;
                return true;
            }
        }
        return false;
    }

    void insert(expr_offset const & n, T const & r) {
        unsigned off = n.get_offset();
        if (off >= m_map.size())
            m_map.resize(off+1, svector<data>());
        svector<data> & v = m_map[off];
        unsigned id       = n.get_expr()->get_id();
        if (id >= v.size())
            v.resize(id+1);
        v[id].m_data      = r;
        v[id].m_timestamp = m_timestamp;
    }

    void reset() {
        m_timestamp++;
        if (m_timestamp == UINT_MAX) {
            typename vector<svector<data> >::iterator it  = m_map.begin();
            typename vector<svector<data> >::iterator end = m_map.end();
            for (; it != end; ++it) {
                svector<data> & v = *it;
                typename svector<data>::iterator it2  = v.begin();
                typename svector<data>::iterator end2 = v.end();
                for (; it2 != end2; ++it2)
                    it2->m_timestamp = 0;
            }
            m_timestamp = 1;
        }
    }
};