summaryrefslogtreecommitdiff
path: root/src/theory/rewriter_tables_template.h
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2019-12-09 11:19:10 -0800
committerGitHub <noreply@github.com>2019-12-09 11:19:10 -0800
commitb6ce0f23ce0aaa0552767e8067fe58dbceee11cb (patch)
tree0783321580ed511c7ecfa3f59363dadcee15acde /src/theory/rewriter_tables_template.h
parentd06b46efade674023236da228601806daf06f1af (diff)
Make theory rewriters non-static (#3547)
This commit changes theory rewriters to be non-static. This refactoring is needed as a stepping stone to making our rewriter configurable: If we have multiple solver objects with different rewrite configurations, we cannot use `static` variables for the rewriter table in the BV rewriter for example. It is also in line with our goal of getting rid of singletons in general. Note that the `Rewriter` class is still a singleton, which will be changed in a future commit.
Diffstat (limited to 'src/theory/rewriter_tables_template.h')
-rw-r--r--src/theory/rewriter_tables_template.h23
1 files changed, 2 insertions, 21 deletions
diff --git a/src/theory/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h
index 531b62a49..e1be6355b 100644
--- a/src/theory/rewriter_tables_template.h
+++ b/src/theory/rewriter_tables_template.h
@@ -29,22 +29,6 @@ ${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}
@@ -77,14 +61,11 @@ ${post_rewrite_set_cache}
}
}
-void Rewriter::init() {
+Rewriter::Rewriter()
+{
${rewrite_init}
}
-void Rewriter::shutdown() {
-${rewrite_shutdown}
-}
-
void Rewriter::clearCachesInternal() {
typedef CVC4::expr::attr::AttributeUniqueId AttributeUniqueId;
std::vector<AttributeUniqueId> preids;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback