GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/rewriter_attributes.h Lines: 30 30 100.0 %
Date: 2021-03-23 Branches: 616 1404 43.9 %

Line Exec Source
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-2021 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
39298505
  static Node getPreRewriteCache(TNode node)
39
  {
40
78597010
    Node cache;
41
39298505
    if (node.hasAttribute(pre_rewrite())) {
42
27683675
      node.getAttribute(pre_rewrite(), cache);
43
    } else {
44
11614830
      return Node::null();
45
    }
46
27683675
    if (cache.isNull()) {
47
23268093
      return node;
48
    } else {
49
4415582
      return cache;
50
    }
51
  }
52
53
  /**
54
   * Set the value of the pre-rewrite cache.
55
   */
56
11959781
  static void setPreRewriteCache(TNode node, TNode cache)
57
  {
58
11959781
    Trace("rewriter") << "setting pre-rewrite of " << node << " to " << cache << std::endl;
59
11959781
    Assert(!cache.isNull());
60
11959781
    if (node == cache) {
61
9843587
      node.setAttribute(pre_rewrite(), Node::null());
62
    } else {
63
2116194
      node.setAttribute(pre_rewrite(), cache);
64
    }
65
11959781
  }
66
67
  /**
68
   * Get the value of the post-rewrite cache.
69
   * none).
70
   */
71
104183318
  static Node getPostRewriteCache(TNode node)
72
  {
73
208366636
    Node cache;
74
104183318
    if (node.hasAttribute(post_rewrite())) {
75
54769581
      node.getAttribute(post_rewrite(), cache);
76
    } else {
77
49413737
      return Node::null();
78
    }
79
54769581
    if (cache.isNull()) {
80
44171794
      return node;
81
    } else {
82
10597787
      return cache;
83
    }
84
  }
85
86
  /**
87
   * Set the value of the post-rewrite cache.  v cannot be a null Node.
88
   */
89
11054629
  static void setPostRewriteCache(TNode node, TNode cache)
90
  {
91
11054629
    Assert(!cache.isNull());
92
11054629
    Trace("rewriter") << "setting rewrite of " << node << " to " << cache << std::endl;
93
11054629
    if (node == cache) {
94
5602364
      node.setAttribute(post_rewrite(), Node::null());
95
    } else {
96
5452265
      node.setAttribute(post_rewrite(), cache);
97
    }
98
11054629
  }
99
};/* struct RewriteAttribute */
100
101
}/* CVC4::theory namespace */
102
}/* CVC4 namespace */