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                 :            :  * A node value.
      11                 :            :  *
      12                 :            :  * The actual node implementation.
      13                 :            :  * Instances of this class are generally referenced through cvc5::internal::Node
      14                 :            :  * rather than by pointer. Note that cvc5::internal::Node maintains the
      15                 :            :  * reference count on NodeValue instances.
      16                 :            :  */
      17                 :            : #include "expr/node_value.h"
      18                 :            : 
      19                 :            : #include <sstream>
      20                 :            : 
      21                 :            : #include "expr/kind.h"
      22                 :            : #include "expr/metakind.h"
      23                 :            : #include "expr/node.h"
      24                 :            : #include "options/base_options.h"
      25                 :            : #include "options/io_utils.h"
      26                 :            : #include "options/language.h"
      27                 :            : #include "options/options.h"
      28                 :            : #include "printer/printer.h"
      29                 :            : 
      30                 :            : using namespace std;
      31                 :            : 
      32                 :            : namespace cvc5::internal {
      33                 :            : namespace expr {
      34                 :            : 
      35                 :      68155 : string NodeValue::toString() const
      36                 :            : {
      37                 :      68155 :   stringstream ss;
      38                 :      68155 :   toStream(ss);
      39                 :     136310 :   return ss.str();
      40                 :      68155 : }
      41                 :            : 
      42                 :    9548831 : void NodeValue::toStream(std::ostream& out) const
      43                 :            : {
      44                 :            :   // Ensure that this node value is live for the length of this call.
      45                 :            :   // It really breaks things badly if we don't have a nonzero ref
      46                 :            :   // count, even just for printing.
      47                 :    9548831 :   RefCountGuard guard(this);
      48                 :            : 
      49                 :    9548831 :   Printer::getPrinter(out)->toStream(out, TNode(this));
      50                 :    9548831 : }
      51                 :            : 
      52                 :          0 : void NodeValue::printAst(std::ostream& out, int ind) const
      53                 :            : {
      54                 :          0 :   RefCountGuard guard(this);
      55                 :            : 
      56                 :          0 :   indent(out, ind);
      57                 :          0 :   out << '(';
      58                 :          0 :   out << getKind();
      59                 :          0 :   if (getMetaKind() == kind::metakind::VARIABLE
      60                 :          0 :       || getMetaKind() == kind::metakind::NULLARY_OPERATOR)
      61                 :            :   {
      62                 :          0 :     out << ' ' << getId();
      63                 :            :   }
      64         [ -  - ]:          0 :   else if (getMetaKind() == kind::metakind::CONSTANT)
      65                 :            :   {
      66                 :          0 :     out << ' ';
      67                 :          0 :     kind::metakind::nodeValueConstantToStream(out, this);
      68                 :            :   }
      69                 :            :   else
      70                 :            :   {
      71         [ -  - ]:          0 :     if (nv_begin() != nv_end())
      72                 :            :     {
      73         [ -  - ]:          0 :       for (const_nv_iterator child = nv_begin(); child != nv_end(); ++child)
      74                 :            :       {
      75                 :          0 :         out << std::endl;
      76                 :          0 :         (*child)->printAst(out, ind + 1);
      77                 :            :       }
      78                 :          0 :       out << std::endl;
      79                 :          0 :       indent(out, ind);
      80                 :            :     }
      81                 :            :   }
      82                 :          0 :   out << ')';
      83                 :          0 : }
      84                 :            : 
      85                 :          0 : NodeValue::iterator<NodeTemplate<true> > operator+(
      86                 :            :     NodeValue::iterator<NodeTemplate<true> >::difference_type p,
      87                 :            :     NodeValue::iterator<NodeTemplate<true> > i)
      88                 :            : {
      89                 :          0 :   return i + p;
      90                 :            : }
      91                 :            : 
      92                 :          0 : NodeValue::iterator<NodeTemplate<false> > operator+(
      93                 :            :     NodeValue::iterator<NodeTemplate<false> >::difference_type p,
      94                 :            :     NodeValue::iterator<NodeTemplate<false> > i)
      95                 :            : {
      96                 :          0 :   return i + p;
      97                 :            : }
      98                 :            : 
      99                 :          0 : std::ostream& operator<<(std::ostream& out, const NodeValue& nv)
     100                 :            : {
     101                 :          0 :   nv.toStream(out);
     102                 :          0 :   return out;
     103                 :            : }
     104                 :            : 
     105                 :          3 : void NodeValue::markRefCountMaxedOut()
     106                 :            : {
     107 [ -  + ][ -  + ]:          3 :   Assert(d_nm != nullptr)
                 [ -  - ]
     108                 :            :       << "No current NodeManager on incrementing of NodeValue: "
     109                 :            :          "maybe a public cvc5 interface function is missing a "
     110                 :          0 :          "NodeManagerScope ?";
     111                 :          3 :   d_nm->markRefCountMaxedOut(this);
     112                 :          3 : }
     113                 :            : 
     114                 :  219085020 : void NodeValue::markForDeletion()
     115                 :            : {
     116 [ -  + ][ -  + ]:  219085020 :   Assert(d_nm != nullptr)
                 [ -  - ]
     117                 :            :       << "No current NodeManager on destruction of NodeValue: "
     118                 :            :          "maybe a public cvc5 interface function is missing a "
     119                 :          0 :          "NodeManagerScope ?";
     120                 :  219085020 :   d_nm->markForDeletion(this);
     121                 :  219085020 : }
     122                 :            : 
     123                 :            : }  // namespace expr
     124                 :            : }  // namespace cvc5::internal