Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * Black box testing of cvc5::Attribute.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include <sstream>
      14                 :            : #include <vector>
      15                 :            : 
      16                 :            : #include "expr/attribute.h"
      17                 :            : #include "expr/node.h"
      18                 :            : #include "expr/node_builder.h"
      19                 :            : #include "expr/node_value.h"
      20                 :            : #include "test_node.h"
      21                 :            : 
      22                 :            : namespace cvc5::internal {
      23                 :            : 
      24                 :            : using namespace kind;
      25                 :            : using namespace smt;
      26                 :            : 
      27                 :            : namespace test {
      28                 :            : 
      29                 :            : class TestNodeBlackAttribute : public TestNode
      30                 :            : {
      31                 :            :  protected:
      32                 :            :   struct PrimitiveIntAttributeId
      33                 :            :   {
      34                 :            :   };
      35                 :            :   using PrimitiveIntAttribute =
      36                 :            :       expr::Attribute<PrimitiveIntAttributeId, uint64_t>;
      37                 :            :   struct TNodeAttributeId
      38                 :            :   {
      39                 :            :   };
      40                 :            :   using TNodeAttribute = expr::Attribute<TNodeAttributeId, TNode>;
      41                 :            :   struct StringAttributeId
      42                 :            :   {
      43                 :            :   };
      44                 :            :   using StringAttribute = expr::Attribute<StringAttributeId, std::string>;
      45                 :            :   struct BoolAttributeId
      46                 :            :   {
      47                 :            :   };
      48                 :            :   using BoolAttribute = expr::Attribute<BoolAttributeId, bool>;
      49                 :            : };
      50                 :            : 
      51                 :          4 : TEST_F(TestNodeBlackAttribute, ints)
      52                 :            : {
      53                 :          1 :   TypeNode booleanType = d_nodeManager->booleanType();
      54                 :          1 :   Node* node = new Node(d_skolemManager->mkDummySkolem("b", booleanType));
      55                 :          1 :   const uint64_t val = 63489;
      56                 :          1 :   uint64_t data0 = 0;
      57                 :          1 :   uint64_t data1 = 0;
      58                 :            : 
      59                 :            :   PrimitiveIntAttribute attr;
      60 [ -  + ][ +  - ]:          1 :   ASSERT_FALSE(node->getAttribute(attr, data0));
      61                 :          1 :   node->setAttribute(attr, val);
      62 [ -  + ][ +  - ]:          1 :   ASSERT_TRUE(node->getAttribute(attr, data1));
      63 [ -  + ][ +  - ]:          1 :   ASSERT_EQ(data1, val);
      64                 :            : 
      65         [ +  - ]:          1 :   delete node;
      66         [ +  - ]:          1 : }
      67                 :            : 
      68                 :          4 : TEST_F(TestNodeBlackAttribute, tnodes)
      69                 :            : {
      70                 :          1 :   TypeNode booleanType = d_nodeManager->booleanType();
      71                 :          1 :   Node* node = new Node(d_skolemManager->mkDummySkolem("b", booleanType));
      72                 :            : 
      73                 :          2 :   Node val(d_skolemManager->mkDummySkolem("b", booleanType));
      74                 :          1 :   TNode data0;
      75                 :          1 :   TNode data1;
      76                 :            : 
      77                 :            :   TNodeAttribute attr;
      78 [ -  + ][ +  - ]:          1 :   ASSERT_FALSE(node->getAttribute(attr, data0));
      79                 :          1 :   node->setAttribute(attr, val);
      80 [ -  + ][ +  - ]:          1 :   ASSERT_TRUE(node->getAttribute(attr, data1));
      81 [ -  + ][ +  - ]:          1 :   ASSERT_EQ(data1, val);
      82                 :            : 
      83         [ +  - ]:          1 :   delete node;
      84 [ +  - ][ +  - ]:          1 : }
         [ +  - ][ +  - ]
      85                 :            : 
      86                 :          4 : TEST_F(TestNodeBlackAttribute, strings)
      87                 :            : {
      88                 :          1 :   TypeNode booleanType = d_nodeManager->booleanType();
      89                 :          1 :   Node* node = new Node(d_skolemManager->mkDummySkolem("b", booleanType));
      90                 :            : 
      91                 :          1 :   std::string val("63489");
      92                 :          1 :   std::string data0;
      93                 :          1 :   std::string data1;
      94                 :            : 
      95                 :            :   StringAttribute attr;
      96 [ -  + ][ +  - ]:          1 :   ASSERT_FALSE(node->getAttribute(attr, data0));
      97                 :          1 :   node->setAttribute(attr, val);
      98 [ -  + ][ +  - ]:          1 :   ASSERT_TRUE(node->getAttribute(attr, data1));
      99 [ -  + ][ +  - ]:          1 :   ASSERT_EQ(data1, val);
     100                 :            : 
     101         [ +  - ]:          1 :   delete node;
     102 [ +  - ][ +  - ]:          1 : }
         [ +  - ][ +  - ]
     103                 :            : 
     104                 :          4 : TEST_F(TestNodeBlackAttribute, bools)
     105                 :            : {
     106                 :          1 :   TypeNode booleanType = d_nodeManager->booleanType();
     107                 :          1 :   Node* node = new Node(d_skolemManager->mkDummySkolem("b", booleanType));
     108                 :            : 
     109                 :          1 :   bool val = true;
     110                 :          1 :   bool data0 = false;
     111                 :          1 :   bool data1 = false;
     112                 :            : 
     113                 :            :   BoolAttribute attr;
     114 [ -  + ][ +  - ]:          1 :   ASSERT_TRUE(node->getAttribute(attr, data0));
     115 [ -  + ][ +  - ]:          1 :   ASSERT_EQ(false, data0);
     116                 :          1 :   node->setAttribute(attr, val);
     117 [ -  + ][ +  - ]:          1 :   ASSERT_TRUE(node->getAttribute(attr, data1));
     118 [ -  + ][ +  - ]:          1 :   ASSERT_EQ(data1, val);
     119                 :            : 
     120         [ +  - ]:          1 :   delete node;
     121         [ +  - ]:          1 : }
     122                 :            : 
     123                 :            : }  // namespace test
     124                 :            : }  // namespace cvc5::internal