src/theory/rewriter.h

   1 /*********************                                                        */
   2 /*! \file rewriter.h
   3  ** \verbatim
   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
  11  **
  12  ** \brief The Rewriter class
  13  **
  14  ** The Rewriter class.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #pragma once
  20
  21 #include "expr/node.h"
  22 #include "theory/theory_rewriter.h"
  23 #include "util/unsafe_interrupt_exception.h"
  24
  25 namespace CVC4 {
  26 namespace theory {
  27
  28 class RewriterInitializer;
  29
  30 /**
  31  * The rewrite environment holds everything that the individual rewrites have
  32  * access to.
  33  */
  34 class RewriteEnvironment
  35 {
  36 };
  37
  38 /**
  39  * The identity rewrite just returns the original node.
  40  *
  41  * @param re The rewrite environment
  42  * @param n The node to rewrite
  43  * @return The original node
  44  */
  45 RewriteResponse identityRewrite(RewriteEnvironment* re, TNode n);
  46
  47 /**
  48  * The main rewriter class.
  49  */
  50 class Rewriter {
  51  public:
  52   Rewriter();
  53
  54   /**
  55    * Rewrites the node using theoryOf() to determine which rewriter to
  56    * use on the node.
  57    */
  58   static Node rewrite(TNode node);
  59
  60   /**
  61    * Garbage collects the rewrite caches.
  62    */
  63   static void clearCaches();
  64
  65   /**
  66    * Registers a theory rewriter with this rewriter. The rewriter does not own
  67    * the theory rewriters.
  68    *
  69    * @param tid The theory that the theory rewriter should be associated with.
  70    * @param trew The theory rewriter to register.
  71    */
  72   static void registerTheoryRewriter(theory::TheoryId tid,
  73                                      TheoryRewriter* trew);
  74
  75   /**
  76    * Register a prerewrite for a given kind.
  77    *
  78    * @param k The kind to register a rewrite for.
  79    * @param fn The function that performs the rewrite.
  80    */
  81   void registerPreRewrite(
  82       Kind k, std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn);
  83
  84   /**
  85    * Register a postrewrite for a given kind.
  86    *
  87    * @param k The kind to register a rewrite for.
  88    * @param fn The function that performs the rewrite.
  89    */
  90   void registerPostRewrite(
  91       Kind k, std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn);
  92
  93   /**
  94    * Register a prerewrite for equalities belonging to a given theory.
  95    *
  96    * @param tid The theory to register a rewrite for.
  97    * @param fn The function that performs the rewrite.
  98    */
  99   void registerPreRewriteEqual(
 100       theory::TheoryId tid,
 101       std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn);
 102
 103   /**
 104    * Register a postrewrite for equalities belonging to a given theory.
 105    *
 106    * @param tid The theory to register a rewrite for.
 107    * @param fn The function that performs the rewrite.
 108    */
 109   void registerPostRewriteEqual(
 110       theory::TheoryId tid,
 111       std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn);
 112
 113  private:
 114   /**
 115    * Get the rewriter associated with the SmtEngine in scope.
 116    *
 117    * TODO(#3468): Get rid of this function (it relies on there being an
 118    * singleton with the current SmtEngine in scope)
 119    */
 120   static Rewriter* getInstance();
 121
 122   /** Returns the appropriate cache for a node */
 123   Node getPreRewriteCache(theory::TheoryId theoryId, TNode node);
 124
 125   /** Returns the appropriate cache for a node */
 126   Node getPostRewriteCache(theory::TheoryId theoryId, TNode node);
 127
 128   /** Sets the appropriate cache for a node */
 129   void setPreRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache);
 130
 131   /** Sets the appropriate cache for a node */
 132   void setPostRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache);
 133
 134   /**
 135    * Rewrites the node using the given theory rewriter.
 136    */
 137   Node rewriteTo(theory::TheoryId theoryId, Node node);
 138
 139   /** Calls the pre-rewriter for the given theory */
 140   RewriteResponse preRewrite(theory::TheoryId theoryId, TNode n);
 141
 142   /** Calls the post-rewriter for the given theory */
 143   RewriteResponse postRewrite(theory::TheoryId theoryId, TNode n);
 144
 145   /**
 146    * Calls the equality-rewriter for the given theory.
 147    */
 148   Node callRewriteEquality(theory::TheoryId theoryId, TNode equality);
 149
 150   void clearCachesInternal();
 151
 152   /** Theory rewriters used by this rewriter instance */
 153   TheoryRewriter* d_theoryRewriters[theory::THEORY_LAST];
 154
 155   unsigned long d_iterationCount = 0;
 156
 157   /** Rewriter table for prewrites. Maps kinds to rewriter function. */
 158   std::function<RewriteResponse(RewriteEnvironment*, TNode)>
 159       d_preRewriters[kind::LAST_KIND];
 160   /** Rewriter table for postrewrites. Maps kinds to rewriter function. */
 161   std::function<RewriteResponse(RewriteEnvironment*, TNode)>
 162       d_postRewriters[kind::LAST_KIND];
 163   /**
 164    * Rewriter table for prerewrites of equalities. Maps theory to rewriter
 165    * function.
 166    */
 167   std::function<RewriteResponse(RewriteEnvironment*, TNode)>
 168       d_preRewritersEqual[theory::THEORY_LAST];
 169   /**
 170    * Rewriter table for postrewrites of equalities. Maps theory to rewriter
 171    * function.
 172    */
 173   std::function<RewriteResponse(RewriteEnvironment*, TNode)>
 174       d_postRewritersEqual[theory::THEORY_LAST];
 175
 176   RewriteEnvironment d_re;
 177
 178 #ifdef CVC4_ASSERTIONS
 179   std::unique_ptr<std::unordered_set<Node, NodeHashFunction>> d_rewriteStack =
 180       nullptr;
 181 #endif /* CVC4_ASSERTIONS */
 182 };/* class Rewriter */
 183
 184 }/* CVC4::theory namespace */
 185 }/* CVC4 namespace */