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                 :            :  * Reference-counted encapsulation of a pointer to node information.
      11                 :            :  */
      12                 :            : #include "expr/node.h"
      13                 :            : 
      14                 :            : #include <cstring>
      15                 :            : #include <iostream>
      16                 :            : #include <sstream>
      17                 :            : 
      18                 :            : #include "base/exception.h"
      19                 :            : #include "base/output.h"
      20                 :            : #include "expr/attribute.h"
      21                 :            : #include "expr/node_manager_attributes.h"
      22                 :            : #include "expr/skolem_manager.h"
      23                 :            : #include "expr/type_checker.h"
      24                 :            : 
      25                 :            : using namespace std;
      26                 :            : 
      27                 :            : namespace cvc5::internal {
      28                 :            : 
      29                 :        255 : TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node,
      30                 :        255 :                                                            std::string message)
      31                 :        255 :     : Exception(message), d_node(new Node(node))
      32                 :            : {
      33                 :            : #ifdef CVC5_DEBUG
      34                 :        255 :   std::stringstream ss;
      35                 :        255 :   LastExceptionBuffer* current = LastExceptionBuffer::getCurrent();
      36         [ +  + ]:        255 :   if (current != NULL)
      37                 :            :   {
      38                 :            :     // Since this node is malformed, we cannot use toString().
      39                 :            :     // Instead, we print the kind and the children.
      40                 :         24 :     ss << "node kind: " << node.getKind() << ". children: ";
      41                 :         24 :     int i = 0;
      42         [ +  + ]:         54 :     for (const TNode& child : node)
      43                 :            :     {
      44                 :         30 :       ss << "child[" << i << "]: " << child << ". ";
      45                 :         30 :       i++;
      46                 :         30 :     }
      47                 :         24 :     string ssstring = ss.str();
      48                 :         24 :     current->setContents(ssstring.c_str());
      49                 :         24 :   }
      50                 :            : #endif /* CVC5_DEBUG */
      51                 :        255 : }
      52                 :            : 
      53         [ +  - ]:        255 : TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() { delete d_node; }
      54                 :            : 
      55                 :          0 : void TypeCheckingExceptionPrivate::toStream(std::ostream& os) const
      56                 :            : {
      57                 :          0 :   os << "Error during type checking: " << d_msg << std::endl
      58                 :          0 :      << *d_node << endl
      59                 :          0 :      << "The ill-typed expression: " << *d_node;
      60                 :          0 : }
      61                 :            : 
      62                 :          0 : NodeTemplate<true> TypeCheckingExceptionPrivate::getNode() const
      63                 :            : {
      64                 :          0 :   return *d_node;
      65                 :            : }
      66                 :            : 
      67                 :          0 : UnknownTypeException::UnknownTypeException(TNode n)
      68                 :            :     : TypeCheckingExceptionPrivate(
      69                 :            :           n,
      70                 :            :           "this expression contains an element of unknown type (such as an "
      71                 :            :           "abstract value);"
      72                 :          0 :           " its type cannot be computed until it is substituted away")
      73                 :            : {
      74                 :          0 : }
      75                 :            : 
      76                 :            : /** Is this node constant? (and has that been computed yet?) */
      77                 :            : struct IsConstTag
      78                 :            : {
      79                 :            : };
      80                 :            : struct IsConstComputedTag
      81                 :            : {
      82                 :            : };
      83                 :            : typedef expr::Attribute<IsConstTag, bool> IsConstAttr;
      84                 :            : typedef expr::Attribute<IsConstComputedTag, bool> IsConstComputedAttr;
      85                 :            : 
      86                 :            : template <bool ref_count>
      87                 :  643269745 : bool NodeTemplate<ref_count>::isConst() const
      88                 :            : {
      89                 :  643269745 :   assertTNodeNotExpired();
      90         [ +  - ]:  643269745 :   Trace("isConst") << "Node::isConst() for: " << *this << std::endl;
      91         [ +  + ]:  643269745 :   if (isNull())
      92                 :            :   {
      93                 :      73993 :     return false;
      94                 :            :   }
      95    [ +  + ][ + ]:  643195752 :   switch (getMetaKind())
      96                 :            :   {
      97                 :  307159981 :     case kind::metakind::CONSTANT:
      98         [ +  - ]:  307159981 :       Trace("isConst") << "Node::isConst() returning true, it's a CONSTANT"
      99                 :          0 :                        << std::endl;
     100                 :  307159981 :       return true;
     101                 :  123078648 :     case kind::metakind::VARIABLE:
     102         [ +  - ]:  123078648 :       Trace("isConst") << "Node::isConst() returning false, it's a VARIABLE"
     103                 :          0 :                        << std::endl;
     104                 :  123078648 :       return false;
     105                 :  212957123 :     default:
     106         [ +  + ]:  212957123 :       if (getAttribute(IsConstComputedAttr()))
     107                 :            :       {
     108                 :  200853438 :         bool bval = getAttribute(IsConstAttr());
     109         [ +  - ]:  401706876 :         Trace("isConst") << "Node::isConst() returning cached value "
     110         [ -  - ]:  200853438 :                          << (bval ? "true" : "false") << " for: " << *this
     111                 :          0 :                          << std::endl;
     112                 :  200853438 :         return bval;
     113                 :            :       }
     114                 :            :       else
     115                 :            :       {
     116                 :   12103685 :         bool bval =
     117                 :   12103685 :             expr::TypeChecker::computeIsConst(d_nv->getNodeManager(), *this);
     118         [ +  - ]:   24207370 :         Trace("isConst") << "Node::isConst() computed value "
     119         [ -  - ]:   12103685 :                          << (bval ? "true" : "false") << " for: " << *this
     120                 :          0 :                          << std::endl;
     121                 :   12103685 :         const_cast<NodeTemplate<ref_count>*>(this)->setAttribute(IsConstAttr(),
     122                 :            :                                                                  bval);
     123                 :   12103685 :         const_cast<NodeTemplate<ref_count>*>(this)->setAttribute(
     124                 :   12103685 :             IsConstComputedAttr(), true);
     125                 :   12103685 :         return bval;
     126                 :            :       }
     127                 :            :   }
     128                 :            : }
     129                 :            : 
     130                 :            : template bool NodeTemplate<true>::isConst() const;
     131                 :            : template bool NodeTemplate<false>::isConst() const;
     132                 :            : 
     133                 :            : template <bool ref_count>
     134                 :   20816014 : bool NodeTemplate<ref_count>::hasName() const
     135                 :            : {
     136                 :   20816014 :   return d_nv->getNodeManager()->hasAttribute(*this, expr::VarNameAttr());
     137                 :            : }
     138                 :            : 
     139                 :            : template bool NodeTemplate<true>::hasName() const;
     140                 :            : template bool NodeTemplate<false>::hasName() const;
     141                 :            : 
     142                 :            : template <bool ref_count>
     143                 :   20607813 : std::string NodeTemplate<ref_count>::getName() const
     144                 :            : {
     145                 :   20607813 :   return d_nv->getNodeManager()->getAttribute(*this, expr::VarNameAttr());
     146                 :            : }
     147                 :            : 
     148                 :            : template std::string NodeTemplate<true>::getName() const;
     149                 :            : template std::string NodeTemplate<false>::getName() const;
     150                 :            : 
     151                 :            : template <bool ref_count>
     152                 :        942 : bool NodeTemplate<ref_count>::isSkolem() const
     153                 :            : {
     154                 :        942 :   return getKind() == Kind::SKOLEM;
     155                 :            : }
     156                 :            : 
     157                 :            : template bool NodeTemplate<true>::isSkolem() const;
     158                 :            : template bool NodeTemplate<false>::isSkolem() const;
     159                 :            : 
     160                 :            : template <bool ref_count>
     161                 :      13820 : SkolemId NodeTemplate<ref_count>::getSkolemId() const
     162                 :            : {
     163                 :      13820 :   return d_nv->getNodeManager()->getSkolemManager()->getId(*this);
     164                 :            : }
     165                 :            : 
     166                 :            : template SkolemId NodeTemplate<true>::getSkolemId() const;
     167                 :            : template SkolemId NodeTemplate<false>::getSkolemId() const;
     168                 :            : 
     169                 :            : template <bool ref_count>
     170                 :         14 : std::vector<Node> NodeTemplate<ref_count>::getSkolemIndices() const
     171                 :            : {
     172                 :         14 :   return d_nv->getNodeManager()->getSkolemManager()->getIndices(*this);
     173                 :            : }
     174                 :            : 
     175                 :            : template std::vector<Node> NodeTemplate<true>::getSkolemIndices() const;
     176                 :            : template std::vector<Node> NodeTemplate<false>::getSkolemIndices() const;
     177                 :            : 
     178                 :            : template <bool ref_count>
     179                 :     441130 : InternalSkolemId NodeTemplate<ref_count>::getInternalSkolemId() const
     180                 :            : {
     181                 :     441130 :   return d_nv->getNodeManager()->getSkolemManager()->getInternalId(*this);
     182                 :            : }
     183                 :            : 
     184                 :            : template InternalSkolemId NodeTemplate<true>::getInternalSkolemId() const;
     185                 :            : template InternalSkolemId NodeTemplate<false>::getInternalSkolemId() const;
     186                 :            : 
     187                 :            : }  // namespace cvc5::internal
     188                 :            : 
     189                 :            : namespace std {
     190                 :            : 
     191                 : 3301145977 : size_t hash<cvc5::internal::Node>::operator()(
     192                 :            :     const cvc5::internal::Node& node) const
     193                 :            : {
     194                 : 3301145977 :   return node.getId();
     195                 :            : }
     196                 :            : 
     197                 : 4535608540 : size_t hash<cvc5::internal::TNode>::operator()(
     198                 :            :     const cvc5::internal::TNode& node) const
     199                 :            : {
     200                 : 4535608540 :   return node.getId();
     201                 :            : }
     202                 :            : 
     203                 :            : }  // namespace std