Merge branch 'master' into heap

.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/api/python/z3/z3printer.py

@@ -1412,8 +1412,10 @@ class HTMLFormatter(Formatter):
         ys_pp = group(seq(ys))
         if a.is_forall():
             header = "∀"
-        else:
+        elif a.is_exists():
             header = "∃"
+        else:
+            header = "λ"
         return group(compose(to_format(header, 1),
                              indent(1, compose(ys_pp, to_format(" :"), line_break(), body_pp))))
 

src/ast/datatype_decl_plugin.cpp

@@ -220,17 +220,33 @@ namespace datatype {
     }
 
     namespace decl {
-
+        
         plugin::~plugin() {
             finalize();
         }
 
         void plugin::finalize() {
-            for (auto& kv : m_defs) {
+            for (auto& kv : m_defs) 
-                dealloc(kv.m_value);
+                dealloc(kv.m_value);            
-            }
             m_defs.reset();
             m_util = nullptr; // force deletion
+            reset();
+        }
+
+        void plugin::reset() {
+            m_datatype2constructors.reset();
+            m_datatype2nonrec_constructor.reset();
+            m_constructor2accessors.reset();
+            m_constructor2recognizer.reset();
+            m_recognizer2constructor.reset();
+            m_accessor2constructor.reset();
+            m_is_recursive.reset();
+            m_is_enum.reset();
+            std::for_each(m_vectors.begin(), m_vectors.end(), delete_proc<ptr_vector<func_decl> >());
+            m_vectors.reset();
+            dealloc(m_asts);
+            m_asts = nullptr;
+            ++m_start;
         }
 
         util & plugin::u() const {
@@ -578,6 +594,7 @@ namespace datatype {
             if (m_defs.find(s, d)) 
                 dealloc(d);
             m_defs.remove(s);
+            reset();
         }
 
         bool plugin::is_value_visit(bool unique, expr * arg, ptr_buffer<app> & todo) const {
@@ -799,7 +816,7 @@ namespace datatype {
             for (unsigned i = 0; i < n; ++i) {
                 sort* ps = get_datatype_parameter_sort(s, i);
                 sz = get_sort_size(params, ps);
-                m_refs.push_back(sz);
+                plugin().m_refs.push_back(sz);
                 S.insert(d.params().get(i), sz); 
             }            
             auto ss = d.sort_size();
@@ -896,7 +913,7 @@ namespace datatype {
             }
             TRACE("datatype", tout << "set sort size " << s << "\n";);
             d.set_sort_size(param_size::size::mk_plus(s_add));
-            m_refs.reset();
+            plugin().m_refs.reset();
         }
     }
     
@@ -1008,9 +1025,7 @@ namespace datatype {
     util::util(ast_manager & m):
         m(m),
         m_family_id(null_family_id),
-        m_plugin(nullptr),
+        m_plugin(nullptr) {
-        m_asts(m),
-        m_start(0) {
     }
 
 
@@ -1027,24 +1042,24 @@ namespace datatype {
 
 
     util::~util() {
-        std::for_each(m_vectors.begin(), m_vectors.end(), delete_proc<ptr_vector<func_decl> >());
+        
     }
 
     ptr_vector<func_decl> const * util::get_datatype_constructors(sort * ty) {
         SASSERT(is_datatype(ty));
         ptr_vector<func_decl> * r = nullptr;
-        if (m_datatype2constructors.find(ty, r))
+        if (plugin().m_datatype2constructors.find(ty, r))
             return r;
         r = alloc(ptr_vector<func_decl>);
-        m_asts.push_back(ty);
+        plugin().add_ast(ty);
-        m_vectors.push_back(r);
+        plugin().m_vectors.push_back(r);
-        m_datatype2constructors.insert(ty, r);
+        plugin().m_datatype2constructors.insert(ty, r);
         if (!is_declared(ty)) 
             m.raise_exception("datatype constructors have not been created");
         def const& d = get_def(ty);
         for (constructor const* c : d) {
             func_decl_ref f = c->instantiate(ty);
-            m_asts.push_back(f);
+            plugin().add_ast(f);
             r->push_back(f);
         }
         return r;
@@ -1053,13 +1068,13 @@ namespace datatype {
     ptr_vector<func_decl> const * util::get_constructor_accessors(func_decl * con) {
         SASSERT(is_constructor(con));
         ptr_vector<func_decl> * res = nullptr;
-        if (m_constructor2accessors.find(con, res)) {
+        if (plugin().m_constructor2accessors.find(con, res)) {
             return res;
         }
         res = alloc(ptr_vector<func_decl>);
-        m_asts.push_back(con);
+        plugin().add_ast(con);
-        m_vectors.push_back(res);
+        plugin().m_vectors.push_back(res);
-        m_constructor2accessors.insert(con, res);
+        plugin().m_constructor2accessors.insert(con, res);
         sort * datatype = con->get_range();
         def const& d = get_def(datatype);
         for (constructor const* c : d) {
@@ -1067,7 +1082,7 @@ namespace datatype {
                 for (accessor const* a : *c) {
                     func_decl_ref fn = a->instantiate(datatype);
                     res->push_back(fn);
-                    m_asts.push_back(fn);
+                    plugin().add_ast(fn);
                 }
                 break;
             }
@@ -1086,7 +1101,7 @@ namespace datatype {
     func_decl * util::get_constructor_recognizer(func_decl * con) {
         SASSERT(is_constructor(con));
         func_decl * d = nullptr;
-        if (m_constructor2recognizer.find(con, d))
+        if (plugin().m_constructor2recognizer.find(con, d))
             return d;
         sort * datatype = con->get_range();
         def const& dd = get_def(datatype);
@@ -1097,9 +1112,9 @@ namespace datatype {
         parameter ps[2] = { parameter(con), parameter(r) };
         d  = m.mk_func_decl(fid(), OP_DT_RECOGNISER, 2, ps, 1, &datatype);
         SASSERT(d);
-        m_asts.push_back(con);
+        plugin().add_ast(con);
-        m_asts.push_back(d);
+        plugin().add_ast(d);
-        m_constructor2recognizer.insert(con, d);
+        plugin().m_constructor2recognizer.insert(con, d);
         return d;
     }
 
@@ -1120,10 +1135,10 @@ namespace datatype {
     bool util::is_recursive(sort * ty) {
         SASSERT(is_datatype(ty));
         bool r = false;
-        if (!m_is_recursive.find(ty, r)) {
+        if (!plugin().m_is_recursive.find(ty, r)) {
             r = is_recursive_core(ty);
-            m_is_recursive.insert(ty, r);
+            plugin().m_is_recursive.insert(ty, r);
-            m_asts.push_back(ty);
+            plugin().add_ast(ty);
         }
         return r;
     }
@@ -1147,21 +1162,21 @@ namespace datatype {
         if (!is_datatype(s)) 
             return false;        
         bool r = false;
-        if (m_is_enum.find(s, r))
+        if (plugin().m_is_enum.find(s, r))
             return r;
         ptr_vector<func_decl> const& cnstrs = *get_datatype_constructors(s);
         r = true;
         for (unsigned i = 0; r && i < cnstrs.size(); ++i) 
             r = cnstrs[i]->get_arity() == 0;        
-        m_is_enum.insert(s, r);
+        plugin().m_is_enum.insert(s, r);
-        m_asts.push_back(s);
+        plugin().add_ast(s);
         return r;
     }
 
     func_decl * util::get_accessor_constructor(func_decl * accessor) { 
         SASSERT(is_accessor(accessor));
         func_decl * r = nullptr;
-        if (m_accessor2constructor.find(accessor, r))
+        if (plugin().m_accessor2constructor.find(accessor, r))
             return r;
         sort * datatype = accessor->get_domain(0);
         symbol c_id   = accessor->get_parameter(1).get_symbol();
@@ -1174,26 +1189,15 @@ namespace datatype {
             }
         }
         r = fn;
-        m_accessor2constructor.insert(accessor, r);
+        plugin().m_accessor2constructor.insert(accessor, r);
-        m_asts.push_back(accessor);
+        plugin().add_ast(accessor);
-        m_asts.push_back(r);
+        plugin().add_ast(r);
         return r;
     }
 
 
     void util::reset() {
-        m_datatype2constructors.reset();
+        plugin().reset();
-        m_datatype2nonrec_constructor.reset();
-        m_constructor2accessors.reset();
-        m_constructor2recognizer.reset();
-        m_recognizer2constructor.reset();
-        m_accessor2constructor.reset();
-        m_is_recursive.reset();
-        m_is_enum.reset();
-        std::for_each(m_vectors.begin(), m_vectors.end(), delete_proc<ptr_vector<func_decl> >());
-        m_vectors.reset();
-        m_asts.reset();
-        ++m_start;
     }
 
 
@@ -1205,7 +1209,7 @@ namespace datatype {
     func_decl * util::get_non_rec_constructor(sort * ty) {
         SASSERT(is_datatype(ty));
         cnstr_depth cd;
-        if (m_datatype2nonrec_constructor.find(ty, cd))
+        if (plugin().m_datatype2nonrec_constructor.find(ty, cd))
             return cd.first;
         ptr_vector<sort> forbidden_set;
         forbidden_set.push_back(ty);
@@ -1222,7 +1226,7 @@ namespace datatype {
        each T_i is not a datatype or it is a datatype t not in forbidden_set,
        and get_non_rec_constructor_core(T_i, forbidden_set union { T_i })
     */
-    util::cnstr_depth util::get_non_rec_constructor_core(sort * ty, ptr_vector<sort> & forbidden_set) {
+    cnstr_depth util::get_non_rec_constructor_core(sort * ty, ptr_vector<sort> & forbidden_set) {
         // We must select a constructor c(T_1, ..., T_n):T such that
         //   1) T_i's are not recursive
         // If there is no such constructor, then we select one that 
@@ -1231,7 +1235,7 @@ namespace datatype {
         ptr_vector<func_decl> const& constructors = *get_datatype_constructors(ty);
         array_util autil(m);
         cnstr_depth result(nullptr, 0);
-        if (m_datatype2nonrec_constructor.find(ty, result))
+        if (plugin().m_datatype2nonrec_constructor.find(ty, result))
             return result;
         TRACE("util_bug", tout << "get-non-rec constructor: " << sort_ref(ty, m) << "\n";
               tout << "forbidden: ";
@@ -1273,9 +1277,9 @@ namespace datatype {
             }
         }
         if (result.first) {
-            m_asts.push_back(result.first);
+            plugin().add_ast(result.first);
-            m_asts.push_back(ty);
+            plugin().add_ast(ty);
-            m_datatype2nonrec_constructor.insert(ty, result);
+            plugin().m_datatype2nonrec_constructor.insert(ty, result);
         }
         return result;
     }
@@ -1291,6 +1295,7 @@ namespace datatype {
         IF_VERBOSE(0, verbose_stream() << f->get_name() << "\n");
         for (constructor* c : d)
             IF_VERBOSE(0, verbose_stream() << "!= " << c->name() << "\n");
+        return UINT_MAX;
         SASSERT(false);
         UNREACHABLE();
         return 0;

src/ast/datatype_decl_plugin.h

@@ -198,6 +198,8 @@ namespace datatype {
         def* translate(ast_translation& tr, util& u);
     };
 
+    typedef std::pair<func_decl*, unsigned> cnstr_depth;
+
     namespace decl {
 
         class plugin : public decl_plugin {
@@ -213,6 +215,7 @@ namespace datatype {
 
             void log_axiom_definitions(symbol const& s, sort * new_sort);
 
+
         public:
             plugin(): m_id_counter(0), m_class_id(0), m_has_nested_rec(false) {}
             ~plugin() override;
@@ -259,6 +262,25 @@ namespace datatype {
 
             bool has_nested_rec() const { return m_has_nested_rec; }
 
+            void reset();
+
+
+            obj_map<sort, ptr_vector<func_decl>*>       m_datatype2constructors;
+            obj_map<sort, cnstr_depth>                  m_datatype2nonrec_constructor;
+            obj_map<func_decl, ptr_vector<func_decl>*>  m_constructor2accessors;
+            obj_map<func_decl, func_decl*>              m_constructor2recognizer;
+            obj_map<func_decl, func_decl*>              m_recognizer2constructor;
+            obj_map<func_decl, func_decl*>              m_accessor2constructor;
+            obj_map<sort, bool>                         m_is_recursive;
+            obj_map<sort, bool>                         m_is_enum;
+            mutable obj_map<sort, bool>                 m_is_fully_interp;
+            mutable ast_ref_vector* m_asts = nullptr;
+            sref_vector<param_size::size>               m_refs;
+            ptr_vector<ptr_vector<func_decl> >          m_vectors;
+            unsigned                                    m_start = 0;
+            mutable ptr_vector<sort>                    m_fully_interp_trail;
+            void add_ast(ast* a) const { if (!m_asts) m_asts = alloc(ast_ref_vector, *m_manager);  m_asts->push_back(a); }
+
         private:
             bool is_value_visit(bool unique, expr * arg, ptr_buffer<app> & todo) const;
             bool is_value_aux(bool unique, app * arg) const;
@@ -295,25 +317,10 @@ namespace datatype {
         ast_manager & m;
         mutable family_id     m_family_id;
         mutable decl::plugin* m_plugin;
-        typedef std::pair<func_decl*, unsigned> cnstr_depth;
+
 
         family_id fid() const;
-                
+                    
-        obj_map<sort, ptr_vector<func_decl> *>      m_datatype2constructors;
-        obj_map<sort, cnstr_depth>                  m_datatype2nonrec_constructor;
-        obj_map<func_decl, ptr_vector<func_decl> *> m_constructor2accessors;
-        obj_map<func_decl, func_decl *>             m_constructor2recognizer;
-        obj_map<func_decl, func_decl *>             m_recognizer2constructor;
-        obj_map<func_decl, func_decl *>             m_accessor2constructor;
-        obj_map<sort, bool>                         m_is_recursive;
-        obj_map<sort, bool>                         m_is_enum;
-        mutable obj_map<sort, bool>                 m_is_fully_interp;
-        mutable ast_ref_vector                      m_asts;
-        sref_vector<param_size::size>               m_refs;
-        ptr_vector<ptr_vector<func_decl> >          m_vectors;
-        unsigned                                    m_start;
-        mutable ptr_vector<sort>                    m_fully_interp_trail;
-        
         cnstr_depth get_non_rec_constructor_core(sort * ty, ptr_vector<sort> & forbidden_set);
 
         friend class decl::plugin;

src/math/lp/lp_settings.h

@@ -97,42 +97,41 @@ public:
 };
 
 struct statistics {
-    unsigned m_make_feasible;
+    unsigned m_make_feasible = 0;
-    unsigned m_total_iterations;
+    unsigned m_total_iterations = 0;
-    unsigned m_iters_with_no_cost_growing;
+    unsigned m_iters_with_no_cost_growing = 0;
-    unsigned m_num_factorizations;
+    unsigned m_num_factorizations = 0;
-    unsigned m_num_of_implied_bounds;
+    unsigned m_num_of_implied_bounds = 0;
-    unsigned m_need_to_solve_inf;
+    unsigned m_need_to_solve_inf = 0;
-    unsigned m_max_cols;
+    unsigned m_max_cols = 0;
-    unsigned m_max_rows;
+    unsigned m_max_rows = 0;
-    unsigned m_gcd_calls;
+    unsigned m_gcd_calls = 0;
-    unsigned m_gcd_conflicts;
+    unsigned m_gcd_conflicts = 0;
-    unsigned m_cube_calls;
+    unsigned m_cube_calls = 0;
-    unsigned m_cube_success;
+    unsigned m_cube_success = 0;
-    unsigned m_patches;
+    unsigned m_patches = 0;
-    unsigned m_patches_success;
+    unsigned m_patches_success = 0;
-    unsigned m_hnf_cutter_calls;
+    unsigned m_hnf_cutter_calls = 0;
-    unsigned m_hnf_cuts;
+    unsigned m_hnf_cuts = 0;
-    unsigned m_nla_calls;
+    unsigned m_nla_calls = 0;
-    unsigned m_gomory_cuts;
+    unsigned m_gomory_cuts = 0;
-    unsigned m_nla_add_bounds;
+    unsigned m_nla_add_bounds = 0;
-    unsigned m_nla_propagate_bounds;
+    unsigned m_nla_propagate_bounds = 0;
-    unsigned m_nla_propagate_eq;
+    unsigned m_nla_propagate_eq = 0;
-    unsigned m_nla_lemmas;
+    unsigned m_nla_lemmas = 0;
-    unsigned m_nra_calls;
+    unsigned m_nra_calls = 0;
-    unsigned m_nla_bounds_improvements;
+    unsigned m_nla_bounds_improvements = 0;
-    unsigned m_horner_calls;
+    unsigned m_horner_calls = 0;
-    unsigned m_horner_conflicts;
+    unsigned m_horner_conflicts = 0;
-    unsigned m_cross_nested_forms;
+    unsigned m_cross_nested_forms = 0;
-    unsigned m_grobner_calls;
+    unsigned m_grobner_calls = 0;
-    unsigned m_grobner_conflicts;
+    unsigned m_grobner_conflicts = 0;
-    unsigned m_offset_eqs;
+    unsigned m_offset_eqs = 0;
-    unsigned m_fixed_eqs;
+    unsigned m_fixed_eqs = 0;
-    ::statistics m_st;
+    ::statistics m_st = {};
-    statistics() { reset(); }
+
     void reset() {
-        memset(this, 0, sizeof(*this));
+        *this = statistics{};
-        m_st.reset();
     }
     void collect_statistics(::statistics& st) const {
         st.update("arith-factorizations", m_num_factorizations);

src/math/lp/static_matrix.h

@@ -79,7 +79,7 @@ public:
         ref(static_matrix & m, unsigned row, unsigned col):m_matrix(m), m_row(row), m_col(col) {}
         ref & operator=(T const & v) { m_matrix.set( m_row, m_col, v); return *this; }
 
-        ref operator=(ref & v) { m_matrix.set(m_row, m_col, v.m_matrix.get(v.m_row, v.m_col)); return *this; }
+        ref operator=(ref & v) { m_matrix.set(m_row, m_col, v.m_matrix.get_elem(v.m_row, v.m_col)); return *this; }
 
         operator T () const { return m_matrix.get_elem(m_row, m_col); }
     };

src/math/lp/static_matrix_def.h

@@ -92,7 +92,7 @@ static_matrix<T, X>::static_matrix(static_matrix const &A, unsigned * /* basis *
     init_row_columns(m, m);
     for (; m-- > 0; ) 
         for (auto & col : A.m_columns[m]) 
-            set(col.var(), m, A.get_value_of_column_cell(col));
+            set(col.var(), m, A.get_column_cell(col));
 }
 
 template <typename T, typename X> void static_matrix<T, X>::clear() {

src/nlsat/nlsat_simplify.cpp

@@ -141,6 +141,8 @@ namespace nlsat {
                 auto& a = *to_ineq_atom(a1);
                 if (a.size() != 2)
                     continue;
+                if (a.is_root_atom())
+                    continue;
 
                 auto* p = a.p(0);
                 auto* q = a.p(1);
@@ -229,6 +231,10 @@ namespace nlsat {
                     }
                     break;
                 }
+                default:
+                    SASSERT(a.is_root_atom());
+                    UNREACHABLE();
+                    break;
                 }
                 IF_VERBOSE(3, 
                 s.display(verbose_stream(), c) << " ->\n";

src/qe/mbp/mbp_basic_tg.cpp

@@ -101,7 +101,7 @@ struct mbp_basic_tg::impl {
                 bool is_or = m.is_or(term);
                 app *c = to_app(term);
                 bool t = is_or ? any_of(*c, is_true) : all_of(*c, is_true);
-                bool f = is_or ? all_of(*c, is_false) : all_of(*c, is_false);
+                bool f = is_or ? all_of(*c, is_false) : any_of(*c, is_false);
                 if (t || f) {
                     mark_seen(term);
                     progress = 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 <cassert>
 #include <iostream>
 #include "util/dlist.h"
@@ -160,10 +177,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 { 
+    bool invariant() const {
-        auto* e = this; 
+        auto* e = this;
-        const T* slow = static_cast<const T*>(this); 
+        do {
-        const T* fast = m_next; 
+            if (e->m_next->m_prev != e)
-        bool looped = false; 
+                return false;
-        // m_next of each node should point back to m_prev of the following node,
+            e = e->m_next;
-        // and m_prev of each node should point forward to m_next of the preceding node.
+        }
-        while (slow != fast) { 
+        while (e != this);
-            if (fast->m_prev->m_next != fast || fast->m_next->m_prev != fast) 
+        return true;
-                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; 
     }
 
     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;
 }