mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

Revert "new heap invariants (#7298)" (#7303)

Browse source 
This reverts commit 80ac7b3438.
This commit is contained in:
Nikolaj Bjorner 2024-07-21 21:07:09 -07:00 committed by GitHub
parent 3d014f8b33
commit 966c9a3764
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 11 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/test/heap.cpp
View file

@ -38,7 +38,7 @@ static void tst1() {
for (int i = 0; i < N * 3; i++) { for (int i = 0; i < N * 3; i++) {
int val = heap_rand() % N; int val = heap_rand() % N;
if (!h.contains(val)) { if (!h.contains(val)) {
VERIFY(!t.contains(val)); ENSURE(!t.contains(val));
h.insert(val); h.insert(val);
t.insert(val); t.insert(val);
} }
@ -46,26 +46,26 @@ static void tst1() {
if (!t.contains(val)) { if (!t.contains(val)) {
for (int v : t) std::cout << v << "\n"; for (int v : t) std::cout << v << "\n";
} }
VERIFY(t.contains(val)); ENSURE(t.contains(val));
} }
} }
VERIFY(h.check_invariant()); ENSURE(h.check_invariant());
for (int v : t) { for (int v : t) {
VERIFY(h.contains(v)); ENSURE(h.contains(v));
} }
while (!h.empty()) { while (!h.empty()) {
int m1 = h.min_value(); int m1 = h.min_value();
int m2 = h.erase_min(); int m2 = h.erase_min();
(void)m1; (void)m1;
(void)m2; (void)m2;
VERIFY(m1 == m2); ENSURE(m1 == m2);
VERIFY(-1 < m2); ENSURE(-1 < m2);
} }
} }
int g_value[N]; int g_value[N];
struct lt_proc2 { bool operator()(int v1, int v2) const { VERIFY(v1 < N && v2 < N); return g_value[v1] < g_value[v2]; } }; struct lt_proc2 { bool operator()(int v1, int v2) const { ENSURE(v1 < N && v2 < N); return g_value[v1] < g_value[v2]; } };
typedef heap<lt_proc2> int_heap2; typedef heap<lt_proc2> int_heap2;
static void init_values() { static void init_values() {
@ -98,7 +98,7 @@ static void tst2() {
TRACE("heap", tout << "inserting: " << val << "\n";); TRACE("heap", tout << "inserting: " << val << "\n";);
h.insert(val); h.insert(val);
TRACE("heap", dump_heap(h, tout);); TRACE("heap", dump_heap(h, tout););
VERIFY(h.contains(val)); ENSURE(h.contains(val));
} }
} }
else if (cmd <= 6) { else if (cmd <= 6) {
@ -107,7 +107,7 @@ static void tst2() {
TRACE("heap", tout << "removing: " << val << "\n";); TRACE("heap", tout << "removing: " << val << "\n";);
h.erase(val); h.erase(val);
TRACE("heap", dump_heap(h, tout);); TRACE("heap", dump_heap(h, tout););
VERIFY(!h.contains(val)); ENSURE(!h.contains(val));
} }
} }
else if (cmd <= 8) { else if (cmd <= 8) {
@ -128,12 +128,10 @@ static void tst2() {
} }
} }
else { else {
VERIFY(h.check_invariant()); ENSURE(h.check_invariant());
} }
} }
VERIFY(h.check_invariant()); ENSURE(h.check_invariant());
h.reset();
VERIFY(h.check_invariant());
} }
void tst_heap() { void tst_heap() {

13
src/util/heap.h
View file

@ -55,19 +55,6 @@ class heap : private LT {
} }
bool check_invariant_core(int idx) const { bool check_invariant_core(int idx) const {
// Check that m_values starts with a dummy value at index 0.
if (m_values.empty() || m_values[0] != -1) {
return false;
}
// All indices in m_value2indices that are not used in m_values should be 0
for (int val = 0; val < static_cast<int>(m_value2indices.size()); ++val) {
if (std::find(m_values.begin(), m_values.end(), val) == m_values.end() && m_value2indices[val] != 0) {
return false; // Unused indices should have a 0 value
}
}
if (idx < static_cast<int>(m_values.size())) { if (idx < static_cast<int>(m_values.size())) {
SASSERT(m_value2indices[m_values[idx]] == idx); SASSERT(m_value2indices[m_values[idx]] == idx);
SASSERT(parent(idx) == 0 || !less_than(m_values[idx], m_values[parent(idx)])); SASSERT(parent(idx) == 0 || !less_than(m_values[idx], m_values[parent(idx)]));