mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

update heap unit tests (#7324)

Browse source 
* new heap invariants

* change ENSURE to SASSERT for unit test heap

* change SASSERT to VERIFY

* update heap tests

* update

* remove one invariant
This commit is contained in:
LiviaSun 2024-08-02 18:29:50 -07:00 • committed by GitHub
parent fce4b36dad
commit d2fc085b8c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 14 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/util/heap.h
View file

@ -55,6 +55,19 @@ class heap : private LT {
}
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())) {
SASSERT(m_value2indices[m_values[idx]] == idx);
SASSERT(parent(idx) == 0 || !less_than(m_values[idx], m_values[parent(idx)]));