GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/ematching/trigger.cpp Lines: 161 180 89.4 %
Date: 2021-03-22 Branches: 249 586 42.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file trigger.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 Implementation of trigger class
13
 **/
14
15
#include "theory/quantifiers/ematching/trigger.h"
16
17
#include "expr/skolem_manager.h"
18
#include "options/quantifiers_options.h"
19
#include "theory/quantifiers/ematching/candidate_generator.h"
20
#include "theory/quantifiers/ematching/ho_trigger.h"
21
#include "theory/quantifiers/ematching/inst_match_generator.h"
22
#include "theory/quantifiers/ematching/inst_match_generator_multi.h"
23
#include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h"
24
#include "theory/quantifiers/ematching/inst_match_generator_simple.h"
25
#include "theory/quantifiers/ematching/pattern_term_selector.h"
26
#include "theory/quantifiers/ematching/trigger_trie.h"
27
#include "theory/quantifiers/inst_match.h"
28
#include "theory/quantifiers/instantiate.h"
29
#include "theory/quantifiers/quantifiers_attributes.h"
30
#include "theory/quantifiers/quantifiers_inference_manager.h"
31
#include "theory/quantifiers/quantifiers_registry.h"
32
#include "theory/quantifiers/quantifiers_state.h"
33
#include "theory/quantifiers/term_util.h"
34
#include "theory/quantifiers_engine.h"
35
#include "theory/valuation.h"
36
37
using namespace CVC4::kind;
38
39
namespace CVC4 {
40
namespace theory {
41
namespace inst {
42
43
/** trigger class constructor */
44
16622
Trigger::Trigger(QuantifiersEngine* qe,
45
                 quantifiers::QuantifiersState& qs,
46
                 quantifiers::QuantifiersInferenceManager& qim,
47
                 quantifiers::QuantifiersRegistry& qr,
48
                 Node q,
49
16622
                 std::vector<Node>& nodes)
50
16622
    : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr), d_quant(q)
51
{
52
  // We must ensure that the ground subterms of the trigger have been
53
  // preprocessed.
54
16622
  Valuation& val = d_qstate.getValuation();
55
34796
  for (const Node& n : nodes)
56
  {
57
36348
    Node np = ensureGroundTermPreprocessed(val, n, d_groundTerms);
58
18174
    d_nodes.push_back(np);
59
  }
60
16622
  if (Trace.isOn("trigger"))
61
  {
62
    quantifiers::QuantAttributes& qa = d_qreg.getQuantAttributes();
63
    Trace("trigger") << "Trigger for " << qa.quantToString(q) << ": "
64
                     << std::endl;
65
    for (const Node& n : d_nodes)
66
    {
67
      Trace("trigger") << "   " << n << std::endl;
68
    }
69
  }
70
16622
  if( d_nodes.size()==1 ){
71
15382
    if (TriggerTermInfo::isSimpleTrigger(d_nodes[0]))
72
    {
73
7660
      d_mg = new InstMatchGeneratorSimple(this, q, d_nodes[0]);
74
7660
      ++(qe->d_statistics.d_triggers);
75
    }else{
76
7722
      d_mg = InstMatchGenerator::mkInstMatchGenerator(this, q, d_nodes[0]);
77
7722
      ++(qe->d_statistics.d_simple_triggers);
78
    }
79
  }else{
80
2486
    if( options::multiTriggerCache() ){
81
15
      d_mg = new InstMatchGeneratorMulti(this, q, d_nodes);
82
    }else{
83
1225
      d_mg = InstMatchGenerator::mkInstMatchGeneratorMulti(this, q, d_nodes);
84
    }
85
1240
    if (Trace.isOn("multi-trigger"))
86
    {
87
      Trace("multi-trigger") << "Trigger for " << q << ": " << std::endl;
88
      for (const Node& nc : d_nodes)
89
      {
90
        Trace("multi-trigger") << "   " << nc << std::endl;
91
      }
92
    }
93
1240
    ++(qe->d_statistics.d_multi_triggers);
94
  }
95
96
16622
  Trace("trigger-debug") << "Finished making trigger." << std::endl;
97
16622
}
98
99
49835
Trigger::~Trigger() {
100
16622
  delete d_mg;
101
33213
}
102
103
148727
void Trigger::resetInstantiationRound() { d_mg->resetInstantiationRound(); }
104
105
148727
void Trigger::reset(Node eqc) { d_mg->reset(eqc); }
106
107
22496
bool Trigger::isMultiTrigger() const { return d_nodes.size() > 1; }
108
109
Node Trigger::getInstPattern() const
110
{
111
  return NodeManager::currentNM()->mkNode( INST_PATTERN, d_nodes );
112
}
113
114
46190
uint64_t Trigger::addInstantiations()
115
{
116
46190
  uint64_t gtAddedLemmas = 0;
117
46190
  if (!d_groundTerms.empty())
118
  {
119
    // for each ground term t that does not exist in the equality engine, we
120
    // add a purification lemma of the form (k = t).
121
3392
    eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
122
6840
    for (const Node& gt : d_groundTerms)
123
    {
124
3448
      if (!ee->hasTerm(gt))
125
      {
126
408
        SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
127
816
        Node k = sm->mkPurifySkolem(gt, "gt");
128
816
        Node eq = k.eqNode(gt);
129
816
        Trace("trigger-gt-lemma")
130
408
            << "Trigger: ground term purify lemma: " << eq << std::endl;
131
408
        d_qim.addPendingLemma(eq, InferenceId::UNKNOWN);
132
408
        gtAddedLemmas++;
133
      }
134
    }
135
  }
136
46190
  uint64_t addedLemmas = d_mg->addInstantiations(d_quant);
137
46190
  if (Debug.isOn("inst-trigger"))
138
  {
139
    if (addedLemmas > 0)
140
    {
141
      Debug("inst-trigger") << "Added " << addedLemmas
142
                            << " lemmas, trigger was " << d_nodes << std::endl;
143
    }
144
  }
145
46190
  return gtAddedLemmas + addedLemmas;
146
}
147
148
173415
bool Trigger::sendInstantiation(std::vector<Node>& m, InferenceId id)
149
{
150
173415
  return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m, id);
151
}
152
153
173575
bool Trigger::sendInstantiation(InstMatch& m, InferenceId id)
154
{
155
173575
  return sendInstantiation(m.d_vals, id);
156
}
157
158
12943
bool Trigger::mkTriggerTerms(Node q,
159
                             std::vector<Node>& nodes,
160
                             size_t nvars,
161
                             std::vector<Node>& trNodes)
162
{
163
  //only take nodes that contribute variables to the trigger when added
164
25886
  std::vector< Node > temp;
165
12943
  temp.insert( temp.begin(), nodes.begin(), nodes.end() );
166
25886
  std::map< Node, bool > vars;
167
25886
  std::map< Node, std::vector< Node > > patterns;
168
12943
  size_t varCount = 0;
169
25886
  std::map< Node, std::vector< Node > > varContains;
170
30055
  for (const Node& pat : temp)
171
  {
172
17112
    quantifiers::TermUtil::computeInstConstContainsForQuant(
173
17112
        q, pat, varContains[pat]);
174
  }
175
15899
  for (const Node& t : temp)
176
  {
177
15899
    const std::vector<Node>& vct = varContains[t];
178
15899
    bool foundVar = false;
179
53282
    for (const Node& v : vct)
180
    {
181
37383
      Assert(quantifiers::TermUtil::getInstConstAttr(v) == q);
182
37383
      if( vars.find( v )==vars.end() ){
183
34229
        varCount++;
184
34229
        vars[ v ] = true;
185
34229
        foundVar = true;
186
      }
187
    }
188
15899
    if( foundVar ){
189
15409
      trNodes.push_back(t);
190
51656
      for (const Node& v : vct)
191
      {
192
36247
        patterns[v].push_back(t);
193
      }
194
    }
195
15899
    if (varCount == nvars)
196
    {
197
12943
      break;
198
    }
199
  }
200
12943
  if (varCount < nvars)
201
  {
202
    Trace("trigger-debug") << "Don't consider trigger since it does not contain specified number of variables." << std::endl;
203
    Trace("trigger-debug") << nodes << std::endl;
204
    //do not generate multi-trigger if it does not contain all variables
205
    return false;
206
  }
207
  // now, minimize the trigger
208
29439
  for (size_t i = 0, tsize = trNodes.size(); i < tsize; i++)
209
  {
210
16496
    bool keepPattern = false;
211
32992
    Node n = trNodes[i];
212
16496
    const std::vector<Node>& vcn = varContains[n];
213
18286
    for (const Node& v : vcn)
214
    {
215
17199
      if (patterns[v].size() == 1)
216
      {
217
15409
        keepPattern = true;
218
15409
        break;
219
      }
220
    }
221
16496
    if (!keepPattern)
222
    {
223
      // remove from pattern vector
224
2556
      for (const Node& v : vcn)
225
      {
226
1469
        std::vector<Node>& pv = patterns[v];
227
1531
        for (size_t k = 0, pvsize = pv.size(); k < pvsize; k++)
228
        {
229
1531
          if (pv[k] == n)
230
          {
231
1469
            pv.erase(pv.begin() + k, pv.begin() + k + 1);
232
1469
            break;
233
          }
234
        }
235
      }
236
      // remove from trigger nodes
237
1087
      trNodes.erase(trNodes.begin() + i, trNodes.begin() + i + 1);
238
1087
      i--;
239
    }
240
  }
241
12943
  return true;
242
}
243
244
16666
Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
245
                            quantifiers::QuantifiersState& qs,
246
                            quantifiers::QuantifiersInferenceManager& qim,
247
                            quantifiers::QuantifiersRegistry& qr,
248
                            Node f,
249
                            std::vector<Node>& nodes,
250
                            bool keepAll,
251
                            int trOption,
252
                            size_t useNVars)
253
{
254
33332
  std::vector< Node > trNodes;
255
16666
  if( !keepAll ){
256
12943
    size_t nvars = useNVars == 0 ? f[0].getNumChildren() : useNVars;
257
12943
    if (!mkTriggerTerms(f, nodes, nvars, trNodes))
258
    {
259
      return nullptr;
260
    }
261
  }else{
262
3723
    trNodes.insert( trNodes.begin(), nodes.begin(), nodes.end() );
263
  }
264
265
  //check for duplicate?
266
16666
  if( trOption!=TR_MAKE_NEW ){
267
12943
    Trigger* t = qe->getTriggerDatabase()->getTrigger( trNodes );
268
12943
    if( t ){
269
44
      if( trOption==TR_GET_OLD ){
270
        //just return old trigger
271
44
        return t;
272
      }else{
273
        return nullptr;
274
      }
275
    }
276
  }
277
278
  // check if higher-order
279
33244
  Trace("trigger-debug") << "Collect higher-order variable triggers..."
280
16622
                         << std::endl;
281
33244
  std::map<Node, std::vector<Node> > ho_apps;
282
16622
  HigherOrderTrigger::collectHoVarApplyTerms(f, trNodes, ho_apps);
283
33244
  Trace("trigger-debug") << "...got " << ho_apps.size()
284
16622
                         << " higher-order applications." << std::endl;
285
  Trigger* t;
286
16622
  if (!ho_apps.empty())
287
  {
288
31
    t = new HigherOrderTrigger(qe, qs, qim, qr, f, trNodes, ho_apps);
289
  }
290
  else
291
  {
292
16591
    t = new Trigger(qe, qs, qim, qr, f, trNodes);
293
  }
294
295
16622
  qe->getTriggerDatabase()->addTrigger( trNodes, t );
296
16622
  return t;
297
}
298
299
11864
Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
300
                            quantifiers::QuantifiersState& qs,
301
                            quantifiers::QuantifiersInferenceManager& qim,
302
                            quantifiers::QuantifiersRegistry& qr,
303
                            Node f,
304
                            Node n,
305
                            bool keepAll,
306
                            int trOption,
307
                            size_t useNVars)
308
{
309
23728
  std::vector< Node > nodes;
310
11864
  nodes.push_back( n );
311
23728
  return mkTrigger(qe, qs, qim, qr, f, nodes, keepAll, trOption, useNVars);
312
}
313
314
int Trigger::getActiveScore() { return d_mg->getActiveScore(); }
315
316
18174
Node Trigger::ensureGroundTermPreprocessed(Valuation& val,
317
                                           Node n,
318
                                           std::vector<Node>& gts)
319
{
320
18174
  NodeManager* nm = NodeManager::currentNM();
321
36348
  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
322
18174
  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
323
36348
  std::vector<TNode> visit;
324
36348
  TNode cur;
325
18174
  visit.push_back(n);
326
133943
  do
327
  {
328
152117
    cur = visit.back();
329
152117
    visit.pop_back();
330
152117
    it = visited.find(cur);
331
152117
    if (it == visited.end())
332
    {
333
103505
      if (cur.getNumChildren() == 0)
334
      {
335
55793
        visited[cur] = cur;
336
      }
337
47712
      else if (!quantifiers::TermUtil::hasInstConstAttr(cur))
338
      {
339
        // cur has no INST_CONSTANT, thus is ground.
340
2674
        Node vcur = val.getPreprocessedTerm(cur);
341
1337
        gts.push_back(vcur);
342
1337
        visited[cur] = vcur;
343
      }
344
      else
345
      {
346
46375
        visited[cur] = Node::null();
347
46375
        visit.push_back(cur);
348
46375
        visit.insert(visit.end(), cur.begin(), cur.end());
349
      }
350
    }
351
48612
    else if (it->second.isNull())
352
    {
353
92750
      Node ret = cur;
354
46375
      bool childChanged = false;
355
92750
      std::vector<Node> children;
356
46375
      if (cur.getMetaKind() == metakind::PARAMETERIZED)
357
      {
358
38758
        children.push_back(cur.getOperator());
359
      }
360
133943
      for (const Node& cn : cur)
361
      {
362
87568
        it = visited.find(cn);
363
87568
        Assert(it != visited.end());
364
87568
        Assert(!it->second.isNull());
365
87568
        childChanged = childChanged || cn != it->second;
366
87568
        children.push_back(it->second);
367
      }
368
46375
      if (childChanged)
369
      {
370
124
        ret = nm->mkNode(cur.getKind(), children);
371
      }
372
46375
      visited[cur] = ret;
373
    }
374
152117
  } while (!visit.empty());
375
18174
  Assert(visited.find(n) != visited.end());
376
18174
  Assert(!visited.find(n)->second.isNull());
377
36348
  return visited[n];
378
}
379
380
33583
void Trigger::debugPrint(const char* c) const
381
{
382
33583
  Trace(c) << "TRIGGER( " << d_nodes << " )" << std::endl;
383
33583
}
384
385
}/* CVC4::theory::inst namespace */
386
}/* CVC4::theory namespace */
387
27922
}/* CVC4 namespace */