GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/uf/ho_extension.cpp Lines: 200 239 83.7 %
Date: 2021-03-22 Branches: 420 1024 41.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file ho_extension.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Gereon Kremer, 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 Implementation of the higher-order extension of TheoryUF.
13
 **
14
 **/
15
16
#include "theory/uf/ho_extension.h"
17
18
#include "expr/node_algorithm.h"
19
#include "options/uf_options.h"
20
#include "theory/theory_model.h"
21
#include "theory/uf/theory_uf_rewriter.h"
22
23
using namespace std;
24
using namespace CVC4::kind;
25
26
namespace CVC4 {
27
namespace theory {
28
namespace uf {
29
30
216
HoExtension::HoExtension(TheoryState& state, TheoryInferenceManager& im)
31
    : d_state(state),
32
      d_im(im),
33
216
      d_extensionality(state.getUserContext()),
34
432
      d_uf_std_skolem(state.getUserContext())
35
{
36
216
  d_true = NodeManager::currentNM()->mkConst(true);
37
216
}
38
39
256
Node HoExtension::ppRewrite(Node node)
40
{
41
  // convert HO_APPLY to APPLY_UF if fully applied
42
256
  if (node[0].getType().getNumChildren() == 2)
43
  {
44
120
    Trace("uf-ho") << "uf-ho : expanding definition : " << node << std::endl;
45
240
    Node ret = getApplyUfForHoApply(node);
46
240
    Trace("uf-ho") << "uf-ho : ppRewrite : " << node << " to " << ret
47
120
                   << std::endl;
48
120
    return ret;
49
  }
50
136
  return node;
51
}
52
53
682
Node HoExtension::getExtensionalityDeq(TNode deq, bool isCached)
54
{
55
682
  Assert(deq.getKind() == NOT && deq[0].getKind() == EQUAL);
56
682
  Assert(deq[0][0].getType().isFunction());
57
682
  if (isCached)
58
  {
59
108
    std::map<Node, Node>::iterator it = d_extensionality_deq.find(deq);
60
108
    if (it != d_extensionality_deq.end())
61
    {
62
      return it->second;
63
    }
64
  }
65
1364
  TypeNode tn = deq[0][0].getType();
66
1364
  std::vector<TypeNode> argTypes = tn.getArgTypes();
67
1364
  std::vector<Node> skolems;
68
682
  NodeManager* nm = NodeManager::currentNM();
69
1391
  for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++)
70
  {
71
    Node k =
72
1418
        nm->mkSkolem("k", argTypes[i], "skolem created for extensionality.");
73
709
    skolems.push_back(k);
74
  }
75
1364
  Node t[2];
76
2046
  for (unsigned i = 0; i < 2; i++)
77
  {
78
2728
    std::vector<Node> children;
79
2728
    Node curr = deq[0][i];
80
1878
    while (curr.getKind() == HO_APPLY)
81
    {
82
257
      children.push_back(curr[1]);
83
257
      curr = curr[0];
84
    }
85
1364
    children.push_back(curr);
86
1364
    std::reverse(children.begin(), children.end());
87
1364
    children.insert(children.end(), skolems.begin(), skolems.end());
88
1364
    t[i] = nm->mkNode(APPLY_UF, children);
89
  }
90
1364
  Node conc = t[0].eqNode(t[1]).negate();
91
682
  if (isCached)
92
  {
93
108
    d_extensionality_deq[deq] = conc;
94
  }
95
682
  return conc;
96
}
97
98
332
unsigned HoExtension::applyExtensionality(TNode deq)
99
{
100
332
  Assert(deq.getKind() == NOT && deq[0].getKind() == EQUAL);
101
332
  Assert(deq[0][0].getType().isFunction());
102
  // apply extensionality
103
332
  if (d_extensionality.find(deq) == d_extensionality.end())
104
  {
105
108
    d_extensionality.insert(deq);
106
216
    Node conc = getExtensionalityDeq(deq);
107
216
    Node lem = NodeManager::currentNM()->mkNode(OR, deq[0], conc);
108
216
    Trace("uf-ho-lemma") << "uf-ho-lemma : extensionality : " << lem
109
108
                         << std::endl;
110
108
    d_im.lemma(lem, InferenceId::UF_HO_EXTENSIONALITY);
111
108
    return 1;
112
  }
113
224
  return 0;
114
}
115
116
120
Node HoExtension::getApplyUfForHoApply(Node node)
117
{
118
120
  Assert(node[0].getType().getNumChildren() == 2);
119
240
  std::vector<TNode> args;
120
240
  Node f = TheoryUfRewriter::decomposeHoApply(node, args, true);
121
240
  Node new_f = f;
122
120
  NodeManager* nm = NodeManager::currentNM();
123
120
  if (!TheoryUfRewriter::canUseAsApplyUfOperator(f))
124
  {
125
2
    NodeNodeMap::const_iterator itus = d_uf_std_skolem.find(f);
126
2
    if (itus == d_uf_std_skolem.end())
127
    {
128
4
      std::unordered_set<Node, NodeHashFunction> fvs;
129
2
      expr::getFreeVariables(f, fvs);
130
4
      Node lem;
131
2
      if (!fvs.empty())
132
      {
133
        std::vector<TypeNode> newTypes;
134
        std::vector<Node> vs;
135
        std::vector<Node> nvs;
136
        for (const Node& v : fvs)
137
        {
138
          TypeNode vt = v.getType();
139
          newTypes.push_back(vt);
140
          Node nv = nm->mkBoundVar(vt);
141
          vs.push_back(v);
142
          nvs.push_back(nv);
143
        }
144
        TypeNode ft = f.getType();
145
        std::vector<TypeNode> argTypes = ft.getArgTypes();
146
        TypeNode rangeType = ft.getRangeType();
147
148
        newTypes.insert(newTypes.end(), argTypes.begin(), argTypes.end());
149
        TypeNode nft = nm->mkFunctionType(newTypes, rangeType);
150
        new_f = nm->mkSkolem("app_uf", nft);
151
        for (const Node& v : vs)
152
        {
153
          new_f = nm->mkNode(HO_APPLY, new_f, v);
154
        }
155
        Assert(new_f.getType() == f.getType());
156
        Node eq = new_f.eqNode(f);
157
        Node seq = eq.substitute(vs.begin(), vs.end(), nvs.begin(), nvs.end());
158
        lem = nm->mkNode(
159
            FORALL, nm->mkNode(BOUND_VAR_LIST, nvs), seq);
160
      }
161
      else
162
      {
163
        // introduce skolem to make a standard APPLY_UF
164
2
        new_f = nm->mkSkolem("app_uf", f.getType());
165
2
        lem = new_f.eqNode(f);
166
      }
167
4
      Trace("uf-ho-lemma")
168
2
          << "uf-ho-lemma : Skolem definition for apply-conversion : " << lem
169
2
          << std::endl;
170
2
      d_im.lemma(lem, InferenceId::UF_HO_APP_CONV_SKOLEM);
171
2
      d_uf_std_skolem[f] = new_f;
172
    }
173
    else
174
    {
175
      new_f = (*itus).second;
176
    }
177
    // unroll the HO_APPLY, adding to the first argument position
178
    // Note arguments in the vector args begin at position 1.
179
2
    while (new_f.getKind() == HO_APPLY)
180
    {
181
      args.insert(args.begin() + 1, new_f[1]);
182
      new_f = new_f[0];
183
    }
184
  }
185
120
  Assert(TheoryUfRewriter::canUseAsApplyUfOperator(new_f));
186
120
  args[0] = new_f;
187
120
  Node ret = nm->mkNode(APPLY_UF, args);
188
120
  Assert(ret.getType() == node.getType());
189
240
  return ret;
190
}
191
192
1516
unsigned HoExtension::checkExtensionality(TheoryModel* m)
193
{
194
1516
  eq::EqualityEngine* ee = d_state.getEqualityEngine();
195
1516
  NodeManager* nm = NodeManager::currentNM();
196
1516
  unsigned num_lemmas = 0;
197
1516
  bool isCollectModel = (m != nullptr);
198
3032
  Trace("uf-ho") << "HoExtension::checkExtensionality, collectModel="
199
1516
                 << isCollectModel << "..." << std::endl;
200
3032
  std::map<TypeNode, std::vector<Node> > func_eqcs;
201
1516
  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
202
65904
  while (!eqcs_i.isFinished())
203
  {
204
64388
    Node eqc = (*eqcs_i);
205
64388
    TypeNode tn = eqc.getType();
206
32194
    if (tn.isFunction())
207
    {
208
      // if during collect model, must have an infinite type
209
      // if not during collect model, must have a finite type
210
4193
      if (tn.isInterpretedFinite() != isCollectModel)
211
      {
212
1475
        func_eqcs[tn].push_back(eqc);
213
2950
        Trace("uf-ho-debug")
214
1475
            << "  func eqc : " << tn << " : " << eqc << std::endl;
215
      }
216
    }
217
32194
    ++eqcs_i;
218
  }
219
220
2335
  for (std::map<TypeNode, std::vector<Node> >::iterator itf = func_eqcs.begin();
221
2335
       itf != func_eqcs.end();
222
       ++itf)
223
  {
224
2294
    for (unsigned j = 0, sizej = itf->second.size(); j < sizej; j++)
225
    {
226
2447
      for (unsigned k = (j + 1), sizek = itf->second.size(); k < sizek; k++)
227
      {
228
        // if these equivalence classes are not explicitly disequal, do
229
        // extensionality to ensure distinctness
230
972
        if (!ee->areDisequal(itf->second[j], itf->second[k], false))
231
        {
232
          Node deq =
233
1222
              Rewriter::rewrite(itf->second[j].eqNode(itf->second[k]).negate());
234
          // either add to model, or add lemma
235
611
          if (isCollectModel)
236
          {
237
            // Add extentionality disequality to the model.
238
            // It is important that we construct new (unconstrained) variables
239
            // k here, so that we do not generate any inconsistencies.
240
1148
            Node edeq = getExtensionalityDeq(deq, false);
241
574
            Assert(edeq.getKind() == NOT && edeq[0].getKind() == EQUAL);
242
            // introducing terms, must add required constraints, e.g. to
243
            // force equalities between APPLY_UF and HO_APPLY terms
244
1722
            for (unsigned r = 0; r < 2; r++)
245
            {
246
1148
              if (!collectModelInfoHoTerm(edeq[0][r], m))
247
              {
248
                return 1;
249
              }
250
            }
251
1148
            Trace("uf-ho-debug")
252
574
                << "Add extensionality deq to model : " << edeq << std::endl;
253
574
            if (!m->assertEquality(edeq[0][0], edeq[0][1], false))
254
            {
255
              Node eq = edeq[0][0].eqNode(edeq[0][1]);
256
              Node lem = nm->mkNode(OR, deq.negate(), eq);
257
              Trace("uf-ho") << "HoExtension: cmi extensionality lemma " << lem
258
                             << std::endl;
259
              d_im.lemma(lem, InferenceId::UF_HO_MODEL_EXTENSIONALITY);
260
              return 1;
261
            }
262
          }
263
          else
264
          {
265
            // apply extensionality lemma
266
37
            num_lemmas += applyExtensionality(deq);
267
          }
268
        }
269
      }
270
    }
271
  }
272
1516
  return num_lemmas;
273
}
274
275
5614
unsigned HoExtension::applyAppCompletion(TNode n)
276
{
277
5614
  Assert(n.getKind() == APPLY_UF);
278
279
5614
  eq::EqualityEngine* ee = d_state.getEqualityEngine();
280
  // must expand into APPLY_HO version if not there already
281
11228
  Node ret = TheoryUfRewriter::getHoApplyForApplyUf(n);
282
5614
  if (!ee->hasTerm(ret) || !ee->areEqual(ret, n))
283
  {
284
1826
    Node eq = n.eqNode(ret);
285
1826
    Trace("uf-ho-lemma") << "uf-ho-lemma : infer, by apply-expand : " << eq
286
913
                         << std::endl;
287
1826
    d_im.assertInternalFact(eq,
288
                            true,
289
                            InferenceId::UF_HO_APP_ENCODE,
290
                            PfRule::HO_APP_ENCODE,
291
                            {},
292
913
                            {n});
293
913
    return 1;
294
  }
295
9402
  Trace("uf-ho-debug") << "    ...already have " << ret << " == " << n << "."
296
4701
                       << std::endl;
297
4701
  return 0;
298
}
299
300
1925
unsigned HoExtension::checkAppCompletion()
301
{
302
1925
  Trace("uf-ho") << "HoExtension::checkApplyCompletion..." << std::endl;
303
  // compute the operators that are relevant (those for which an HO_APPLY exist)
304
3850
  std::set<TNode> rlvOp;
305
1925
  eq::EqualityEngine* ee = d_state.getEqualityEngine();
306
1925
  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
307
3850
  std::map<TNode, std::vector<Node> > apply_uf;
308
73979
  while (!eqcs_i.isFinished())
309
  {
310
72967
    Node eqc = (*eqcs_i);
311
73880
    Trace("uf-ho-debug") << "  apply completion : visit eqc " << eqc
312
36940
                         << std::endl;
313
36940
    eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee);
314
499410
    while (!eqc_i.isFinished())
315
    {
316
463383
      Node n = *eqc_i;
317
232148
      if (n.getKind() == APPLY_UF || n.getKind() == HO_APPLY)
318
      {
319
77850
        int curr_sum = 0;
320
154787
        std::map<TNode, bool> curr_rops;
321
77850
        if (n.getKind() == APPLY_UF)
322
        {
323
142912
          TNode rop = ee->getRepresentative(n.getOperator());
324
71687
          if (rlvOp.find(rop) != rlvOp.end())
325
          {
326
            // try if its operator is relevant
327
2882
            curr_sum = applyAppCompletion(n);
328
2882
            if (curr_sum > 0)
329
            {
330
462
              return curr_sum;
331
            }
332
          }
333
          else
334
          {
335
            // add to pending list
336
68805
            apply_uf[rop].push_back(n);
337
          }
338
          // Arguments are also relevant operators.
339
          // It might be possible include fewer terms here, see #1115.
340
207388
          for (unsigned k = 0; k < n.getNumChildren(); k++)
341
          {
342
136163
            if (n[k].getType().isFunction())
343
            {
344
3528
              TNode rop2 = ee->getRepresentative(n[k]);
345
1764
              curr_rops[rop2] = true;
346
            }
347
          }
348
        }
349
        else
350
        {
351
6163
          Assert(n.getKind() == HO_APPLY);
352
12326
          TNode rop = ee->getRepresentative(n[0]);
353
6163
          curr_rops[rop] = true;
354
        }
355
84860
        for (std::map<TNode, bool>::iterator itc = curr_rops.begin();
356
84860
             itc != curr_rops.end();
357
             ++itc)
358
        {
359
15395
          TNode rop = itc->first;
360
7923
          if (rlvOp.find(rop) == rlvOp.end())
361
          {
362
2956
            rlvOp.insert(rop);
363
            // now, try each pending APPLY_UF for this operator
364
            std::map<TNode, std::vector<Node> >::iterator itu =
365
2956
                apply_uf.find(rop);
366
2956
            if (itu != apply_uf.end())
367
            {
368
2835
              for (unsigned j = 0, size = itu->second.size(); j < size; j++)
369
              {
370
2732
                curr_sum = applyAppCompletion(itu->second[j]);
371
2732
                if (curr_sum > 0)
372
                {
373
451
                  return curr_sum;
374
                }
375
              }
376
            }
377
          }
378
        }
379
      }
380
231235
      ++eqc_i;
381
    }
382
36027
    ++eqcs_i;
383
  }
384
1012
  return 0;
385
}
386
387
1074
unsigned HoExtension::check()
388
{
389
1074
  Trace("uf-ho") << "HoExtension::checkHigherOrder..." << std::endl;
390
391
  // infer new facts based on apply completion until fixed point
392
  unsigned num_facts;
393
851
  do
394
  {
395
1925
    num_facts = checkAppCompletion();
396
1925
    if (d_state.isInConflict())
397
    {
398
62
      Trace("uf-ho") << "...conflict during app-completion." << std::endl;
399
62
      return 1;
400
    }
401
1863
  } while (num_facts > 0);
402
403
71258
  if (options::ufHoExt())
404
  {
405
1012
    unsigned num_lemmas = 0;
406
407
1012
    num_lemmas = checkExtensionality();
408
1012
    if (num_lemmas > 0)
409
    {
410
50
      Trace("uf-ho") << "...extensionality returned " << num_lemmas
411
25
                     << " lemmas." << std::endl;
412
25
      return num_lemmas;
413
    }
414
  }
415
416
987
  Trace("uf-ho") << "...finished check higher order." << std::endl;
417
418
987
  return 0;
419
}
420
421
504
bool HoExtension::collectModelInfoHo(TheoryModel* m,
422
                                     const std::set<Node>& termSet)
423
{
424
3632
  for (std::set<Node>::iterator it = termSet.begin(); it != termSet.end(); ++it)
425
  {
426
6256
    Node n = *it;
427
    // For model-building with ufHo, we require that APPLY_UF is always
428
    // expanded to HO_APPLY. That is, we always expand to a fully applicative
429
    // encoding during model construction.
430
3128
    if (!collectModelInfoHoTerm(n, m))
431
    {
432
      return false;
433
    }
434
  }
435
504
  int addedLemmas = checkExtensionality(m);
436
504
  return addedLemmas == 0;
437
}
438
439
4276
bool HoExtension::collectModelInfoHoTerm(Node n, TheoryModel* m)
440
{
441
4276
  if (n.getKind() == APPLY_UF)
442
  {
443
4344
    Node hn = TheoryUfRewriter::getHoApplyForApplyUf(n);
444
2172
    if (!m->assertEquality(n, hn, true))
445
    {
446
      Node eq = n.eqNode(hn);
447
      Trace("uf-ho") << "HoExtension: cmi app completion lemma " << eq
448
                     << std::endl;
449
      d_im.lemma(eq, InferenceId::UF_HO_MODEL_APP_ENCODE);
450
      return false;
451
    }
452
  }
453
4276
  return true;
454
}
455
456
}  // namespace uf
457
}  // namespace theory
458
96922
}  // namespace CVC4