src/theory/theory_rewriter.h

   1 /*********************                                                        */
   2 /*! \file theory_rewriter.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andres Noetzli, Andrew Reynolds, Morgan Deters
   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 TheoryRewriter class
  13  **
  14  ** The TheoryRewriter class is the interface that theory rewriters implement.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef CVC4__THEORY__THEORY_REWRITER_H
  20 #define CVC4__THEORY__THEORY_REWRITER_H
  21
  22 #include "expr/node.h"
  23 #include "theory/trust_node.h"
  24
  25 namespace CVC4 {
  26 namespace theory {
  27
  28 class Rewriter;
  29
  30 /**
  31  * Theory rewriters signal whether more rewriting is needed (or not)
  32  * by using a member of this enumeration.  See RewriteResponse, below.
  33  */
  34 enum RewriteStatus
  35 {
  36   /** The node is fully rewritten (no more rewrites apply) */
  37   REWRITE_DONE,
  38   /** The node may be rewritten further */
  39   REWRITE_AGAIN,
  40   /** Subnodes of the node may be rewritten further */
  41   REWRITE_AGAIN_FULL
  42 }; /* enum RewriteStatus */
  43
  44 /**
  45  * Instances of this class serve as response codes from
  46  * TheoryRewriter::preRewrite() and TheoryRewriter::postRewrite(). The response
  47  * consists of the rewritten node as well as a status that indicates whether
  48  * more rewriting is needed or not.
  49  */
  50 struct RewriteResponse
  51 {
  52   const RewriteStatus d_status;
  53   const Node d_node;
  54   RewriteResponse(RewriteStatus status, Node n) : d_status(status), d_node(n) {}
  55 }; /* struct RewriteResponse */
  56
  57 /** Same as above, with trust node instead of node. */
  58 struct TrustRewriteResponse
  59 {
  60   TrustRewriteResponse(RewriteStatus status,
  61                        Node n,
  62                        Node nr,
  63                        ProofGenerator* pg);
  64   /** The status of the rewrite */
  65   const RewriteStatus d_status;
  66   /**
  67    * The trust node corresponding to the rewrite.
  68    */
  69   TrustNode d_node;
  70 };
  71
  72 /**
  73  * The interface that a theory rewriter has to implement.
  74  *
  75  * Note: A theory rewriter is expected to handle all kinds of a theory, even
  76  * the ones that are removed by `Theory::expandDefinition()` since it may be
  77  * called on terms before the definitions have been expanded.
  78  */
  79 class TheoryRewriter
  80 {
  81  public:
  82   virtual ~TheoryRewriter() = default;
  83
  84   /**
  85    * Registers the rewrites of a given theory with the rewriter.
  86    *
  87    * @param rewriter The rewriter to register the rewrites with.
  88    */
  89   virtual void registerRewrites(Rewriter* rewriter) {}
  90
  91   /**
  92    * Performs a pre-rewrite step.
  93    *
  94    * @param node The node to rewrite
  95    */
  96   virtual RewriteResponse postRewrite(TNode node) = 0;
  97
  98   /**
  99    * Performs a pre-rewrite step, with proofs.
 100    *
 101    * @param node The node to rewrite
 102    */
 103   virtual TrustRewriteResponse postRewriteWithProof(TNode node);
 104
 105   /**
 106    * Performs a post-rewrite step.
 107    *
 108    * @param node The node to rewrite
 109    */
 110   virtual RewriteResponse preRewrite(TNode node) = 0;
 111
 112   /**
 113    * Performs a pre-rewrite step, with proofs.
 114    *
 115    * @param node The node to rewrite
 116    */
 117   virtual TrustRewriteResponse preRewriteWithProof(TNode node);
 118
 119   /** rewrite equality extended
 120    *
 121    * This method returns a formula that is equivalent to the equality between
 122    * two terms s = t, given by node.
 123    *
 124    * Specifically, this method performs rewrites whose conclusion is not
 125    * necessarily one of { s = t, t = s, true, false }. This is in constrast
 126    * to postRewrite and preRewrite above, where the rewritten form of an
 127    * equality must be one of these.
 128    *
 129    * @param node The node to rewrite
 130    */
 131   virtual Node rewriteEqualityExt(Node node);
 132
 133   /** rewrite equality extended, with proofs
 134    *
 135    * @param node The node to rewrite
 136    * @return A trust node of kind TrustNodeKind::REWRITE, or the null trust
 137    * node if no rewrites are applied.
 138    */
 139   virtual TrustNode rewriteEqualityExtWithProof(Node node);
 140 };
 141
 142 }  // namespace theory
 143 }  // namespace CVC4
 144
 145 #endif /* CVC4__THEORY__THEORY_REWRITER_H */