From 9803e9ef6e35e4087182c02f151c317360ab2e09 Mon Sep 17 00:00:00 2001
From: LiviaSun <33578456+ChuyueSun@users.noreply.github.com>
Date: Thu, 18 Jul 2024 10:08:41 -0700
Subject: [PATCH] unit tests for dlist.h (#7293)

---
 src/test/CMakeLists.txt |   1 +
 src/test/dlist.cpp      | 170 ++++++++++++++++++++++++++++++++++++++++
 src/test/main.cpp       |   1 +
 3 files changed, 172 insertions(+)
 create mode 100644 src/test/dlist.cpp

diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt
index 4ddc1b8cb..a273d4e77 100644
--- a/src/test/CMakeLists.txt
+++ b/src/test/CMakeLists.txt
@@ -37,6 +37,7 @@ add_executable(test-z3
   dl_table.cpp
   dl_util.cpp
   doc.cpp
+  dlist.cpp
   egraph.cpp
   escaped.cpp
   euf_bv_plugin.cpp
diff --git a/src/test/dlist.cpp b/src/test/dlist.cpp
new file mode 100644
index 000000000..81689699f
--- /dev/null
+++ b/src/test/dlist.cpp
@@ -0,0 +1,170 @@
+#include <cassert>
+#include <iostream>
+#include "util/dlist.h"
+
+class TestNode : public dll_base<TestNode> {
+public:
+    int value;
+    TestNode(int val) : value(val) {
+        init(this);
+    }
+};
+
+// Test the prev() method
+void test_prev() {
+    TestNode node(1);
+    assert(node.prev() == &node);
+    std::cout << "test_prev passed." << std::endl;
+}
+
+// Test the next() method
+void test_next() {
+    TestNode node(1);
+    assert(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);
+    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);
+    std::cout << "test_const_next passed." << std::endl;
+}
+
+// Test the init() method
+void test_init() {
+    TestNode node(1);
+    node.init(&node);
+    assert(node.next() == &node);
+    assert(node.prev() == &node);
+    assert(node.invariant());
+    std::cout << "test_init passed." << std::endl;
+}
+
+// Test the pop() method
+void test_pop() {
+    TestNode* list = nullptr;
+    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);
+    std::cout << "test_pop passed." << std::endl;
+}
+
+// Test the insert_after() method
+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());
+    std::cout << "test_insert_after passed." << std::endl;
+}
+
+// Test the insert_before() method
+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());
+    std::cout << "test_insert_before passed." << std::endl;
+}
+
+// Test the remove_from() method
+void test_remove_from() {
+    TestNode* list = nullptr;
+    TestNode node1(1);
+    TestNode node2(2);
+    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);
+    std::cout << "test_remove_from passed." << std::endl;
+}
+
+// Test the push_to_front() method
+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);
+    std::cout << "test_push_to_front passed." << std::endl;
+}
+
+// Test the detach() method
+void test_detach() {
+    TestNode node(1);
+    TestNode::detach(&node);
+    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);
+    assert(node1.invariant());
+    TestNode node2(2);
+    node1.insert_after(&node2);
+    assert(node1.invariant());
+    assert(node2.invariant());
+    std::cout << "test_invariant passed." << std::endl;
+}
+
+// Test the contains() method
+void test_contains() {
+    TestNode* list = nullptr;
+    TestNode node1(1);
+    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));
+    TestNode node3(3);
+    assert(!TestNode::contains(list, &node3));
+    std::cout << "test_contains passed." << std::endl;
+}
+
+int tst_dlist() {
+    test_prev();
+    test_next();
+    test_const_prev();
+    test_const_next();
+    test_init();
+    test_pop();
+    test_insert_after();
+    test_insert_before();
+    test_remove_from();
+    test_push_to_front();
+    test_detach();
+    test_invariant();
+    test_contains();
+    std::cout << "All tests passed." << std::endl;
+    return 0;
+}
diff --git a/src/test/main.cpp b/src/test/main.cpp
index 0c3d0e01a..0d3679529 100644
--- a/src/test/main.cpp
+++ b/src/test/main.cpp
@@ -188,6 +188,7 @@ int main(int argc, char ** argv) {
     TST(total_order);
     TST(dl_table);
     TST(dl_context);
+    TST(dlist);
     TST(dl_util);
     TST(dl_product_relation);
     TST(dl_relation);