src/theory/rewriter_tables_template.h

   1 /*********************                                                        */
   2 /*! \file rewriter_tables_template.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Dejan Jovanovic, Tim King, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2016 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 Rewriter tables for various theories
  13  **
  14  ** This file contains template code for the rewriter tables that are generated
  15  ** from the Theory kinds files.
  16  **/
  17
  18 #include "cvc4_private.h"
  19
  20 #pragma once
  21
  22 #include "theory/rewriter.h"
  23 #include "theory/rewriter_attributes.h"
  24 #include "expr/attribute_unique_id.h"
  25 #include "expr/attribute.h"
  26
  27 ${rewriter_includes}
  28
  29 namespace CVC4 {
  30 namespace theory {
  31
  32 RewriteResponse Rewriter::callPreRewrite(theory::TheoryId theoryId, TNode node) {
  33   switch(theoryId) {
  34 ${pre_rewrite_calls}
  35   default:
  36     Unreachable();
  37   }
  38 }
  39
  40 RewriteResponse Rewriter::callPostRewrite(theory::TheoryId theoryId, TNode node) {
  41   switch(theoryId) {
  42 ${post_rewrite_calls}
  43   default:
  44     Unreachable();
  45   }
  46 }
  47
  48 Node Rewriter::getPreRewriteCache(theory::TheoryId theoryId, TNode node) {
  49   switch(theoryId) {
  50 ${pre_rewrite_get_cache}
  51   default:
  52     Unreachable();
  53   }
  54 }
  55
  56 Node Rewriter::getPostRewriteCache(theory::TheoryId theoryId, TNode node) {
  57   switch(theoryId) {
  58 ${post_rewrite_get_cache}
  59     default:
  60     Unreachable();
  61   }
  62 }
  63
  64 void Rewriter::setPreRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache) {
  65   switch(theoryId) {
  66 ${pre_rewrite_set_cache}
  67   default:
  68     Unreachable();
  69   }
  70 }
  71
  72 void Rewriter::setPostRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache) {
  73   switch(theoryId) {
  74 ${post_rewrite_set_cache}
  75   default:
  76     Unreachable();
  77   }
  78 }
  79
  80 void Rewriter::init() {
  81 ${rewrite_init}
  82 }
  83
  84 void Rewriter::shutdown() {
  85 ${rewrite_shutdown}
  86 }
  87
  88 void Rewriter::clearCachesInternal() {
  89   typedef CVC4::expr::attr::AttributeUniqueId AttributeUniqueId;
  90   std::vector<AttributeUniqueId> preids;
  91   ${pre_rewrite_attribute_ids}
  92
  93   std::vector<AttributeUniqueId> postids;
  94   ${post_rewrite_attribute_ids}
  95
  96   std::vector<const AttributeUniqueId*> allids;
  97   for(unsigned i = 0; i < preids.size(); ++i){
  98     allids.push_back(&preids[i]);
  99   }
 100   for(unsigned i = 0; i < postids.size(); ++i){
 101     allids.push_back(&postids[i]);
 102   }
 103   NodeManager::currentNM()->deleteAttributes(allids);
 104 }
 105
 106 }/* CVC4::theory namespace */
 107 }/* CVC4 namespace */