diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml index 679eeee3a..b371a03b5 100644 --- a/.github/workflows/coverage.yml +++ b/.github/workflows/coverage.yml @@ -3,6 +3,8 @@ name: Code Coverage on: push: branches: [ master ] + pull_request: + branches: [ master ] schedule: - cron: "0 11 * * *" diff --git a/.github/workflows/docker-image.yml b/.github/workflows/docker-image.yml index 3c02e2c2b..931ed071e 100644 --- a/.github/workflows/docker-image.yml +++ b/.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 diff --git a/src/api/python/z3/z3printer.py b/src/api/python/z3/z3printer.py index 2da5f89da..d7ee17f4a 100644 --- a/src/api/python/z3/z3printer.py +++ b/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)))) diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index a4ddbdaed..cc5c6eb75 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/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) { - dealloc(kv.m_value); - } + for (auto& kv : m_defs) + 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 >()); + 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 & 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_asts(m), - m_start(0) { + m_plugin(nullptr) { } @@ -1027,24 +1042,24 @@ namespace datatype { util::~util() { - std::for_each(m_vectors.begin(), m_vectors.end(), delete_proc >()); + } ptr_vector const * util::get_datatype_constructors(sort * ty) { SASSERT(is_datatype(ty)); ptr_vector * r = nullptr; - if (m_datatype2constructors.find(ty, r)) + if (plugin().m_datatype2constructors.find(ty, r)) return r; r = alloc(ptr_vector); - m_asts.push_back(ty); - m_vectors.push_back(r); - m_datatype2constructors.insert(ty, r); + plugin().add_ast(ty); + plugin().m_vectors.push_back(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 const * util::get_constructor_accessors(func_decl * con) { SASSERT(is_constructor(con)); ptr_vector * res = nullptr; - if (m_constructor2accessors.find(con, res)) { + if (plugin().m_constructor2accessors.find(con, res)) { return res; } res = alloc(ptr_vector); - m_asts.push_back(con); - m_vectors.push_back(res); - m_constructor2accessors.insert(con, res); + plugin().add_ast(con); + plugin().m_vectors.push_back(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); - m_asts.push_back(d); - m_constructor2recognizer.insert(con, d); + plugin().add_ast(con); + plugin().add_ast(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); - m_asts.push_back(ty); + plugin().m_is_recursive.insert(ty, r); + 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 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); - m_asts.push_back(s); + plugin().m_is_enum.insert(s, r); + 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); - m_asts.push_back(accessor); - m_asts.push_back(r); + plugin().m_accessor2constructor.insert(accessor, r); + plugin().add_ast(accessor); + plugin().add_ast(r); return r; } void util::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 >()); - m_vectors.reset(); - m_asts.reset(); - ++m_start; + plugin().reset(); } @@ -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 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 & forbidden_set) { + cnstr_depth util::get_non_rec_constructor_core(sort * ty, ptr_vector & 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 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); - m_asts.push_back(ty); - m_datatype2nonrec_constructor.insert(ty, result); + plugin().add_ast(result.first); + plugin().add_ast(ty); + 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; diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index 341f3669b..ca33b48c1 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -198,6 +198,8 @@ namespace datatype { def* translate(ast_translation& tr, util& u); }; + typedef std::pair 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*> m_datatype2constructors; + obj_map m_datatype2nonrec_constructor; + obj_map*> m_constructor2accessors; + obj_map m_constructor2recognizer; + obj_map m_recognizer2constructor; + obj_map m_accessor2constructor; + obj_map m_is_recursive; + obj_map m_is_enum; + mutable obj_map m_is_fully_interp; + mutable ast_ref_vector* m_asts = nullptr; + sref_vector m_refs; + ptr_vector > m_vectors; + unsigned m_start = 0; + mutable ptr_vector 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 & 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 cnstr_depth; + family_id fid() const; - - obj_map *> m_datatype2constructors; - obj_map m_datatype2nonrec_constructor; - obj_map *> m_constructor2accessors; - obj_map m_constructor2recognizer; - obj_map m_recognizer2constructor; - obj_map m_accessor2constructor; - obj_map m_is_recursive; - obj_map m_is_enum; - mutable obj_map m_is_fully_interp; - mutable ast_ref_vector m_asts; - sref_vector m_refs; - ptr_vector > m_vectors; - unsigned m_start; - mutable ptr_vector m_fully_interp_trail; - + cnstr_depth get_non_rec_constructor_core(sort * ty, ptr_vector & forbidden_set); friend class decl::plugin; diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index d1a4be21c..0d47877c7 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -97,42 +97,41 @@ public: }; struct statistics { - unsigned m_make_feasible; - unsigned m_total_iterations; - unsigned m_iters_with_no_cost_growing; - unsigned m_num_factorizations; - unsigned m_num_of_implied_bounds; - unsigned m_need_to_solve_inf; - unsigned m_max_cols; - unsigned m_max_rows; - unsigned m_gcd_calls; - unsigned m_gcd_conflicts; - unsigned m_cube_calls; - unsigned m_cube_success; - unsigned m_patches; - unsigned m_patches_success; - unsigned m_hnf_cutter_calls; - unsigned m_hnf_cuts; - unsigned m_nla_calls; - unsigned m_gomory_cuts; - unsigned m_nla_add_bounds; - unsigned m_nla_propagate_bounds; - unsigned m_nla_propagate_eq; - unsigned m_nla_lemmas; - unsigned m_nra_calls; - unsigned m_nla_bounds_improvements; - unsigned m_horner_calls; - unsigned m_horner_conflicts; - unsigned m_cross_nested_forms; - unsigned m_grobner_calls; - unsigned m_grobner_conflicts; - unsigned m_offset_eqs; - unsigned m_fixed_eqs; - ::statistics m_st; - statistics() { reset(); } + unsigned m_make_feasible = 0; + unsigned m_total_iterations = 0; + unsigned m_iters_with_no_cost_growing = 0; + unsigned m_num_factorizations = 0; + unsigned m_num_of_implied_bounds = 0; + unsigned m_need_to_solve_inf = 0; + unsigned m_max_cols = 0; + unsigned m_max_rows = 0; + unsigned m_gcd_calls = 0; + unsigned m_gcd_conflicts = 0; + unsigned m_cube_calls = 0; + unsigned m_cube_success = 0; + unsigned m_patches = 0; + unsigned m_patches_success = 0; + unsigned m_hnf_cutter_calls = 0; + unsigned m_hnf_cuts = 0; + unsigned m_nla_calls = 0; + unsigned m_gomory_cuts = 0; + unsigned m_nla_add_bounds = 0; + unsigned m_nla_propagate_bounds = 0; + unsigned m_nla_propagate_eq = 0; + unsigned m_nla_lemmas = 0; + unsigned m_nra_calls = 0; + unsigned m_nla_bounds_improvements = 0; + unsigned m_horner_calls = 0; + unsigned m_horner_conflicts = 0; + unsigned m_cross_nested_forms = 0; + unsigned m_grobner_calls = 0; + unsigned m_grobner_conflicts = 0; + unsigned m_offset_eqs = 0; + unsigned m_fixed_eqs = 0; + ::statistics m_st = {}; + void reset() { - memset(this, 0, sizeof(*this)); - m_st.reset(); + *this = statistics{}; } void collect_statistics(::statistics& st) const { st.update("arith-factorizations", m_num_factorizations); diff --git a/src/math/lp/static_matrix.h b/src/math/lp/static_matrix.h index 9d6bb8599..42dd476b5 100644 --- a/src/math/lp/static_matrix.h +++ b/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); } }; diff --git a/src/math/lp/static_matrix_def.h b/src/math/lp/static_matrix_def.h index 0370ee899..c3b2fc168 100644 --- a/src/math/lp/static_matrix_def.h +++ b/src/math/lp/static_matrix_def.h @@ -92,7 +92,7 @@ static_matrix::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 void static_matrix::clear() { diff --git a/src/nlsat/nlsat_simplify.cpp b/src/nlsat/nlsat_simplify.cpp index 8148d721f..2901d22c2 100644 --- a/src/nlsat/nlsat_simplify.cpp +++ b/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"; diff --git a/src/qe/mbp/mbp_basic_tg.cpp b/src/qe/mbp/mbp_basic_tg.cpp index ce5e99eb1..693624871 100644 --- a/src/qe/mbp/mbp_basic_tg.cpp +++ b/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; diff --git a/src/test/dlist.cpp b/src/test/dlist.cpp index dfc1138b7..1bf3f17ef 100644 --- a/src/test/dlist.cpp +++ b/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 #include #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; } diff --git a/src/test/hashtable.cpp b/src/test/hashtable.cpp index fb8042dc7..e26fbd5d8 100644 --- a/src/test/hashtable.cpp +++ b/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 #include #include - #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 ht; + VERIFY(ht.empty()); + VERIFY(ht.size() == 0); + VERIFY(ht.capacity() == DEFAULT_HASHTABLE_INITIAL_CAPACITY); + + // Copy constructor + hashtable ht_copy(ht); + VERIFY(ht_copy.empty()); + VERIFY(ht_copy.size() == 0); + VERIFY(ht_copy.capacity() == ht.capacity()); + + // Move constructor + hashtable 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 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 ht; + ht.insert(1); + ht.remove(1); + VERIFY(ht.empty()); + VERIFY(ht.size() == 0); +} + +void test_hashtable_find() { + hashtable ht; + ht.insert(1); + int value; + VERIFY(ht.find(1, value) && value == 1); + VERIFY(!ht.find(2, value)); +} + +void test_hashtable_contains() { + hashtable ht; + ht.insert(1); + VERIFY(ht.contains(1)); + VERIFY(!ht.contains(2)); +} + +void test_hashtable_reset() { + hashtable ht; + ht.insert(1); + ht.reset(); + VERIFY(ht.empty()); + VERIFY(ht.size() == 0); +} + +void test_hashtable_finalize() { + hashtable ht; + ht.insert(1); + ht.finalize(); + VERIFY(ht.empty()); + VERIFY(ht.size() == 0); +} + +void test_hashtable_iterators() { + hashtable 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 ht1; + hashtable 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() { diff --git a/src/util/dlist.h b/src/util/dlist.h index 52cb25548..4c0e51e58 100644 --- a/src/util/dlist.h +++ b/src/util/dlist.h @@ -155,23 +155,15 @@ public: elem->init(elem); } - bool invariant() const { - auto* e = this; - const T* slow = static_cast(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(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) { diff --git a/src/util/hashtable.h b/src/util/hashtable.h index b59a2e7d8..acbe2a818 100644 --- a/src/util/hashtable.h +++ b/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; 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; }