Branch data     Line data    Source code

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