google test: expr: Migrate type_node_white. (#5872)

diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt
index 18201b8a8071d5ced209227f60c1ad3a0b432aaf..39545d056773c36c6b004a71503c52ad824174be 100644 (file)
--- a/test/unit/expr/CMakeLists.txt
+++ b/test/unit/expr/CMakeLists.txt
@@ -25,4 +25,4 @@ cvc4_add_unit_test_black(node_traversal_black expr)
 cvc4_add_unit_test_white(node_white expr)
 cvc4_add_unit_test_black(symbol_table_black expr)
 cvc4_add_cxx_unit_test_black(type_cardinality_public expr)
-cvc4_add_cxx_unit_test_white(type_node_white expr)
+cvc4_add_unit_test_white(type_node_white expr)

diff --git a/test/unit/expr/type_node_white.cpp b/test/unit/expr/type_node_white.cpp
new file mode 100644 (file)
index 0000000..085b576
--- /dev/null
+++ b/test/unit/expr/type_node_white.cpp
@@ -0,0 +1,99 @@
+/*********************                                                        */
+/*! \file type_node_white.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Andrew Reynolds
+ ** 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 TypeNode
+ **
+ ** White box testing of TypeNode.
+ **/
+
+#include <iostream>
+#include <sstream>
+#include <string>
+
+#include "expr/expr.h"
+#include "expr/expr_manager.h"
+#include "expr/node_manager.h"
+#include "expr/type_node.h"
+#include "smt/smt_engine.h"
+#include "test_node.h"
+
+namespace CVC4 {
+
+using namespace kind;
+using namespace context;
+
+namespace test {
+
+class TestNodeWhiteTypeNode : public TestNodeWhite
+{
+ protected:
+  void SetUp() override
+  {
+    TestNodeWhite::SetUp();
+    d_smt.reset(new SmtEngine(d_nodeManager.get()));
+  }
+  std::unique_ptr<SmtEngine> d_smt;
+};
+
+TEST_F(TestNodeWhiteTypeNode, sub_types)
+{
+  TypeNode realType = d_nodeManager->realType();
+  TypeNode integerType = d_nodeManager->realType();
+  TypeNode booleanType = d_nodeManager->booleanType();
+  TypeNode arrayType = d_nodeManager->mkArrayType(realType, integerType);
+  TypeNode bvType = d_nodeManager->mkBitVectorType(32);
+
+  Node x = d_nodeManager->mkBoundVar("x", realType);
+  Node xPos = d_nodeManager->mkNode(GT, x, d_nodeManager->mkConst(Rational(0)));
+  TypeNode funtype = d_nodeManager->mkFunctionType(integerType, booleanType);
+  Node lambda = d_nodeManager->mkVar("lambda", funtype);
+  std::vector<Node> formals;
+  formals.push_back(x);
+  d_smt->defineFunction(lambda, formals, xPos);
+
+  ASSERT_FALSE(realType.isComparableTo(booleanType));
+  ASSERT_TRUE(realType.isComparableTo(integerType));
+  ASSERT_TRUE(realType.isComparableTo(realType));
+  ASSERT_FALSE(realType.isComparableTo(arrayType));
+  ASSERT_FALSE(realType.isComparableTo(bvType));
+
+  ASSERT_FALSE(booleanType.isComparableTo(integerType));
+  ASSERT_FALSE(booleanType.isComparableTo(realType));
+  ASSERT_TRUE(booleanType.isComparableTo(booleanType));
+  ASSERT_FALSE(booleanType.isComparableTo(arrayType));
+  ASSERT_FALSE(booleanType.isComparableTo(bvType));
+
+  ASSERT_TRUE(integerType.isComparableTo(realType));
+  ASSERT_TRUE(integerType.isComparableTo(integerType));
+  ASSERT_FALSE(integerType.isComparableTo(booleanType));
+  ASSERT_FALSE(integerType.isComparableTo(arrayType));
+  ASSERT_FALSE(integerType.isComparableTo(bvType));
+
+  ASSERT_FALSE(arrayType.isComparableTo(booleanType));
+  ASSERT_FALSE(arrayType.isComparableTo(integerType));
+  ASSERT_FALSE(arrayType.isComparableTo(realType));
+  ASSERT_TRUE(arrayType.isComparableTo(arrayType));
+  ASSERT_FALSE(arrayType.isComparableTo(bvType));
+
+  ASSERT_FALSE(bvType.isComparableTo(booleanType));
+  ASSERT_FALSE(bvType.isComparableTo(integerType));
+  ASSERT_FALSE(bvType.isComparableTo(realType));
+  ASSERT_FALSE(bvType.isComparableTo(arrayType));
+  ASSERT_TRUE(bvType.isComparableTo(bvType));
+
+  ASSERT_TRUE(realType.getBaseType() == realType);
+  ASSERT_TRUE(integerType.getBaseType() == realType);
+  ASSERT_TRUE(booleanType.getBaseType() == booleanType);
+  ASSERT_TRUE(arrayType.getBaseType() == arrayType);
+  ASSERT_TRUE(bvType.getBaseType() == bvType);
+}
+}  // namespace test
+}  // namespace CVC4

diff --git a/test/unit/expr/type_node_white.h b/test/unit/expr/type_node_white.h
deleted file mode 100644 (file)
index 042a7b1..0000000
--- a/test/unit/expr/type_node_white.h
+++ /dev/null
@@ -1,109 +0,0 @@
-/*********************                                                        */
-/*! \file type_node_white.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Andrew Reynolds, Andres Noetzli
- ** 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 TypeNode
- **
- ** White box testing of TypeNode.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include <iostream>
-#include <string>
-#include <sstream>
-
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
-#include "expr/node_manager.h"
-#include "expr/type_node.h"
-#include "smt/smt_engine.h"
-
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace std;
-
-class TypeNodeWhite : public CxxTest::TestSuite {
-  ExprManager* d_em;
-  NodeManager* d_nm;
-  NodeManagerScope* d_scope;
-  SmtEngine* d_smt;
-
- public:
-  void setUp() override
-  {
-    d_em = new ExprManager();
-    d_nm = d_em->getNodeManager();
-    d_smt = new SmtEngine(d_nm);
-    d_scope = new NodeManagerScope(d_nm);
-  }
-
-  void tearDown() override
-  {
-    delete d_scope;
-    delete d_smt;
-    delete d_em;
-  }
-
-  void testSubtypes() {
-    TypeNode realType = d_nm->realType();
-    TypeNode integerType = d_nm->realType();
-    TypeNode booleanType = d_nm->booleanType();
-    TypeNode arrayType = d_nm->mkArrayType(realType, integerType);
-    TypeNode bvType = d_nm->mkBitVectorType(32);
-
-    Node x = d_nm->mkBoundVar("x", realType);
-    Node xPos = d_nm->mkNode(GT, x, d_nm->mkConst(Rational(0)));
-    TypeNode funtype = d_nm->mkFunctionType(integerType, booleanType);
-    Node lambda = d_nm->mkVar("lambda", funtype);
-    vector<Node> formals;
-    formals.push_back(x);
-    d_smt->defineFunction(lambda, formals, xPos);
-
-    TS_ASSERT( not realType.isComparableTo(booleanType) );
-    TS_ASSERT( realType.isComparableTo(integerType) );
-    TS_ASSERT( realType.isComparableTo(realType) );
-    TS_ASSERT( not realType.isComparableTo(arrayType) );
-    TS_ASSERT( not realType.isComparableTo(bvType) );
-
-    TS_ASSERT( not booleanType.isComparableTo(integerType) );
-    TS_ASSERT( not booleanType.isComparableTo(realType) );
-    TS_ASSERT( booleanType.isComparableTo(booleanType) );
-    TS_ASSERT( not booleanType.isComparableTo(arrayType) );
-    TS_ASSERT( not booleanType.isComparableTo(bvType) );
-
-    TS_ASSERT( integerType.isComparableTo(realType) );
-    TS_ASSERT( integerType.isComparableTo(integerType) );
-    TS_ASSERT( not integerType.isComparableTo(booleanType) );
-    TS_ASSERT( not integerType.isComparableTo(arrayType) );
-    TS_ASSERT( not integerType.isComparableTo(bvType) );
-
-    TS_ASSERT( not arrayType.isComparableTo(booleanType) );
-    TS_ASSERT( not arrayType.isComparableTo(integerType) );
-    TS_ASSERT( not arrayType.isComparableTo(realType) );
-    TS_ASSERT( arrayType.isComparableTo(arrayType) );
-    TS_ASSERT( not arrayType.isComparableTo(bvType) );
-
-    TS_ASSERT( not bvType.isComparableTo(booleanType) );
-    TS_ASSERT( not bvType.isComparableTo(integerType) );
-    TS_ASSERT( not bvType.isComparableTo(realType) );
-    TS_ASSERT( not bvType.isComparableTo(arrayType) );
-    TS_ASSERT( bvType.isComparableTo(bvType) );
-
-    TS_ASSERT(realType.getBaseType() == realType);
-    TS_ASSERT(integerType.getBaseType() == realType);
-    TS_ASSERT(booleanType.getBaseType() == booleanType);
-    TS_ASSERT(arrayType.getBaseType() == arrayType);
-    TS_ASSERT(bvType.getBaseType() == bvType);
-  }
-
-};/* TypeNodeWhite */
-