GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/theory_rewriter.h Lines: 5 6 83.3 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_rewriter.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andres Noetzli, Andrew Reynolds, 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 The TheoryRewriter class
13
 **
14
 ** The TheoryRewriter class is the interface that theory rewriters implement.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__THEORY_REWRITER_H
20
#define CVC4__THEORY__THEORY_REWRITER_H
21
22
#include "expr/node.h"
23
#include "theory/trust_node.h"
24
25
namespace CVC4 {
26
namespace theory {
27
28
class Rewriter;
29
30
/**
31
 * Theory rewriters signal whether more rewriting is needed (or not)
32
 * by using a member of this enumeration.  See RewriteResponse, below.
33
 */
34
enum RewriteStatus
35
{
36
  /** The node is fully rewritten (no more rewrites apply) */
37
  REWRITE_DONE,
38
  /** The node may be rewritten further */
39
  REWRITE_AGAIN,
40
  /** Subnodes of the node may be rewritten further */
41
  REWRITE_AGAIN_FULL
42
}; /* enum RewriteStatus */
43
44
/**
45
 * Instances of this class serve as response codes from
46
 * TheoryRewriter::preRewrite() and TheoryRewriter::postRewrite(). The response
47
 * consists of the rewritten node as well as a status that indicates whether
48
 * more rewriting is needed or not.
49
 */
50
45809016
struct RewriteResponse
51
{
52
  const RewriteStatus d_status;
53
  const Node d_node;
54
34869336
  RewriteResponse(RewriteStatus status, Node n) : d_status(status), d_node(n) {}
55
}; /* struct RewriteResponse */
56
57
/** Same as above, with trust node instead of node. */
58
694350
struct TrustRewriteResponse
59
{
60
  TrustRewriteResponse(RewriteStatus status,
61
                       Node n,
62
                       Node nr,
63
                       ProofGenerator* pg);
64
  /** The status of the rewrite */
65
  const RewriteStatus d_status;
66
  /**
67
   * The trust node corresponding to the rewrite.
68
   */
69
  TrustNode d_node;
70
};
71
72
/**
73
 * The interface that a theory rewriter has to implement.
74
 *
75
 * Note: A theory rewriter is expected to handle all kinds of a theory, even
76
 * the ones that are removed by `Theory::expandDefinition()` since it may be
77
 * called on terms before the definitions have been expanded.
78
 */
79
117321
class TheoryRewriter
80
{
81
 public:
82
117282
  virtual ~TheoryRewriter() = default;
83
84
  /**
85
   * Registers the rewrites of a given theory with the rewriter.
86
   *
87
   * @param rewriter The rewriter to register the rewrites with.
88
   */
89
  virtual void registerRewrites(Rewriter* rewriter) {}
90
91
  /**
92
   * Performs a pre-rewrite step.
93
   *
94
   * @param node The node to rewrite
95
   */
96
  virtual RewriteResponse postRewrite(TNode node) = 0;
97
98
  /**
99
   * Performs a pre-rewrite step, with proofs.
100
   *
101
   * @param node The node to rewrite
102
   */
103
  virtual TrustRewriteResponse postRewriteWithProof(TNode node);
104
105
  /**
106
   * Performs a post-rewrite step.
107
   *
108
   * @param node The node to rewrite
109
   */
110
  virtual RewriteResponse preRewrite(TNode node) = 0;
111
112
  /**
113
   * Performs a pre-rewrite step, with proofs.
114
   *
115
   * @param node The node to rewrite
116
   */
117
  virtual TrustRewriteResponse preRewriteWithProof(TNode node);
118
119
  /** rewrite equality extended
120
   *
121
   * This method returns a formula that is equivalent to the equality between
122
   * two terms s = t, given by node.
123
   *
124
   * Specifically, this method performs rewrites whose conclusion is not
125
   * necessarily one of { s = t, t = s, true, false }. This is in constrast
126
   * to postRewrite and preRewrite above, where the rewritten form of an
127
   * equality must be one of these.
128
   *
129
   * @param node The node to rewrite
130
   */
131
  virtual Node rewriteEqualityExt(Node node);
132
133
  /** rewrite equality extended, with proofs
134
   *
135
   * @param node The node to rewrite
136
   * @return A trust node of kind TrustNodeKind::REWRITE, or the null trust
137
   * node if no rewrites are applied.
138
   */
139
  virtual TrustNode rewriteEqualityExtWithProof(Node node);
140
};
141
142
}  // namespace theory
143
}  // namespace CVC4
144
145
#endif /* CVC4__THEORY__THEORY_REWRITER_H */