src/theory/rewriter_attributes.h

   1 /*********************                                                        */
   2 /*! \file rewriter_attributes.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Dejan Jovanovic, Tim King, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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.\endverbatim
  11  **
  12  ** \brief Rewriter attributes
  13  **
  14  ** Rewriter attributes.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #pragma once
  20
  21 #include "expr/attribute.h"
  22
  23 namespace CVC4 {
  24 namespace theory {
  25
  26 template <bool pre, theory::TheoryId theoryId>
  27 struct RewriteCacheTag {};
  28
  29 template <theory::TheoryId theoryId>
  30 struct RewriteAttibute {
  31
  32   typedef expr::Attribute< RewriteCacheTag<true, theoryId>, Node> pre_rewrite;
  33   typedef expr::Attribute< RewriteCacheTag<false, theoryId>, Node> post_rewrite;
  34
  35   /**
  36    * Get the value of the pre-rewrite cache.
  37    */
  38   static Node getPreRewriteCache(TNode node)
  39   {
  40     Node cache;
  41     if (node.hasAttribute(pre_rewrite())) {
  42       node.getAttribute(pre_rewrite(), cache);
  43     } else {
  44       return Node::null();
  45     }
  46     if (cache.isNull()) {
  47       return node;
  48     } else {
  49       return cache;
  50     }
  51   }
  52
  53   /**
  54    * Set the value of the pre-rewrite cache.
  55    */
  56   static void setPreRewriteCache(TNode node, TNode cache)
  57   {
  58     Trace("rewriter") << "setting pre-rewrite of " << node << " to " << cache << std::endl;
  59     Assert(!cache.isNull());
  60     if (node == cache) {
  61       node.setAttribute(pre_rewrite(), Node::null());
  62     } else {
  63       node.setAttribute(pre_rewrite(), cache);
  64     }
  65   }
  66
  67   /**
  68    * Get the value of the post-rewrite cache.
  69    * none).
  70    */
  71   static Node getPostRewriteCache(TNode node)
  72   {
  73     Node cache;
  74     if (node.hasAttribute(post_rewrite())) {
  75       node.getAttribute(post_rewrite(), cache);
  76     } else {
  77       return Node::null();
  78     }
  79     if (cache.isNull()) {
  80       return node;
  81     } else {
  82       return cache;
  83     }
  84   }
  85
  86   /**
  87    * Set the value of the post-rewrite cache.  v cannot be a null Node.
  88    */
  89   static void setPostRewriteCache(TNode node, TNode cache)
  90   {
  91     Assert(!cache.isNull());
  92     Trace("rewriter") << "setting rewrite of " << node << " to " << cache << std::endl;
  93     if (node == cache) {
  94       node.setAttribute(post_rewrite(), Node::null());
  95     } else {
  96       node.setAttribute(post_rewrite(), cache);
  97     }
  98   }
  99 };/* struct RewriteAttribute */
 100
 101 }/* CVC4::theory namespace */
 102 }/* CVC4 namespace */