google test: expr: Migrate attribute_black. (#5598)

diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt
index 2c698f953eee45f509383d6c5076e9b60b411737..762d075fccbc60ac256feddc2dfb0ba784ff4d29 100644 (file)
--- a/test/unit/expr/CMakeLists.txt
+++ b/test/unit/expr/CMakeLists.txt
@@ -11,7 +11,7 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_cxx_unit_test_black(attribute_black expr)
+cvc4_add_unit_test_black(attribute_black expr)
 cvc4_add_cxx_unit_test_white(attribute_white expr)
 cvc4_add_cxx_unit_test_black(expr_manager_public expr)
 cvc4_add_cxx_unit_test_black(expr_public expr)

diff --git a/test/unit/expr/attribute_black.cpp b/test/unit/expr/attribute_black.cpp
new file mode 100644 (file)
index 0000000..0d0fee4
--- /dev/null
+++ b/test/unit/expr/attribute_black.cpp
@@ -0,0 +1,128 @@
+/*********************                                                        */
+/*! \file attribute_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Tim King, Morgan Deters
+ ** 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::Attribute.
+ **
+ ** Black box testing of CVC4::Attribute.
+ **/
+
+#include <sstream>
+#include <vector>
+
+#include "expr/attribute.h"
+#include "expr/node.h"
+#include "expr/node_builder.h"
+#include "expr/node_value.h"
+#include "test_expr.h"
+
+namespace CVC4 {
+
+using namespace kind;
+using namespace smt;
+
+namespace test {
+
+class TextExprBlackAttributeBlack : public TestExprBlack
+{
+ protected:
+  struct PrimitiveIntAttributeId
+  {
+  };
+  using PrimitiveIntAttribute =
+      expr::Attribute<PrimitiveIntAttributeId, uint64_t>;
+  struct TNodeAttributeId
+  {
+  };
+  using TNodeAttribute = expr::Attribute<TNodeAttributeId, TNode>;
+  struct StringAttributeId
+  {
+  };
+  using StringAttribute = expr::Attribute<StringAttributeId, std::string>;
+  struct BoolAttributeId
+  {
+  };
+  using BoolAttribute = expr::Attribute<BoolAttributeId, bool>;
+};
+
+TEST_F(TextExprBlackAttributeBlack, ints)
+{
+  TypeNode booleanType = d_nodeManager->booleanType();
+  Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
+  const uint64_t val = 63489;
+  uint64_t data0 = 0;
+  uint64_t data1 = 0;
+
+  PrimitiveIntAttribute attr;
+  ASSERT_FALSE(node->getAttribute(attr, data0));
+  node->setAttribute(attr, val);
+  ASSERT_TRUE(node->getAttribute(attr, data1));
+  EXPECT_EQ(data1, val);
+
+  delete node;
+}
+
+TEST_F(TextExprBlackAttributeBlack, tnodes)
+{
+  TypeNode booleanType = d_nodeManager->booleanType();
+  Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
+
+  Node val(d_nodeManager->mkSkolem("b", booleanType));
+  TNode data0;
+  TNode data1;
+
+  TNodeAttribute attr;
+  ASSERT_FALSE(node->getAttribute(attr, data0));
+  node->setAttribute(attr, val);
+  ASSERT_TRUE(node->getAttribute(attr, data1));
+  EXPECT_EQ(data1, val);
+
+  delete node;
+}
+
+TEST_F(TextExprBlackAttributeBlack, strings)
+{
+  TypeNode booleanType = d_nodeManager->booleanType();
+  Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
+
+  std::string val("63489");
+  std::string data0;
+  std::string data1;
+
+  StringAttribute attr;
+  ASSERT_FALSE(node->getAttribute(attr, data0));
+  node->setAttribute(attr, val);
+  ASSERT_TRUE(node->getAttribute(attr, data1));
+  EXPECT_EQ(data1, val);
+
+  delete node;
+}
+
+TEST_F(TextExprBlackAttributeBlack, bools)
+{
+  TypeNode booleanType = d_nodeManager->booleanType();
+  Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
+
+  bool val = true;
+  bool data0 = false;
+  bool data1 = false;
+
+  BoolAttribute attr;
+  ASSERT_TRUE(node->getAttribute(attr, data0));
+  EXPECT_EQ(false, data0);
+  node->setAttribute(attr, val);
+  ASSERT_TRUE(node->getAttribute(attr, data1));
+  EXPECT_EQ(data1, val);
+
+  delete node;
+}
+
+}  // namespace test
+}  // namespace CVC4

diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h
deleted file mode 100644 (file)
index c293949..0000000
--- a/test/unit/expr/attribute_black.h
+++ /dev/null
@@ -1,138 +0,0 @@
-/*********************                                                        */
-/*! \file attribute_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Tim King, Morgan Deters, 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 Black box testing of CVC4::Attribute.
- **
- ** Black box testing of CVC4::Attribute.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-//Used in some of the tests
-#include <sstream>
-#include <vector>
-
-#include "api/cvc4cpp.h"
-#include "expr/attribute.h"
-#include "expr/expr_manager.h"
-#include "expr/node.h"
-#include "expr/node_builder.h"
-#include "expr/node_manager.h"
-#include "expr/node_value.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
-
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::smt;
-using namespace std;
-
-class AttributeBlack : public CxxTest::TestSuite {
- public:
-  void setUp() override
-  {
-    d_slv = new api::Solver();
-    d_exprManager = d_slv->getExprManager();
-    d_nodeManager = NodeManager::fromExprManager(d_exprManager);
-    d_smtEngine = d_slv->getSmtEngine();
-    d_scope = new SmtScope(d_smtEngine);
-  }
-
-  void tearDown() override
-  {
-    delete d_scope;
-    delete d_slv;
-  }
-
-  struct PrimitiveIntAttributeId {};
-  typedef expr::Attribute<PrimitiveIntAttributeId,uint64_t> PrimitiveIntAttribute;
-  void testInts(){
-    TypeNode booleanType = d_nodeManager->booleanType();
-    Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
-    const uint64_t val = 63489;
-    uint64_t data0 = 0;
-    uint64_t data1 = 0;
-
-    PrimitiveIntAttribute attr;
-    TS_ASSERT(!node->getAttribute(attr, data0));
-    node->setAttribute(attr, val);
-    TS_ASSERT(node->getAttribute(attr, data1));
-    TS_ASSERT_EQUALS(data1, val);
-
-    delete node;
-  }
-
-  struct TNodeAttributeId {};
-
-  typedef expr::Attribute<TNodeAttributeId, TNode> TNodeAttribute;
-  void testTNodes(){
-    TypeNode booleanType = d_nodeManager->booleanType();
-    Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
-
-    Node val(d_nodeManager->mkSkolem("b", booleanType));
-    TNode data0;
-    TNode data1;
-
-    TNodeAttribute attr;
-    TS_ASSERT(!node->getAttribute(attr, data0));
-    node->setAttribute(attr, val);
-    TS_ASSERT(node->getAttribute(attr, data1));
-    TS_ASSERT_EQUALS(data1, val);
-
-    delete node;
-  }
-
-  struct StringAttributeId {};
-  typedef expr::Attribute<StringAttributeId, std::string> StringAttribute;
-  void testStrings(){
-    TypeNode booleanType = d_nodeManager->booleanType();
-    Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
-
-    std::string val("63489");
-    std::string data0;
-    std::string data1;
-
-    StringAttribute attr;
-    TS_ASSERT(!node->getAttribute(attr, data0));
-    node->setAttribute(attr, val);
-    TS_ASSERT(node->getAttribute(attr, data1));
-    TS_ASSERT_EQUALS(data1, val);
-
-    delete node;
-  }
-
-  struct BoolAttributeId {};
-  typedef expr::Attribute<BoolAttributeId, bool> BoolAttribute;
-  void testBools(){
-    TypeNode booleanType = d_nodeManager->booleanType();
-    Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
-
-    bool val = true;
-    bool data0 = false;
-    bool data1 = false;
-
-    BoolAttribute attr;
-    TS_ASSERT(node->getAttribute(attr, data0));
-    TS_ASSERT_EQUALS(false, data0);
-    node->setAttribute(attr, val);
-    TS_ASSERT(node->getAttribute(attr, data1));
-    TS_ASSERT_EQUALS(data1, val);
-
-    delete node;
-  }
-
- private:
-  api::Solver* d_slv;
-  ExprManager* d_exprManager;
-  NodeManager* d_nodeManager;
-  SmtEngine* d_smtEngine;
-  SmtScope* d_scope;
-};

diff --git a/test/unit/test_expr.h b/test/unit/test_expr.h
new file mode 100644 (file)
index 0000000..7bcef5e
--- /dev/null
+++ b/test/unit/test_expr.h
@@ -0,0 +1,46 @@
+/*********************                                                        */
+/*! \file test_expr.h
+ ** \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 Common header for Expr unit test.
+ **/
+
+#ifndef CVC4__TEST__UNIT__TEST_EXPR_H
+#define CVC4__TEST__UNIT__TEST_EXPR_H
+
+#include "expr/expr_manager.h"
+#include "expr/node_manager.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+#include "test.h"
+#include "test_api.h"
+
+namespace CVC4 {
+namespace test {
+
+class TestExprBlack : public TestApi
+{
+ protected:
+  void SetUp() override
+  {
+    d_exprManager = d_solver.getExprManager();
+    d_nodeManager = NodeManager::fromExprManager(d_exprManager);
+    d_smtEngine = d_solver.getSmtEngine();
+    d_scope.reset(new smt::SmtScope(d_smtEngine));
+  }
+  std::unique_ptr<smt::SmtScope> d_scope;
+  ExprManager* d_exprManager;
+  NodeManager* d_nodeManager;
+  SmtEngine* d_smtEngine;
+};
+
+}  // namespace test
+}  // namespace CVC4
+#endif