Revert "add scoped vector unit test"

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

src/test/dlist.cpp

@@ -15,6 +15,7 @@ Module Name:
 
 --*/
 
+#include <cassert>
 #include <iostream>
 #include "util/dlist.h"
 
@@ -29,38 +30,38 @@ class TestNode : public dll_base<TestNode> {
 // 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;
 }
 
 // Test the init() method
 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,30 +127,30 @@ 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;
 }
 
 // Test the detach() method
 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;
 }
 

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);
 }

src/util/scoped_vector.h

@@ -176,46 +176,8 @@ class scoped_vector {
     }
 
     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();
     }
 };