From 49dc1bb721519601b36e3922f1f793e3ca71a7d5 Mon Sep 17 00:00:00 2001
From: LiviaSun <33578456+ChuyueSun@users.noreply.github.com>
Date: Fri, 19 Jul 2024 19:27:23 -0700
Subject: [PATCH] add new permutation class invariant (#7299)

* new heap invariants

* change ENSURE to SASSERT for unit test heap

* change SASSERT to VERIFY

* new permutation invariant

* remove heap changes

* use bool_vector
---
 src/util/permutation.cpp | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/util/permutation.cpp b/src/util/permutation.cpp
index 8b7adedf3..47b9d85a1 100644
--- a/src/util/permutation.cpp
+++ b/src/util/permutation.cpp
@@ -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;
 }