GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/ematching/inst_match_generator_multi.cpp Lines: 133 141 94.3 %
Date: 2021-03-23 Branches: 207 394 52.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file inst_match_generator_multi.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, Tim King
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 multi inst match generator class
13
 **/
14
15
#include "theory/quantifiers/ematching/inst_match_generator_multi.h"
16
17
#include "theory/quantifiers/quantifiers_state.h"
18
#include "theory/quantifiers/term_util.h"
19
#include "theory/quantifiers_engine.h"
20
#include "theory/uf/equality_engine_iterator.h"
21
22
using namespace CVC4::kind;
23
24
namespace CVC4 {
25
namespace theory {
26
namespace inst {
27
28
15
InstMatchGeneratorMulti::InstMatchGeneratorMulti(Trigger* tparent,
29
                                                 Node q,
30
15
                                                 std::vector<Node>& pats)
31
15
    : IMGenerator(tparent), d_quant(q)
32
{
33
30
  Trace("multi-trigger-cache")
34
15
      << "Making smart multi-trigger for " << q << std::endl;
35
30
  std::map<Node, std::vector<Node> > var_contains;
36
51
  for (const Node& pat : pats)
37
  {
38
36
    quantifiers::TermUtil::computeInstConstContainsForQuant(
39
36
        q, pat, var_contains[pat]);
40
  }
41
  // convert to indicies
42
51
  for (std::pair<const Node, std::vector<Node> >& vc : var_contains)
43
  {
44
36
    Trace("multi-trigger-cache") << "Pattern " << vc.first << " contains: ";
45
164
    for (const Node& vcn : vc.second)
46
    {
47
128
      Trace("multi-trigger-cache") << vcn << " ";
48
128
      uint64_t index = vcn.getAttribute(InstVarNumAttribute());
49
128
      d_var_contains[vc.first].push_back(index);
50
128
      d_var_to_node[index].push_back(vc.first);
51
    }
52
36
    Trace("multi-trigger-cache") << std::endl;
53
  }
54
15
  size_t patsSize = pats.size();
55
51
  for (size_t i = 0; i < patsSize; i++)
56
  {
57
72
    Node n = pats[i];
58
    // make the match generator
59
    InstMatchGenerator* img =
60
36
        InstMatchGenerator::mkInstMatchGenerator(tparent, q, n);
61
36
    img->setActiveAdd(false);
62
36
    d_children.push_back(img);
63
    // compute unique/shared variables
64
72
    std::vector<uint64_t> unique_vars;
65
72
    std::map<uint64_t, bool> shared_vars;
66
36
    unsigned numSharedVars = 0;
67
36
    std::vector<uint64_t>& vctn = d_var_contains[n];
68
164
    for (size_t j = 0, vctnSize = vctn.size(); j < vctnSize; j++)
69
    {
70
128
      if (d_var_to_node[vctn[j]].size() == 1)
71
      {
72
164
        Trace("multi-trigger-cache")
73
82
            << "Var " << vctn[j] << " is unique to " << pats[i] << std::endl;
74
82
        unique_vars.push_back(vctn[j]);
75
      }
76
      else
77
      {
78
46
        shared_vars[vctn[j]] = true;
79
46
        numSharedVars++;
80
      }
81
    }
82
    // we use the latest shared variables, then unique variables
83
72
    std::vector<uint64_t> vars;
84
36
    size_t index = i == 0 ? pats.size() - 1 : (i - 1);
85
118
    while (numSharedVars > 0 && index != i)
86
    {
87
97
      for (std::pair<const uint64_t, bool>& sv : shared_vars)
88
      {
89
56
        if (sv.second)
90
        {
91
51
          std::vector<uint64_t>& vctni = d_var_contains[pats[index]];
92
51
          if (std::find(vctni.begin(), vctni.end(), sv.first) != vctni.end())
93
          {
94
46
            vars.push_back(sv.first);
95
46
            shared_vars[sv.first] = false;
96
46
            numSharedVars--;
97
          }
98
        }
99
      }
100
41
      index = index == 0 ? patsSize - 1 : (index - 1);
101
    }
102
36
    vars.insert(vars.end(), unique_vars.begin(), unique_vars.end());
103
36
    if (Trace.isOn("multi-trigger-cache"))
104
    {
105
      Trace("multi-trigger-cache") << "   Index[" << i << "]: ";
106
      for (uint64_t v : vars)
107
      {
108
        Trace("multi-trigger-cache") << v << " ";
109
      }
110
      Trace("multi-trigger-cache") << std::endl;
111
    }
112
    // make ordered inst match trie
113
36
    d_imtio[i] = new InstMatchTrie::ImtIndexOrder;
114
72
    d_imtio[i]->d_order.insert(
115
72
        d_imtio[i]->d_order.begin(), vars.begin(), vars.end());
116
36
    d_children_trie.push_back(InstMatchTrieOrdered(d_imtio[i]));
117
  }
118
15
}
119
120
45
InstMatchGeneratorMulti::~InstMatchGeneratorMulti()
121
{
122
51
  for (size_t i = 0, csize = d_children.size(); i < csize; i++)
123
  {
124
36
    delete d_children[i];
125
  }
126
51
  for (std::pair<const size_t, InstMatchTrie::ImtIndexOrder*>& i : d_imtio)
127
  {
128
36
    delete i.second;
129
  }
130
30
}
131
132
/** reset instantiation round (call this whenever equivalence classes have
133
 * changed) */
134
232
void InstMatchGeneratorMulti::resetInstantiationRound()
135
{
136
777
  for (InstMatchGenerator* c : d_children)
137
  {
138
545
    c->resetInstantiationRound();
139
  }
140
232
}
141
142
/** reset, eqc is the equivalence class to search in (any if eqc=null) */
143
232
bool InstMatchGeneratorMulti::reset(Node eqc)
144
{
145
777
  for (InstMatchGenerator* c : d_children)
146
  {
147
545
    if (!c->reset(eqc))
148
    {
149
      // do not return false here
150
    }
151
  }
152
232
  return true;
153
}
154
155
67
uint64_t InstMatchGeneratorMulti::addInstantiations(Node q)
156
{
157
67
  uint64_t addedLemmas = 0;
158
67
  Trace("multi-trigger-cache") << "Process smart multi trigger" << std::endl;
159
214
  for (size_t i = 0, csize = d_children.size(); i < csize; i++)
160
  {
161
147
    Trace("multi-trigger-cache") << "Calculate matches " << i << std::endl;
162
294
    std::vector<InstMatch> newMatches;
163
294
    InstMatch m(q);
164
6575
    while (d_children[i]->getNextMatch(q, m) > 0)
165
    {
166
      // m.makeRepresentative( qe );
167
3214
      newMatches.push_back(InstMatch(&m));
168
3214
      m.clear();
169
    }
170
294
    Trace("multi-trigger-cache") << "Made " << newMatches.size()
171
147
                                 << " new matches for index " << i << std::endl;
172
3361
    for (size_t j = 0, nmatches = newMatches.size(); j < nmatches; j++)
173
    {
174
6428
      Trace("multi-trigger-cache2")
175
6428
          << "...processing " << j << " / " << newMatches.size()
176
3214
          << ", #lemmas = " << addedLemmas << std::endl;
177
3214
      processNewMatch(newMatches[j], i, addedLemmas);
178
3214
      if (d_qstate.isInConflict())
179
      {
180
        return addedLemmas;
181
      }
182
    }
183
  }
184
67
  return addedLemmas;
185
}
186
187
3214
void InstMatchGeneratorMulti::processNewMatch(InstMatch& m,
188
                                              size_t fromChildIndex,
189
                                              uint64_t& addedLemmas)
190
{
191
  // see if these produce new matches
192
3214
  d_children_trie[fromChildIndex].addInstMatch(d_qstate, d_quant, m.d_vals);
193
  // possibly only do the following if we know that new matches will be
194
  // produced? the issue is that instantiations are filtered in quantifiers
195
  // engine, and so there is no guarentee that
196
  // we can safely skip the following lines, even when we have already produced
197
  // this match.
198
6428
  Trace("multi-trigger-cache-debug")
199
3214
      << "Child " << fromChildIndex << " produced match " << m << std::endl;
200
  // process new instantiations
201
3214
  size_t childIndex = (fromChildIndex + 1) % d_children.size();
202
6428
  processNewInstantiations(m,
203
                           addedLemmas,
204
3214
                           d_children_trie[childIndex].getTrie(),
205
                           0,
206
                           childIndex,
207
                           fromChildIndex,
208
                           true);
209
3214
}
210
211
103374
void InstMatchGeneratorMulti::processNewInstantiations(InstMatch& m,
212
                                                       uint64_t& addedLemmas,
213
                                                       InstMatchTrie* tr,
214
                                                       size_t trieIndex,
215
                                                       size_t childIndex,
216
                                                       size_t endChildIndex,
217
                                                       bool modEq)
218
{
219
103374
  Assert(!d_qstate.isInConflict());
220
103374
  if (childIndex == endChildIndex)
221
  {
222
    // m is an instantiation
223
34290
    if (sendInstantiation(m, InferenceId::QUANTIFIERS_INST_E_MATCHING_MT))
224
    {
225
1498
      addedLemmas++;
226
2996
      Trace("multi-trigger-cache-debug")
227
1498
          << "-> Produced instantiation " << m << std::endl;
228
    }
229
34290
    return;
230
  }
231
69084
  InstMatchTrie::ImtIndexOrder* iio = d_children_trie[childIndex].getOrdering();
232
69084
  if (trieIndex < iio->d_order.size())
233
  {
234
33395
    size_t curr_index = iio->d_order[trieIndex];
235
39278
    Node n = m.get(curr_index);
236
33395
    if (n.isNull())
237
    {
238
      // add to InstMatch
239
87781
      for (std::pair<const Node, InstMatchTrie>& d : tr->d_data)
240
      {
241
120538
        InstMatch mn(&m);
242
60269
        mn.setValue(curr_index, d.first);
243
60269
        processNewInstantiations(mn,
244
                                 addedLemmas,
245
                                 &(d.second),
246
                                 trieIndex + 1,
247
                                 childIndex,
248
                                 endChildIndex,
249
                                 modEq);
250
60269
        if (d_qstate.isInConflict())
251
        {
252
          break;
253
        }
254
      }
255
    }
256
    // shared and set variable, try to merge
257
33395
    std::map<Node, InstMatchTrie>::iterator it = tr->d_data.find(n);
258
33395
    if (it != tr->d_data.end())
259
    {
260
7600
      processNewInstantiations(m,
261
                               addedLemmas,
262
3800
                               &(it->second),
263
                               trieIndex + 1,
264
                               childIndex,
265
                               endChildIndex,
266
                               modEq);
267
    }
268
33395
    if (!modEq)
269
    {
270
      return;
271
    }
272
33395
    quantifiers::QuantifiersState& qs = d_qstate;
273
    // check modulo equality for other possible instantiations
274
33395
    if (!qs.hasTerm(n))
275
    {
276
27512
      return;
277
    }
278
5883
    eq::EqClassIterator eqc(qs.getRepresentative(n), qs.getEqualityEngine());
279
33505
    while (!eqc.isFinished())
280
    {
281
27622
      Node en = (*eqc);
282
13811
      if (en != n)
283
      {
284
7928
        std::map<Node, InstMatchTrie>::iterator itc = tr->d_data.find(en);
285
7928
        if (itc != tr->d_data.end())
286
        {
287
804
          processNewInstantiations(m,
288
                                   addedLemmas,
289
402
                                   &(itc->second),
290
                                   trieIndex + 1,
291
                                   childIndex,
292
                                   endChildIndex,
293
                                   modEq);
294
402
          if (d_qstate.isInConflict())
295
          {
296
            break;
297
          }
298
        }
299
      }
300
13811
      ++eqc;
301
    }
302
  }
303
  else
304
  {
305
35689
    size_t newChildIndex = (childIndex + 1) % d_children.size();
306
71378
    processNewInstantiations(m,
307
                             addedLemmas,
308
35689
                             d_children_trie[newChildIndex].getTrie(),
309
                             0,
310
                             newChildIndex,
311
                             endChildIndex,
312
                             modEq);
313
  }
314
}
315
316
}  // namespace inst
317
}  // namespace theory
318
26685
}  // namespace CVC4