mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

add new permutation class invariant (#7299)

Browse source 
* new heap invariants

* change ENSURE to SASSERT for unit test heap

* change SASSERT to VERIFY

* new permutation invariant

* remove heap changes

* use bool_vector
This commit is contained in:
LiviaSun 2024-07-19 19:27:23 -07:00 • committed by GitHub
parent 5003d41cdb
commit 49dc1bb721
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 9 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/util/permutation.cpp
View file

@ -36,6 +36,7 @@ void permutation::swap(unsigned i, unsigned j) noexcept {
unsigned j_prime = m_p[j];
std::swap(m_p[i], m_p[j]);
std::swap(m_inv_p[i_prime], m_inv_p[j_prime]);
SASSERT(check_invariant());
}
/**
@ -66,11 +67,19 @@ void permutation::display(std::ostream & out) const {
bool permutation::check_invariant() const {
SASSERT(m_p.size() == m_inv_p.size());
unsigned n = m_p.size();
bool_vector check_vector(n, false); // To check for duplicate and out-of-range values
for (unsigned i = 0; i < n; i++) {
unsigned pi = m_p[i];
SASSERT(m_p[i] < n);
SASSERT(m_inv_p[i] < n);
SASSERT(m_p[m_inv_p[i]] == i);
SASSERT(m_inv_p[m_p[i]] == i);
// Check the inversion hasn't been checked yet
if (check_vector[pi]) {
return false;
}
// Mark this value as checked
check_vector[pi] = true;
}
return true;
}