GCC Code Coverage Report
Directory: . Exec Total Coverage
File: build-coverage/src/theory/rewriter_tables.h Lines: 68 112 60.7 %
Date: 2021-03-22 Branches: 142 356 39.9 %

Line Exec Source
1
/*********************                                                        */
2
/** rewriter_tables.h
3
 **
4
 ** Copyright 2010-2014  New York University and The University of Iowa,
5
 ** and as below.
6
 **
7
 ** This header file automatically generated by:
8
 **
9
 **     ../../../src/theory/mkrewriter /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-22/src/theory/rewriter_tables_template.h /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-22/src/theory/builtin/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-22/src/theory/booleans/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-22/src/theory/uf/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-22/src/theory/arith/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-22/src/theory/bv/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-22/src/theory/fp/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-22/src/theory/arrays/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-22/src/theory/datatypes/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-22/src/theory/sep/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-22/src/theory/sets/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-22/src/theory/bags/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-22/src/theory/strings/kinds /barrett/scratch/cvc4-nightly/src/cvc4-2021-03-22/src/theory/quantifiers/kinds
10
 **
11
 ** for the CVC4 project.
12
 **/
13
14
/*********************                                                        */
15
/*! \file rewriter_tables_template.h
16
 ** \verbatim
17
 ** Top contributors (to current version):
18
 **   Dejan Jovanovic, Tim King, Andres Noetzli
19
 ** This file is part of the CVC4 project.
20
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
21
 ** in the top-level source directory and their institutional affiliations.
22
 ** All rights reserved.  See the file COPYING in the top-level source
23
 ** directory for licensing information.\endverbatim
24
 **
25
 ** \brief Rewriter tables for various theories
26
 **
27
 ** This file contains template code for the rewriter tables that are generated
28
 ** from the Theory kinds files.
29
 **/
30
31
#include "cvc4_private.h"
32
33
#pragma once
34
35
#include "theory/rewriter.h"
36
#include "theory/rewriter_attributes.h"
37
#include "expr/attribute_unique_id.h"
38
#include "expr/attribute.h"
39
40
#include "theory/builtin/theory_builtin_rewriter.h"
41
#include "theory/booleans/theory_bool_rewriter.h"
42
#include "theory/uf/theory_uf_rewriter.h"
43
#include "theory/arith/arith_rewriter.h"
44
#include "theory/bv/theory_bv_rewriter.h"
45
#include "theory/fp/theory_fp_rewriter.h"
46
#include "theory/arrays/theory_arrays_rewriter.h"
47
#include "theory/datatypes/datatypes_rewriter.h"
48
#include "theory/sep/theory_sep_rewriter.h"
49
#include "theory/sets/theory_sets_rewriter.h"
50
#include "theory/bags/bags_rewriter.h"
51
#include "theory/strings/sequences_rewriter.h"
52
#include "theory/quantifiers/quantifiers_rewriter.h"
53
54
55
namespace CVC4 {
56
namespace theory {
57
58
39283163
Node Rewriter::getPreRewriteCache(theory::TheoryId theoryId, TNode node) {
59
39283163
  switch(theoryId) {
60
6182921
    case THEORY_BUILTIN: return RewriteAttibute<THEORY_BUILTIN>::getPreRewriteCache(node);
61
14447438
    case THEORY_BOOL: return RewriteAttibute<THEORY_BOOL>::getPreRewriteCache(node);
62
1169570
    case THEORY_UF: return RewriteAttibute<THEORY_UF>::getPreRewriteCache(node);
63
9132006
    case THEORY_ARITH: return RewriteAttibute<THEORY_ARITH>::getPreRewriteCache(node);
64
5599925
    case THEORY_BV: return RewriteAttibute<THEORY_BV>::getPreRewriteCache(node);
65
21641
    case THEORY_FP: return RewriteAttibute<THEORY_FP>::getPreRewriteCache(node);
66
104133
    case THEORY_ARRAYS: return RewriteAttibute<THEORY_ARRAYS>::getPreRewriteCache(node);
67
928716
    case THEORY_DATATYPES: return RewriteAttibute<THEORY_DATATYPES>::getPreRewriteCache(node);
68
5088
    case THEORY_SEP: return RewriteAttibute<THEORY_SEP>::getPreRewriteCache(node);
69
141360
    case THEORY_SETS: return RewriteAttibute<THEORY_SETS>::getPreRewriteCache(node);
70
6895
    case THEORY_BAGS: return RewriteAttibute<THEORY_BAGS>::getPreRewriteCache(node);
71
1256246
    case THEORY_STRINGS: return RewriteAttibute<THEORY_STRINGS>::getPreRewriteCache(node);
72
287224
    case THEORY_QUANTIFIERS: return RewriteAttibute<THEORY_QUANTIFIERS>::getPreRewriteCache(node);
73
74
  default:
75
    Unreachable();
76
  }
77
}
78
79
104142284
Node Rewriter::getPostRewriteCache(theory::TheoryId theoryId, TNode node) {
80
104142284
  switch(theoryId) {
81
6252054
    case THEORY_BUILTIN: return RewriteAttibute<THEORY_BUILTIN>::getPostRewriteCache(node);
82
42831848
    case THEORY_BOOL: return RewriteAttibute<THEORY_BOOL>::getPostRewriteCache(node);
83
8613791
    case THEORY_UF: return RewriteAttibute<THEORY_UF>::getPostRewriteCache(node);
84
26204674
    case THEORY_ARITH: return RewriteAttibute<THEORY_ARITH>::getPostRewriteCache(node);
85
10774278
    case THEORY_BV: return RewriteAttibute<THEORY_BV>::getPostRewriteCache(node);
86
46717
    case THEORY_FP: return RewriteAttibute<THEORY_FP>::getPostRewriteCache(node);
87
269820
    case THEORY_ARRAYS: return RewriteAttibute<THEORY_ARRAYS>::getPostRewriteCache(node);
88
3409550
    case THEORY_DATATYPES: return RewriteAttibute<THEORY_DATATYPES>::getPostRewriteCache(node);
89
16083
    case THEORY_SEP: return RewriteAttibute<THEORY_SEP>::getPostRewriteCache(node);
90
529370
    case THEORY_SETS: return RewriteAttibute<THEORY_SETS>::getPostRewriteCache(node);
91
13546
    case THEORY_BAGS: return RewriteAttibute<THEORY_BAGS>::getPostRewriteCache(node);
92
4326856
    case THEORY_STRINGS: return RewriteAttibute<THEORY_STRINGS>::getPostRewriteCache(node);
93
853697
    case THEORY_QUANTIFIERS: return RewriteAttibute<THEORY_QUANTIFIERS>::getPostRewriteCache(node);
94
95
    default:
96
    Unreachable();
97
  }
98
}
99
100
11953852
void Rewriter::setPreRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache) {
101
11953852
  switch(theoryId) {
102
373286
    case THEORY_BUILTIN: return RewriteAttibute<THEORY_BUILTIN>::setPreRewriteCache(node, cache);
103
6099610
    case THEORY_BOOL: return RewriteAttibute<THEORY_BOOL>::setPreRewriteCache(node, cache);
104
418479
    case THEORY_UF: return RewriteAttibute<THEORY_UF>::setPreRewriteCache(node, cache);
105
2921459
    case THEORY_ARITH: return RewriteAttibute<THEORY_ARITH>::setPreRewriteCache(node, cache);
106
1355486
    case THEORY_BV: return RewriteAttibute<THEORY_BV>::setPreRewriteCache(node, cache);
107
5456
    case THEORY_FP: return RewriteAttibute<THEORY_FP>::setPreRewriteCache(node, cache);
108
32657
    case THEORY_ARRAYS: return RewriteAttibute<THEORY_ARRAYS>::setPreRewriteCache(node, cache);
109
302523
    case THEORY_DATATYPES: return RewriteAttibute<THEORY_DATATYPES>::setPreRewriteCache(node, cache);
110
1746
    case THEORY_SEP: return RewriteAttibute<THEORY_SEP>::setPreRewriteCache(node, cache);
111
54435
    case THEORY_SETS: return RewriteAttibute<THEORY_SETS>::setPreRewriteCache(node, cache);
112
1069
    case THEORY_BAGS: return RewriteAttibute<THEORY_BAGS>::setPreRewriteCache(node, cache);
113
258885
    case THEORY_STRINGS: return RewriteAttibute<THEORY_STRINGS>::setPreRewriteCache(node, cache);
114
128761
    case THEORY_QUANTIFIERS: return RewriteAttibute<THEORY_QUANTIFIERS>::setPreRewriteCache(node, cache);
115
116
  default:
117
    Unreachable();
118
  }
119
}
120
121
11048918
void Rewriter::setPostRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache) {
122
11048918
  switch(theoryId) {
123
375510
    case THEORY_BUILTIN: return RewriteAttibute<THEORY_BUILTIN>::setPostRewriteCache(node, cache);
124
5494878
    case THEORY_BOOL: return RewriteAttibute<THEORY_BOOL>::setPostRewriteCache(node, cache);
125
413602
    case THEORY_UF: return RewriteAttibute<THEORY_UF>::setPostRewriteCache(node, cache);
126
2923993
    case THEORY_ARITH: return RewriteAttibute<THEORY_ARITH>::setPostRewriteCache(node, cache);
127
1057764
    case THEORY_BV: return RewriteAttibute<THEORY_BV>::setPostRewriteCache(node, cache);
128
5417
    case THEORY_FP: return RewriteAttibute<THEORY_FP>::setPostRewriteCache(node, cache);
129
30627
    case THEORY_ARRAYS: return RewriteAttibute<THEORY_ARRAYS>::setPostRewriteCache(node, cache);
130
302442
    case THEORY_DATATYPES: return RewriteAttibute<THEORY_DATATYPES>::setPostRewriteCache(node, cache);
131
1746
    case THEORY_SEP: return RewriteAttibute<THEORY_SEP>::setPostRewriteCache(node, cache);
132
54262
    case THEORY_SETS: return RewriteAttibute<THEORY_SETS>::setPostRewriteCache(node, cache);
133
1062
    case THEORY_BAGS: return RewriteAttibute<THEORY_BAGS>::setPostRewriteCache(node, cache);
134
258885
    case THEORY_STRINGS: return RewriteAttibute<THEORY_STRINGS>::setPostRewriteCache(node, cache);
135
128730
    case THEORY_QUANTIFIERS: return RewriteAttibute<THEORY_QUANTIFIERS>::setPostRewriteCache(node, cache);
136
137
  default:
138
    Unreachable();
139
  }
140
}
141
142
9620
Rewriter::Rewriter() : d_tpg(nullptr)
143
{
144
3116880
for (size_t i = 0; i < kind::LAST_KIND; ++i)
145
{
146
3107260
  d_preRewriters[i] = nullptr;
147
3107260
  d_postRewriters[i] = nullptr;
148
}
149
150
134680
for (size_t i = 0; i < theory::THEORY_LAST; ++i)
151
{
152
125060
  d_preRewritersEqual[i] = nullptr;
153
125060
  d_postRewritersEqual[i] = nullptr;
154
}
155
9620
}
156
157
void Rewriter::clearCachesInternal() {
158
  typedef CVC4::expr::attr::AttributeUniqueId AttributeUniqueId;
159
  std::vector<AttributeUniqueId> preids;
160
   preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BUILTIN>::pre_rewrite()));
161
 preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BOOL>::pre_rewrite()));
162
 preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_UF>::pre_rewrite()));
163
 preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_ARITH>::pre_rewrite()));
164
 preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BV>::pre_rewrite()));
165
 preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_FP>::pre_rewrite()));
166
 preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_ARRAYS>::pre_rewrite()));
167
 preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_DATATYPES>::pre_rewrite()));
168
 preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_SEP>::pre_rewrite()));
169
 preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_SETS>::pre_rewrite()));
170
 preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BAGS>::pre_rewrite()));
171
 preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_STRINGS>::pre_rewrite()));
172
 preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_QUANTIFIERS>::pre_rewrite()));
173
174
175
  std::vector<AttributeUniqueId> postids;
176
   postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BUILTIN>::post_rewrite()));
177
 postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BOOL>::post_rewrite()));
178
 postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_UF>::post_rewrite()));
179
 postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_ARITH>::post_rewrite()));
180
 postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BV>::post_rewrite()));
181
 postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_FP>::post_rewrite()));
182
 postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_ARRAYS>::post_rewrite()));
183
 postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_DATATYPES>::post_rewrite()));
184
 postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_SEP>::post_rewrite()));
185
 postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_SETS>::post_rewrite()));
186
 postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BAGS>::post_rewrite()));
187
 postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_STRINGS>::post_rewrite()));
188
 postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_QUANTIFIERS>::post_rewrite()));
189
190
191
  std::vector<const AttributeUniqueId*> allids;
192
  for(unsigned i = 0; i < preids.size(); ++i){
193
    allids.push_back(&preids[i]);
194
  }
195
  for(unsigned i = 0; i < postids.size(); ++i){
196
    allids.push_back(&postids[i]);
197
  }
198
  NodeManager::currentNM()->deleteAttributes(allids);
199
}
200
201
}/* CVC4::theory namespace */
202
}/* CVC4 namespace */