src/theory/rewriter.h

   1 /*********************                                                        */
   2 /*! \file rewriter.h
   3  ** \verbatim
   4  ** Original author: dejan
   5  ** Major contributors: mdeters
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief The Rewriter class
  15  **
  16  ** The Rewriter class.
  17  **/
  18
  19 #include "cvc4_private.h"
  20
  21 #pragma once
  22
  23 #include "expr/node.h"
  24 #include "expr/attribute.h"
  25
  26 namespace CVC4 {
  27 namespace theory {
  28
  29 /**
  30  * Theory rewriters signal whether more rewriting is needed (or not)
  31  * by using a member of this enumeration.  See RewriteResponse, below.
  32  */
  33 enum RewriteStatus {
  34   REWRITE_DONE,
  35   REWRITE_AGAIN,
  36   REWRITE_AGAIN_FULL
  37 };/* enum RewriteStatus */
  38
  39 /**
  40  * Instances of this class serve as response codes from
  41  * Theory::preRewrite() and Theory::postRewrite().  Instances of
  42  * derived classes RewriteComplete(n), RewriteAgain(n), and
  43  * FullRewriteNeeded(n) should be used, giving self-documenting
  44  * rewrite behavior.
  45  */
  46 struct RewriteResponse {
  47   const RewriteStatus status;
  48   const Node node;
  49   RewriteResponse(RewriteStatus status, Node node) :
  50     status(status), node(node) {}
  51 };/* struct RewriteResponse */
  52
  53 class RewriterInitializer;
  54
  55 /**
  56  * The main rewriter class.  All functionality is static.
  57  */
  58 class Rewriter {
  59
  60   friend class RewriterInitializer;
  61
  62   /** Returns the appropriate cache for a node */
  63   static Node getPreRewriteCache(theory::TheoryId theoryId, TNode node);
  64
  65   /** Returns the appropriate cache for a node */
  66   static Node getPostRewriteCache(theory::TheoryId theoryId, TNode node);
  67
  68   /** Sets the appropriate cache for a node */
  69   static void setPreRewriteCache(theory::TheoryId theoryId,
  70                                  TNode node, TNode cache);
  71
  72   /** Sets the appropriate cache for a node */
  73   static void setPostRewriteCache(theory::TheoryId theoryId,
  74                                   TNode node, TNode cache);
  75
  76   // disable construction of rewriters; all functionality is static
  77   Rewriter() CVC4_UNDEFINED;
  78   Rewriter(const Rewriter&) CVC4_UNDEFINED;
  79
  80   /**
  81    * Rewrites the node using the given theory rewriter.
  82    */
  83   static Node rewriteTo(theory::TheoryId theoryId, Node node);
  84
  85   /** Calls the pre-rewriter for the given theory */
  86   static RewriteResponse callPreRewrite(theory::TheoryId theoryId, TNode node);
  87
  88   /** Calls the post-rewriter for the given theory */
  89   static RewriteResponse callPostRewrite(theory::TheoryId theoryId, TNode node);
  90
  91   /**
  92    * Calls the equality-rewriter for the given theory.
  93    */
  94   static Node callRewriteEquality(theory::TheoryId theoryId, TNode equality);
  95
  96   /**
  97    * Should be called before the rewriter gets used for the first time.
  98    */
  99   static void init();
 100
 101   /**
 102    * Should be called to clean up any state.
 103    */
 104   static void shutdown();
 105
 106 public:
 107
 108   /**
 109    * Rewrites the node using theoryOf() to determine which rewriter to
 110    * use on the node.
 111    */
 112   static Node rewrite(TNode node);
 113
 114 };/* class Rewriter */
 115
 116 }/* CVC4::theory namespace */
 117 }/* CVC4 namespace */