From: Aina Niemetz Date: Fri, 4 Dec 2020 20:47:30 +0000 (-0800) Subject: google test: expr: Migrate attribute_black. (#5598) X-Git-Tag: cvc5-1.0.0~2497 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1029d9d55d254372951448d1af08bec4d9d1a31a;p=cvc5.git google test: expr: Migrate attribute_black. (#5598) --- diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt index 2c698f953..762d075fc 100644 --- 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 index 000000000..0d0fee4ea --- /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 +#include + +#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; + struct TNodeAttributeId + { + }; + using TNodeAttribute = expr::Attribute; + struct StringAttributeId + { + }; + using StringAttribute = expr::Attribute; + struct BoolAttributeId + { + }; + using BoolAttribute = expr::Attribute; +}; + +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 index c29394918..000000000 --- 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 - -//Used in some of the tests -#include -#include - -#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 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 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 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 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 index 000000000..7bcef5e0a --- /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 d_scope; + ExprManager* d_exprManager; + NodeManager* d_nodeManager; + SmtEngine* d_smtEngine; +}; + +} // namespace test +} // namespace CVC4 +#endif