From 7c30cbfe48f65f9aa27a954c7ad5845863a6ea94 Mon Sep 17 00:00:00 2001 From: LiviaSun <33578456+ChuyueSun@users.noreply.github.com> Date: Fri, 2 Aug 2024 19:21:40 -0700 Subject: [PATCH] add scoped_vector invariants and unit tests (#7327) * add scoped vector unit test * fix dlist tests * add new scoped vector invariants * remove all loop invariants --- src/test/CMakeLists.txt | 1 + src/test/dlist.cpp | 2 - src/test/main.cpp | 1 + src/test/scoped_vector.cpp | 99 ++++++++++++++++++++++++++++++++++++++ src/util/scoped_vector.h | 44 +++++++++++++++-- 5 files changed, 142 insertions(+), 5 deletions(-) create mode 100644 src/test/scoped_vector.cpp diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index 8464cedf917..658647ea618 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 bf404631b5f..32a54f9ffc6 100644 --- a/src/test/dlist.cpp +++ b/src/test/dlist.cpp @@ -117,8 +117,6 @@ static void test_remove_from() { SASSERT(list == &node2); SASSERT(node2.next() == &node2); SASSERT(node2.prev() == &node2); - SASSERT(node1.next() == &node1); - SASSERT(node1.prev() == &node1); std::cout << "test_remove_from passed." << std::endl; } diff --git a/src/test/main.cpp b/src/test/main.cpp index 0d36795295c..f028d6ceb35 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 00000000000..05d98fcf103 --- /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 2c6cfaa2199..7d0cec472b2 100644 --- a/src/util/scoped_vector.h +++ b/src/util/scoped_vector.h @@ -176,8 +176,46 @@ class scoped_vector { } 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; + } };