Merge branch 'master' into scoped_vector

.github/workflows/coverage.yml

@@ -3,6 +3,8 @@ name: Code Coverage
 on:
   push:
     branches: [ master ]
+  pull_request:
+    branches: [ master ]
   schedule:
     - cron: "0 11 * * *"
 

.github/workflows/docker-image.yml

@@ -41,7 +41,7 @@ jobs:
             type=edge
             type=sha,prefix=ubuntu-20.04-bare-z3-sha-
       - name: Build and push Bare Z3 Docker Image
-        uses: docker/build-push-action@v6.4.0
+        uses: docker/build-push-action@v6.5.0
         with:  
           context: .
           push: true

src/test/dlist.cpp

@@ -1,3 +1,20 @@
+/*++
+Copyright (c) 2024 Microsoft Corporation
+
+Module Name:
+
+    tst_dlist.cpp
+
+Abstract:
+
+    Test dlist module
+
+Author:
+
+    Chuyue Sun 2024-07-18.
+
+--*/
+
 #include <iostream>
 #include "util/dlist.h"
 
@@ -157,10 +174,12 @@ void tst_dlist() {
     test_pop();
     test_insert_after();
     test_insert_before();
+#if 0
     test_remove_from();
     test_push_to_front();
     test_detach();
     test_invariant();
     test_contains();
+#endif
     std::cout << "All tests passed." << std::endl;
 }

src/test/hashtable.cpp

@@ -12,6 +12,7 @@ Abstract:
 Author:
 
     Leonardo de Moura (leonardo) 2006-09-12.
+    Chuyue Sun (liviasun) 2024-07-18.
 
 Revision History:
 
@@ -20,7 +21,6 @@ Revision History:
 #include<iostream>
 #include<unordered_set>
 #include<stdlib.h>
-
 #include "util/hashtable.h"
 
 
@@ -119,11 +119,126 @@ static void tst3() {
     ENSURE(h2.size() == 2);
 }
 
+// Custom hash and equality functions for testing
+struct my_hash {
+    unsigned operator()(int x) const { return x; }
+};
+
+struct my_eq {
+    bool operator()(int x, int y) const { return x == y; }
+};
+
+void test_hashtable_constructors() {
+    hashtable<int, my_hash, my_eq> ht;
+    VERIFY(ht.empty());
+    VERIFY(ht.size() == 0);
+    VERIFY(ht.capacity() == DEFAULT_HASHTABLE_INITIAL_CAPACITY);
+
+    // Copy constructor
+    hashtable<int, my_hash, my_eq> ht_copy(ht);
+    VERIFY(ht_copy.empty());
+    VERIFY(ht_copy.size() == 0);
+    VERIFY(ht_copy.capacity() == ht.capacity());
+
+    // Move constructor
+    hashtable<int, my_hash, my_eq> ht_move(std::move(ht));
+    VERIFY(ht_move.empty());
+    VERIFY(ht_move.size() == 0);
+    VERIFY(ht_move.capacity() == ht_copy.capacity());
+}
+
+void test_hashtable_insert() {
+    hashtable<int, my_hash, my_eq> ht;
+    ht.insert(1);
+    VERIFY(!ht.empty());
+    VERIFY(ht.size() == 1);
+    int value;
+    VERIFY(ht.find(1, value) && value == 1);
+}
+
+void test_hashtable_remove() {
+    hashtable<int, my_hash, my_eq> ht;
+    ht.insert(1);
+    ht.remove(1);
+    VERIFY(ht.empty());
+    VERIFY(ht.size() == 0);
+}
+
+void test_hashtable_find() {
+    hashtable<int, my_hash, my_eq> ht;
+    ht.insert(1);
+    int value;
+    VERIFY(ht.find(1, value) && value == 1);
+    VERIFY(!ht.find(2, value));
+}
+
+void test_hashtable_contains() {
+    hashtable<int, my_hash, my_eq> ht;
+    ht.insert(1);
+    VERIFY(ht.contains(1));
+    VERIFY(!ht.contains(2));
+}
+
+void test_hashtable_reset() {
+    hashtable<int, my_hash, my_eq> ht;
+    ht.insert(1);
+    ht.reset();
+    VERIFY(ht.empty());
+    VERIFY(ht.size() == 0);
+}
+
+void test_hashtable_finalize() {
+    hashtable<int, my_hash, my_eq> ht;
+    ht.insert(1);
+    ht.finalize();
+    VERIFY(ht.empty());
+    VERIFY(ht.size() == 0);
+}
+
+void test_hashtable_iterators() {
+    hashtable<int, my_hash, my_eq> ht;
+    ht.insert(1);
+    ht.insert(2);
+    ht.insert(3);
+    
+    int count = 0;
+    for(auto it = ht.begin(); it != ht.end(); ++it) {
+        ++count;
+    }
+    VERIFY(count == 3);
+}
+
+void test_hashtable_operators() {
+    hashtable<int, my_hash, my_eq> ht1;
+    hashtable<int, my_hash, my_eq> ht2;
+    
+    ht1.insert(1);
+    ht2.insert(2);
+    
+    ht1 |= ht2;
+    VERIFY(ht1.contains(1));
+    VERIFY(ht1.contains(2));
+    
+    ht1 &= ht2;
+    VERIFY(!ht1.contains(1));
+    VERIFY(ht1.contains(2));
+}
+
 void tst_hashtable() {
     tst3();
     for (int i = 0; i < 100; i++) 
         tst2();
     tst1();
+    test_hashtable_constructors();
+    test_hashtable_insert();
+    test_hashtable_remove();
+    test_hashtable_find();
+    test_hashtable_contains();
+    test_hashtable_reset();
+    test_hashtable_finalize();
+    test_hashtable_iterators();
+    test_hashtable_operators();
+    std::cout << "All tests passed!" << std::endl;
 }
 #else
 void tst_hashtable() {

src/util/dlist.h

@@ -155,23 +155,15 @@ public:
         elem->init(elem);
     }
 
-    bool invariant() const { 
-        auto* e = this; 
-        const T* slow = static_cast<const T*>(this); 
-        const T* fast = m_next; 
-        bool looped = false; 
-        // m_next of each node should point back to m_prev of the following node,
-        // and m_prev of each node should point forward to m_next of the preceding node.
-        while (slow != fast) { 
-            if (fast->m_prev->m_next != fast || fast->m_next->m_prev != fast) 
-                return false;             
-            fast = fast->m_next; 
-            looped = looped || (fast == static_cast<const T*>(this)); 
-            if (!looped && fast == m_next)  
-                // We should be able to traverse back to the starting node. 
-                return false;             
-        } 
-        return true; 
+    bool invariant() const {
+        auto* e = this;
+        do {
+            if (e->m_next->m_prev != e)
+                return false;
+            e = e->m_next;
+        }
+        while (e != this);
+        return true;
     }
 
     static bool contains(T const* list, T const* elem) {

src/util/hashtable.h

@@ -12,6 +12,7 @@ Abstract:
 Author:
 
     Leonardo de Moura (leonardo) 2006-09-11.
+    Chuyue Sun (liviasun) 2024-07-18.
 
 Revision History:
 
@@ -639,6 +640,19 @@ public:
 
 #ifdef Z3DEBUG
     bool check_invariant() {
+        // The capacity must always be a power of two.
+        if (!is_power_of_two(m_capacity))
+            return false;
+
+        // The number of deleted plus the size must not exceed the capacity.
+        if (m_num_deleted + m_size > m_capacity)
+            return false;
+
+        // Checking that m_num_deleted is less than or equal to m_size.
+        if (m_num_deleted > m_size) {
+            return false;
+        }
+
         entry * curr = m_table;
         entry * end  = m_table + m_capacity;
         unsigned num_deleted = 0;

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;
 }