z3-src 501.0.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
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186

/*++
Copyright (c) 2024 Microsoft Corporation

Module Name:

    tst_dlist.cpp

Abstract:

    Test dlist module

Author:

    Chuyue Sun 2024-07-18.

--*/

#include <cassert>
#include <iostream>
#include "util/dlist.h"

class TestNode : public dll_base<TestNode> {
public:
    int value;
    TestNode(int val) : value(val) {
        init(this);
    }
};

// Test the prev() method
void test_prev() {
    TestNode node(1);
    ENSURE(node.prev() == &node);
    std::cout << "test_prev passed." << std::endl;
}

// Test the next() method
static void test_next() {
    TestNode node(1);
    ENSURE(node.next() == &node);
    std::cout << "test_next passed." << std::endl;
}

// Test the const prev() method
static void test_const_prev() {
    const TestNode node(1);
    ENSURE(node.prev() == &node);
    std::cout << "test_const_prev passed." << std::endl;
}

// Test the const next() method
static void test_const_next() {
    const TestNode node(1);
    ENSURE(node.next() == &node);
    std::cout << "test_const_next passed." << std::endl;
}

// Test the init() method
static void test_init() {
    TestNode node(1);
    node.init(&node);
    ENSURE(node.next() == &node);
    ENSURE(node.prev() == &node);
    ENSURE(node.invariant());
    std::cout << "test_init passed." << std::endl;
}

// Test the pop() method
static void test_pop() {
    TestNode* list = nullptr;
    TestNode node1(1);
    TestNode::push_to_front(list, &node1);
    [[maybe_unused]] TestNode* popped = TestNode::pop(list);
    ENSURE(popped == &node1);
    ENSURE(list == nullptr);
    ENSURE(popped->next() == popped);
    ENSURE(popped->prev() == popped);
    std::cout << "test_pop passed." << std::endl;
}

// Test the insert_after() method
static void test_insert_after() {
    TestNode node1(1);
    TestNode node2(2);
    node1.insert_after(&node2);
    ENSURE(node1.next() == &node2);
    ENSURE(node2.prev() == &node1);
    ENSURE(node1.prev() == &node2);
    ENSURE(node2.next() == &node1);
    ENSURE(node1.invariant());
    ENSURE(node2.invariant());
    std::cout << "test_insert_after passed." << std::endl;
}

// Test the insert_before() method
static void test_insert_before() {
    TestNode node1(1);
    TestNode node2(2);
    node1.insert_before(&node2);
    ENSURE(node1.prev() == &node2);
    ENSURE(node2.next() == &node1);
    ENSURE(node1.next() == &node2);
    ENSURE(node2.prev() == &node1);
    ENSURE(node1.invariant());
    ENSURE(node2.invariant());
    std::cout << "test_insert_before passed." << std::endl;
}

#if 0
// Test the remove_from() method
static void test_remove_from() {
    TestNode* list = nullptr;
    TestNode node1(1);
    TestNode node2(2);
    TestNode::push_to_front(list, &node1);
    TestNode::push_to_front(list, &node2);
    TestNode::remove_from(list, &node1);
    ENSURE(list == &node2);
    ENSURE(node2.next() == &node2);
    ENSURE(node2.prev() == &node2);
    std::cout << "test_remove_from passed." << std::endl;
}
#endif

// Test the push_to_front() method
static void test_push_to_front() {
    TestNode* list = nullptr;
    TestNode node1(1);
    TestNode::push_to_front(list, &node1);
    ENSURE(list == &node1);
    ENSURE(node1.next() == &node1);
    ENSURE(node1.prev() == &node1);
    std::cout << "test_push_to_front passed." << std::endl;
}

// Test the detach() method
static void test_detach() {
    TestNode node(1);
    TestNode::detach(&node);
    ENSURE(node.next() == &node);
    ENSURE(node.prev() == &node);
    ENSURE(node.invariant());
    std::cout << "test_detach passed." << std::endl;
}

// Test the invariant() method
static void test_invariant() {
    TestNode node1(1);
    ENSURE(node1.invariant());
    TestNode node2(2);
    node1.insert_after(&node2);
    ENSURE(node1.invariant());
    ENSURE(node2.invariant());
    std::cout << "test_invariant passed." << std::endl;
}

// Test the contains() method
static void test_contains() {
    TestNode* list = nullptr;
    TestNode node1(1);
    TestNode node2(2);
    TestNode::push_to_front(list, &node1);
    TestNode::push_to_front(list, &node2);
    ENSURE(TestNode::contains(list, &node1));
    ENSURE(TestNode::contains(list, &node2));
    TestNode node3(3);
    ENSURE(!TestNode::contains(list, &node3));
    std::cout << "test_contains passed." << std::endl;
}

void tst_dlist() {
    test_prev();
    test_next();
    test_const_prev();
    test_const_next();
    test_init();
    test_pop();
    test_insert_after();
    test_insert_before();
    test_push_to_front();
    test_detach();
    test_invariant();
    test_contains();
    //test_remove_from;
    std::cout << "All tests passed." << std::endl;
}