1 /********************* */
4 ** Top contributors (to current version):
5 ** Morgan Deters, Dejan Jovanovic, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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 Rewriter class
14 ** The Rewriter class.
17 #include "cvc4_private.h"
21 #include "expr/node.h"
22 #include "theory/theory_rewriter.h"
23 #include "util/unsafe_interrupt_exception.h"
28 class RewriterInitializer
;
31 * The main rewriter class.
38 * Rewrites the node using theoryOf() to determine which rewriter to
41 static Node
rewrite(TNode node
);
44 * Garbage collects the rewrite caches.
46 static void clearCaches();
50 * Get the (singleton) instance of the rewriter.
52 * TODO(#3468): Get rid of this singleton
54 static Rewriter
& getInstance();
56 /** Returns the appropriate cache for a node */
57 Node
getPreRewriteCache(theory::TheoryId theoryId
, TNode node
);
59 /** Returns the appropriate cache for a node */
60 Node
getPostRewriteCache(theory::TheoryId theoryId
, TNode node
);
62 /** Sets the appropriate cache for a node */
63 void setPreRewriteCache(theory::TheoryId theoryId
, TNode node
, TNode cache
);
65 /** Sets the appropriate cache for a node */
66 void setPostRewriteCache(theory::TheoryId theoryId
, TNode node
, TNode cache
);
69 * Rewrites the node using the given theory rewriter.
71 Node
rewriteTo(theory::TheoryId theoryId
, Node node
);
73 /** Calls the pre-rewriter for the given theory */
74 RewriteResponse
callPreRewrite(theory::TheoryId theoryId
, TNode node
);
76 /** Calls the post-rewriter for the given theory */
77 RewriteResponse
callPostRewrite(theory::TheoryId theoryId
, TNode node
);
80 * Calls the equality-rewriter for the given theory.
82 Node
callRewriteEquality(theory::TheoryId theoryId
, TNode equality
);
84 void clearCachesInternal();
86 /** Theory rewriters managed by this rewriter instance */
87 std::unique_ptr
<TheoryRewriter
> d_theoryRewriters
[theory::THEORY_LAST
];
89 unsigned long d_iterationCount
= 0;
91 #ifdef CVC4_ASSERTIONS
92 std::unique_ptr
<std::unordered_set
<Node
, NodeHashFunction
>> d_rewriteStack
=
94 #endif /* CVC4_ASSERTIONS */
95 };/* class Rewriter */
97 }/* CVC4::theory namespace */