From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 9 Dec 2020 09:26:31 +0000 (-0800)
Subject: google test: context: Migrate context_white. (#5630)
X-Git-Tag: cvc5-1.0.0~2469
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=adc9bb5dff0c3d705b91d862d61a0c3057350688;p=cvc5.git

google test: context: Migrate context_white. (#5630)

google test: context: Migrate context_white.
---

diff --git a/test/unit/context/CMakeLists.txt b/test/unit/context/CMakeLists.txt
index 7d99fcbb2..6752f0e78 100644
--- a/test/unit/context/CMakeLists.txt
+++ b/test/unit/context/CMakeLists.txt
@@ -17,4 +17,4 @@ cvc4_add_unit_test_white(cdmap_white context)
 cvc4_add_unit_test_black(cdo_black context)
 cvc4_add_unit_test_black(context_black context)
 cvc4_add_unit_test_black(context_mm_black context)
-cvc4_add_cxx_unit_test_white(context_white context)
\ No newline at end of file
+cvc4_add_unit_test_white(context_white context)
diff --git a/test/unit/context/context_white.cpp b/test/unit/context/context_white.cpp
new file mode 100644
index 000000000..c8ea59848
--- /dev/null
+++ b/test/unit/context/context_white.cpp
@@ -0,0 +1,183 @@
+/*********************                                                        */
+/*! \file context_white.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief White box testing of CVC4::context::Context.
+ **
+ ** White box testing of CVC4::context::Context.
+ **/
+
+#include "base/check.h"
+#include "context/cdo.h"
+#include "test_context.h"
+
+namespace CVC4 {
+
+using namespace context;
+
+namespace test {
+
+class TestContextWhite : public TestContext
+{
+};
+
+TEST_F(TestContextWhite, simple)
+{
+  Scope* s = d_context->getTopScope();
+
+  EXPECT_EQ(s, d_context->getBottomScope());
+  EXPECT_EQ(d_context->getLevel(), 0);
+  EXPECT_EQ(d_context->d_scopeList.size(), 1);
+
+  EXPECT_EQ(s->d_pContext, d_context.get());
+  EXPECT_EQ(s->d_pCMM, d_context->d_pCMM);
+  EXPECT_EQ(s->d_level, 0);
+  EXPECT_EQ(s->d_pContextObjList, nullptr);
+
+  CDO<int> a(d_context.get());
+
+  EXPECT_EQ(s->d_pContext, d_context.get());
+  EXPECT_EQ(s->d_pCMM, d_context->d_pCMM);
+  EXPECT_EQ(s->d_level, 0);
+  EXPECT_EQ(s->d_pContextObjList, &a);
+
+  EXPECT_EQ(a.d_pScope, s);
+  EXPECT_EQ(a.d_pContextObjRestore, nullptr);
+  EXPECT_EQ(a.d_pContextObjNext, nullptr);
+  EXPECT_EQ(a.d_ppContextObjPrev, &s->d_pContextObjList);
+
+  CDO<int> b(d_context.get());
+
+  EXPECT_EQ(s->d_pContext, d_context.get());
+  EXPECT_EQ(s->d_pCMM, d_context->d_pCMM);
+  EXPECT_EQ(s->d_level, 0);
+  EXPECT_EQ(s->d_pContextObjList, &b);
+
+  EXPECT_EQ(a.d_pScope, s);
+  EXPECT_EQ(a.d_pContextObjRestore, nullptr);
+  EXPECT_EQ(a.d_pContextObjNext, nullptr);
+  EXPECT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext);
+
+  EXPECT_EQ(b.d_pScope, s);
+  EXPECT_EQ(b.d_pContextObjRestore, nullptr);
+  EXPECT_EQ(b.d_pContextObjNext, &a);
+  EXPECT_EQ(b.d_ppContextObjPrev, &s->d_pContextObjList);
+
+  d_context->push();
+  Scope* t = d_context->getTopScope();
+  EXPECT_NE(s, t);
+
+  EXPECT_EQ(s, d_context->getBottomScope());
+  EXPECT_EQ(d_context->getLevel(), 1);
+  EXPECT_EQ(d_context->d_scopeList.size(), 2);
+
+  EXPECT_EQ(s->d_pContext, d_context.get());
+  EXPECT_EQ(s->d_pCMM, d_context->d_pCMM);
+  EXPECT_EQ(s->d_level, 0);
+  EXPECT_EQ(s->d_pContextObjList, &b);
+
+  EXPECT_EQ(t->d_pContext, d_context.get());
+  EXPECT_EQ(t->d_pCMM, d_context->d_pCMM);
+  EXPECT_EQ(t->d_level, 1);
+  EXPECT_EQ(t->d_pContextObjList, nullptr);
+
+  EXPECT_EQ(a.d_pScope, s);
+  EXPECT_EQ(a.d_pContextObjRestore, nullptr);
+  EXPECT_EQ(a.d_pContextObjNext, nullptr);
+  EXPECT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext);
+
+  EXPECT_EQ(b.d_pScope, s);
+  EXPECT_EQ(b.d_pContextObjRestore, nullptr);
+  EXPECT_EQ(b.d_pContextObjNext, &a);
+  EXPECT_EQ(b.d_ppContextObjPrev, &s->d_pContextObjList);
+
+  a = 5;
+
+  EXPECT_EQ(t->d_pContext, d_context.get());
+  EXPECT_EQ(t->d_pCMM, d_context->d_pCMM);
+  EXPECT_EQ(t->d_level, 1);
+  EXPECT_EQ(t->d_pContextObjList, &a);
+
+  EXPECT_EQ(a.d_pScope, t);
+  EXPECT_NE(a.d_pContextObjRestore, nullptr);
+  EXPECT_EQ(a.d_pContextObjNext, nullptr);
+  EXPECT_EQ(a.d_ppContextObjPrev, &t->d_pContextObjList);
+
+  b = 3;
+
+  EXPECT_EQ(t->d_pContext, d_context.get());
+  EXPECT_EQ(t->d_pCMM, d_context->d_pCMM);
+  EXPECT_EQ(t->d_level, 1);
+  EXPECT_EQ(t->d_pContextObjList, &b);
+
+  EXPECT_EQ(a.d_pScope, t);
+  EXPECT_NE(a.d_pContextObjRestore, nullptr);
+  EXPECT_EQ(a.d_pContextObjNext, nullptr);
+  EXPECT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext);
+
+  EXPECT_EQ(b.d_pScope, t);
+  EXPECT_NE(b.d_pContextObjRestore, nullptr);
+  EXPECT_EQ(b.d_pContextObjNext, &a);
+  EXPECT_EQ(b.d_ppContextObjPrev, &t->d_pContextObjList);
+
+  d_context->push();
+  Scope* u = d_context->getTopScope();
+  EXPECT_NE(u, t);
+  EXPECT_NE(u, s);
+
+  CDO<int> c(d_context.get());
+  c = 4;
+
+  EXPECT_EQ(c.d_pScope, u);
+  EXPECT_NE(c.d_pContextObjRestore, nullptr);
+  EXPECT_EQ(c.d_pContextObjNext, nullptr);
+  EXPECT_EQ(c.d_ppContextObjPrev, &u->d_pContextObjList);
+
+  d_context->pop();
+
+  EXPECT_EQ(t->d_pContext, d_context.get());
+  EXPECT_EQ(t->d_pCMM, d_context->d_pCMM);
+  EXPECT_EQ(t->d_level, 1);
+  EXPECT_EQ(t->d_pContextObjList, &b);
+
+  EXPECT_EQ(a.d_pScope, t);
+  EXPECT_NE(a.d_pContextObjRestore, nullptr);
+  EXPECT_EQ(a.d_pContextObjNext, nullptr);
+  EXPECT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext);
+
+  EXPECT_EQ(b.d_pScope, t);
+  EXPECT_NE(b.d_pContextObjRestore, nullptr);
+  EXPECT_EQ(b.d_pContextObjNext, &a);
+  EXPECT_EQ(b.d_ppContextObjPrev, &t->d_pContextObjList);
+
+  d_context->pop();
+
+  EXPECT_EQ(s->d_pContext, d_context.get());
+  EXPECT_EQ(s->d_pCMM, d_context->d_pCMM);
+  EXPECT_EQ(s->d_level, 0);
+  EXPECT_EQ(s->d_pContextObjList, &c);
+
+  EXPECT_EQ(a.d_pScope, s);
+  EXPECT_EQ(a.d_pContextObjRestore, nullptr);
+  EXPECT_EQ(a.d_pContextObjNext, nullptr);
+  EXPECT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext);
+
+  EXPECT_EQ(b.d_pScope, s);
+  EXPECT_EQ(b.d_pContextObjRestore, nullptr);
+  EXPECT_EQ(b.d_pContextObjNext, &a);
+  EXPECT_EQ(b.d_ppContextObjPrev, &c.d_pContextObjNext);
+
+  EXPECT_EQ(c.d_pScope, s);
+  EXPECT_EQ(c.d_pContextObjRestore, nullptr);
+  EXPECT_EQ(c.d_pContextObjNext, &b);
+  EXPECT_EQ(c.d_ppContextObjPrev, &s->d_pContextObjList);
+}
+}  // namespace test
+}  // namespace CVC4
diff --git a/test/unit/context/context_white.h b/test/unit/context/context_white.h
deleted file mode 100644
index 4fd0f8d7f..000000000
--- a/test/unit/context/context_white.h
+++ /dev/null
@@ -1,188 +0,0 @@
-/*********************                                                        */
-/*! \file context_white.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Andres Noetzli, Dejan Jovanovic
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief White box testing of CVC4::context::Context.
- **
- ** White box testing of CVC4::context::Context.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include "base/check.h"
-#include "context/cdo.h"
-#include "context/context.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::context;
-
-class ContextWhite : public CxxTest::TestSuite {
-private:
-
-  Context* d_context;
-
- public:
-  void setUp() override { d_context = new Context; }
-
-  void tearDown() override { delete d_context; }
-
-  void testContextSimple()
-  {
-    Scope* s = d_context->getTopScope();
-
-    TS_ASSERT(s == d_context->getBottomScope());
-    TS_ASSERT(d_context->getLevel() == 0);
-    TS_ASSERT(d_context->d_scopeList.size() == 1);
-
-    TS_ASSERT(s->d_pContext == d_context);
-    TS_ASSERT(s->d_pCMM == d_context->d_pCMM);
-    TS_ASSERT(s->d_level == 0);
-    TS_ASSERT(s->d_pContextObjList == NULL);
-
-    CDO<int> a(d_context);
-
-    TS_ASSERT(s->d_pContext == d_context);
-    TS_ASSERT(s->d_pCMM == d_context->d_pCMM);
-    TS_ASSERT(s->d_level == 0);
-    TS_ASSERT(s->d_pContextObjList == &a);
-
-    TS_ASSERT(a.d_pScope == s);
-    TS_ASSERT(a.d_pContextObjRestore == NULL);
-    TS_ASSERT(a.d_pContextObjNext == NULL);
-    TS_ASSERT(a.d_ppContextObjPrev == &s->d_pContextObjList);
-
-    CDO<int> b(d_context);
-
-    TS_ASSERT(s->d_pContext == d_context);
-    TS_ASSERT(s->d_pCMM == d_context->d_pCMM);
-    TS_ASSERT(s->d_level == 0);
-    TS_ASSERT(s->d_pContextObjList == &b);
-
-    TS_ASSERT(a.d_pScope == s);
-    TS_ASSERT(a.d_pContextObjRestore == NULL);
-    TS_ASSERT(a.d_pContextObjNext == NULL);
-    TS_ASSERT(a.d_ppContextObjPrev == &b.d_pContextObjNext);
-
-    TS_ASSERT(b.d_pScope == s);
-    TS_ASSERT(b.d_pContextObjRestore == NULL);
-    TS_ASSERT(b.d_pContextObjNext == &a);
-    TS_ASSERT(b.d_ppContextObjPrev == &s->d_pContextObjList);
-
-    d_context->push();
-    Scope* t = d_context->getTopScope();
-    TS_ASSERT(s != t);
-
-    TS_ASSERT(s == d_context->getBottomScope());
-    TS_ASSERT(d_context->getLevel() == 1);
-    TS_ASSERT(d_context->d_scopeList.size() == 2);
-
-    TS_ASSERT(s->d_pContext == d_context);
-    TS_ASSERT(s->d_pCMM == d_context->d_pCMM);
-    TS_ASSERT(s->d_level == 0);
-    TS_ASSERT(s->d_pContextObjList == &b);
-
-    TS_ASSERT(t->d_pContext == d_context);
-    TS_ASSERT(t->d_pCMM == d_context->d_pCMM);
-    TS_ASSERT(t->d_level == 1);
-    TS_ASSERT(t->d_pContextObjList == NULL);
-
-    TS_ASSERT(a.d_pScope == s);
-    TS_ASSERT(a.d_pContextObjRestore == NULL);
-    TS_ASSERT(a.d_pContextObjNext == NULL);
-    TS_ASSERT(a.d_ppContextObjPrev == &b.d_pContextObjNext);
-
-    TS_ASSERT(b.d_pScope == s);
-    TS_ASSERT(b.d_pContextObjRestore == NULL);
-    TS_ASSERT(b.d_pContextObjNext == &a);
-    TS_ASSERT(b.d_ppContextObjPrev == &s->d_pContextObjList);
-
-    a = 5;
-
-    TS_ASSERT(t->d_pContext == d_context);
-    TS_ASSERT(t->d_pCMM == d_context->d_pCMM);
-    TS_ASSERT(t->d_level == 1);
-    TS_ASSERT(t->d_pContextObjList == &a);
-
-    TS_ASSERT(a.d_pScope == t);
-    TS_ASSERT(a.d_pContextObjRestore != NULL);
-    TS_ASSERT(a.d_pContextObjNext == NULL);
-    TS_ASSERT(a.d_ppContextObjPrev == &t->d_pContextObjList);
-
-    b = 3;
-
-    TS_ASSERT(t->d_pContext == d_context);
-    TS_ASSERT(t->d_pCMM == d_context->d_pCMM);
-    TS_ASSERT(t->d_level == 1);
-    TS_ASSERT(t->d_pContextObjList == &b);
-
-    TS_ASSERT(a.d_pScope == t);
-    TS_ASSERT(a.d_pContextObjRestore != NULL);
-    TS_ASSERT(a.d_pContextObjNext == NULL);
-    TS_ASSERT(a.d_ppContextObjPrev == &b.d_pContextObjNext);
-
-    TS_ASSERT(b.d_pScope == t);
-    TS_ASSERT(b.d_pContextObjRestore != NULL);
-    TS_ASSERT(b.d_pContextObjNext == &a);
-    TS_ASSERT(b.d_ppContextObjPrev == &t->d_pContextObjList);
-
-    d_context->push();
-    Scope* u = d_context->getTopScope();
-    TS_ASSERT(u != t);
-    TS_ASSERT(u != s);
-
-    CDO<int> c(d_context);
-    c = 4;
-
-    TS_ASSERT(c.d_pScope == u);
-    TS_ASSERT(c.d_pContextObjRestore != NULL);
-    TS_ASSERT(c.d_pContextObjNext == NULL);
-    TS_ASSERT(c.d_ppContextObjPrev == &u->d_pContextObjList);
-
-    d_context->pop();
-
-    TS_ASSERT(t->d_pContext == d_context);
-    TS_ASSERT(t->d_pCMM == d_context->d_pCMM);
-    TS_ASSERT(t->d_level == 1);
-    TS_ASSERT(t->d_pContextObjList == &b);
-
-    TS_ASSERT(a.d_pScope == t);
-    TS_ASSERT(a.d_pContextObjRestore != NULL);
-    TS_ASSERT(a.d_pContextObjNext == NULL);
-    TS_ASSERT(a.d_ppContextObjPrev == &b.d_pContextObjNext);
-
-    TS_ASSERT(b.d_pScope == t);
-    TS_ASSERT(b.d_pContextObjRestore != NULL);
-    TS_ASSERT(b.d_pContextObjNext == &a);
-    TS_ASSERT(b.d_ppContextObjPrev == &t->d_pContextObjList);
-
-    d_context->pop();
-
-    TS_ASSERT(s->d_pContext == d_context);
-    TS_ASSERT(s->d_pCMM == d_context->d_pCMM);
-    TS_ASSERT(s->d_level == 0);
-    TS_ASSERT(s->d_pContextObjList == &c);
-
-    TS_ASSERT(a.d_pScope == s);
-    TS_ASSERT(a.d_pContextObjRestore == NULL);
-    TS_ASSERT(a.d_pContextObjNext == NULL);
-    TS_ASSERT(a.d_ppContextObjPrev == &b.d_pContextObjNext);
-
-    TS_ASSERT(b.d_pScope == s);
-    TS_ASSERT(b.d_pContextObjRestore == NULL);
-    TS_ASSERT(b.d_pContextObjNext == &a);
-    TS_ASSERT(b.d_ppContextObjPrev == &c.d_pContextObjNext);
-
-    TS_ASSERT(c.d_pScope == s);
-    TS_ASSERT(c.d_pContextObjRestore == NULL);
-    TS_ASSERT(c.d_pContextObjNext == &b);
-    TS_ASSERT(c.d_ppContextObjPrev == &s->d_pContextObjList);
-  }
-};