src/theory/rewriter.h

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