Make theory rewriters non-static (#3547)

This commit changes theory rewriters to be non-static. This refactoring
is needed as a stepping stone to making our rewriter configurable: If we
have multiple solver objects with different rewrite configurations, we
cannot use `static` variables for the rewriter table in the BV rewriter
for example. It is also in line with our goal of getting rid of
  singletons in general. Note that the `Rewriter` class is still a
  singleton, which will be changed in a future commit.

1 files changed, 79 insertions, 0 deletions

diff --git a/src/theory/theory_rewriter.h b/src/theory/theory_rewriter.h
new file mode 100644
index 000000000..b0171813b
--- /dev/null
+++ b/src/theory/theory_rewriter.h
@@ -0,0 +1,79 @@
+/*********************                                                        */
+/*! \file theory_rewriter.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The TheoryRewriter class
+ **
+ ** The TheoryRewriter class is the interface that theory rewriters implement.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__THEORY_REWRITER_H
+#define CVC4__THEORY__THEORY_REWRITER_H
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+
+/**
+ * Theory rewriters signal whether more rewriting is needed (or not)
+ * by using a member of this enumeration.  See RewriteResponse, below.
+ */
+enum RewriteStatus
+{
+  /** The node is fully rewritten (no more rewrites apply) */
+  REWRITE_DONE,
+  /** The node may be rewritten further */
+  REWRITE_AGAIN,
+  /** Subnodes of the node may be rewritten further */
+  REWRITE_AGAIN_FULL
+}; /* enum RewriteStatus */
+
+/**
+ * Instances of this class serve as response codes from
+ * TheoryRewriter::preRewrite() and TheoryRewriter::postRewrite(). The response
+ * consists of the rewritten node as well as a status that indicates whether
+ * more rewriting is needed or not.
+ */
+struct RewriteResponse
+{
+  const RewriteStatus status;
+  const Node node;
+  RewriteResponse(RewriteStatus status, Node node) : status(status), node(node)
+  {
+  }
+}; /* struct RewriteResponse */
+
+class TheoryRewriter
+{
+ public:
+  virtual ~TheoryRewriter() = default;
+
+  /**
+   * Performs a pre-rewrite step.
+   *
+   * @param node The node to rewrite
+   */
+  virtual RewriteResponse postRewrite(TNode node) = 0;
+
+  /**
+   * Performs a post-rewrite step.
+   *
+   * @param node The node to rewrite
+   */
+  virtual RewriteResponse preRewrite(TNode node) = 0;
+};
+
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__THEORY_REWRITER_H */