GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/substitutions.h Lines: 21 23 91.3 %
Date: 2021-03-22 Branches: 9 20 45.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file substitutions.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Dejan Jovanovic, Clark Barrett
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 "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__SUBSTITUTIONS_H
20
#define CVC4__THEORY__SUBSTITUTIONS_H
21
22
//#include <algorithm>
23
#include <utility>
24
#include <vector>
25
#include <unordered_map>
26
27
#include "expr/node.h"
28
#include "context/context.h"
29
#include "context/cdo.h"
30
#include "context/cdhashmap.h"
31
#include "util/hash.h"
32
33
namespace CVC4 {
34
namespace theory {
35
36
/**
37
 * The type for the Substitutions mapping output by
38
 * Theory::simplify(), TheoryEngine::simplify(), and
39
 * Valuation::simplify().  This is in its own header to
40
 * avoid circular dependences between those three.
41
 *
42
 * This map is context-dependent.
43
 */
44
85578
class SubstitutionMap {
45
46
public:
47
48
  typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
49
50
  typedef NodeMap::iterator iterator;
51
  typedef NodeMap::const_iterator const_iterator;
52
53
private:
54
55
  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeCache;
56
57
  /** The variables, in order of addition */
58
  NodeMap d_substitutions;
59
60
  /** Cache of the already performed substitutions */
61
  NodeCache d_substitutionCache;
62
63
  /** Whether or not to substitute under quantifiers */
64
  bool d_substituteUnderQuantifiers;
65
66
  /** Has the cache been invalidated? */
67
  bool d_cacheInvalidated;
68
69
  /** Internal method that performs substitution */
70
  Node internalSubstitute(TNode t, NodeCache& cache);
71
72
  /** Helper class to invalidate cache on user pop */
73
85578
  class CacheInvalidator : public context::ContextNotifyObj {
74
    bool& d_cacheInvalidated;
75
  protected:
76
5069689
   void contextNotifyPop() override { d_cacheInvalidated = true; }
77
78
  public:
79
85617
    CacheInvalidator(context::Context* context, bool& cacheInvalidated) :
80
      context::ContextNotifyObj(context),
81
85617
      d_cacheInvalidated(cacheInvalidated) {
82
85617
    }
83
84
  };/* class SubstitutionMap::CacheInvalidator */
85
86
  /**
87
   * This object is notified on user pop and marks the SubstitutionMap's
88
   * cache as invalidated.
89
   */
90
  CacheInvalidator d_cacheInvalidator;
91
92
public:
93
85617
 SubstitutionMap(context::Context* context,
94
                 bool substituteUnderQuantifiers = true)
95
85617
     : d_substitutions(context),
96
       d_substitutionCache(),
97
       d_substituteUnderQuantifiers(substituteUnderQuantifiers),
98
       d_cacheInvalidated(false),
99
85617
       d_cacheInvalidator(context, d_cacheInvalidated)
100
 {
101
85617
  }
102
103
  /**
104
   * Adds a substitution from x to t.
105
   */
106
  void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
107
108
  /**
109
   * Merge subMap into current set of substitutions
110
   */
111
  void addSubstitutions(SubstitutionMap& subMap, bool invalidateCache = true);
112
113
  /**
114
   * Returns true iff x is in the substitution map
115
   */
116
44897
  bool hasSubstitution(TNode x) const {
117
44897
    return d_substitutions.find(x) != d_substitutions.end();
118
  }
119
120
  /**
121
   * Returns the substitution mapping that was given for x via
122
   * addSubstitution().  Note that the returned value might itself
123
   * be in the map; for the actual substitution that would be
124
   * performed for x, use .apply(x).  This getSubstitution() function
125
   * is mainly intended for constructing assertions about what has
126
   * already been put in the map.
127
   */
128
61
  TNode getSubstitution(TNode x) const {
129
61
    AssertArgument(hasSubstitution(x), x, "element not in this substitution map");
130
61
    return (*d_substitutions.find(x)).second;
131
  }
132
133
  /**
134
   * Apply the substitutions to the node.
135
   */
136
  Node apply(TNode t, bool doRewrite = false);
137
138
  /**
139
   * Apply the substitutions to the node.
140
   */
141
284275
  Node apply(TNode t, bool doRewrite = false) const {
142
284275
    return const_cast<SubstitutionMap*>(this)->apply(t, doRewrite);
143
  }
144
145
45299
  iterator begin() {
146
45299
    return d_substitutions.begin();
147
  }
148
149
146475
  iterator end() {
150
146475
    return d_substitutions.end();
151
  }
152
153
  const_iterator begin() const {
154
    return d_substitutions.begin();
155
  }
156
157
  const_iterator end() const {
158
    return d_substitutions.end();
159
  }
160
161
  bool empty() const {
162
    return d_substitutions.empty();
163
  }
164
165
  /**
166
   * Print to the output stream
167
   */
168
  void print(std::ostream& out) const;
169
  void debugPrint() const;
170
171
};/* class SubstitutionMap */
172
173
inline std::ostream& operator << (std::ostream& out, const SubstitutionMap& subst) {
174
  subst.print(out);
175
  return out;
176
}
177
178
}/* CVC4::theory namespace */
179
180
std::ostream& operator<<(std::ostream& out, const theory::SubstitutionMap::iterator& i);
181
182
}/* CVC4 namespace */
183
184
#endif /* CVC4__THEORY__SUBSTITUTIONS_H */