src/theory/rewriter.h

   1 /*********************                                                        */
   2 /*! \file rewriter.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andres Noetzli, Andrew Reynolds, Dejan Jovanovic
   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
  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 "expr/term_conversion_proof_generator.h"
  23 #include "theory/theory_rewriter.h"
  24 #include "theory/trust_node.h"
  25 #include "util/unsafe_interrupt_exception.h"
  26
  27 namespace CVC4 {
  28 namespace theory {
  29
  30 namespace builtin {
  31 class BuiltinProofRuleChecker;
  32 }
  33
  34 class RewriterInitializer;
  35
  36 /**
  37  * The rewrite environment holds everything that the individual rewrites have
  38  * access to.
  39  */
  40 class RewriteEnvironment
  41 {
  42 };
  43
  44 /**
  45  * The identity rewrite just returns the original node.
  46  *
  47  * @param re The rewrite environment
  48  * @param n The node to rewrite
  49  * @return The original node
  50  */
  51 RewriteResponse identityRewrite(RewriteEnvironment* re, TNode n);
  52
  53 /**
  54  * The main rewriter class.
  55  */
  56 class Rewriter {
  57   friend builtin::BuiltinProofRuleChecker;
  58
  59  public:
  60   Rewriter();
  61
  62   /**
  63    * Rewrites the node using theoryOf() to determine which rewriter to
  64    * use on the node.
  65    */
  66   static Node rewrite(TNode node);
  67
  68   /**
  69    * Rewrites the equality node using theoryOf() to determine which rewriter to
  70    * use on the node corresponding to an equality s = t.
  71    *
  72    * Specifically, this method performs rewrites whose conclusion is not
  73    * necessarily one of { s = t, t = s, true, false }, which is an invariant
  74    * guaranted by the above method. This invariant is motivated by theory
  75    * combination, which needs to guarantee that equalities between terms
  76    * can be communicated for all pairs of terms.
  77    */
  78   static Node rewriteEqualityExt(TNode node);
  79
  80   /**
  81    * Rewrite with proof production, which is managed by the term conversion
  82    * proof generator managed by this class (d_tpg). This method requires a call
  83    * to setProofNodeManager prior to this call.
  84    *
  85    * @param node The node to rewrite.
  86    * @param elimTheoryRewrite Whether we also want fine-grained proofs for
  87    * THEORY_REWRITE steps.
  88    * @param isExtEq Whether node is an equality which we are applying
  89    * rewriteEqualityExt on.
  90    * @return The trust node of kind TrustNodeKind::REWRITE that contains the
  91    * rewritten form of node.
  92    */
  93   TrustNode rewriteWithProof(TNode node,
  94                              bool elimTheoryRewrite = false,
  95                              bool isExtEq = false);
  96
  97   /** Set proof node manager */
  98   void setProofNodeManager(ProofNodeManager* pnm);
  99
 100   /**
 101    * Garbage collects the rewrite caches.
 102    */
 103   static void clearCaches();
 104
 105   /**
 106    * Registers a theory rewriter with this rewriter. The rewriter does not own
 107    * the theory rewriters.
 108    *
 109    * @param tid The theory that the theory rewriter should be associated with.
 110    * @param trew The theory rewriter to register.
 111    */
 112   static void registerTheoryRewriter(theory::TheoryId tid,
 113                                      TheoryRewriter* trew);
 114
 115   /**
 116    * Register a prerewrite for a given kind.
 117    *
 118    * @param k The kind to register a rewrite for.
 119    * @param fn The function that performs the rewrite.
 120    */
 121   void registerPreRewrite(
 122       Kind k, std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn);
 123
 124   /**
 125    * Register a postrewrite for a given kind.
 126    *
 127    * @param k The kind to register a rewrite for.
 128    * @param fn The function that performs the rewrite.
 129    */
 130   void registerPostRewrite(
 131       Kind k, std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn);
 132
 133   /**
 134    * Register a prerewrite for equalities belonging to a given theory.
 135    *
 136    * @param tid The theory to register a rewrite for.
 137    * @param fn The function that performs the rewrite.
 138    */
 139   void registerPreRewriteEqual(
 140       theory::TheoryId tid,
 141       std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn);
 142
 143   /**
 144    * Register a postrewrite for equalities belonging to a given theory.
 145    *
 146    * @param tid The theory to register a rewrite for.
 147    * @param fn The function that performs the rewrite.
 148    */
 149   void registerPostRewriteEqual(
 150       theory::TheoryId tid,
 151       std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn);
 152
 153  private:
 154   /**
 155    * Get the rewriter associated with the SmtEngine in scope.
 156    *
 157    * TODO(#3468): Get rid of this function (it relies on there being an
 158    * singleton with the current SmtEngine in scope)
 159    */
 160   static Rewriter* getInstance();
 161
 162   /** Returns the appropriate cache for a node */
 163   Node getPreRewriteCache(theory::TheoryId theoryId, TNode node);
 164
 165   /** Returns the appropriate cache for a node */
 166   Node getPostRewriteCache(theory::TheoryId theoryId, TNode node);
 167
 168   /** Sets the appropriate cache for a node */
 169   void setPreRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache);
 170
 171   /** Sets the appropriate cache for a node */
 172   void setPostRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache);
 173
 174   /**
 175    * Rewrites the node using the given theory rewriter.
 176    */
 177   Node rewriteTo(theory::TheoryId theoryId,
 178                  Node node,
 179                  TConvProofGenerator* tcpg = nullptr);
 180
 181   /** Calls the pre-rewriter for the given theory */
 182   RewriteResponse preRewrite(theory::TheoryId theoryId,
 183                              TNode n,
 184                              TConvProofGenerator* tcpg = nullptr);
 185
 186   /** Calls the post-rewriter for the given theory */
 187   RewriteResponse postRewrite(theory::TheoryId theoryId,
 188                               TNode n,
 189                               TConvProofGenerator* tcpg = nullptr);
 190   /** processes a trust rewrite response */
 191   RewriteResponse processTrustRewriteResponse(
 192       theory::TheoryId theoryId,
 193       const TrustRewriteResponse& tresponse,
 194       bool isPre,
 195       TConvProofGenerator* tcpg);
 196
 197   /**
 198    * Calls the equality-rewriter for the given theory.
 199    */
 200   Node callRewriteEquality(theory::TheoryId theoryId, TNode equality);
 201
 202   void clearCachesInternal();
 203
 204   /** Theory rewriters used by this rewriter instance */
 205   TheoryRewriter* d_theoryRewriters[theory::THEORY_LAST];
 206
 207   unsigned long d_iterationCount = 0;
 208
 209   /** Rewriter table for prewrites. Maps kinds to rewriter function. */
 210   std::function<RewriteResponse(RewriteEnvironment*, TNode)>
 211       d_preRewriters[kind::LAST_KIND];
 212   /** Rewriter table for postrewrites. Maps kinds to rewriter function. */
 213   std::function<RewriteResponse(RewriteEnvironment*, TNode)>
 214       d_postRewriters[kind::LAST_KIND];
 215   /**
 216    * Rewriter table for prerewrites of equalities. Maps theory to rewriter
 217    * function.
 218    */
 219   std::function<RewriteResponse(RewriteEnvironment*, TNode)>
 220       d_preRewritersEqual[theory::THEORY_LAST];
 221   /**
 222    * Rewriter table for postrewrites of equalities. Maps theory to rewriter
 223    * function.
 224    */
 225   std::function<RewriteResponse(RewriteEnvironment*, TNode)>
 226       d_postRewritersEqual[theory::THEORY_LAST];
 227
 228   RewriteEnvironment d_re;
 229
 230   /** The proof generator */
 231   std::unique_ptr<TConvProofGenerator> d_tpg;
 232 #ifdef CVC4_ASSERTIONS
 233   std::unique_ptr<std::unordered_set<Node, NodeHashFunction>> d_rewriteStack =
 234       nullptr;
 235 #endif /* CVC4_ASSERTIONS */
 236 };/* class Rewriter */
 237
 238 }/* CVC4::theory namespace */
 239 }/* CVC4 namespace */