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, Andres Noetzli
   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 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 Node Rewriter::getPreRewriteCache(theory::TheoryId theoryId, TNode node) {
  33   switch(theoryId) {
  34 ${pre_rewrite_get_cache}
  35   default:
  36     Unreachable();
  37   }
  38 }
  39
  40 Node Rewriter::getPostRewriteCache(theory::TheoryId theoryId, TNode node) {
  41   switch(theoryId) {
  42 ${post_rewrite_get_cache}
  43     default:
  44     Unreachable();
  45   }
  46 }
  47
  48 void Rewriter::setPreRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache) {
  49   switch(theoryId) {
  50 ${pre_rewrite_set_cache}
  51   default:
  52     Unreachable();
  53   }
  54 }
  55
  56 void Rewriter::setPostRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache) {
  57   switch(theoryId) {
  58 ${post_rewrite_set_cache}
  59   default:
  60     Unreachable();
  61   }
  62 }
  63
  64 Rewriter::Rewriter() : d_tpg(nullptr)
  65 {
  66 for (size_t i = 0; i < kind::LAST_KIND; ++i)
  67 {
  68   d_preRewriters[i] = nullptr;
  69   d_postRewriters[i] = nullptr;
  70 }
  71
  72 for (size_t i = 0; i < theory::THEORY_LAST; ++i)
  73 {
  74   d_preRewritersEqual[i] = nullptr;
  75   d_postRewritersEqual[i] = nullptr;
  76 }
  77 }
  78
  79 void Rewriter::clearCachesInternal() {
  80   typedef CVC4::expr::attr::AttributeUniqueId AttributeUniqueId;
  81   std::vector<AttributeUniqueId> preids;
  82   ${pre_rewrite_attribute_ids}
  83
  84   std::vector<AttributeUniqueId> postids;
  85   ${post_rewrite_attribute_ids}
  86
  87   std::vector<const AttributeUniqueId*> allids;
  88   for(unsigned i = 0; i < preids.size(); ++i){
  89     allids.push_back(&preids[i]);
  90   }
  91   for(unsigned i = 0; i < postids.size(); ++i){
  92     allids.push_back(&postids[i]);
  93   }
  94   NodeManager::currentNM()->deleteAttributes(allids);
  95 }
  96
  97 }/* CVC4::theory namespace */
  98 }/* CVC4 namespace */