GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/inst_match_trie.cpp Lines: 70 155 45.2 %
Date: 2021-03-22 Branches: 83 394 21.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file inst_match_trie.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, 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 Implementation of inst match trie class
13
 **/
14
15
#include "theory/quantifiers/inst_match_trie.h"
16
17
#include "theory/quantifiers/instantiate.h"
18
#include "theory/quantifiers/quant_util.h"
19
#include "theory/quantifiers/quantifiers_state.h"
20
#include "theory/quantifiers/term_database.h"
21
#include "theory/quantifiers_engine.h"
22
#include "theory/uf/equality_engine_iterator.h"
23
24
using namespace CVC4::context;
25
26
namespace CVC4 {
27
namespace theory {
28
namespace inst {
29
30
bool InstMatchTrie::existsInstMatch(quantifiers::QuantifiersState& qs,
31
                                    Node q,
32
                                    const std::vector<Node>& m,
33
                                    bool modEq,
34
                                    ImtIndexOrder* imtio,
35
                                    unsigned index)
36
{
37
  return !addInstMatch(qs, q, m, modEq, imtio, true, index);
38
}
39
40
270401
bool InstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs,
41
                                 Node f,
42
                                 const std::vector<Node>& m,
43
                                 bool modEq,
44
                                 ImtIndexOrder* imtio,
45
                                 bool onlyExist,
46
                                 unsigned index)
47
{
48
811203
  if (index == f[0].getNumChildren()
49
811203
      || (imtio && index == imtio->d_order.size()))
50
  {
51
79280
    return false;
52
  }
53
191121
  unsigned i_index = imtio ? imtio->d_order[index] : index;
54
382242
  Node n = m[i_index];
55
191121
  std::map<Node, InstMatchTrie>::iterator it = d_data.find(n);
56
191121
  if (it != d_data.end())
57
  {
58
    bool ret =
59
122327
        it->second.addInstMatch(qs, f, m, modEq, imtio, onlyExist, index + 1);
60
122327
    if (!onlyExist || !ret)
61
    {
62
122327
      return ret;
63
    }
64
  }
65
68794
  if (modEq)
66
  {
67
    // check modulo equality if any other instantiation match exists
68
    if (!n.isNull() && qs.hasTerm(n))
69
    {
70
      eq::EqClassIterator eqc(qs.getRepresentative(n), qs.getEqualityEngine());
71
      while (!eqc.isFinished())
72
      {
73
        Node en = (*eqc);
74
        if (en != n)
75
        {
76
          std::map<Node, InstMatchTrie>::iterator itc = d_data.find(en);
77
          if (itc != d_data.end())
78
          {
79
            if (itc->second.addInstMatch(
80
                    qs, f, m, modEq, imtio, true, index + 1))
81
            {
82
              return false;
83
            }
84
          }
85
        }
86
        ++eqc;
87
      }
88
    }
89
  }
90
68794
  if (!onlyExist)
91
  {
92
68794
    d_data[n].addInstMatch(qs, f, m, modEq, imtio, false, index + 1);
93
  }
94
68794
  return true;
95
}
96
97
bool InstMatchTrie::removeInstMatch(Node q,
98
                                    const std::vector<Node>& m,
99
                                    ImtIndexOrder* imtio,
100
                                    unsigned index)
101
{
102
  Assert(index < q[0].getNumChildren());
103
  Assert(!imtio || index < imtio->d_order.size());
104
  unsigned i_index = imtio ? imtio->d_order[index] : index;
105
  Node n = m[i_index];
106
  std::map<Node, InstMatchTrie>::iterator it = d_data.find(n);
107
  if (it != d_data.end())
108
  {
109
    if ((index + 1) == q[0].getNumChildren()
110
        || (imtio && (index + 1) == imtio->d_order.size()))
111
    {
112
      d_data.erase(n);
113
      return true;
114
    }
115
    return it->second.removeInstMatch(q, m, imtio, index + 1);
116
  }
117
  return false;
118
}
119
120
void InstMatchTrie::print(std::ostream& out,
121
                          Node q,
122
                          std::vector<TNode>& terms) const
123
{
124
  if (terms.size() == q[0].getNumChildren())
125
  {
126
    out << "  ( ";
127
    for (unsigned i = 0, size = terms.size(); i < size; i++)
128
    {
129
      if (i > 0)
130
      {
131
        out << ", ";
132
      }
133
      out << terms[i];
134
    }
135
    out << " )" << std::endl;
136
  }
137
  else
138
  {
139
    for (const std::pair<const Node, InstMatchTrie>& d : d_data)
140
    {
141
      terms.push_back(d.first);
142
      d.second.print(out, q, terms);
143
      terms.pop_back();
144
    }
145
  }
146
}
147
148
85
void InstMatchTrie::getInstantiations(
149
    Node q, std::vector<std::vector<Node>>& insts) const
150
{
151
170
  std::vector<Node> terms;
152
85
  getInstantiations(q, insts, terms);
153
85
}
154
155
728
void InstMatchTrie::getInstantiations(Node q,
156
                                      std::vector<std::vector<Node>>& insts,
157
                                      std::vector<Node>& terms) const
158
{
159
728
  if (terms.size() == q[0].getNumChildren())
160
  {
161
204
    insts.push_back(terms);
162
  }
163
  else
164
  {
165
1167
    for (const std::pair<const Node, InstMatchTrie>& d : d_data)
166
    {
167
643
      terms.push_back(d.first);
168
643
      d.second.getInstantiations(q, insts, terms);
169
643
      terms.pop_back();
170
    }
171
  }
172
728
}
173
174
void InstMatchTrie::clear() { d_data.clear(); }
175
176
void InstMatchTrie::print(std::ostream& out, Node q) const
177
{
178
  std::vector<TNode> terms;
179
  print(out, q, terms);
180
}
181
182
8232
CDInstMatchTrie::~CDInstMatchTrie()
183
{
184
7617
  for (std::pair<const Node, CDInstMatchTrie*>& d : d_data)
185
  {
186
3501
    CDInstMatchTrie* current = d.second;
187
3501
    delete current;
188
  }
189
4116
  d_data.clear();
190
4116
}
191
192
bool CDInstMatchTrie::existsInstMatch(quantifiers::QuantifiersState& qs,
193
                                      Node q,
194
                                      const std::vector<Node>& m,
195
                                      bool modEq,
196
                                      unsigned index)
197
{
198
  return !addInstMatch(qs, q, m, modEq, index, true);
199
}
200
201
10638
bool CDInstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs,
202
                                   Node f,
203
                                   const std::vector<Node>& m,
204
                                   bool modEq,
205
                                   unsigned index,
206
                                   bool onlyExist)
207
{
208
10638
  bool reset = false;
209
10638
  if (!d_valid.get())
210
  {
211
4518
    if (onlyExist)
212
    {
213
      return true;
214
    }
215
    else
216
    {
217
4518
      d_valid.set(true);
218
4518
      reset = true;
219
    }
220
  }
221
10638
  if (index == f[0].getNumChildren())
222
  {
223
4344
    return reset;
224
  }
225
12588
  Node n = m[index];
226
6294
  std::map<Node, CDInstMatchTrie*>::iterator it = d_data.find(n);
227
6294
  if (it != d_data.end())
228
  {
229
2793
    bool ret = it->second->addInstMatch(qs, f, m, modEq, index + 1, onlyExist);
230
2793
    if (!onlyExist || !ret)
231
    {
232
2793
      return reset || ret;
233
    }
234
  }
235
3501
  if (modEq)
236
  {
237
    // check modulo equality if any other instantiation match exists
238
    if (!n.isNull() && qs.hasTerm(n))
239
    {
240
      eq::EqClassIterator eqc(qs.getRepresentative(n), qs.getEqualityEngine());
241
      while (!eqc.isFinished())
242
      {
243
        Node en = (*eqc);
244
        if (en != n)
245
        {
246
          std::map<Node, CDInstMatchTrie*>::iterator itc = d_data.find(en);
247
          if (itc != d_data.end())
248
          {
249
            if (itc->second->addInstMatch(qs, f, m, modEq, index + 1, true))
250
            {
251
              return false;
252
            }
253
          }
254
        }
255
        ++eqc;
256
      }
257
    }
258
  }
259
260
3501
  if (!onlyExist)
261
  {
262
3501
    CDInstMatchTrie* imt = new CDInstMatchTrie(qs.getUserContext());
263
3501
    Assert(d_data.find(n) == d_data.end());
264
3501
    d_data[n] = imt;
265
3501
    imt->addInstMatch(qs, f, m, modEq, index + 1, false);
266
  }
267
3501
  return true;
268
}
269
270
bool CDInstMatchTrie::removeInstMatch(Node q,
271
                                      const std::vector<Node>& m,
272
                                      unsigned index)
273
{
274
  if (index == q[0].getNumChildren())
275
  {
276
    if (d_valid.get())
277
    {
278
      d_valid.set(false);
279
      return true;
280
    }
281
    return false;
282
  }
283
  std::map<Node, CDInstMatchTrie*>::iterator it = d_data.find(m[index]);
284
  if (it != d_data.end())
285
  {
286
    return it->second->removeInstMatch(q, m, index + 1);
287
  }
288
  return false;
289
}
290
291
void CDInstMatchTrie::print(std::ostream& out,
292
                            Node q,
293
                            std::vector<TNode>& terms) const
294
{
295
  if (d_valid.get())
296
  {
297
    if (terms.size() == q[0].getNumChildren())
298
    {
299
      out << "  ( ";
300
      for (unsigned i = 0; i < terms.size(); i++)
301
      {
302
        if (i > 0) out << " ";
303
        out << terms[i];
304
      }
305
      out << " )" << std::endl;
306
    }
307
    else
308
    {
309
      for (const std::pair<const Node, CDInstMatchTrie*>& d : d_data)
310
      {
311
        terms.push_back(d.first);
312
        d.second->print(out, q, terms);
313
        terms.pop_back();
314
      }
315
    }
316
  }
317
}
318
319
2
void CDInstMatchTrie::getInstantiations(
320
    Node q, std::vector<std::vector<Node>>& insts) const
321
{
322
4
  std::vector<Node> terms;
323
2
  getInstantiations(q, insts, terms);
324
2
}
325
326
5
void CDInstMatchTrie::getInstantiations(Node q,
327
                                        std::vector<std::vector<Node>>& insts,
328
                                        std::vector<Node>& terms) const
329
{
330
5
  if (!d_valid.get())
331
  {
332
    // do nothing
333
  }
334
4
  else if (terms.size() == q[0].getNumChildren())
335
  {
336
2
    insts.push_back(terms);
337
  }
338
  else
339
  {
340
5
    for (const std::pair<const Node, CDInstMatchTrie*>& d : d_data)
341
    {
342
3
      terms.push_back(d.first);
343
3
      d.second->getInstantiations(q, insts, terms);
344
3
      terms.pop_back();
345
    }
346
  }
347
5
}
348
349
void CDInstMatchTrie::print(std::ostream& out, Node q) const
350
{
351
  std::vector<TNode> terms;
352
  print(out, q, terms);
353
}
354
355
3214
bool InstMatchTrieOrdered::addInstMatch(quantifiers::QuantifiersState& qs,
356
                                        Node q,
357
                                        const std::vector<Node>& m,
358
                                        bool modEq)
359
{
360
3214
  return d_imt.addInstMatch(qs, q, m, modEq, d_imtio);
361
}
362
363
bool InstMatchTrieOrdered::existsInstMatch(quantifiers::QuantifiersState& qs,
364
                                           Node q,
365
                                           const std::vector<Node>& m,
366
                                           bool modEq)
367
{
368
  return d_imt.existsInstMatch(qs, q, m, modEq, d_imtio);
369
}
370
371
} /* CVC4::theory::inst namespace */
372
} /* CVC4::theory namespace */
373
26676
} /* CVC4 namespace */