From bc636d7ee00b7ead1de4e9537930fce9d85a958d Mon Sep 17 00:00:00 2001 From: LiviaSun <33578456+ChuyueSun@users.noreply.github.com> Date: Fri, 19 Jul 2024 14:01:42 -0700 Subject: [PATCH 01/18] new hashtable.h invariants (#7296) * add copyright for dlist unit test * new hashtable invariants * add copyright --- src/test/dlist.cpp | 17 +++++++++++++++++ src/util/hashtable.h | 14 ++++++++++++++ 2 files changed, 31 insertions(+) diff --git a/src/test/dlist.cpp b/src/test/dlist.cpp index dfc1138b7..200a0a329 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" 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; From 80ac7b34387cddb88f2286b0716dd44ede982b78 Mon Sep 17 00:00:00 2001 From: LiviaSun <33578456+ChuyueSun@users.noreply.github.com> Date: Fri, 19 Jul 2024 14:03:21 -0700 Subject: [PATCH 02/18] new heap invariants (#7298) * new heap invariants * change ENSURE to SASSERT for unit test heap * change SASSERT to VERIFY --- src/test/heap.cpp | 24 +++++++++++++----------- src/util/heap.h | 13 +++++++++++++ 2 files changed, 26 insertions(+), 11 deletions(-) diff --git a/src/test/heap.cpp b/src/test/heap.cpp index 6a5bc7b9f..f30f45c32 100644 --- a/src/test/heap.cpp +++ b/src/test/heap.cpp @@ -38,7 +38,7 @@ static void tst1() { for (int i = 0; i < N * 3; i++) { int val = heap_rand() % N; if (!h.contains(val)) { - ENSURE(!t.contains(val)); + VERIFY(!t.contains(val)); h.insert(val); t.insert(val); } @@ -46,26 +46,26 @@ static void tst1() { if (!t.contains(val)) { for (int v : t) std::cout << v << "\n"; } - ENSURE(t.contains(val)); + VERIFY(t.contains(val)); } } - ENSURE(h.check_invariant()); + VERIFY(h.check_invariant()); for (int v : t) { - ENSURE(h.contains(v)); + VERIFY(h.contains(v)); } while (!h.empty()) { int m1 = h.min_value(); int m2 = h.erase_min(); (void)m1; (void)m2; - ENSURE(m1 == m2); - ENSURE(-1 < m2); + VERIFY(m1 == m2); + VERIFY(-1 < m2); } } int g_value[N]; -struct lt_proc2 { bool operator()(int v1, int v2) const { ENSURE(v1 < N && v2 < N); return g_value[v1] < g_value[v2]; } }; +struct lt_proc2 { bool operator()(int v1, int v2) const { VERIFY(v1 < N && v2 < N); return g_value[v1] < g_value[v2]; } }; typedef heap int_heap2; static void init_values() { @@ -98,7 +98,7 @@ static void tst2() { TRACE("heap", tout << "inserting: " << val << "\n";); h.insert(val); TRACE("heap", dump_heap(h, tout);); - ENSURE(h.contains(val)); + VERIFY(h.contains(val)); } } else if (cmd <= 6) { @@ -107,7 +107,7 @@ static void tst2() { TRACE("heap", tout << "removing: " << val << "\n";); h.erase(val); TRACE("heap", dump_heap(h, tout);); - ENSURE(!h.contains(val)); + VERIFY(!h.contains(val)); } } else if (cmd <= 8) { @@ -128,10 +128,12 @@ static void tst2() { } } else { - ENSURE(h.check_invariant()); + VERIFY(h.check_invariant()); } } - ENSURE(h.check_invariant()); + VERIFY(h.check_invariant()); + h.reset(); + VERIFY(h.check_invariant()); } void tst_heap() { diff --git a/src/util/heap.h b/src/util/heap.h index c080c6ebd..3bee2fe9f 100644 --- a/src/util/heap.h +++ b/src/util/heap.h @@ -55,6 +55,19 @@ class heap : private LT { } bool check_invariant_core(int idx) const { + + // Check that m_values starts with a dummy value at index 0. + if (m_values.empty() || m_values[0] != -1) { + return false; + } + + // All indices in m_value2indices that are not used in m_values should be 0 + for (int val = 0; val < static_cast(m_value2indices.size()); ++val) { + if (std::find(m_values.begin(), m_values.end(), val) == m_values.end() && m_value2indices[val] != 0) { + return false; // Unused indices should have a 0 value + } + } + if (idx < static_cast(m_values.size())) { SASSERT(m_value2indices[m_values[idx]] == idx); SASSERT(parent(idx) == 0 || !less_than(m_values[idx], m_values[parent(idx)])); From 5003d41cdbc392eacea5d73d1065259ec9a0dadf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 19 Jul 2024 19:11:54 -0700 Subject: [PATCH 03/18] Revert "New invariant for dlist (#7294)" (#7301) This reverts commit cf4d0e74a53428192d5c4cb8d5a033431828deb2. --- src/util/dlist.h | 26 +++++++++----------------- 1 file changed, 9 insertions(+), 17 deletions(-) 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) { 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 04/18] 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; } From 3d014f8b335a3ed88fbdae0265d46bae9b196399 Mon Sep 17 00:00:00 2001 From: LiviaSun <33578456+ChuyueSun@users.noreply.github.com> Date: Fri, 19 Jul 2024 20:34:29 -0700 Subject: [PATCH 05/18] add new hashtable unit tests (#7297) * add new hashtable unit tests * add copyright * use VERIFY instead of assert --- src/test/hashtable.cpp | 117 ++++++++++++++++++++++++++++++++++++++++- 1 file changed, 116 insertions(+), 1 deletion(-) 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() { From 966c9a3764dd760efc079b1ee3a5732210c4a8ac Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 21 Jul 2024 21:07:09 -0700 Subject: [PATCH 06/18] Revert "new heap invariants (#7298)" (#7303) This reverts commit 80ac7b34387cddb88f2286b0716dd44ede982b78. --- src/test/heap.cpp | 24 +++++++++++------------- src/util/heap.h | 13 ------------- 2 files changed, 11 insertions(+), 26 deletions(-) diff --git a/src/test/heap.cpp b/src/test/heap.cpp index f30f45c32..6a5bc7b9f 100644 --- a/src/test/heap.cpp +++ b/src/test/heap.cpp @@ -38,7 +38,7 @@ static void tst1() { for (int i = 0; i < N * 3; i++) { int val = heap_rand() % N; if (!h.contains(val)) { - VERIFY(!t.contains(val)); + ENSURE(!t.contains(val)); h.insert(val); t.insert(val); } @@ -46,26 +46,26 @@ static void tst1() { if (!t.contains(val)) { for (int v : t) std::cout << v << "\n"; } - VERIFY(t.contains(val)); + ENSURE(t.contains(val)); } } - VERIFY(h.check_invariant()); + ENSURE(h.check_invariant()); for (int v : t) { - VERIFY(h.contains(v)); + ENSURE(h.contains(v)); } while (!h.empty()) { int m1 = h.min_value(); int m2 = h.erase_min(); (void)m1; (void)m2; - VERIFY(m1 == m2); - VERIFY(-1 < m2); + ENSURE(m1 == m2); + ENSURE(-1 < m2); } } int g_value[N]; -struct lt_proc2 { bool operator()(int v1, int v2) const { VERIFY(v1 < N && v2 < N); return g_value[v1] < g_value[v2]; } }; +struct lt_proc2 { bool operator()(int v1, int v2) const { ENSURE(v1 < N && v2 < N); return g_value[v1] < g_value[v2]; } }; typedef heap int_heap2; static void init_values() { @@ -98,7 +98,7 @@ static void tst2() { TRACE("heap", tout << "inserting: " << val << "\n";); h.insert(val); TRACE("heap", dump_heap(h, tout);); - VERIFY(h.contains(val)); + ENSURE(h.contains(val)); } } else if (cmd <= 6) { @@ -107,7 +107,7 @@ static void tst2() { TRACE("heap", tout << "removing: " << val << "\n";); h.erase(val); TRACE("heap", dump_heap(h, tout);); - VERIFY(!h.contains(val)); + ENSURE(!h.contains(val)); } } else if (cmd <= 8) { @@ -128,12 +128,10 @@ static void tst2() { } } else { - VERIFY(h.check_invariant()); + ENSURE(h.check_invariant()); } } - VERIFY(h.check_invariant()); - h.reset(); - VERIFY(h.check_invariant()); + ENSURE(h.check_invariant()); } void tst_heap() { diff --git a/src/util/heap.h b/src/util/heap.h index 3bee2fe9f..c080c6ebd 100644 --- a/src/util/heap.h +++ b/src/util/heap.h @@ -55,19 +55,6 @@ class heap : private LT { } bool check_invariant_core(int idx) const { - - // Check that m_values starts with a dummy value at index 0. - if (m_values.empty() || m_values[0] != -1) { - return false; - } - - // All indices in m_value2indices that are not used in m_values should be 0 - for (int val = 0; val < static_cast(m_value2indices.size()); ++val) { - if (std::find(m_values.begin(), m_values.end(), val) == m_values.end() && m_value2indices[val] != 0) { - return false; // Unused indices should have a 0 value - } - } - if (idx < static_cast(m_values.size())) { SASSERT(m_value2indices[m_values[idx]] == idx); SASSERT(parent(idx) == 0 || !less_than(m_values[idx], m_values[parent(idx)])); From 2013cd13b20ba1f9a36e41872ccd4f696657ec58 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 21 Jul 2024 21:08:53 -0700 Subject: [PATCH 07/18] Update coverage.yml run code coverage on pull requests --- .github/workflows/coverage.yml | 2 ++ 1 file changed, 2 insertions(+) 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 * * *" From b535509cca09f6c5593d5755c251d74daba4de50 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 22 Jul 2024 08:43:22 -0700 Subject: [PATCH 08/18] remove crashing test Signed-off-by: Nikolaj Bjorner --- src/test/dlist.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/test/dlist.cpp b/src/test/dlist.cpp index 200a0a329..1bf3f17ef 100644 --- a/src/test/dlist.cpp +++ b/src/test/dlist.cpp @@ -177,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; } From 1e6b13741c6368a1bc66c06c1497891da1c95b7c Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Mon, 22 Jul 2024 15:42:40 -0700 Subject: [PATCH 09/18] Bump docker/build-push-action from 6.4.0 to 6.5.0 (#7304) Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 6.4.0 to 6.5.0. - [Release notes](https://github.com/docker/build-push-action/releases) - [Commits](https://github.com/docker/build-push-action/compare/v6.4.0...v6.5.0) --- updated-dependencies: - dependency-name: docker/build-push-action dependency-type: direct:production update-type: version-update:semver-minor ... Signed-off-by: dependabot[bot] Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> --- .github/workflows/docker-image.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 From 5f6bb3db3e3fd054f42ee1382bab1152f4b86a5c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 27 Jul 2024 08:26:42 +0200 Subject: [PATCH 10/18] fix #7311 Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_simplify.cpp | 6 ++++++ 1 file changed, 6 insertions(+) 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"; From f94500c3cad3e8a1ac855bcf205a6bc38e84bc69 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 28 Jul 2024 13:18:08 +0200 Subject: [PATCH 11/18] fix #7309 --- src/ast/datatype_decl_plugin.cpp | 103 +++++++++++++++++-------------- src/ast/datatype_decl_plugin.h | 41 +++++++----- 2 files changed, 79 insertions(+), 65 deletions(-) diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index a4ddbdaed..c39b09d5e 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -231,6 +231,24 @@ namespace datatype { } m_defs.reset(); m_util = nullptr; // force deletion + dealloc(m_asts); + std::for_each(m_vectors.begin(), m_vectors.end(), delete_proc >()); + } + + 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 +596,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 +818,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 +915,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 +1027,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 +1044,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 +1070,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 +1084,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 +1103,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 +1114,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 +1137,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 +1164,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 +1191,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 +1211,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 +1228,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 +1237,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 +1279,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 +1297,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..f68dcfbdd 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,24 @@ namespace datatype { void log_axiom_definitions(symbol const& s, sort * new_sort); + + friend class util; + 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); } + public: plugin(): m_id_counter(0), m_class_id(0), m_has_nested_rec(false) {} ~plugin() override; @@ -259,6 +279,8 @@ namespace datatype { bool has_nested_rec() const { return m_has_nested_rec; } + void reset(); + 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; From ac7014a68b26363676a09badc1249bf9637316fd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 29 Jul 2024 03:18:20 +0200 Subject: [PATCH 12/18] expose public Signed-off-by: Nikolaj Bjorner --- src/ast/datatype_decl_plugin.h | 34 +++++++++++++++++----------------- 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index f68dcfbdd..ca33b48c1 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -216,23 +216,6 @@ namespace datatype { void log_axiom_definitions(symbol const& s, sort * new_sort); - friend class util; - 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); } - public: plugin(): m_id_counter(0), m_class_id(0), m_has_nested_rec(false) {} ~plugin() override; @@ -281,6 +264,23 @@ namespace datatype { 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; From 25e683e4e195609c8f6e728305aa9517f7d5fe61 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 28 Jul 2024 19:10:30 -0700 Subject: [PATCH 13/18] fix finalize method Signed-off-by: Nikolaj Bjorner --- src/ast/datatype_decl_plugin.cpp | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index c39b09d5e..cc5c6eb75 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -220,19 +220,17 @@ 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 - dealloc(m_asts); - std::for_each(m_vectors.begin(), m_vectors.end(), delete_proc >()); + reset(); } void plugin::reset() { From 2ce89e5f491fa817d02d8fdce8c62798beab258b Mon Sep 17 00:00:00 2001 From: David Seifert <16636962+SoapGentoo@users.noreply.github.com> Date: Mon, 29 Jul 2024 20:07:10 +0200 Subject: [PATCH 14/18] Gcc 15 two phase (#7313) * Fix `-Wclass-memaccess` * Fix for GCC 15 two-phase lookup * GCC 15 is more aggressive about checking dependent names: https://gcc.gnu.org/git/?p=gcc.git;a=commitdiff;h=r15-2117-g313afcfdabeab3 Bug: https://bugs.gentoo.org/936634 --- src/math/lp/lp_settings.h | 69 ++++++++++++++++----------------- src/math/lp/static_matrix.h | 2 +- src/math/lp/static_matrix_def.h | 2 +- 3 files changed, 36 insertions(+), 37 deletions(-) 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() { From 2ae3d87b21c99184951f7ec0380675a5e00ba778 Mon Sep 17 00:00:00 2001 From: LiviaSun <33578456+ChuyueSun@users.noreply.github.com> Date: Mon, 29 Jul 2024 11:08:54 -0700 Subject: [PATCH 15/18] add scoped vector unit test (#7307) * add scoped vector unit test * fix dlist tests * add new scoped vector invariants --- src/test/CMakeLists.txt | 1 + src/test/dlist.cpp | 79 +++++++++++++++--------------- src/test/main.cpp | 1 + src/test/scoped_vector.cpp | 99 ++++++++++++++++++++++++++++++++++++++ src/util/scoped_vector.h | 44 +++++++++++++++-- 5 files changed, 180 insertions(+), 44 deletions(-) create mode 100644 src/test/scoped_vector.cpp diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index 8464cedf9..658647ea6 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -106,6 +106,7 @@ add_executable(test-z3 sat_lookahead.cpp sat_user_scope.cpp scoped_timer.cpp + scoped_vector.cpp simple_parser.cpp simplex.cpp simplifier.cpp diff --git a/src/test/dlist.cpp b/src/test/dlist.cpp index 1bf3f17ef..14991c9ac 100644 --- a/src/test/dlist.cpp +++ b/src/test/dlist.cpp @@ -15,7 +15,6 @@ Author: --*/ -#include #include #include "util/dlist.h" @@ -30,28 +29,28 @@ public: // Test the prev() method void test_prev() { TestNode node(1); - assert(node.prev() == &node); + SASSERT(node.prev() == &node); std::cout << "test_prev passed." << std::endl; } // Test the next() method void test_next() { TestNode node(1); - assert(node.next() == &node); + SASSERT(node.next() == &node); std::cout << "test_next passed." << std::endl; } // Test the const prev() method void test_const_prev() { const TestNode node(1); - assert(node.prev() == &node); + SASSERT(node.prev() == &node); std::cout << "test_const_prev passed." << std::endl; } // Test the const next() method void test_const_next() { const TestNode node(1); - assert(node.next() == &node); + SASSERT(node.next() == &node); std::cout << "test_const_next passed." << std::endl; } @@ -59,9 +58,9 @@ void test_const_next() { void test_init() { TestNode node(1); node.init(&node); - assert(node.next() == &node); - assert(node.prev() == &node); - assert(node.invariant()); + SASSERT(node.next() == &node); + SASSERT(node.prev() == &node); + SASSERT(node.invariant()); std::cout << "test_init passed." << std::endl; } @@ -71,10 +70,10 @@ void test_pop() { TestNode node1(1); TestNode::push_to_front(list, &node1); TestNode* popped = TestNode::pop(list); - assert(popped == &node1); - assert(list == nullptr); - assert(popped->next() == popped); - assert(popped->prev() == popped); + SASSERT(popped == &node1); + SASSERT(list == nullptr); + SASSERT(popped->next() == popped); + SASSERT(popped->prev() == popped); std::cout << "test_pop passed." << std::endl; } @@ -83,12 +82,12 @@ void test_insert_after() { TestNode node1(1); TestNode node2(2); node1.insert_after(&node2); - assert(node1.next() == &node2); - assert(node2.prev() == &node1); - assert(node1.prev() == &node2); - assert(node2.next() == &node1); - assert(node1.invariant()); - assert(node2.invariant()); + SASSERT(node1.next() == &node2); + SASSERT(node2.prev() == &node1); + SASSERT(node1.prev() == &node2); + SASSERT(node2.next() == &node1); + SASSERT(node1.invariant()); + SASSERT(node2.invariant()); std::cout << "test_insert_after passed." << std::endl; } @@ -97,12 +96,12 @@ void test_insert_before() { TestNode node1(1); TestNode node2(2); node1.insert_before(&node2); - assert(node1.prev() == &node2); - assert(node2.next() == &node1); - assert(node1.next() == &node2); - assert(node2.prev() == &node1); - assert(node1.invariant()); - assert(node2.invariant()); + SASSERT(node1.prev() == &node2); + SASSERT(node2.next() == &node1); + SASSERT(node1.next() == &node2); + SASSERT(node2.prev() == &node1); + SASSERT(node1.invariant()); + SASSERT(node2.invariant()); std::cout << "test_insert_before passed." << std::endl; } @@ -114,11 +113,9 @@ void test_remove_from() { TestNode::push_to_front(list, &node1); TestNode::push_to_front(list, &node2); TestNode::remove_from(list, &node1); - assert(list == &node2); - assert(node2.next() == &node2); - assert(node2.prev() == &node2); - assert(node1.next() == &node1); - assert(node1.prev() == &node1); + SASSERT(list == &node2); + SASSERT(node2.next() == &node2); + SASSERT(node2.prev() == &node2); std::cout << "test_remove_from passed." << std::endl; } @@ -127,9 +124,9 @@ void test_push_to_front() { TestNode* list = nullptr; TestNode node1(1); TestNode::push_to_front(list, &node1); - assert(list == &node1); - assert(node1.next() == &node1); - assert(node1.prev() == &node1); + SASSERT(list == &node1); + SASSERT(node1.next() == &node1); + SASSERT(node1.prev() == &node1); std::cout << "test_push_to_front passed." << std::endl; } @@ -137,20 +134,20 @@ void test_push_to_front() { void test_detach() { TestNode node(1); TestNode::detach(&node); - assert(node.next() == &node); - assert(node.prev() == &node); - assert(node.invariant()); + SASSERT(node.next() == &node); + SASSERT(node.prev() == &node); + SASSERT(node.invariant()); std::cout << "test_detach passed." << std::endl; } // Test the invariant() method void test_invariant() { TestNode node1(1); - assert(node1.invariant()); + SASSERT(node1.invariant()); TestNode node2(2); node1.insert_after(&node2); - assert(node1.invariant()); - assert(node2.invariant()); + SASSERT(node1.invariant()); + SASSERT(node2.invariant()); std::cout << "test_invariant passed." << std::endl; } @@ -161,10 +158,10 @@ void test_contains() { TestNode node2(2); TestNode::push_to_front(list, &node1); TestNode::push_to_front(list, &node2); - assert(TestNode::contains(list, &node1)); - assert(TestNode::contains(list, &node2)); + SASSERT(TestNode::contains(list, &node1)); + SASSERT(TestNode::contains(list, &node2)); TestNode node3(3); - assert(!TestNode::contains(list, &node3)); + SASSERT(!TestNode::contains(list, &node3)); std::cout << "test_contains passed." << std::endl; } diff --git a/src/test/main.cpp b/src/test/main.cpp index 0d3679529..f028d6ceb 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -269,4 +269,5 @@ int main(int argc, char ** argv) { TST(euf_bv_plugin); TST(euf_arith_plugin); TST(sls_test); + TST(scoped_vector); } diff --git a/src/test/scoped_vector.cpp b/src/test/scoped_vector.cpp new file mode 100644 index 000000000..05d98fcf1 --- /dev/null +++ b/src/test/scoped_vector.cpp @@ -0,0 +1,99 @@ +#include +#include "util/scoped_vector.h" + +void test_push_back_and_access() { + scoped_vector sv; + sv.push_back(10); + + sv.push_back(20); + + SASSERT(sv.size() == 2); + SASSERT(sv[0] == 10); + SASSERT(sv[1] == 20); + + std::cout << "test_push_back_and_access passed." << std::endl; +} + +void test_scopes() { + scoped_vector sv; + sv.push_back(10); + sv.push_back(20); + + sv.push_scope(); + sv.push_back(30); + sv.push_back(40); + + SASSERT(sv.size() == 4); + SASSERT(sv[2] == 30); + SASSERT(sv[3] == 40); + + sv.pop_scope(1); + + std::cout << "test_scopes passed." << std::endl; + SASSERT(sv.size() == 2); + SASSERT(sv[0] == 10); + SASSERT(sv[1] == 20); + + std::cout << "test_scopes passed." << std::endl; +} + +void test_set() { + scoped_vector sv; + sv.push_back(10); + sv.push_back(20); + + sv.set(0, 30); + sv.set(1, 40); + + SASSERT(sv.size() == 2); + SASSERT(sv[0] == 30); + SASSERT(sv[1] == 40); + + sv.push_scope(); + sv.set(0, 50); + SASSERT(sv[0] == 50); + sv.pop_scope(1); + SASSERT(sv[0] == 30); + + std::cout << "test_set passed." << std::endl; +} + +void test_pop_back() { + scoped_vector sv; + sv.push_back(10); + sv.push_back(20); + + SASSERT(sv.size() == 2); + sv.pop_back(); + SASSERT(sv.size() == 1); + SASSERT(sv[0] == 10); + sv.pop_back(); + SASSERT(sv.size() == 0); + + std::cout << "test_pop_back passed." << std::endl; +} + +void test_erase_and_swap() { + scoped_vector sv; + sv.push_back(10); + sv.push_back(20); + sv.push_back(30); + + sv.erase_and_swap(1); + + SASSERT(sv.size() == 2); + SASSERT(sv[0] == 10); + SASSERT(sv[1] == 30); + + std::cout << "test_erase_and_swap passed." << std::endl; +} + +void tst_scoped_vector() { + test_push_back_and_access(); + test_scopes(); + test_set(); + test_pop_back(); + test_erase_and_swap(); + + std::cout << "All tests passed." << std::endl; +} diff --git a/src/util/scoped_vector.h b/src/util/scoped_vector.h index 2c6cfaa21..b5945fb44 100644 --- a/src/util/scoped_vector.h +++ b/src/util/scoped_vector.h @@ -176,8 +176,46 @@ private: } bool invariant() const { - return - m_size <= m_elems.size() && - m_elems_start <= m_elems.size(); + + + if (!(m_size <= m_elems.size() && m_elems_start <= m_elems.size())) + return false; + + // Check that source and destination trails have the same length. + if (m_src.size() != m_dst.size()) + return false; + // The size of m_src, m_dst, and m_src_lim should be consistent with the scope stack. + if (m_src_lim.size() != m_sizes.size() || m_src.size() != m_dst.size()) + return false; + + // m_elems_lim stores the past sizes of m_elems for each scope. Each element in m_elems_lim should be + // within bounds and in non-decreasing order. + for (unsigned i = 1; i < m_elems_lim.size(); ++i) { + if (m_elems_lim[i - 1] > m_elems_lim[i]) return false; + } + + + // m_sizes tracks the size of the vector at each scope level. + // Each element in m_sizes should be non-decreasing and within the size of m_elems. + for (unsigned i = 1; i < m_sizes.size(); ++i) { + if (m_sizes[i - 1] > m_sizes[i]) + return false; + } + + // The m_src and m_dst vectors should have the same size and should contain valid indices. + if (m_src.size() != m_dst.size()) return false; + for (unsigned i = 0; i < m_src.size(); ++i) { + if (m_src[i] >= m_index.size() || m_dst[i] >= m_elems.size()) return false; + } + + + // The size of m_src_lim should be less than or equal to the size of m_sizes and store valid indices. + if (m_src_lim.size() > m_sizes.size()) return false; + for (unsigned elem : m_src_lim) { + if (elem > m_src.size()) return false; + } + + return true; + } }; From 5fcc50f60635fd2a0a77e3c5dfc2c6234cb8a81a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Jul 2024 11:34:02 -0700 Subject: [PATCH 16/18] Revert "add scoped vector unit test (#7307)" (#7317) This reverts commit 2ae3d87b21c99184951f7ec0380675a5e00ba778. --- src/test/CMakeLists.txt | 1 - src/test/dlist.cpp | 79 +++++++++++++++--------------- src/test/main.cpp | 1 - src/test/scoped_vector.cpp | 99 -------------------------------------- src/util/scoped_vector.h | 44 ++--------------- 5 files changed, 44 insertions(+), 180 deletions(-) delete mode 100644 src/test/scoped_vector.cpp diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index 658647ea6..8464cedf9 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -106,7 +106,6 @@ add_executable(test-z3 sat_lookahead.cpp sat_user_scope.cpp scoped_timer.cpp - scoped_vector.cpp simple_parser.cpp simplex.cpp simplifier.cpp diff --git a/src/test/dlist.cpp b/src/test/dlist.cpp index 14991c9ac..1bf3f17ef 100644 --- a/src/test/dlist.cpp +++ b/src/test/dlist.cpp @@ -15,6 +15,7 @@ Author: --*/ +#include #include #include "util/dlist.h" @@ -29,28 +30,28 @@ public: // Test the prev() method void test_prev() { TestNode node(1); - SASSERT(node.prev() == &node); + assert(node.prev() == &node); std::cout << "test_prev passed." << std::endl; } // Test the next() method void test_next() { TestNode node(1); - SASSERT(node.next() == &node); + assert(node.next() == &node); std::cout << "test_next passed." << std::endl; } // Test the const prev() method void test_const_prev() { const TestNode node(1); - SASSERT(node.prev() == &node); + assert(node.prev() == &node); std::cout << "test_const_prev passed." << std::endl; } // Test the const next() method void test_const_next() { const TestNode node(1); - SASSERT(node.next() == &node); + assert(node.next() == &node); std::cout << "test_const_next passed." << std::endl; } @@ -58,9 +59,9 @@ void test_const_next() { void test_init() { TestNode node(1); node.init(&node); - SASSERT(node.next() == &node); - SASSERT(node.prev() == &node); - SASSERT(node.invariant()); + assert(node.next() == &node); + assert(node.prev() == &node); + assert(node.invariant()); std::cout << "test_init passed." << std::endl; } @@ -70,10 +71,10 @@ void test_pop() { TestNode node1(1); TestNode::push_to_front(list, &node1); TestNode* popped = TestNode::pop(list); - SASSERT(popped == &node1); - SASSERT(list == nullptr); - SASSERT(popped->next() == popped); - SASSERT(popped->prev() == popped); + assert(popped == &node1); + assert(list == nullptr); + assert(popped->next() == popped); + assert(popped->prev() == popped); std::cout << "test_pop passed." << std::endl; } @@ -82,12 +83,12 @@ void test_insert_after() { TestNode node1(1); TestNode node2(2); node1.insert_after(&node2); - SASSERT(node1.next() == &node2); - SASSERT(node2.prev() == &node1); - SASSERT(node1.prev() == &node2); - SASSERT(node2.next() == &node1); - SASSERT(node1.invariant()); - SASSERT(node2.invariant()); + assert(node1.next() == &node2); + assert(node2.prev() == &node1); + assert(node1.prev() == &node2); + assert(node2.next() == &node1); + assert(node1.invariant()); + assert(node2.invariant()); std::cout << "test_insert_after passed." << std::endl; } @@ -96,12 +97,12 @@ void test_insert_before() { TestNode node1(1); TestNode node2(2); node1.insert_before(&node2); - SASSERT(node1.prev() == &node2); - SASSERT(node2.next() == &node1); - SASSERT(node1.next() == &node2); - SASSERT(node2.prev() == &node1); - SASSERT(node1.invariant()); - SASSERT(node2.invariant()); + assert(node1.prev() == &node2); + assert(node2.next() == &node1); + assert(node1.next() == &node2); + assert(node2.prev() == &node1); + assert(node1.invariant()); + assert(node2.invariant()); std::cout << "test_insert_before passed." << std::endl; } @@ -113,9 +114,11 @@ void test_remove_from() { TestNode::push_to_front(list, &node1); TestNode::push_to_front(list, &node2); TestNode::remove_from(list, &node1); - SASSERT(list == &node2); - SASSERT(node2.next() == &node2); - SASSERT(node2.prev() == &node2); + assert(list == &node2); + assert(node2.next() == &node2); + assert(node2.prev() == &node2); + assert(node1.next() == &node1); + assert(node1.prev() == &node1); std::cout << "test_remove_from passed." << std::endl; } @@ -124,9 +127,9 @@ void test_push_to_front() { TestNode* list = nullptr; TestNode node1(1); TestNode::push_to_front(list, &node1); - SASSERT(list == &node1); - SASSERT(node1.next() == &node1); - SASSERT(node1.prev() == &node1); + assert(list == &node1); + assert(node1.next() == &node1); + assert(node1.prev() == &node1); std::cout << "test_push_to_front passed." << std::endl; } @@ -134,20 +137,20 @@ void test_push_to_front() { void test_detach() { TestNode node(1); TestNode::detach(&node); - SASSERT(node.next() == &node); - SASSERT(node.prev() == &node); - SASSERT(node.invariant()); + assert(node.next() == &node); + assert(node.prev() == &node); + assert(node.invariant()); std::cout << "test_detach passed." << std::endl; } // Test the invariant() method void test_invariant() { TestNode node1(1); - SASSERT(node1.invariant()); + assert(node1.invariant()); TestNode node2(2); node1.insert_after(&node2); - SASSERT(node1.invariant()); - SASSERT(node2.invariant()); + assert(node1.invariant()); + assert(node2.invariant()); std::cout << "test_invariant passed." << std::endl; } @@ -158,10 +161,10 @@ void test_contains() { TestNode node2(2); TestNode::push_to_front(list, &node1); TestNode::push_to_front(list, &node2); - SASSERT(TestNode::contains(list, &node1)); - SASSERT(TestNode::contains(list, &node2)); + assert(TestNode::contains(list, &node1)); + assert(TestNode::contains(list, &node2)); TestNode node3(3); - SASSERT(!TestNode::contains(list, &node3)); + assert(!TestNode::contains(list, &node3)); std::cout << "test_contains passed." << std::endl; } diff --git a/src/test/main.cpp b/src/test/main.cpp index f028d6ceb..0d3679529 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -269,5 +269,4 @@ int main(int argc, char ** argv) { TST(euf_bv_plugin); TST(euf_arith_plugin); TST(sls_test); - TST(scoped_vector); } diff --git a/src/test/scoped_vector.cpp b/src/test/scoped_vector.cpp deleted file mode 100644 index 05d98fcf1..000000000 --- a/src/test/scoped_vector.cpp +++ /dev/null @@ -1,99 +0,0 @@ -#include -#include "util/scoped_vector.h" - -void test_push_back_and_access() { - scoped_vector sv; - sv.push_back(10); - - sv.push_back(20); - - SASSERT(sv.size() == 2); - SASSERT(sv[0] == 10); - SASSERT(sv[1] == 20); - - std::cout << "test_push_back_and_access passed." << std::endl; -} - -void test_scopes() { - scoped_vector sv; - sv.push_back(10); - sv.push_back(20); - - sv.push_scope(); - sv.push_back(30); - sv.push_back(40); - - SASSERT(sv.size() == 4); - SASSERT(sv[2] == 30); - SASSERT(sv[3] == 40); - - sv.pop_scope(1); - - std::cout << "test_scopes passed." << std::endl; - SASSERT(sv.size() == 2); - SASSERT(sv[0] == 10); - SASSERT(sv[1] == 20); - - std::cout << "test_scopes passed." << std::endl; -} - -void test_set() { - scoped_vector sv; - sv.push_back(10); - sv.push_back(20); - - sv.set(0, 30); - sv.set(1, 40); - - SASSERT(sv.size() == 2); - SASSERT(sv[0] == 30); - SASSERT(sv[1] == 40); - - sv.push_scope(); - sv.set(0, 50); - SASSERT(sv[0] == 50); - sv.pop_scope(1); - SASSERT(sv[0] == 30); - - std::cout << "test_set passed." << std::endl; -} - -void test_pop_back() { - scoped_vector sv; - sv.push_back(10); - sv.push_back(20); - - SASSERT(sv.size() == 2); - sv.pop_back(); - SASSERT(sv.size() == 1); - SASSERT(sv[0] == 10); - sv.pop_back(); - SASSERT(sv.size() == 0); - - std::cout << "test_pop_back passed." << std::endl; -} - -void test_erase_and_swap() { - scoped_vector sv; - sv.push_back(10); - sv.push_back(20); - sv.push_back(30); - - sv.erase_and_swap(1); - - SASSERT(sv.size() == 2); - SASSERT(sv[0] == 10); - SASSERT(sv[1] == 30); - - std::cout << "test_erase_and_swap passed." << std::endl; -} - -void tst_scoped_vector() { - test_push_back_and_access(); - test_scopes(); - test_set(); - test_pop_back(); - test_erase_and_swap(); - - std::cout << "All tests passed." << std::endl; -} diff --git a/src/util/scoped_vector.h b/src/util/scoped_vector.h index b5945fb44..2c6cfaa21 100644 --- a/src/util/scoped_vector.h +++ b/src/util/scoped_vector.h @@ -176,46 +176,8 @@ private: } bool invariant() const { - - - if (!(m_size <= m_elems.size() && m_elems_start <= m_elems.size())) - return false; - - // Check that source and destination trails have the same length. - if (m_src.size() != m_dst.size()) - return false; - // The size of m_src, m_dst, and m_src_lim should be consistent with the scope stack. - if (m_src_lim.size() != m_sizes.size() || m_src.size() != m_dst.size()) - return false; - - // m_elems_lim stores the past sizes of m_elems for each scope. Each element in m_elems_lim should be - // within bounds and in non-decreasing order. - for (unsigned i = 1; i < m_elems_lim.size(); ++i) { - if (m_elems_lim[i - 1] > m_elems_lim[i]) return false; - } - - - // m_sizes tracks the size of the vector at each scope level. - // Each element in m_sizes should be non-decreasing and within the size of m_elems. - for (unsigned i = 1; i < m_sizes.size(); ++i) { - if (m_sizes[i - 1] > m_sizes[i]) - return false; - } - - // The m_src and m_dst vectors should have the same size and should contain valid indices. - if (m_src.size() != m_dst.size()) return false; - for (unsigned i = 0; i < m_src.size(); ++i) { - if (m_src[i] >= m_index.size() || m_dst[i] >= m_elems.size()) return false; - } - - - // The size of m_src_lim should be less than or equal to the size of m_sizes and store valid indices. - if (m_src_lim.size() > m_sizes.size()) return false; - for (unsigned elem : m_src_lim) { - if (elem > m_src.size()) return false; - } - - return true; - + return + m_size <= m_elems.size() && + m_elems_start <= m_elems.size(); } }; From 0c16d34eb0eb9eb2627606431c631d896d547f6f Mon Sep 17 00:00:00 2001 From: Hari Govind V K Date: Tue, 30 Jul 2024 14:35:33 -0400 Subject: [PATCH 17/18] fix #7292 (#7316) --- src/qe/mbp/mbp_basic_tg.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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; From e7382d6ff9322e21aef87118dc6bf448f56d41f2 Mon Sep 17 00:00:00 2001 From: Philip Zucker Date: Wed, 31 Jul 2024 11:14:16 -0400 Subject: [PATCH 18/18] Added "λ" pretty printing to python (#7320) --- src/api/python/z3/z3printer.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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))))