z3-src 503.2.1

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

/*++
Copyright (c) 2017 Microsoft Corporation

Module Name:

    queue.h

Abstract:
   
    Generic queue.

Author:

    Nikolaj Bjorner (nbjorner) 2017-4-17

Notes:

--*/
#pragma once

#include "vector.h"

template<class T>
class queue {
    vector<T> m_elems;
    unsigned  m_head = 0;
    unsigned  m_capacity = 0;
    
public:
    void push(T const& t) { m_elems.push_back(t); }

    bool empty() const { 
        return m_head == m_elems.size(); 
    }

    T top() const {
        return m_elems[m_head];
    }

    T pop_front() { 
        SASSERT(!empty());
        m_capacity = std::max(m_capacity, m_elems.size());
        SASSERT(m_head < m_elems.size()); 
        if (2 * m_head > m_capacity && m_capacity > 10) {
            for (unsigned i = 0; i < m_elems.size() - m_head; ++i) {
                m_elems[i] = m_elems[i + m_head];
            }
            m_elems.shrink(m_elems.size() - m_head);
            m_head = 0;
        } 
        return m_elems[m_head++];        
    }


    T back() const {
        return m_elems[m_elems.size() - 1];
    }

    T pop_back() {
        SASSERT(!empty());
        SASSERT(m_head < m_elems.size()); 
        T result = back();
        m_elems.shrink(m_elems.size() - 1);
        return result;
    }
};