mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
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
This commit is contained in:
parent
d2fc085b8c
commit
7c30cbfe48
|
@ -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
|
||||
|
|
|
@ -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;
|
||||
}
|
||||
|
||||
|
|
|
@ -269,4 +269,5 @@ int main(int argc, char ** argv) {
|
|||
TST(euf_bv_plugin);
|
||||
TST(euf_arith_plugin);
|
||||
TST(sls_test);
|
||||
TST(scoped_vector);
|
||||
}
|
||||
|
|
99
src/test/scoped_vector.cpp
Normal file
99
src/test/scoped_vector.cpp
Normal file
|
@ -0,0 +1,99 @@
|
|||
#include <iostream>
|
||||
#include "util/scoped_vector.h"
|
||||
|
||||
void test_push_back_and_access() {
|
||||
scoped_vector<int> 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<int> 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<int> 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<int> 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<int> 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;
|
||||
}
|
|
@ -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;
|
||||
|
||||
}
|
||||
};
|
||||
|
|
Loading…
Reference in a new issue