google test: util: Migrate array_store_all_white. (#6008)

diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt
index 52719e6f4cca94bd51d0b56f3b67b17203d0c5af..ab7bf25f571f8b8faa1be8b58862e9981ddfe020 100644 (file)
--- a/test/unit/util/CMakeLists.txt
+++ b/test/unit/util/CMakeLists.txt
@@ -11,7 +11,7 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_cxx_unit_test_white(array_store_all_white util)
+cvc4_add_unit_test_white(array_store_all_white util)
 cvc4_add_unit_test_white(assert_white util)
 cvc4_add_unit_test_black(binary_heap_black util)
 cvc4_add_cxx_unit_test_black(bitvector_black util)

diff --git a/test/unit/util/array_store_all_white.cpp b/test/unit/util/array_store_all_white.cpp
new file mode 100644 (file)
index 0000000..a0a9540
--- /dev/null
+++ b/test/unit/util/array_store_all_white.cpp
@@ -0,0 +1,81 @@
+/*********************                                                        */
+/*! \file array_store_all_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 Black box testing of CVC4::ArrayStoreAll
+ **
+ ** Black box testing of CVC4::ArrayStoreAll.
+ **/
+
+#include "expr/array_store_all.h"
+#include "expr/expr.h"
+#include "expr/type.h"
+#include "test_smt.h"
+#include "test_utils.h"
+
+namespace CVC4 {
+namespace test {
+
+class TestUtilWhiteArrayStoreAll : public TestSmt
+{
+};
+
+TEST_F(TestUtilWhiteArrayStoreAll, store_all)
+{
+  TypeNode usort = d_nodeManager->mkSort("U");
+  ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->integerType(),
+                                           d_nodeManager->realType()),
+                d_nodeManager->mkConst(Rational(9, 2)));
+  ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkSort("U"), usort),
+                d_nodeManager->mkConst(UninterpretedConstant(usort, 0)));
+  ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(8),
+                                           d_nodeManager->realType()),
+                d_nodeManager->mkConst(Rational(0)));
+  ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(8),
+                                           d_nodeManager->integerType()),
+                d_nodeManager->mkConst(Rational(0)));
+}
+
+TEST_F(TestUtilWhiteArrayStoreAll, type_errors)
+{
+  ASSERT_THROW(ArrayStoreAll(d_nodeManager->integerType(),
+                             d_nodeManager->mkConst(UninterpretedConstant(
+                                 d_nodeManager->mkSort("U"), 0))),
+               IllegalArgumentException);
+  ASSERT_THROW(ArrayStoreAll(d_nodeManager->integerType(),
+                             d_nodeManager->mkConst(Rational(9, 2))),
+               IllegalArgumentException);
+  ASSERT_THROW(
+      ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->integerType(),
+                                               d_nodeManager->mkSort("U")),
+                    d_nodeManager->mkConst(Rational(9, 2))),
+      IllegalArgumentException);
+}
+
+TEST_F(TestUtilWhiteArrayStoreAll, const_error)
+{
+  TypeNode usort = d_nodeManager->mkSort("U");
+  ASSERT_THROW(ArrayStoreAll(d_nodeManager->mkArrayType(
+                                 d_nodeManager->mkSort("U"), usort),
+                             d_nodeManager->mkVar(usort)),
+               IllegalArgumentException);
+  ASSERT_THROW(
+      ArrayStoreAll(d_nodeManager->integerType(),
+                    d_nodeManager->mkVar("x", d_nodeManager->integerType())),
+      IllegalArgumentException);
+  ASSERT_THROW(
+      ArrayStoreAll(d_nodeManager->integerType(),
+                    d_nodeManager->mkNode(kind::PLUS,
+                                          d_nodeManager->mkConst(Rational(1)),
+                                          d_nodeManager->mkConst(Rational(0)))),
+      IllegalArgumentException);
+}
+}  // namespace test
+}  // namespace CVC4

diff --git a/test/unit/util/array_store_all_white.h b/test/unit/util/array_store_all_white.h
deleted file mode 100644 (file)
index 2e107f6..0000000
--- a/test/unit/util/array_store_all_white.h
+++ /dev/null
@@ -1,94 +0,0 @@
-/*********************                                                        */
-/*! \file array_store_all_white.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andres Noetzli, Morgan Deters, Clark Barrett
- ** 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 Black box testing of CVC4::ArrayStoreAll
- **
- ** Black box testing of CVC4::ArrayStoreAll.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include "api/cvc4cpp.h"
-#include "expr/array_store_all.h"
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
-#include "expr/type.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
-#include "test_utils.h"
-
-using namespace CVC4;
-using namespace std;
-
-class ArrayStoreAllWhite : public CxxTest::TestSuite
-{
- public:
-  void setUp() override
-  {
-    d_slv = new api::Solver();
-    d_scope = new smt::SmtScope(d_slv->getSmtEngine());
-    d_nm = d_slv->getSmtEngine()->d_nodeManager;
-  }
-
-  void tearDown() override
-  {
-    delete d_scope;
-    delete d_slv;
-  }
-
-  void testStoreAll()
-  {
-    TypeNode usort = d_nm->mkSort("U");
-    ArrayStoreAll(d_nm->mkArrayType(d_nm->integerType(), d_nm->realType()),
-                  d_nm->mkConst(Rational(9, 2)));
-    ArrayStoreAll(d_nm->mkArrayType(d_nm->mkSort("U"), usort),
-                  d_nm->mkConst(UninterpretedConstant(usort, 0)));
-    ArrayStoreAll(d_nm->mkArrayType(d_nm->mkBitVectorType(8), d_nm->realType()),
-                  d_nm->mkConst(Rational(0)));
-    ArrayStoreAll(
-        d_nm->mkArrayType(d_nm->mkBitVectorType(8), d_nm->integerType()),
-        d_nm->mkConst(Rational(0)));
-  }
-
-  void testTypeErrors()
-  {
-    TS_ASSERT_THROWS(ArrayStoreAll(d_nm->integerType(),
-                                   d_nm->mkConst(UninterpretedConstant(
-                                       d_nm->mkSort("U"), 0))),
-                     IllegalArgumentException&);
-    TS_ASSERT_THROWS(
-        ArrayStoreAll(d_nm->integerType(), d_nm->mkConst(Rational(9, 2))),
-        IllegalArgumentException&);
-    TS_ASSERT_THROWS(
-        ArrayStoreAll(d_nm->mkArrayType(d_nm->integerType(), d_nm->mkSort("U")),
-                      d_nm->mkConst(Rational(9, 2))),
-        IllegalArgumentException&);
-  }
-
-  void testConstError()
-  {
-    TypeNode usort = d_nm->mkSort("U");
-    TS_ASSERT_THROWS_ANYTHING(ArrayStoreAll(
-        d_nm->mkArrayType(d_nm->mkSort("U"), usort), d_nm->mkVar(usort)));
-    TS_ASSERT_THROWS_ANYTHING(ArrayStoreAll(
-        d_nm->integerType(), d_nm->mkVar("x", d_nm->integerType())));
-    TS_ASSERT_THROWS_ANYTHING(
-        ArrayStoreAll(d_nm->integerType(),
-                      d_nm->mkNode(kind::PLUS,
-                                   d_nm->mkConst(Rational(1)),
-                                   d_nm->mkConst(Rational(0)))));
-  }
-
- private:
-  api::Solver* d_slv;
-  smt::SmtScope* d_scope;
-  NodeManager* d_nm;
-}; /* class ArrayStoreAllBlack */