mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

fix dlist tests

Browse source
This commit is contained in:
Chuyue Sun 2024-07-23 21:28:53 +00:00
parent 81c8dfbd8d
commit e34f561b78
1 changed files with 38 additions and 41 deletions
Download patch file Download diff file Expand all files Collapse all files

79
src/test/dlist.cpp
View file

@ -1,4 +1,3 @@
#include <cassert>
#include <iostream>
#include "util/dlist.h"
@ -13,28 +12,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;
}
@ -42,9 +41,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;
}
@ -54,10 +53,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;
}
@ -66,12 +65,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;
}
@ -80,12 +79,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;
}
@ -97,11 +96,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;
}
@ -110,9 +107,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;
}
@ -120,20 +117,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;
}
@ -144,10 +141,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;
}