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                 :            : 
      18                 :            : #include "cvc5_private.h"
      19                 :            : 
      20                 :            : #ifndef CVC5__EXPR__NODE_VALUE_H
      21                 :            : #define CVC5__EXPR__NODE_VALUE_H
      22                 :            : 
      23                 :            : #include <iterator>
      24                 :            : #include <string>
      25                 :            : 
      26                 :            : #include "expr/kind.h"
      27                 :            : #include "expr/metakind.h"
      28                 :            : #include "options/language.h"
      29                 :            : 
      30                 :            : namespace cvc5::internal {
      31                 :            : 
      32                 :            : template <bool ref_count>
      33                 :            : class NodeTemplate;
      34                 :            : class TypeNode;
      35                 :            : class NodeBuilder;
      36                 :            : class NodeManager;
      37                 :            : 
      38                 :            : namespace expr {
      39                 :            : class NodeValue;
      40                 :            : }
      41                 :            : 
      42                 :            : namespace kind {
      43                 :            : namespace metakind {
      44                 :            : 
      45                 :            : template <cvc5::internal::Kind k, class T, bool pool>
      46                 :            : struct NodeValueConstCompare;
      47                 :            : 
      48                 :            : struct NodeValueCompare;
      49                 :            : 
      50                 :            : }  // namespace metakind
      51                 :            : }  // namespace kind
      52                 :            : 
      53                 :            : namespace expr {
      54                 :            : 
      55                 :            : /**
      56                 :            :  * This is a NodeValue.
      57                 :            :  */
      58                 :            : class CVC5_EXPORT NodeValue
      59                 :            : {
      60                 :            :   template <bool>
      61                 :            :   friend class cvc5::internal::NodeTemplate;
      62                 :            :   friend class cvc5::internal::TypeNode;
      63                 :            :   friend class cvc5::internal::NodeBuilder;
      64                 :            :   friend class cvc5::internal::NodeManager;
      65                 :            : 
      66                 :            :   template <Kind k, class T, bool pool>
      67                 :            :   friend struct kind::metakind::NodeValueConstCompare;
      68                 :            : 
      69                 :            :   friend struct kind::metakind::NodeValueCompare;
      70                 :            : 
      71                 :            :   friend void kind::metakind::nodeValueConstantToStream(std::ostream& out,
      72                 :            :                                                         const NodeValue* nv);
      73                 :            :   friend void kind::metakind::deleteNodeValueConstant(NodeValue* nv);
      74                 :            : 
      75                 :            :   friend class RefCountGuard;
      76                 :            : 
      77                 :            :   /* ------------------------------------------------------------------------ */
      78                 :            :  public:
      79                 :            :   /* ------------------------------------------------------------------------ */
      80                 :            : 
      81                 :            :   using nv_iterator = NodeValue**;
      82                 :            :   using const_nv_iterator = NodeValue const* const*;
      83                 :            : 
      84                 :            :   template <class T>
      85                 :            :   class iterator
      86                 :            :   {
      87                 :            :    public:
      88                 :            :     using iterator_category = std::random_access_iterator_tag;
      89                 :            :     using value_type = T;
      90                 :            :     using difference_type = std::ptrdiff_t;
      91                 :            :     using pointer = T*;
      92                 :            :     using reference = T;
      93                 :            : 
      94                 :  306475915 :     iterator() : d_i(nullptr) {}
      95                 : 2885933643 :     explicit iterator(const_nv_iterator i) : d_i(i) {}
      96                 :            : 
      97                 :            :     /** Conversion of a TNode iterator to a Node iterator. */
      98                 :  316751266 :     inline operator NodeValue::iterator<NodeTemplate<true> >() const
      99                 :            :     {
     100                 :  316751266 :       return iterator<NodeTemplate<true> >(d_i);
     101                 :            :     }
     102                 :            : 
     103                 : 2448220798 :     T operator*() const { return T(*d_i); }
     104                 :            : 
     105                 :  616643351 :     bool operator==(const iterator& i) const { return d_i == i.d_i; }
     106                 :            : 
     107                 : 3235789952 :     bool operator!=(const iterator& i) const { return d_i != i.d_i; }
     108                 :            : 
     109                 : 2124340053 :     iterator& operator++()
     110                 :            :     {
     111                 : 2124340053 :       ++d_i;
     112                 : 2124340053 :       return *this;
     113                 :            :     }
     114                 :            : 
     115                 :     125682 :     iterator operator++(int) { return iterator(d_i++); }
     116                 :            : 
     117                 :   50258982 :     iterator& operator--()
     118                 :            :     {
     119                 :   50258982 :       --d_i;
     120                 :   50258982 :       return *this;
     121                 :            :     }
     122                 :            : 
     123                 :            :     iterator operator--(int) { return iterator(d_i--); }
     124                 :            : 
     125                 :   85404655 :     iterator& operator+=(difference_type p)
     126                 :            :     {
     127                 :   85404655 :       d_i += p;
     128                 :   85404655 :       return *this;
     129                 :            :     }
     130                 :            : 
     131                 :    3137174 :     iterator& operator-=(difference_type p)
     132                 :            :     {
     133                 :    3137174 :       d_i -= p;
     134                 :    3137174 :       return *this;
     135                 :            :     }
     136                 :            : 
     137                 :    1342276 :     iterator operator+(difference_type p) const { return iterator(d_i + p); }
     138                 :            : 
     139                 :    2609854 :     iterator operator-(difference_type p) const { return iterator(d_i - p); }
     140                 :            : 
     141                 :  469798294 :     difference_type operator-(iterator i) const { return d_i - i.d_i; }
     142                 :            : 
     143                 :            :    private:
     144                 :            :     const_nv_iterator d_i;
     145                 :            : 
     146                 :            :   }; /* class NodeValue::iterator<T> */
     147                 :            : 
     148                 :15712592186 :   uint64_t getId() const { return d_id; }
     149                 :            : 
     150                 :17220012173 :   Kind getKind() const { return dKindToKind(d_kind); }
     151                 :            : 
     152                 :12112543148 :   kind::MetaKind getMetaKind() const { return kind::metaKindOf(getKind()); }
     153                 :            : 
     154                 : 8258404446 :   NodeManager* getNodeManager() const { return d_nm; }
     155                 :            : 
     156                 : 2757834162 :   uint32_t getNumChildren() const
     157                 :            :   {
     158         [ +  + ]: 2757834162 :     return (getMetaKind() == kind::metakind::PARAMETERIZED) ? d_nchildren - 1
     159                 : 2757834162 :                                                             : d_nchildren;
     160                 :            :   }
     161                 :            : 
     162                 :            :   /* ------------------------------ Header ---------------------------------- */
     163                 :            :   /** Number of bits reserved for reference counting. */
     164                 :            :   static constexpr uint32_t NBITS_REFCOUNT = 20;
     165                 :            :   /** Number of bits reserved for node kind. */
     166                 :            :   static constexpr uint32_t NBITS_KIND = 10;
     167                 :            :   /** Number of bits reserved for node id. */
     168                 :            :   static constexpr uint32_t NBITS_ID = 40;
     169                 :            :   /** Number of bits reserved for number of children. */
     170                 :            :   static const uint32_t NBITS_NCHILDREN = 26;
     171                 :            :   static_assert(NBITS_REFCOUNT + NBITS_KIND + NBITS_ID + NBITS_NCHILDREN == 96,
     172                 :            :                 "NodeValue header bit assignment does not sum to 96 !");
     173                 :            :   /* ------------------- This header fits into 96 bits ---------------------- */
     174                 :            : 
     175                 :            :   /** Maximum number of children possible. */
     176                 :            :   static constexpr uint32_t MAX_CHILDREN =
     177                 :            :       (static_cast<uint32_t>(1) << NBITS_NCHILDREN) - 1;
     178                 :            : 
     179                 :            :   uint32_t getRefCount() const { return d_rc; }
     180                 :            : 
     181                 :            :   NodeValue* getOperator() const;
     182                 :            :   NodeValue* getChild(int i) const;
     183                 :            : 
     184                 :            :   /** If this is a CONST_* Node, extract the constant from it.  */
     185                 :            :   template <class T>
     186                 :            :   const T& getConst() const;
     187                 :            : 
     188                 :19048183012 :   static inline NodeValue& null()
     189                 :            :   {
     190 [ +  + ][ +  - ]:19048183012 :     static NodeValue* s_null = new NodeValue(0);
                 [ -  - ]
     191                 :19048183012 :     return *s_null;
     192                 :            :   }
     193                 :            : 
     194                 :            :   /**
     195                 :            :    * Hash this NodeValue.  For hash_maps, hash_sets, etc.. but this is
     196                 :            :    * for expr package internal use only at present!  This is likely to
     197                 :            :    * be POORLY PERFORMING for other uses!  For example, this gives
     198                 :            :    * collisions for all VARIABLEs.
     199                 :            :    * @return the hash value of this expression.
     200                 :            :    */
     201                 : 1667705280 :   size_t poolHash() const
     202                 :            :   {
     203         [ +  + ]: 1667705280 :     if (getMetaKind() == kind::metakind::CONSTANT)
     204                 :            :     {
     205                 :  530905222 :       return kind::metakind::NodeValueCompare::constHash(this);
     206                 :            :     }
     207                 :            : 
     208                 : 1136800058 :     size_t hash = d_kind;
     209                 : 1136800058 :     const_nv_iterator i = nv_begin();
     210                 : 1136800058 :     const_nv_iterator i_end = nv_end();
     211         [ +  + ]: 4122172286 :     while (i != i_end)
     212                 :            :     {
     213                 : 2985372228 :       hash ^= (*i)->d_id + 0x9e3779b9 + (hash << 6) + (hash >> 2);
     214                 : 2985372228 :       ++i;
     215                 :            :     }
     216                 : 1136800058 :     return hash;
     217                 :            :   }
     218                 :            : 
     219                 :  718206825 :   static inline uint32_t kindToDKind(Kind k)
     220                 :            :   {
     221                 :  718206825 :     return ((uint32_t)k) & kindMask;
     222                 :            :   }
     223                 :            : 
     224                 :17220012173 :   static inline Kind dKindToKind(uint32_t d)
     225                 :            :   {
     226         [ +  + ]:17220012173 :     return (d == kindMask) ? Kind::UNDEFINED_KIND : Kind(d);
     227                 :            :   }
     228                 :            : 
     229                 :            :   std::string toString() const;
     230                 :            : 
     231                 :            :   void toStream(std::ostream& out) const;
     232                 :            : 
     233                 :            :   void printAst(std::ostream& out, int indent = 0) const;
     234                 :            : 
     235                 :            :   template <typename T>
     236                 :            :   inline iterator<T> begin() const;
     237                 :            :   template <typename T>
     238                 :            :   inline iterator<T> end() const;
     239                 :            : 
     240                 :            :   /* ------------------------------------------------------------------------ */
     241                 :            :  private:
     242                 :            :   /* ------------------------------------------------------------------------ */
     243                 :            : 
     244                 :            :   /**
     245                 :            :    * RAII guard that increases the reference count if the reference count to be
     246                 :            :    * > 0.  Otherwise, this does nothing. This does not just increment the
     247                 :            :    * reference count to avoid maxing out the d_rc field. This is only for low
     248                 :            :    * level functions.
     249                 :            :    */
     250                 :            :   class RefCountGuard
     251                 :            :   {
     252                 :            :    public:
     253                 :    9466299 :     RefCountGuard(const NodeValue* nv) : d_nv(const_cast<NodeValue*>(nv))
     254                 :            :     {
     255                 :    9466299 :       d_increased = (d_nv->d_rc == 0);
     256         [ -  + ]:    9466299 :       if (d_increased)
     257                 :            :       {
     258                 :          0 :         d_nv->d_rc = 1;
     259                 :            :       }
     260                 :    9466299 :     }
     261                 :    9466299 :     ~RefCountGuard()
     262                 :            :     {
     263                 :            :       // dec() without marking for deletion: we don't want to garbage
     264                 :            :       // collect this NodeValue if ours is the last reference to it.
     265                 :            :       // E.g., this can happen when debugging code calls the print
     266                 :            :       // routines below.  As RefCountGuards are scoped on the stack,
     267                 :            :       // this should be fine---but not in multithreaded contexts!
     268         [ -  + ]:    9466299 :       if (d_increased)
     269                 :            :       {
     270                 :          0 :         --d_nv->d_rc;
     271                 :            :       }
     272                 :    9466299 :     }
     273                 :            : 
     274                 :            :    private:
     275                 :            :     NodeValue* d_nv;
     276                 :            :     bool d_increased;
     277                 :            :   }; /* NodeValue::RefCountGuard */
     278                 :            : 
     279                 :            :   /** Maximum reference count possible.  Used for sticky
     280                 :            :    *  reference-counting.  Should be (1 << num_bits(d_rc)) - 1 */
     281                 :            :   static constexpr uint32_t MAX_RC =
     282                 :            :       (static_cast<uint32_t>(1) << NBITS_REFCOUNT) - 1;
     283                 :            : 
     284                 :            :   /** A mask for d_kind */
     285                 :            :   static constexpr uint32_t kindMask =
     286                 :            :       (static_cast<uint32_t>(1) << NBITS_KIND) - 1;
     287                 :            : 
     288                 :            :   /** Uninitializing constructor for NodeBuilder's use.  */
     289                 : 1188758104 :   NodeValue() { /* do not initialize! */ }
     290                 :            :   /** Private constructor for the null value. */
     291                 :            :   NodeValue(int);
     292                 :            : 
     293                 :41243738687 :   void inc()
     294                 :            :   {
     295         [ +  + ]:41243738687 :     if (__builtin_expect((d_rc < MAX_RC - 1), true))
     296                 :            :     {
     297                 :31748434254 :       ++d_rc;
     298                 :            :     }
     299         [ +  + ]: 9495304433 :     else if (__builtin_expect((d_rc == MAX_RC - 1), false))
     300                 :            :     {
     301                 :          3 :       ++d_rc;
     302                 :          3 :       markRefCountMaxedOut();
     303                 :            :     }
     304                 :41243738687 :   }
     305                 :            : 
     306                 :48588452094 :   void dec()
     307                 :            :   {
     308         [ +  + ]:48588452094 :     if (__builtin_expect((d_rc < MAX_RC), true))
     309                 :            :     {
     310                 :31742947911 :       --d_rc;
     311         [ +  + ]:31742947911 :       if (__builtin_expect((d_rc == 0), false))
     312                 :            :       {
     313                 :  218698720 :         markForDeletion();
     314                 :            :       }
     315                 :            :     }
     316                 :48588452094 :   }
     317                 :            : 
     318                 :            :   void markRefCountMaxedOut();
     319                 :            :   void markForDeletion();
     320                 :            : 
     321                 :            :   /** Decrement ref counts of children */
     322                 :            :   inline void decrRefCounts();
     323                 :            : 
     324                 :            :   /** Returns true if the reference count is maximized. */
     325                 :          6 :   inline bool HasMaximizedReferenceCount() { return d_rc == MAX_RC; }
     326                 :            : 
     327                 :            :   nv_iterator nv_begin();
     328                 :            :   nv_iterator nv_end();
     329                 :            : 
     330                 :            :   const_nv_iterator nv_begin() const;
     331                 :            :   const_nv_iterator nv_end() const;
     332                 :            : 
     333                 :            :   /**
     334                 :            :    * Indents the given stream a given amount of spaces.
     335                 :            :    * @param out the stream to indent
     336                 :            :    * @param indent the numer of spaces
     337                 :            :    */
     338                 :          0 :   static inline void indent(std::ostream& out, int indent)
     339                 :            :   {
     340         [ -  - ]:          0 :     for (int i = 0; i < indent; i++)
     341                 :            :     {
     342                 :          0 :       out << ' ';
     343                 :            :     }
     344                 :          0 :   }
     345                 :            : 
     346                 :            :   /** The ID (0 is reserved for the null value) */
     347                 :            :   uint64_t d_id : NBITS_ID;
     348                 :            : 
     349                 :            :   /** The expression's reference count. */
     350                 :            :   uint32_t d_rc : NBITS_REFCOUNT;
     351                 :            : 
     352                 :            :   /** Kind of the expression */
     353                 :            :   uint32_t d_kind : NBITS_KIND;
     354                 :            : 
     355                 :            :   /** Number of children */
     356                 :            :   uint32_t d_nchildren : NBITS_NCHILDREN;
     357                 :            : 
     358                 :            :   /** Associated node manager. */
     359                 :            :   NodeManager* d_nm = nullptr;
     360                 :            : 
     361                 :            :   /** Variable number of child nodes */
     362                 :            :   NodeValue* d_children[0];
     363                 :            : }; /* class NodeValue */
     364                 :            : 
     365                 :            : /**
     366                 :            :  * Provides a symmetric addition operator to that already defined in
     367                 :            :  * the iterator class.
     368                 :            :  */
     369                 :            : NodeValue::iterator<NodeTemplate<true> > operator+(
     370                 :            :     NodeValue::iterator<NodeTemplate<true> >::difference_type p,
     371                 :            :     NodeValue::iterator<NodeTemplate<true> > i);
     372                 :            : 
     373                 :            : /**
     374                 :            :  * Provides a symmetric addition operator to that already defined in
     375                 :            :  * the iterator class.
     376                 :            :  */
     377                 :            : NodeValue::iterator<NodeTemplate<false> > operator+(
     378                 :            :     NodeValue::iterator<NodeTemplate<false> >::difference_type p,
     379                 :            :     NodeValue::iterator<NodeTemplate<false> > i);
     380                 :            : 
     381                 :            : /**
     382                 :            :  * For hash_maps, hash_sets, etc.. but this is for expr package
     383                 :            :  * internal use only at present!  This is likely to be POORLY
     384                 :            :  * PERFORMING for other uses!  NodeValue::poolHash() will lead to
     385                 :            :  * collisions for all VARIABLEs.
     386                 :            :  */
     387                 :            : struct NodeValuePoolHashFunction
     388                 :            : {
     389                 : 1667705280 :   inline size_t operator()(const NodeValue* nv) const
     390                 :            :   {
     391                 : 1667705280 :     return (size_t)nv->poolHash();
     392                 :            :   }
     393                 :            : }; /* struct NodeValuePoolHashFunction */
     394                 :            : 
     395                 :            : /**
     396                 :            :  * For hash_maps, hash_sets, etc.
     397                 :            :  */
     398                 :            : struct NodeValueIDHashFunction
     399                 :            : {
     400                 :  477992307 :   inline size_t operator()(const NodeValue* nv) const
     401                 :            :   {
     402                 :  477992307 :     return (size_t)nv->getId();
     403                 :            :   }
     404                 :            : }; /* struct NodeValueIDHashFunction */
     405                 :            : 
     406                 :            : /**
     407                 :            :  * An equality predicate that is applicable between pointers to fully
     408                 :            :  * constructed NodeValues.
     409                 :            :  */
     410                 :            : struct NodeValueIDEquality
     411                 :            : {
     412                 :  121784454 :   inline bool operator()(const NodeValue* a, const NodeValue* b) const
     413                 :            :   {
     414                 :  121784454 :     return a->getId() == b->getId();
     415                 :            :   }
     416                 :            : };
     417                 :            : 
     418                 :            : std::ostream& operator<<(std::ostream& out, const NodeValue& nv);
     419                 :            : 
     420                 :      29636 : inline NodeValue::NodeValue(int)
     421                 :      29636 :     : d_id(0),
     422                 :      29636 :       d_rc(MAX_RC),
     423                 :      29636 :       d_kind(static_cast<uint32_t>(Kind::NULL_EXPR)),
     424                 :      29636 :       d_nchildren(0)
     425                 :            : {
     426                 :      29636 : }
     427                 :            : 
     428                 :  176339014 : inline void NodeValue::decrRefCounts()
     429                 :            : {
     430         [ +  + ]:  573661730 :   for (nv_iterator i = nv_begin(); i != nv_end(); ++i)
     431                 :            :   {
     432                 :  397322716 :     (*i)->dec();
     433                 :            :   }
     434                 :  176339014 : }
     435                 :            : 
     436                 : 1098097371 : inline NodeValue::nv_iterator NodeValue::nv_begin() { return d_children; }
     437                 :            : 
     438                 : 2437783000 : inline NodeValue::nv_iterator NodeValue::nv_end()
     439                 :            : {
     440                 : 2437783000 :   return d_children + d_nchildren;
     441                 :            : }
     442                 :            : 
     443                 : 2652710952 : inline NodeValue::const_nv_iterator NodeValue::nv_begin() const
     444                 :            : {
     445                 : 2652710952 :   return d_children;
     446                 :            : }
     447                 :            : 
     448                 : 1894755505 : inline NodeValue::const_nv_iterator NodeValue::nv_end() const
     449                 :            : {
     450                 : 1894755505 :   return d_children + d_nchildren;
     451                 :            : }
     452                 :            : 
     453                 :            : template <typename T>
     454                 :  988513610 : inline NodeValue::iterator<T> NodeValue::begin() const
     455                 :            : {
     456                 :  988513610 :   NodeValue* const* firstChild = d_children;
     457         [ +  + ]:  988513610 :   if (getMetaKind() == kind::metakind::PARAMETERIZED)
     458                 :            :   {
     459                 :   77083835 :     ++firstChild;
     460                 :            :   }
     461                 :  988513610 :   return iterator<T>(firstChild);
     462                 :            : }
     463                 :            : 
     464                 :            : template <typename T>
     465                 : 1576590955 : inline NodeValue::iterator<T> NodeValue::end() const
     466                 :            : {
     467                 : 1576590955 :   return iterator<T>(d_children + d_nchildren);
     468                 :            : }
     469                 :            : 
     470                 :          0 : inline NodeValue* NodeValue::getOperator() const
     471                 :            : {
     472                 :          0 :   Assert(getMetaKind() == kind::metakind::PARAMETERIZED);
     473                 :          0 :   return d_children[0];
     474                 :            : }
     475                 :            : 
     476                 : 2841170079 : inline NodeValue* NodeValue::getChild(int i) const
     477                 :            : {
     478         [ +  + ]: 2841170079 :   if (getMetaKind() == kind::metakind::PARAMETERIZED)
     479                 :            :   {
     480                 :  164702281 :     ++i;
     481                 :            :   }
     482                 :            : 
     483 [ +  - ][ +  - ]: 2841170079 :   Assert(i >= 0 && unsigned(i) < d_nchildren);
         [ -  + ][ -  + ]
                 [ -  - ]
     484                 : 2841170079 :   return d_children[i];
     485                 :            : }
     486                 :            : 
     487                 :            : }  // namespace expr
     488                 :            : }  // namespace cvc5::internal
     489                 :            : 
     490                 :            : #endif /* CVC5__EXPR__NODE_VALUE_H */