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                 :            :  * Rewriter attributes.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "cvc5_private.h"
      14                 :            : 
      15                 :            : #pragma once
      16                 :            : 
      17                 :            : #include "expr/attribute.h"
      18                 :            : 
      19                 :            : namespace cvc5::internal {
      20                 :            : namespace theory {
      21                 :            : 
      22                 :            : template <bool pre, theory::TheoryId theoryId>
      23                 :            : struct RewriteCacheTag
      24                 :            : {
      25                 :            : };
      26                 :            : 
      27                 :            : template <theory::TheoryId theoryId>
      28                 :            : struct RewriteAttibute
      29                 :            : {
      30                 :            :   typedef expr::Attribute<RewriteCacheTag<true, theoryId>, Node> pre_rewrite;
      31                 :            :   typedef expr::Attribute<RewriteCacheTag<false, theoryId>, Node> post_rewrite;
      32                 :            : 
      33                 :            :   /**
      34                 :            :    * Get the value of the pre-rewrite cache.
      35                 :            :    */
      36                 :   65987518 :   static Node getPreRewriteCache(TNode node)
      37                 :            :   {
      38                 :   65987518 :     Node cache;
      39         [ +  + ]:   65987518 :     if (node.hasAttribute(pre_rewrite()))
      40                 :            :     {
      41                 :   43690571 :       node.getAttribute(pre_rewrite(), cache);
      42                 :            :     }
      43                 :            :     else
      44                 :            :     {
      45                 :   22296947 :       return Node::null();
      46                 :            :     }
      47         [ +  + ]:   43690571 :     if (cache.isNull())
      48                 :            :     {
      49                 :   33958883 :       return node;
      50                 :            :     }
      51                 :            :     else
      52                 :            :     {
      53                 :    9731688 :       return cache;
      54                 :            :     }
      55                 :   65987518 :   }
      56                 :            : 
      57                 :            :   /**
      58                 :            :    * Set the value of the pre-rewrite cache.
      59                 :            :    */
      60                 :   24133009 :   static void setPreRewriteCache(TNode node, TNode cache)
      61                 :            :   {
      62         [ +  - ]:   24133009 :     Trace("rewriter") << "setting pre-rewrite of " << node << " to " << cache
      63                 :          0 :                       << std::endl;
      64 [ -  + ][ -  + ]:   24133009 :     Assert(!cache.isNull());
                 [ -  - ]
      65         [ +  + ]:   24133009 :     if (node == cache)
      66                 :            :     {
      67                 :   18757954 :       node.setAttribute(pre_rewrite(), Node::null());
      68                 :            :     }
      69                 :            :     else
      70                 :            :     {
      71                 :    5375055 :       node.setAttribute(pre_rewrite(), cache);
      72                 :            :     }
      73                 :   24133009 :   }
      74                 :            : 
      75                 :            :   /**
      76                 :            :    * Get the value of the post-rewrite cache.
      77                 :            :    * none).
      78                 :            :    */
      79                 :  153837027 :   static Node getPostRewriteCache(TNode node)
      80                 :            :   {
      81                 :  153837027 :     Node cache;
      82         [ +  + ]:  153837027 :     if (node.hasAttribute(post_rewrite()))
      83                 :            :     {
      84                 :  118869903 :       node.getAttribute(post_rewrite(), cache);
      85                 :            :     }
      86                 :            :     else
      87                 :            :     {
      88                 :   34967124 :       return Node::null();
      89                 :            :     }
      90         [ +  + ]:  118869903 :     if (cache.isNull())
      91                 :            :     {
      92                 :   87647218 :       return node;
      93                 :            :     }
      94                 :            :     else
      95                 :            :     {
      96                 :   31222685 :       return cache;
      97                 :            :     }
      98                 :  153837027 :   }
      99                 :            : 
     100                 :            :   /**
     101                 :            :    * Set the value of the post-rewrite cache.  v cannot be a null Node.
     102                 :            :    */
     103                 :   65987518 :   static void setPostRewriteCache(TNode node, TNode cache)
     104                 :            :   {
     105 [ -  + ][ -  + ]:   65987518 :     Assert(!cache.isNull());
                 [ -  - ]
     106         [ +  - ]:   65987518 :     Trace("rewriter") << "setting rewrite of " << node << " to " << cache
     107                 :          0 :                       << std::endl;
     108         [ +  + ]:   65987518 :     if (node == cache)
     109                 :            :     {
     110                 :   42442038 :       node.setAttribute(post_rewrite(), Node::null());
     111                 :            :     }
     112                 :            :     else
     113                 :            :     {
     114                 :   23545480 :       node.setAttribute(post_rewrite(), cache);
     115                 :            :     }
     116                 :   65987518 :   }
     117                 :            : }; /* struct RewriteAttribute */
     118                 :            : 
     119                 :            : }  // namespace theory
     120                 :            : }  // namespace cvc5::internal