GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/inst_match_trie.h Lines: 10 10 100.0 %
Date: 2021-03-22 Branches: 1 2 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file inst_match_trie.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, Mathias Preiner
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 inst match trie class
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H
18
#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H
19
20
#include <map>
21
22
#include "context/cdlist.h"
23
#include "context/cdo.h"
24
#include "expr/node.h"
25
26
namespace CVC4 {
27
namespace theory {
28
29
class QuantifiersEngine;
30
31
namespace quantifiers {
32
class QuantifiersState;
33
}
34
35
namespace inst {
36
37
/** trie for InstMatch objects
38
 *
39
 * This class is used for storing instantiations of a quantified formula q.
40
 * It is a trie data structure for which entries can be added and removed.
41
 * This class has interfaces for adding instantiations that are either
42
 * represented by std::vectors or InstMatch objects (see inst_match.h).
43
 */
44
63
class InstMatchTrie
45
{
46
 public:
47
  /** index ordering */
48
72
  class ImtIndexOrder
49
  {
50
   public:
51
    std::vector<unsigned> d_order;
52
  };
53
54
 public:
55
74020
  InstMatchTrie() {}
56
74083
  ~InstMatchTrie() {}
57
  /** exists inst match
58
   *
59
   * This method considers the entry given by m, starting at the given index.
60
   * The domain of m is the bound variables of quantified formula q.
61
   * It returns true if (the suffix) of m exists in this trie.
62
   * If modEq is true, we check for duplication modulo equality the current
63
   * equalities in the equality engine of qs.
64
   */
65
  bool existsInstMatch(quantifiers::QuantifiersState& qs,
66
                       Node q,
67
                       const std::vector<Node>& m,
68
                       bool modEq = false,
69
                       ImtIndexOrder* imtio = nullptr,
70
                       unsigned index = 0);
71
  /** add inst match
72
   *
73
   * This method adds (the suffix of) m starting at the given index to this
74
   * trie, and returns true if and only if m did not already occur in this trie.
75
   * The domain of m is the bound variables of quantified formula q.
76
   * If modEq is true, we check for duplication modulo equality the current
77
   * equalities in the equality engine of qs.
78
   */
79
  bool addInstMatch(quantifiers::QuantifiersState& qs,
80
                    Node f,
81
                    const std::vector<Node>& m,
82
                    bool modEq = false,
83
                    ImtIndexOrder* imtio = nullptr,
84
                    bool onlyExist = false,
85
                    unsigned index = 0);
86
  /** remove inst match
87
   *
88
   * This removes (the suffix of) m starting at the given index from this trie.
89
   * It returns true if and only if this entry existed in this trie.
90
   * The domain of m is the bound variables of quantified formula q.
91
   */
92
  bool removeInstMatch(Node f,
93
                       const std::vector<Node>& m,
94
                       ImtIndexOrder* imtio = nullptr,
95
                       unsigned index = 0);
96
  /**
97
   * Adds the instantiations for q into insts.
98
   */
99
  void getInstantiations(Node q, std::vector<std::vector<Node>>& insts) const;
100
101
  /** clear the data of this class */
102
  void clear();
103
  /** print this class */
104
  void print(std::ostream& out, Node q) const;
105
  /** the data */
106
  std::map<Node, InstMatchTrie> d_data;
107
108
 private:
109
  /** Helper for getInstantiations.*/
110
  void getInstantiations(Node q,
111
                         std::vector<std::vector<Node>>& insts,
112
                         std::vector<Node>& terms) const;
113
  /** helper for print
114
   * terms accumulates the path we are on in the trie.
115
   */
116
  void print(std::ostream& out, Node q, std::vector<TNode>& terms) const;
117
};
118
119
/** trie for InstMatch objects
120
 *
121
 * This is a context-dependent version of the above class.
122
 */
123
class CDInstMatchTrie
124
{
125
 public:
126
4116
  CDInstMatchTrie(context::Context* c) : d_valid(c, false) {}
127
  ~CDInstMatchTrie();
128
129
  /** exists inst match
130
   *
131
   * This method considers the entry given by m, starting at the given index.
132
   * The domain of m is the bound variables of quantified formula q.
133
   * It returns true if (the suffix) of m exists in this trie.
134
   * If modEq is true, we check for duplication modulo equality the current
135
   * equalities in the equality engine of qs.
136
   * It additionally takes a context c, for which the entry is valid in.
137
   */
138
  bool existsInstMatch(quantifiers::QuantifiersState& qs,
139
                       Node q,
140
                       const std::vector<Node>& m,
141
                       bool modEq = false,
142
                       unsigned index = 0);
143
  /** add inst match
144
   *
145
   * This method adds (the suffix of) m starting at the given index to this
146
   * trie, and returns true if and only if m did not already occur in this trie.
147
   * The domain of m is the bound variables of quantified formula q.
148
   * If modEq is true, we check for duplication modulo equality the current
149
   * equalities in the equality engine of qs.
150
   * It additionally takes a context c, for which the entry is valid in.
151
   */
152
  bool addInstMatch(quantifiers::QuantifiersState& qs,
153
                    Node q,
154
                    const std::vector<Node>& m,
155
                    bool modEq = false,
156
                    unsigned index = 0,
157
                    bool onlyExist = false);
158
  /** remove inst match
159
   *
160
   * This removes (the suffix of) m starting at the given index from this trie.
161
   * It returns true if and only if this entry existed in this trie.
162
   * The domain of m is the bound variables of quantified formula q.
163
   */
164
  bool removeInstMatch(Node q, const std::vector<Node>& m, unsigned index = 0);
165
  /**
166
   * Adds the instantiations for q into insts.
167
   */
168
  void getInstantiations(Node q, std::vector<std::vector<Node>>& insts) const;
169
170
  /** print this class */
171
  void print(std::ostream& out, Node q) const;
172
173
 private:
174
  /** Helper for getInstantiations.*/
175
  void getInstantiations(Node q,
176
                         std::vector<std::vector<Node>>& insts,
177
                         std::vector<Node>& terms) const;
178
  /** helper for print
179
   * terms accumulates the path we are on in the trie.
180
   */
181
  void print(std::ostream& out, Node q, std::vector<TNode>& terms) const;
182
  /** the data */
183
  std::map<Node, CDInstMatchTrie*> d_data;
184
  /** is valid */
185
  context::CDO<bool> d_valid;
186
};
187
188
/** inst match trie ordered
189
 *
190
 * This is an ordered version of the context-independent instantiation match
191
 * trie. It stores a variable order and a base InstMatchTrie.
192
 */
193
63
class InstMatchTrieOrdered
194
{
195
 public:
196
36
  InstMatchTrieOrdered(InstMatchTrie::ImtIndexOrder* imtio) : d_imtio(imtio) {}
197
99
  ~InstMatchTrieOrdered() {}
198
  /** get the ordering */
199
69084
  InstMatchTrie::ImtIndexOrder* getOrdering() { return d_imtio; }
200
  /** get the trie data */
201
38903
  InstMatchTrie* getTrie() { return &d_imt; }
202
  /** add match m for quantified formula q
203
   *
204
   * This method returns true if the match m was not previously added to this
205
   * class. If modEq is true, we consider duplicates modulo the current
206
   * equalities stored in the equality engine of qs.
207
   */
208
  bool addInstMatch(quantifiers::QuantifiersState& qs,
209
                    Node q,
210
                    const std::vector<Node>& m,
211
                    bool modEq = false);
212
  /** returns true if this trie contains m
213
   *
214
   * This method returns true if the match m exists in this
215
   * class. If modEq is true, we consider duplicates modulo the current
216
   * equalities stored in the equality engine of qs.
217
   */
218
  bool existsInstMatch(quantifiers::QuantifiersState& qs,
219
                       Node q,
220
                       const std::vector<Node>& m,
221
                       bool modEq = false);
222
223
 private:
224
  /** the ordering */
225
  InstMatchTrie::ImtIndexOrder* d_imtio;
226
  /** the data of this class */
227
  InstMatchTrie d_imt;
228
};
229
230
} /* CVC4::theory::inst namespace */
231
} /* CVC4::theory namespace */
232
} /* CVC4 namespace */
233
234
#endif /* CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */