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, 2010, 2011  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 /**
  54  * The main rewriter class.  All functionality is static.
  55  */
  56 class Rewriter {
  57
  58   /** Returns the appropriate cache for a node */
  59   static Node getPreRewriteCache(theory::TheoryId theoryId, TNode node);
  60
  61   /** Returns the appropriate cache for a node */
  62   static Node getPostRewriteCache(theory::TheoryId theoryId, TNode node);
  63
  64   /** Sets the appropriate cache for a node */
  65   static void setPreRewriteCache(theory::TheoryId theoryId,
  66                                  TNode node, TNode cache);
  67
  68   /** Sets the appropriate cache for a node */
  69   static void setPostRewriteCache(theory::TheoryId theoryId,
  70                                   TNode node, TNode cache);
  71
  72   // disable construction of rewriters; all functionality is static
  73   Rewriter() CVC4_UNUSED;
  74   Rewriter(const Rewriter&) CVC4_UNUSED;
  75
  76   /**
  77    * Rewrites the node using the given theory rewriter.
  78    */
  79   static Node rewriteTo(theory::TheoryId theoryId, Node node);
  80
  81   /** Calls the pre-rewriter for the given theory */
  82   static RewriteResponse callPreRewrite(theory::TheoryId theoryId, TNode node);
  83
  84   /** Calls the post-rewriter for the given theory */
  85   static RewriteResponse callPostRewrite(theory::TheoryId theoryId, TNode node);
  86
  87   /**
  88    * Calls the equality-rewriter for the given theory.
  89    */
  90   static Node callRewriteEquality(theory::TheoryId theoryId, TNode equality);
  91
  92 public:
  93
  94
  95   /**
  96    * Rewrites the node using theoryOf() to determine which rewriter to
  97    * use on the node.
  98    */
  99   static Node rewrite(TNode node);
 100
 101   /**
 102    * Should be called before the rewriter gets used for the first time.
 103    */
 104   static void init();
 105
 106   /**
 107    * Should be called to clean up any state.
 108    */
 109   static void shutdown();
 110
 111
 112 };/* class Rewriter */
 113
 114 }/* CVC4::theory namespace */
 115 }/* CVC4 namespace */