1 /********************* */
2 /*! \file theory_rewriter.h
4 ** Top contributors (to current version):
5 ** Andres Noetzli, Morgan Deters, Andrew Reynolds
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
12 ** \brief The TheoryRewriter class
14 ** The TheoryRewriter class is the interface that theory rewriters implement.
17 #include "cvc4_private.h"
19 #ifndef CVC4__THEORY__THEORY_REWRITER_H
20 #define CVC4__THEORY__THEORY_REWRITER_H
22 #include "expr/node.h"
30 * Theory rewriters signal whether more rewriting is needed (or not)
31 * by using a member of this enumeration. See RewriteResponse, below.
35 /** The node is fully rewritten (no more rewrites apply) */
37 /** The node may be rewritten further */
39 /** Subnodes of the node may be rewritten further */
41 }; /* enum RewriteStatus */
44 * Instances of this class serve as response codes from
45 * TheoryRewriter::preRewrite() and TheoryRewriter::postRewrite(). The response
46 * consists of the rewritten node as well as a status that indicates whether
47 * more rewriting is needed or not.
49 struct RewriteResponse
51 const RewriteStatus d_status
;
53 RewriteResponse(RewriteStatus status
, Node n
) : d_status(status
), d_node(n
) {}
54 }; /* struct RewriteResponse */
57 * The interface that a theory rewriter has to implement.
59 * Note: A theory rewriter is expected to handle all kinds of a theory, even
60 * the ones that are removed by `Theory::expandDefinition()` since it may be
61 * called on terms before the definitions have been expanded.
66 virtual ~TheoryRewriter() = default;
69 * Registers the rewrites of a given theory with the rewriter.
71 * @param rewriter The rewriter to register the rewrites with.
73 virtual void registerRewrites(Rewriter
* rewriter
) {}
76 * Performs a pre-rewrite step.
78 * @param node The node to rewrite
80 virtual RewriteResponse
postRewrite(TNode node
) = 0;
83 * Performs a post-rewrite step.
85 * @param node The node to rewrite
87 virtual RewriteResponse
preRewrite(TNode node
) = 0;
93 #endif /* CVC4__THEORY__THEORY_REWRITER_H */