GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/substitutions.cpp Lines: 95 111 85.6 %
Date: 2021-03-23 Branches: 226 546 41.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file substitutions.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Dejan Jovanovic, Clark Barrett, Morgan Deters
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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 A substitution mapping for theory simplification
13
 **
14
 ** A substitution mapping for theory simplification.
15
 **/
16
17
#include "theory/substitutions.h"
18
#include "expr/node_algorithm.h"
19
#include "theory/rewriter.h"
20
21
using namespace std;
22
23
namespace CVC4 {
24
namespace theory {
25
26
9196558
struct substitution_stack_element {
27
  TNode d_node;
28
  bool d_children_added;
29
2124642
  substitution_stack_element(TNode node) : d_node(node), d_children_added(false)
30
  {
31
2124642
  }
32
};/* struct substitution_stack_element */
33
34
1579299
Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) {
35
36
1579299
  Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << ")" << endl;
37
38
1579299
  if (d_substitutions.empty()) {
39
983282
    return t;
40
  }
41
42
  // Do a topological sort of the subexpressions and substitute them
43
1192034
  vector<substitution_stack_element> toVisit;
44
596017
  toVisit.push_back((TNode) t);
45
46
7498697
  while (!toVisit.empty())
47
  {
48
    // The current node we are processing
49
3451340
    substitution_stack_element& stackHead = toVisit.back();
50
6464607
    TNode current = stackHead.d_node;
51
52
3451340
    Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): processing " << current << endl;
53
54
    // If node already in the cache we're done, pop from the stack
55
3451340
    NodeCache::iterator find = cache.find(current);
56
3769425
    if (find != cache.end()) {
57
318085
      toVisit.pop_back();
58
318085
      continue;
59
    }
60
61
3133620
    if (!d_substituteUnderQuantifiers && current.isClosure())
62
    {
63
365
      Debug("substitution::internal") << "--not substituting under quantifier" << endl;
64
365
      cache[current] = current;
65
365
      toVisit.pop_back();
66
365
      continue;
67
    }
68
69
3132890
    NodeMap::iterator find2 = d_substitutions.find(current);
70
3132890
    if (find2 != d_substitutions.end()) {
71
239246
      Node rhs = (*find2).second;
72
119623
      Assert(rhs != current);
73
119623
      internalSubstitute(rhs, cache);
74
119623
      d_substitutions[current] = cache[rhs];
75
119623
      cache[current] = cache[rhs];
76
119623
      toVisit.pop_back();
77
119623
      continue;
78
    }
79
80
    // Not yet substituted, so process
81
3013267
    if (stackHead.d_children_added)
82
    {
83
      // Children have been processed, so substitute
84
2653396
      NodeBuilder<> builder(current.getKind());
85
1326698
      if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
86
119657
        builder << Node(cache[current.getOperator()]);
87
      }
88
4646892
      for (unsigned i = 0; i < current.getNumChildren(); ++ i) {
89
3320194
        Assert(cache.find(current[i]) != cache.end());
90
3320194
        builder << Node(cache[current[i]]);
91
      }
92
      // Mark the substitution and continue
93
2653396
      Node result = builder;
94
1326698
      if (result != current) {
95
552984
        find = cache.find(result);
96
552984
        if (find != cache.end()) {
97
5043
          result = find->second;
98
        }
99
        else {
100
547941
          find2 = d_substitutions.find(result);
101
547941
          if (find2 != d_substitutions.end()) {
102
            Node rhs = (*find2).second;
103
            Assert(rhs != result);
104
            internalSubstitute(rhs, cache);
105
            d_substitutions[result] = cache[rhs];
106
            cache[result] = cache[rhs];
107
            result = cache[rhs];
108
          }
109
        }
110
      }
111
1326698
      Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << result << endl;
112
1326698
      cache[current] = result;
113
1326698
      toVisit.pop_back();
114
    }
115
    else
116
    {
117
      // Mark that we have added the children if any
118
1686569
      if (current.getNumChildren() > 0 || current.getMetaKind() == kind::metakind::PARAMETERIZED) {
119
1326698
        stackHead.d_children_added = true;
120
        // We need to add the operator, if any
121
1326698
        if(current.getMetaKind() == kind::metakind::PARAMETERIZED) {
122
239314
          TNode opNode = current.getOperator();
123
119657
          NodeCache::iterator opFind = cache.find(opNode);
124
119657
          if (opFind == cache.end()) {
125
30405
            toVisit.push_back(opNode);
126
          }
127
        }
128
        // We need to add the children
129
4646892
        for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
130
6640388
          TNode childNode = *child_it;
131
3320194
          NodeCache::iterator childFind = cache.find(childNode);
132
3320194
          if (childFind == cache.end()) {
133
1498220
            toVisit.push_back(childNode);
134
          }
135
        }
136
      } else {
137
        // No children, so we're done
138
359871
        Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << current << endl;
139
359871
        cache[current] = current;
140
359871
        toVisit.pop_back();
141
      }
142
    }
143
  }
144
145
  // Return the substituted version
146
596017
  return cache[t];
147
}/* SubstitutionMap::internalSubstitute() */
148
149
150
98911
void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache)
151
{
152
98911
  Debug("substitution") << "SubstitutionMap::addSubstitution(" << x << ", " << t << ")" << endl;
153
98911
  Assert(d_substitutions.find(x) == d_substitutions.end());
154
155
  // this causes a later assert-fail (the rhs != current one, above) anyway
156
  // putting it here is easier to diagnose
157
98911
  Assert(x != t) << "cannot substitute a term for itself";
158
159
98911
  d_substitutions[x] = t;
160
161
  // Also invalidate the cache if necessary
162
98911
  if (invalidateCache) {
163
98842
    d_cacheInvalidated = true;
164
  }
165
  else {
166
69
    d_substitutionCache[x] = d_substitutions[x];
167
  }
168
98911
}
169
170
171
7805
void SubstitutionMap::addSubstitutions(SubstitutionMap& subMap, bool invalidateCache)
172
{
173
7805
  SubstitutionMap::NodeMap::const_iterator it = subMap.begin();
174
7805
  SubstitutionMap::NodeMap::const_iterator it_end = subMap.end();
175
92843
  for (; it != it_end; ++ it) {
176
42519
    Assert(d_substitutions.find((*it).first) == d_substitutions.end());
177
42519
    d_substitutions[(*it).first] = (*it).second;
178
42519
    if (!invalidateCache) {
179
      d_substitutionCache[(*it).first] = d_substitutions[(*it).first];
180
    }
181
  }
182
7805
  if (invalidateCache) {
183
7805
    d_cacheInvalidated = true;
184
  }
185
7805
}
186
187
1459676
Node SubstitutionMap::apply(TNode t, bool doRewrite) {
188
189
1459676
  Debug("substitution") << "SubstitutionMap::apply(" << t << ")" << endl;
190
191
  // Setup the cache
192
1459676
  if (d_cacheInvalidated) {
193
66745
    d_substitutionCache.clear();
194
66745
    d_cacheInvalidated = false;
195
66745
    Debug("substitution") << "-- reset the cache" << endl;
196
  }
197
198
  // Perform the substitution
199
1459676
  Node result = internalSubstitute(t, d_substitutionCache);
200
1459676
  Debug("substitution") << "SubstitutionMap::apply(" << t << ") => " << result << endl;
201
202
1459676
  if (doRewrite)
203
  {
204
647484
    result = Rewriter::rewrite(result);
205
  }
206
207
1459674
  return result;
208
}
209
210
void SubstitutionMap::print(ostream& out) const {
211
  NodeMap::const_iterator it = d_substitutions.begin();
212
  NodeMap::const_iterator it_end = d_substitutions.end();
213
  for (; it != it_end; ++ it) {
214
    out << (*it).first << " -> " << (*it).second << endl;
215
  }
216
}
217
218
void SubstitutionMap::debugPrint() const { print(CVC4Message.getStream()); }
219
220
}/* CVC4::theory namespace */
221
222
std::ostream& operator<<(std::ostream& out, const theory::SubstitutionMap::iterator& i) {
223
  return out << "[CDMap-iterator]";
224
}
225
226
26685
}/* CVC4 namespace */