Add new interfaces to term formula removal and theory preprocess (#5717)

[cvc5.git] / src / theory / rewriter_tables_template.h

diff --git a/src/theory/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h
index e26c879e47d7ea66e5ee31f6401643f70df17f2f..4e350dca95377063cf57b8c93020252358cd77d3 100644 (file)
--- a/src/theory/rewriter_tables_template.h
+++ b/src/theory/rewriter_tables_template.h
@@ -1,29 +1,34 @@
+/*********************                                                        */
+/*! \file rewriter_tables_template.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Dejan Jovanovic, Tim King, Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Rewriter tables for various theories
+ **
+ ** This file contains template code for the rewriter tables that are generated
+ ** from the Theory kinds files.
+ **/
+
+#include "cvc4_private.h"
+
 #pragma once
 
 #include "theory/rewriter.h"
 #include "theory/rewriter_attributes.h"
+#include "expr/attribute_unique_id.h"
+#include "expr/attribute.h"
 
 ${rewriter_includes}
 
 namespace CVC4 {
 namespace theory {
 
-RewriteResponse Rewriter::callPreRewrite(theory::TheoryId theoryId, TNode node) {
-  switch(theoryId) {
-${pre_rewrite_calls}
-  default:
-    Unreachable();
-  }
-}
-
-RewriteResponse Rewriter::callPostRewrite(theory::TheoryId theoryId, TNode node) {
-  switch(theoryId) {
-${post_rewrite_calls}
-  default:
-    Unreachable();
-  }
-}
-
 Node Rewriter::getPreRewriteCache(theory::TheoryId theoryId, TNode node) {
   switch(theoryId) {
 ${pre_rewrite_get_cache}
@@ -56,14 +61,38 @@ ${post_rewrite_set_cache}
   }
 }
 
-
-void Rewriter::init() {
-${rewrite_init}
+Rewriter::Rewriter() : d_tpg(nullptr)
+{
+for (size_t i = 0; i < kind::LAST_KIND; ++i)
+{
+  d_preRewriters[i] = nullptr;
+  d_postRewriters[i] = nullptr;
 }
 
-void Rewriter::shutdown() {
-${rewrite_shutdown}
+for (size_t i = 0; i < theory::THEORY_LAST; ++i)
+{
+  d_preRewritersEqual[i] = nullptr;
+  d_postRewritersEqual[i] = nullptr;
 }
-
 }
+
+void Rewriter::clearCachesInternal() {
+  typedef CVC4::expr::attr::AttributeUniqueId AttributeUniqueId;
+  std::vector<AttributeUniqueId> preids;
+  ${pre_rewrite_attribute_ids}
+
+  std::vector<AttributeUniqueId> postids;
+  ${post_rewrite_attribute_ids}
+
+  std::vector<const AttributeUniqueId*> allids;
+  for(unsigned i = 0; i < preids.size(); ++i){
+    allids.push_back(&preids[i]);
+  }
+  for(unsigned i = 0; i < postids.size(); ++i){
+    allids.push_back(&postids[i]);
+  }
+  NodeManager::currentNM()->deleteAttributes(allids);
 }
+
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */