GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/ematching/ho_trigger.cpp Lines: 230 258 89.1 %
Date: 2021-03-23 Branches: 466 1136 41.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file ho_trigger.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, Gereon Kremer
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 higher-order trigger class
13
 **/
14
15
#include <stack>
16
17
#include "theory/quantifiers/ematching/ho_trigger.h"
18
#include "theory/quantifiers/instantiate.h"
19
#include "theory/quantifiers/quantifiers_inference_manager.h"
20
#include "theory/quantifiers/quantifiers_registry.h"
21
#include "theory/quantifiers/quantifiers_state.h"
22
#include "theory/quantifiers/term_database.h"
23
#include "theory/quantifiers/term_util.h"
24
#include "theory/quantifiers_engine.h"
25
#include "theory/uf/theory_uf_rewriter.h"
26
#include "util/hash.h"
27
28
using namespace CVC4::kind;
29
30
namespace CVC4 {
31
namespace theory {
32
namespace inst {
33
34
31
HigherOrderTrigger::HigherOrderTrigger(
35
    QuantifiersEngine* qe,
36
    quantifiers::QuantifiersState& qs,
37
    quantifiers::QuantifiersInferenceManager& qim,
38
    quantifiers::QuantifiersRegistry& qr,
39
    Node q,
40
    std::vector<Node>& nodes,
41
31
    std::map<Node, std::vector<Node> >& ho_apps)
42
31
    : Trigger(qe, qs, qim, qr, q, nodes), d_ho_var_apps(ho_apps)
43
{
44
31
  NodeManager* nm = NodeManager::currentNM();
45
  // process the higher-order variable applications
46
69
  for (std::pair<const Node, std::vector<Node> >& as : d_ho_var_apps)
47
  {
48
76
    Node n = as.first;
49
38
    d_ho_var_list.push_back(n);
50
76
    TypeNode tn = n.getType();
51
38
    Assert(tn.isFunction());
52
38
    if (Trace.isOn("ho-quant-trigger"))
53
    {
54
      Trace("ho-quant-trigger") << "  have " << as.second.size();
55
      Trace("ho-quant-trigger") << " patterns with variable operator " << n
56
                                << ":" << std::endl;
57
      for (unsigned j = 0; j < as.second.size(); j++)
58
      {
59
        Trace("ho-quant-trigger") << "  " << as.second[j] << std::endl;
60
      }
61
    }
62
38
    if (d_ho_var_types.find(tn) == d_ho_var_types.end())
63
    {
64
76
      Trace("ho-quant-trigger") << "  type " << tn
65
38
                                << " needs higher-order matching." << std::endl;
66
38
      d_ho_var_types.insert(tn);
67
    }
68
    // make the bound variable lists
69
38
    d_ho_var_bvl[n] = nm->getBoundVarListForFunctionType(tn);
70
95
    for (const Node& nc : d_ho_var_bvl[n])
71
    {
72
57
      d_ho_var_bvs[n].push_back(nc);
73
    }
74
  }
75
31
}
76
77
62
HigherOrderTrigger::~HigherOrderTrigger() {}
78
void HigherOrderTrigger::collectHoVarApplyTerms(
79
    Node q, Node& n, std::map<Node, std::vector<Node> >& apps)
80
{
81
  std::vector<Node> ns;
82
  ns.push_back(n);
83
  collectHoVarApplyTerms(q, ns, apps);
84
  Assert(ns.size() == 1);
85
  n = ns[0];
86
}
87
88
16622
void HigherOrderTrigger::collectHoVarApplyTerms(
89
    Node q, std::vector<Node>& ns, std::map<Node, std::vector<Node> >& apps)
90
{
91
33244
  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
92
16622
  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
93
  // whether the visited node is a child of a HO_APPLY chain
94
33244
  std::unordered_map<TNode, bool, TNodeHashFunction> withinApply;
95
33244
  std::vector<TNode> visit;
96
33244
  TNode cur;
97
34796
  for (unsigned i = 0, size = ns.size(); i < size; i++)
98
  {
99
18174
    visit.push_back(ns[i]);
100
18174
    withinApply[ns[i]] = false;
101
194510
    do
102
    {
103
212684
      cur = visit.back();
104
212684
      visit.pop_back();
105
106
212684
      it = visited.find(cur);
107
212684
      if (it == visited.end())
108
      {
109
        // do not look in nested quantifiers
110
104304
        if (cur.getKind() == FORALL)
111
        {
112
          visited[cur] = cur;
113
        }
114
        else
115
        {
116
104304
          bool curWithinApply = withinApply[cur];
117
104304
          visited[cur] = Node::null();
118
104304
          visit.push_back(cur);
119
194510
          for (unsigned j = 0, sizec = cur.getNumChildren(); j < sizec; j++)
120
          {
121
90206
            withinApply[cur[j]] = curWithinApply && j == 0;
122
90206
            visit.push_back(cur[j]);
123
          }
124
        }
125
      }
126
108380
      else if (it->second.isNull())
127
      {
128
        // carry the conversion
129
208608
        Node ret = cur;
130
104304
        bool childChanged = false;
131
208608
        std::vector<Node> children;
132
104304
        if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
133
        {
134
40319
          children.push_back(cur.getOperator());
135
        }
136
194510
        for (const Node& nc : cur)
137
        {
138
90206
          it = visited.find(nc);
139
90206
          Assert(it != visited.end());
140
90206
          Assert(!it->second.isNull());
141
90206
          childChanged = childChanged || nc != it->second;
142
90206
          children.push_back(it->second);
143
        }
144
104304
        if (childChanged)
145
        {
146
22
          ret = NodeManager::currentNM()->mkNode(cur.getKind(), children);
147
        }
148
        // now, convert and store the application
149
104304
        if (!withinApply[cur])
150
        {
151
208608
          TNode op;
152
104304
          if (ret.getKind() == kind::APPLY_UF)
153
          {
154
            // could be a fully applied function variable
155
37318
            op = ret.getOperator();
156
          }
157
66986
          else if (ret.getKind() == kind::HO_APPLY)
158
          {
159
93
            op = ret;
160
317
            while (op.getKind() == kind::HO_APPLY)
161
            {
162
112
              op = op[0];
163
            }
164
          }
165
104304
          if (!op.isNull())
166
          {
167
37411
            if (op.getKind() == kind::INST_CONSTANT)
168
            {
169
38
              Assert(quantifiers::TermUtil::getInstConstAttr(ret) == q);
170
76
              Trace("ho-quant-trigger-debug")
171
38
                  << "Ho variable apply term : " << ret << " with head " << op
172
38
                  << std::endl;
173
38
              if (ret.getKind() == kind::APPLY_UF)
174
              {
175
62
                Node prev = ret;
176
                // for consistency, convert to HO_APPLY if fully applied
177
31
                ret = uf::TheoryUfRewriter::getHoApplyForApplyUf(ret);
178
              }
179
38
              apps[op].push_back(ret);
180
            }
181
          }
182
        }
183
104304
        visited[cur] = ret;
184
      }
185
212684
    } while (!visit.empty());
186
187
    // store the conversion
188
18174
    Assert(visited.find(ns[i]) != visited.end());
189
18174
    ns[i] = visited[ns[i]];
190
  }
191
16622
}
192
193
93
uint64_t HigherOrderTrigger::addInstantiations()
194
{
195
  // call the base class implementation
196
93
  uint64_t addedFoLemmas = Trigger::addInstantiations();
197
  // also adds predicate lemms to force app completion
198
93
  uint64_t addedHoLemmas = addHoTypeMatchPredicateLemmas();
199
93
  return addedHoLemmas + addedFoLemmas;
200
}
201
202
160
bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m, InferenceId id)
203
{
204
320
  if (options::hoMatching())
205
  {
206
    // get substitution corresponding to m
207
320
    std::vector<TNode> vars;
208
320
    std::vector<TNode> subs;
209
588
    for (unsigned i = 0, size = d_quant[0].getNumChildren(); i < size; i++)
210
    {
211
428
      subs.push_back(m[i]);
212
428
      vars.push_back(d_qreg.getInstantiationConstant(d_quant, i));
213
    }
214
215
160
    Trace("ho-unif-debug") << "Run higher-order unification..." << std::endl;
216
217
    // get the substituted form of all variable-operator ho application terms
218
320
    std::map<TNode, std::vector<Node> > ho_var_apps_subs;
219
336
    for (std::pair<const Node, std::vector<Node> >& ha : d_ho_var_apps)
220
    {
221
352
      TNode var = ha.first;
222
352
      for (unsigned j = 0, size = ha.second.size(); j < size; j++)
223
      {
224
352
        TNode app = ha.second[j];
225
        Node sapp =
226
352
            app.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
227
176
        ho_var_apps_subs[var].push_back(sapp);
228
352
        Trace("ho-unif-debug") << "  app[" << var << "] : " << app << " -> "
229
176
                               << sapp << std::endl;
230
      }
231
    }
232
233
    // compute argument vectors for each variable
234
160
    d_lchildren.clear();
235
160
    d_arg_to_arg_rep.clear();
236
160
    d_arg_vector.clear();
237
160
    quantifiers::QuantifiersState& qs = d_quantEngine->getState();
238
336
    for (std::pair<const TNode, std::vector<Node> >& ha : ho_var_apps_subs)
239
    {
240
352
      TNode var = ha.first;
241
176
      unsigned vnum = var.getAttribute(InstVarNumAttribute());
242
352
      TNode value = m[vnum];
243
176
      Trace("ho-unif-debug") << "  val[" << var << "] = " << value << std::endl;
244
245
352
      Trace("ho-unif-debug2") << "initialize lambda information..."
246
176
                              << std::endl;
247
      // initialize the lambda children
248
176
      d_lchildren[vnum].push_back(value);
249
      std::map<TNode, std::vector<Node> >::iterator ithb =
250
176
          d_ho_var_bvs.find(var);
251
176
      Assert(ithb != d_ho_var_bvs.end());
252
352
      d_lchildren[vnum].insert(
253
352
          d_lchildren[vnum].end(), ithb->second.begin(), ithb->second.end());
254
255
176
      Trace("ho-unif-debug2") << "compute fixed arguments..." << std::endl;
256
      // compute for each argument if it is only applied to a fixed value modulo
257
      // equality
258
352
      std::map<unsigned, Node> fixed_vals;
259
352
      for (unsigned i = 0; i < ha.second.size(); i++)
260
      {
261
352
        std::vector<TNode> args;
262
        // must substitute the operator we matched with the original
263
        // higher-order variable (var) that matched it. This ensures that the
264
        // argument vector (args) below is of the proper length. This handles,
265
        // for example, matches like:
266
        //   (@ x y) with (@ (@ k1 k2) k3)
267
        // where k3 but not k2 should be an argument of the match.
268
352
        Node hmatch = ha.second[i];
269
176
        Trace("ho-unif-debug2") << "Match is " << hmatch << std::endl;
270
176
        hmatch = hmatch.substitute(value, var);
271
176
        Trace("ho-unif-debug2") << "Pre-subs match is " << hmatch << std::endl;
272
352
        Node f = uf::TheoryUfRewriter::decomposeHoApply(hmatch, args);
273
        // Assert( f==value );
274
464
        for (unsigned k = 0, size = args.size(); k < size; k++)
275
        {
276
          // must now subsitute back, to handle cases like
277
          // (@ x y) matching (@ t (@ t s))
278
          // where the above substitution would produce (@ x (@ x s)),
279
          // but the argument should be (@ t s).
280
288
          args[k] = args[k].substitute(var, value);
281
576
          Node val = args[k];
282
288
          std::map<unsigned, Node>::iterator itf = fixed_vals.find(k);
283
288
          if (itf == fixed_vals.end())
284
          {
285
288
            fixed_vals[k] = val;
286
          }
287
          else if (!itf->second.isNull())
288
          {
289
            if (!qs.areEqual(itf->second, args[k]))
290
            {
291
              if (!d_quantEngine->getTermDatabase()->isEntailed(
292
                      itf->second.eqNode(args[k]), true))
293
              {
294
                fixed_vals[k] = Node::null();
295
              }
296
            }
297
          }
298
        }
299
      }
300
176
      if (Trace.isOn("ho-unif-debug"))
301
      {
302
        for (std::map<unsigned, Node>::iterator itf = fixed_vals.begin();
303
             itf != fixed_vals.end();
304
             ++itf)
305
        {
306
          Trace("ho-unif-debug") << "  arg[" << var << "][" << itf->first
307
                                 << "] : " << itf->second << std::endl;
308
        }
309
      }
310
311
      // now construct argument vectors
312
176
      Trace("ho-unif-debug2") << "compute argument vectors..." << std::endl;
313
352
      std::map<Node, unsigned> arg_to_rep;
314
480
      for (unsigned index = 0, size = ithb->second.size(); index < size;
315
           index++)
316
      {
317
608
        Node bv_at_index = ithb->second[index];
318
304
        std::map<unsigned, Node>::iterator itf = fixed_vals.find(index);
319
304
        Trace("ho-unif-debug") << "  * arg[" << var << "][" << index << "]";
320
304
        if (itf != fixed_vals.end())
321
        {
322
288
          if (!itf->second.isNull())
323
          {
324
576
            Node r = qs.getRepresentative(itf->second);
325
288
            std::map<Node, unsigned>::iterator itfr = arg_to_rep.find(r);
326
288
            if (itfr != arg_to_rep.end())
327
            {
328
52
              d_arg_to_arg_rep[vnum][index] = itfr->second;
329
              // function applied to equivalent values at multiple arguments,
330
              // can permute variables
331
52
              d_arg_vector[vnum][itfr->second].push_back(bv_at_index);
332
104
              Trace("ho-unif-debug") << " = { self } ++ arg[" << var << "]["
333
52
                                     << itfr->second << "]" << std::endl;
334
            }
335
            else
336
            {
337
236
              arg_to_rep[r] = index;
338
              // function applied to single value, can either use variable or
339
              // value at this argument position
340
236
              d_arg_vector[vnum][index].push_back(bv_at_index);
341
236
              d_arg_vector[vnum][index].push_back(itf->second);
342
472
              if (!options::hoMatchingVarArgPriority())
343
              {
344
                std::reverse(d_arg_vector[vnum][index].begin(),
345
                             d_arg_vector[vnum][index].end());
346
              }
347
472
              Trace("ho-unif-debug") << " = { self, " << itf->second << " } "
348
236
                                     << std::endl;
349
            }
350
          }
351
          else
352
          {
353
            // function is applied to disequal values, can only use variable at
354
            // this argument position
355
            d_arg_vector[vnum][index].push_back(bv_at_index);
356
            Trace("ho-unif-debug") << " = { self } (disequal)" << std::endl;
357
          }
358
        }
359
        else
360
        {
361
          // argument is irrelevant to matching, assume identity variable
362
16
          d_arg_vector[vnum][index].push_back(bv_at_index);
363
16
          Trace("ho-unif-debug") << " = { self } (irrelevant)" << std::endl;
364
        }
365
      }
366
176
      Trace("ho-unif-debug2") << "finished." << std::endl;
367
    }
368
369
160
    bool ret = sendInstantiation(m, 0);
370
160
    Trace("ho-unif-debug") << "Finished, success = " << ret << std::endl;
371
160
    return ret;
372
  }
373
  else
374
  {
375
    // do not run higher-order matching
376
    return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m, id);
377
  }
378
}
379
380
// recursion depth limited by number of arguments of higher order variables
381
// occurring as pattern operators (very small)
382
624
bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m,
383
                                           size_t var_index)
384
{
385
1248
  Trace("ho-unif-debug2") << "send inst " << var_index << " / "
386
624
                          << d_ho_var_list.size() << std::endl;
387
624
  if (var_index == d_ho_var_list.size())
388
  {
389
    // we now have an instantiation to try
390
878
    return d_quantEngine->getInstantiate()->addInstantiation(
391
439
        d_quant, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_HO);
392
  }
393
  else
394
  {
395
370
    Node var = d_ho_var_list[var_index];
396
185
    unsigned vnum = var.getAttribute(InstVarNumAttribute());
397
185
    Assert(vnum < m.size());
398
370
    Node value = m[vnum];
399
185
    Assert(d_lchildren[vnum][0] == value);
400
185
    Assert(d_ho_var_bvl.find(var) != d_ho_var_bvl.end());
401
402
    // now, recurse on arguments to enumerate equivalent matching lambda
403
    // expressions
404
    bool ret =
405
185
        sendInstantiationArg(m, var_index, vnum, 0, d_ho_var_bvl[var], false);
406
407
    // reset the value
408
185
    m[vnum] = value;
409
410
185
    return ret;
411
  }
412
}
413
414
850
bool HigherOrderTrigger::sendInstantiationArg(std::vector<Node>& m,
415
                                              unsigned var_index,
416
                                              unsigned vnum,
417
                                              unsigned arg_index,
418
                                              Node lbvl,
419
                                              bool arg_changed)
420
{
421
1700
  Trace("ho-unif-debug2") << "send inst arg " << arg_index << " / "
422
850
                          << lbvl.getNumChildren() << std::endl;
423
850
  if (arg_index == lbvl.getNumChildren())
424
  {
425
    // construct the lambda
426
464
    if (arg_changed)
427
    {
428
614
      Trace("ho-unif-debug2")
429
307
          << "  make lambda from children: " << d_lchildren[vnum] << std::endl;
430
      Node body =
431
614
          NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_lchildren[vnum]);
432
307
      Trace("ho-unif-debug2") << "  got " << body << std::endl;
433
614
      Node lam = NodeManager::currentNM()->mkNode(kind::LAMBDA, lbvl, body);
434
307
      m[vnum] = lam;
435
307
      Trace("ho-unif-debug2") << "  try " << vnum << " -> " << lam << std::endl;
436
    }
437
464
    return sendInstantiation(m, var_index + 1);
438
  }
439
  else
440
  {
441
    std::map<unsigned, unsigned>::iterator itr =
442
386
        d_arg_to_arg_rep[vnum].find(arg_index);
443
    unsigned rindex =
444
386
        itr != d_arg_to_arg_rep[vnum].end() ? itr->second : arg_index;
445
    std::map<unsigned, std::vector<Node> >::iterator itv =
446
386
        d_arg_vector[vnum].find(rindex);
447
386
    Assert(itv != d_arg_vector[vnum].end());
448
772
    Node prev = lbvl[arg_index];
449
386
    bool ret = false;
450
    // try each argument in the vector
451
796
    for (unsigned i = 0, size = itv->second.size(); i < size; i++)
452
    {
453
665
      bool new_arg_changed = arg_changed || prev != itv->second[i];
454
665
      d_lchildren[vnum][arg_index + 1] = itv->second[i];
455
665
      if (sendInstantiationArg(
456
              m, var_index, vnum, arg_index + 1, lbvl, new_arg_changed))
457
      {
458
255
        ret = true;
459
255
        break;
460
      }
461
    }
462
    // clean up
463
386
    d_lchildren[vnum][arg_index + 1] = prev;
464
386
    return ret;
465
  }
466
}
467
468
93
uint64_t HigherOrderTrigger::addHoTypeMatchPredicateLemmas()
469
{
470
93
  if (d_ho_var_types.empty())
471
  {
472
    return 0;
473
  }
474
93
  Trace("ho-quant-trigger") << "addHoTypeMatchPredicateLemmas..." << std::endl;
475
93
  uint64_t numLemmas = 0;
476
  // this forces expansion of APPLY_UF terms to curried HO_APPLY chains
477
93
  quantifiers::TermDb* tdb = d_quantEngine->getTermDatabase();
478
93
  unsigned size = tdb->getNumOperators();
479
93
  NodeManager* nm = NodeManager::currentNM();
480
596
  for (unsigned j = 0; j < size; j++)
481
  {
482
1006
    Node f = tdb->getOperator(j);
483
503
    if (f.isVar())
484
    {
485
770
      TypeNode tn = f.getType();
486
385
      if (tn.isFunction())
487
      {
488
770
        std::vector<TypeNode> argTypes = tn.getArgTypes();
489
385
        Assert(argTypes.size() > 0);
490
770
        TypeNode range = tn.getRangeType();
491
        // for each function type suffix of the type of f, for example if
492
        // f : (Int -> (Int -> Int))
493
        // we iterate with stn = (Int -> (Int -> Int)) and (Int -> Int)
494
843
        for (unsigned a = 0, arg_size = argTypes.size(); a < arg_size; a++)
495
        {
496
916
          std::vector<TypeNode> sargts;
497
458
          sargts.insert(sargts.begin(), argTypes.begin() + a, argTypes.end());
498
458
          Assert(sargts.size() > 0);
499
916
          TypeNode stn = nm->mkFunctionType(sargts, range);
500
916
          Trace("ho-quant-trigger-debug")
501
458
              << "For " << f << ", check " << stn << "..." << std::endl;
502
          // if a variable of this type occurs in this trigger
503
458
          if (d_ho_var_types.find(stn) != d_ho_var_types.end())
504
          {
505
312
            Node u = tdb->getHoTypeMatchPredicate(tn);
506
312
            Node au = nm->mkNode(kind::APPLY_UF, u, f);
507
156
            if (d_qim.addPendingLemma(au, InferenceId::UNKNOWN))
508
            {
509
              // this forces f to be a first-class member of the quantifier-free
510
              // equality engine, which in turn forces the quantifier-free
511
              // theory solver to expand it to an HO_APPLY chain.
512
100
              Trace("ho-quant")
513
50
                  << "Added ho match predicate lemma : " << au << std::endl;
514
50
              numLemmas++;
515
            }
516
          }
517
        }
518
      }
519
    }
520
  }
521
522
93
  return numLemmas;
523
}
524
525
} /* CVC4::theory::inst namespace */
526
} /* CVC4::theory namespace */
527
27081
} /* CVC4 namespace */