Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Morgan Deters, Andrew Reynolds, Tim King
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
       8                 :            :  * in the top-level source directory and their institutional affiliations.
       9                 :            :  * All rights reserved.  See the file COPYING in the top-level source
      10                 :            :  * directory for licensing information.
      11                 :            :  * ****************************************************************************
      12                 :            :  *
      13                 :            :  * Reference-counted encapsulation of a pointer to node information.
      14                 :            :  */
      15                 :            : #include "expr/node.h"
      16                 :            : 
      17                 :            : #include <cstring>
      18                 :            : #include <iostream>
      19                 :            : #include <sstream>
      20                 :            : 
      21                 :            : #include "base/exception.h"
      22                 :            : #include "base/output.h"
      23                 :            : #include "expr/attribute.h"
      24                 :            : #include "expr/node_manager_attributes.h"
      25                 :            : #include "expr/skolem_manager.h"
      26                 :            : #include "expr/type_checker.h"
      27                 :            : 
      28                 :            : using namespace std;
      29                 :            : 
      30                 :            : namespace cvc5::internal {
      31                 :            : 
      32                 :        245 : TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node,
      33                 :        245 :                                                            std::string message)
      34                 :        245 :     : Exception(message), d_node(new Node(node))
      35                 :            : {
      36                 :            : #ifdef CVC5_DEBUG
      37                 :        490 :   std::stringstream ss;
      38                 :        245 :   LastExceptionBuffer* current = LastExceptionBuffer::getCurrent();
      39         [ +  + ]:        245 :   if(current != NULL){
      40                 :            :     // Since this node is malformed, we cannot use toString().
      41                 :            :     // Instead, we print the kind and the children.
      42                 :         14 :     ss << "node kind: " << node.getKind() << ". children: ";
      43                 :         14 :     int i = 0;
      44         [ +  + ]:         29 :     for (const TNode& child : node)
      45                 :            :     {
      46                 :         15 :       ss << "child[" << i << "]: " << child << ". ";
      47                 :         15 :       i++;
      48                 :            :     }
      49                 :         28 :     string ssstring = ss.str();
      50                 :         14 :     current->setContents(ssstring.c_str());
      51                 :            :   }
      52                 :            : #endif /* CVC5_DEBUG */
      53                 :        245 : }
      54                 :            : 
      55         [ +  - ]:        245 : TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() { delete d_node; }
      56                 :            : 
      57                 :          0 : void TypeCheckingExceptionPrivate::toStream(std::ostream& os) const
      58                 :            : {
      59                 :          0 :   os << "Error during type checking: " << d_msg << std::endl << *d_node << endl << "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                 :            : struct IsConstComputedTag { };
      79                 :            : typedef expr::Attribute<IsConstTag, bool> IsConstAttr;
      80                 :            : typedef expr::Attribute<IsConstComputedTag, bool> IsConstComputedAttr;
      81                 :            : 
      82                 :            : template <bool ref_count>
      83                 :  648396000 : bool NodeTemplate<ref_count>::isConst() const {
      84                 :  648396000 :   assertTNodeNotExpired();
      85         [ +  - ]:  648396000 :   Trace("isConst") << "Node::isConst() for: " << *this << std::endl;
      86         [ +  + ]:  648396000 :   if(isNull()) {
      87                 :      62361 :     return false;
      88                 :            :   }
      89    [ +  + ][ + ]:  648334000 :   switch(getMetaKind()) {
      90                 :  292463600 :   case kind::metakind::CONSTANT:
      91         [ +  - ]:  292463600 :     Trace("isConst") << "Node::isConst() returning true, it's a CONSTANT" << std::endl;
      92                 :  292463600 :     return true;
      93                 :  136479700 :   case kind::metakind::VARIABLE:
      94         [ +  - ]:  136479700 :     Trace("isConst") << "Node::isConst() returning false, it's a VARIABLE" << std::endl;
      95                 :  136479700 :     return false;
      96                 :  219390300 :   default:
      97         [ +  + ]:  219390300 :     if(getAttribute(IsConstComputedAttr())) {
      98                 :  206272200 :       bool bval = getAttribute(IsConstAttr());
      99 [ +  - ][ -  - ]:  206272200 :       Trace("isConst") << "Node::isConst() returning cached value " << (bval ? "true" : "false") << " for: " << *this << std::endl;
     100                 :  206272200 :       return bval;
     101                 :            :     } else {
     102                 :   13118110 :       bool bval =
     103                 :   13118110 :           expr::TypeChecker::computeIsConst(d_nv->getNodeManager(), *this);
     104 [ +  - ][ -  - ]:   13118110 :       Trace("isConst") << "Node::isConst() computed value " << (bval ? "true" : "false") << " for: " << *this << std::endl;
     105                 :   13118110 :       const_cast< NodeTemplate<ref_count>* >(this)->setAttribute(IsConstAttr(), bval);
     106                 :   13118110 :       const_cast< NodeTemplate<ref_count>* >(this)->setAttribute(IsConstComputedAttr(), true);
     107                 :   13118110 :       return bval;
     108                 :            :     }
     109                 :            :   }
     110                 :            : }
     111                 :            : 
     112                 :            : template bool NodeTemplate<true>::isConst() const;
     113                 :            : template bool NodeTemplate<false>::isConst() const;
     114                 :            : 
     115                 :            : template <bool ref_count>
     116                 :   28856545 : bool NodeTemplate<ref_count>::hasName() const
     117                 :            : {
     118                 :   28856545 :   return d_nv->getNodeManager()->hasAttribute(*this, expr::VarNameAttr());
     119                 :            : }
     120                 :            : 
     121                 :            : template bool NodeTemplate<true>::hasName() const;
     122                 :            : template bool NodeTemplate<false>::hasName() const;
     123                 :            : 
     124                 :            : template <bool ref_count>
     125                 :   27871132 : std::string NodeTemplate<ref_count>::getName() const
     126                 :            : {
     127                 :   27871132 :   return d_nv->getNodeManager()->getAttribute(*this, expr::VarNameAttr());
     128                 :            : }
     129                 :            : 
     130                 :            : template std::string NodeTemplate<true>::getName() const;
     131                 :            : template std::string NodeTemplate<false>::getName() const;
     132                 :            : 
     133                 :            : template <bool ref_count>
     134                 :         27 : bool NodeTemplate<ref_count>::isSkolem() const
     135                 :            : {
     136                 :         27 :   return getKind() == Kind::SKOLEM;
     137                 :            : }
     138                 :            : 
     139                 :            : template bool NodeTemplate<true>::isSkolem() const;
     140                 :            : template bool NodeTemplate<false>::isSkolem() const;
     141                 :            : 
     142                 :            : template <bool ref_count>
     143                 :      16998 : SkolemId NodeTemplate<ref_count>::getSkolemId() const
     144                 :            : {
     145                 :      16998 :   return d_nv->getNodeManager()->getSkolemManager()->getId(*this);
     146                 :            : }
     147                 :            : 
     148                 :            : template SkolemId NodeTemplate<true>::getSkolemId() const;
     149                 :            : template SkolemId NodeTemplate<false>::getSkolemId() const;
     150                 :            : 
     151                 :            : template <bool ref_count>
     152                 :         15 : std::vector<Node> NodeTemplate<ref_count>::getSkolemIndices() const
     153                 :            : {
     154                 :         15 :   return d_nv->getNodeManager()->getSkolemManager()->getIndices(*this);
     155                 :            : }
     156                 :            : 
     157                 :            : template std::vector<Node> NodeTemplate<true>::getSkolemIndices() const;
     158                 :            : template std::vector<Node> NodeTemplate<false>::getSkolemIndices() const;
     159                 :            : 
     160                 :            : template <bool ref_count>
     161                 :    1141040 : InternalSkolemId NodeTemplate<ref_count>::getInternalSkolemId() const
     162                 :            : {
     163                 :    1141040 :   return d_nv->getNodeManager()->getSkolemManager()->getInternalId(*this);
     164                 :            : }
     165                 :            : 
     166                 :            : template InternalSkolemId NodeTemplate<true>::getInternalSkolemId() const;
     167                 :            : template InternalSkolemId NodeTemplate<false>::getInternalSkolemId() const;
     168                 :            : 
     169                 :            : }  // namespace cvc5::internal
     170                 :            : 
     171                 :            : namespace std {
     172                 :            : 
     173                 : 3090180000 : size_t hash<cvc5::internal::Node>::operator()(const cvc5::internal::Node& node) const
     174                 :            : {
     175                 : 3090180000 :   return node.getId();
     176                 :            : }
     177                 :            : 
     178                 : 7043220000 : size_t hash<cvc5::internal::TNode>::operator()(const cvc5::internal::TNode& node) const
     179                 :            : {
     180                 : 7043220000 :   return node.getId();
     181                 :            : }
     182                 :            : 
     183                 :            : }  // namespace std