GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/single_inv_partition.cpp Lines: 273 307 88.9 %
Date: 2021-03-23 Branches: 498 1034 48.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file single_inv_partition.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, 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 utility for processing single invocation synthesis conjectures
13
 **
14
 **/
15
#include "theory/quantifiers/single_inv_partition.h"
16
17
#include <sstream>
18
19
#include "expr/node_algorithm.h"
20
#include "theory/quantifiers/term_util.h"
21
#include "theory/rewriter.h"
22
23
using namespace CVC4;
24
using namespace CVC4::kind;
25
using namespace std;
26
27
namespace CVC4 {
28
namespace theory {
29
namespace quantifiers {
30
31
bool SingleInvocationPartition::init(Node n)
32
{
33
  // first, get types of arguments for functions
34
  std::vector<TypeNode> typs;
35
  std::map<Node, bool> visited;
36
  std::vector<Node> funcs;
37
  if (inferArgTypes(n, typs, visited))
38
  {
39
    return init(funcs, typs, n, false);
40
  }
41
  else
42
  {
43
    Trace("si-prt") << "Could not infer argument types." << std::endl;
44
    return false;
45
  }
46
}
47
48
126
Node SingleInvocationPartition::getFirstOrderVariableForFunction(Node f) const
49
{
50
126
  std::map<Node, Node>::const_iterator it = d_func_fo_var.find(f);
51
126
  if (it != d_func_fo_var.end())
52
  {
53
126
    return it->second;
54
  }
55
  return Node::null();
56
}
57
58
Node SingleInvocationPartition::getFunctionForFirstOrderVariable(Node v) const
59
{
60
  std::map<Node, Node>::const_iterator it = d_fo_var_to_func.find(v);
61
  if (it != d_fo_var_to_func.end())
62
  {
63
    return it->second;
64
  }
65
  return Node::null();
66
}
67
68
126
Node SingleInvocationPartition::getFunctionInvocationFor(Node f) const
69
{
70
126
  std::map<Node, Node>::const_iterator it = d_func_inv.find(f);
71
126
  if (it != d_func_inv.end())
72
  {
73
126
    return it->second;
74
  }
75
  return Node::null();
76
}
77
78
130
void SingleInvocationPartition::getFunctionVariables(
79
    std::vector<Node>& fvars) const
80
{
81
130
  fvars.insert(fvars.end(), d_func_vars.begin(), d_func_vars.end());
82
130
}
83
84
482
void SingleInvocationPartition::getFunctions(std::vector<Node>& fs) const
85
{
86
482
  fs.insert(fs.end(), d_all_funcs.begin(), d_all_funcs.end());
87
482
}
88
89
134
void SingleInvocationPartition::getSingleInvocationVariables(
90
    std::vector<Node>& sivars) const
91
{
92
134
  sivars.insert(sivars.end(), d_si_vars.begin(), d_si_vars.end());
93
134
}
94
95
4
void SingleInvocationPartition::getAllVariables(std::vector<Node>& vars) const
96
{
97
4
  vars.insert(vars.end(), d_all_vars.begin(), d_all_vars.end());
98
4
}
99
100
// gets the argument type list for the first APPLY_UF we see
101
bool SingleInvocationPartition::inferArgTypes(Node n,
102
                                              std::vector<TypeNode>& typs,
103
                                              std::map<Node, bool>& visited)
104
{
105
  if (visited.find(n) == visited.end())
106
  {
107
    visited[n] = true;
108
    if (n.getKind() != FORALL)
109
    {
110
      if (n.getKind() == APPLY_UF)
111
      {
112
        for (unsigned i = 0; i < n.getNumChildren(); i++)
113
        {
114
          typs.push_back(n[i].getType());
115
        }
116
        return true;
117
      }
118
      else
119
      {
120
        for (unsigned i = 0; i < n.getNumChildren(); i++)
121
        {
122
          if (inferArgTypes(n[i], typs, visited))
123
          {
124
            return true;
125
          }
126
        }
127
      }
128
    }
129
  }
130
  return false;
131
}
132
133
516
bool SingleInvocationPartition::init(std::vector<Node>& funcs, Node n)
134
{
135
1032
  Trace("si-prt") << "Initialize with " << funcs.size() << " input functions ("
136
516
                  << funcs << ")..." << std::endl;
137
1032
  std::vector<TypeNode> typs;
138
516
  if (!funcs.empty())
139
  {
140
1009
    TypeNode tn0 = funcs[0].getType();
141
516
    if (tn0.getNumChildren() > 0)
142
    {
143
1618
      for (unsigned i = 0, nargs = tn0.getNumChildren() - 1; i < nargs; i++)
144
      {
145
1174
        typs.push_back(tn0[i]);
146
      }
147
    }
148
1004
    for (unsigned i = 1, size = funcs.size(); i < size; i++)
149
    {
150
999
      TypeNode tni = funcs[i].getType();
151
511
      if (tni.getNumChildren() != tn0.getNumChildren())
152
      {
153
        // can't anti-skolemize functions of different sort
154
23
        Trace("si-prt") << "...type mismatch" << std::endl;
155
23
        return false;
156
      }
157
488
      else if (tni.getNumChildren() > 0)
158
      {
159
1566
        for (unsigned j = 0, nargs = tni.getNumChildren() - 1; j < nargs; j++)
160
        {
161
1163
          if (tni[j] != typs[j])
162
          {
163
            Trace("si-prt") << "...argument type mismatch" << std::endl;
164
            return false;
165
          }
166
        }
167
      }
168
    }
169
  }
170
493
  Trace("si-prt") << "#types = " << typs.size() << std::endl;
171
493
  return init(funcs, typs, n, true);
172
}
173
174
493
bool SingleInvocationPartition::init(std::vector<Node>& funcs,
175
                                     std::vector<TypeNode>& typs,
176
                                     Node n,
177
                                     bool has_funcs)
178
{
179
493
  Assert(d_arg_types.empty());
180
493
  Assert(d_input_funcs.empty());
181
493
  Assert(d_si_vars.empty());
182
493
  NodeManager* nm = NodeManager::currentNM();
183
493
  d_has_input_funcs = has_funcs;
184
493
  d_arg_types.insert(d_arg_types.end(), typs.begin(), typs.end());
185
493
  d_input_funcs.insert(d_input_funcs.end(), funcs.begin(), funcs.end());
186
493
  Trace("si-prt") << "Initialize..." << std::endl;
187
1655
  for (unsigned j = 0; j < d_arg_types.size(); j++)
188
  {
189
2324
    std::stringstream ss;
190
1162
    ss << "s_" << j;
191
2324
    Node si_v = nm->mkBoundVar(ss.str(), d_arg_types[j]);
192
1162
    d_si_vars.push_back(si_v);
193
  }
194
493
  Assert(d_si_vars.size() == d_arg_types.size());
195
1468
  for (const Node& inf : d_input_funcs)
196
  {
197
1950
    Node sk = nm->mkSkolem("_sik", inf.getType());
198
975
    d_input_func_sks.push_back(sk);
199
  }
200
493
  Trace("si-prt") << "SingleInvocationPartition::process " << n << std::endl;
201
493
  Trace("si-prt") << "Get conjuncts..." << std::endl;
202
986
  std::vector<Node> conj;
203
493
  if (collectConjuncts(n, true, conj))
204
  {
205
488
    Trace("si-prt") << "...success." << std::endl;
206
2059
    for (unsigned i = 0; i < conj.size(); i++)
207
    {
208
3142
      std::vector<Node> si_terms;
209
3142
      std::vector<Node> si_subs;
210
1571
      Trace("si-prt") << "Process conjunct : " << conj[i] << std::endl;
211
      // do DER on conjunct
212
      // Must avoid eliminating the first-order input functions in the
213
      // getQuantSimplify step below. We use a substitution to avoid this.
214
      // This makes it so that e.g. the synthesis conjecture:
215
      //   exists f. f!=0 ^ P
216
      // is not rewritten to exists f. (f=0 => false) ^ P and subsquently
217
      // rewritten to exists f. false ^ P by the elimination f -> 0.
218
1571
      Node cr = conj[i].substitute(d_input_funcs.begin(),
219
                                   d_input_funcs.end(),
220
                                   d_input_func_sks.begin(),
221
3142
                                   d_input_func_sks.end());
222
1571
      cr = TermUtil::getQuantSimplify(cr);
223
1571
      cr = cr.substitute(d_input_func_sks.begin(),
224
                         d_input_func_sks.end(),
225
                         d_input_funcs.begin(),
226
                         d_input_funcs.end());
227
1571
      if (cr != conj[i])
228
      {
229
683
        Trace("si-prt-debug") << "...rewritten to " << cr << std::endl;
230
      }
231
3142
      std::map<Node, bool> visited;
232
      // functions to arguments
233
3142
      std::vector<Node> args;
234
3142
      std::vector<Node> terms;
235
3142
      std::vector<Node> subs;
236
1571
      bool singleInvocation = true;
237
1571
      bool ngroundSingleInvocation = false;
238
1571
      if (processConjunct(cr, visited, args, terms, subs))
239
      {
240
3322
        for (unsigned j = 0; j < terms.size(); j++)
241
        {
242
1858
          si_terms.push_back(subs[j]);
243
3716
          Node op = subs[j].hasOperator() ? subs[j].getOperator() : subs[j];
244
1858
          Assert(d_func_fo_var.find(op) != d_func_fo_var.end());
245
1858
          si_subs.push_back(d_func_fo_var[op]);
246
        }
247
2928
        std::map<Node, Node> subs_map;
248
2928
        std::map<Node, Node> subs_map_rev;
249
        // normalize the invocations
250
1464
        if (!terms.empty())
251
        {
252
1425
          Assert(terms.size() == subs.size());
253
1425
          cr = cr.substitute(
254
              terms.begin(), terms.end(), subs.begin(), subs.end());
255
        }
256
2928
        std::vector<Node> children;
257
1464
        children.push_back(cr);
258
1464
        terms.clear();
259
1464
        subs.clear();
260
2928
        Trace("si-prt") << "...single invocation, with arguments: "
261
1464
                        << std::endl;
262
4557
        for (unsigned j = 0; j < args.size(); j++)
263
        {
264
3093
          Trace("si-prt") << args[j] << " ";
265
6186
          if (args[j].getKind() == BOUND_VARIABLE
266
3093
              && std::find(terms.begin(), terms.end(), args[j]) == terms.end())
267
          {
268
1274
            terms.push_back(args[j]);
269
1274
            subs.push_back(d_si_vars[j]);
270
          }
271
          else
272
          {
273
1819
            children.push_back(d_si_vars[j].eqNode(args[j]).negate());
274
          }
275
        }
276
1464
        Trace("si-prt") << std::endl;
277
2928
        cr = children.size() == 1
278
2928
                 ? children[0]
279
                 : NodeManager::currentNM()->mkNode(OR, children);
280
1464
        Assert(terms.size() == subs.size());
281
1464
        cr =
282
2928
            cr.substitute(terms.begin(), terms.end(), subs.begin(), subs.end());
283
2928
        Trace("si-prt-debug") << "...normalized invocations to " << cr
284
1464
                              << std::endl;
285
        // now must check if it has other bound variables
286
2928
        std::unordered_set<Node, NodeHashFunction> fvs;
287
1464
        expr::getFreeVariables(cr, fvs);
288
        // bound variables must be contained in the single invocation variables
289
6463
        for (const Node& bv : fvs)
290
        {
291
14997
          if (std::find(d_si_vars.begin(), d_si_vars.end(), bv)
292
14997
              == d_si_vars.end())
293
          {
294
            // getFreeVariables also collects functions in the rare case that
295
            // we are synthesizing a function with 0 arguments, take this into
296
            // account here.
297
5718
            if (std::find(d_input_funcs.begin(), d_input_funcs.end(), bv)
298
5718
                == d_input_funcs.end())
299
            {
300
96
              Trace("si-prt")
301
48
                  << "...not ground single invocation." << std::endl;
302
48
              ngroundSingleInvocation = true;
303
48
              singleInvocation = false;
304
            }
305
          }
306
        }
307
1464
        if (singleInvocation)
308
        {
309
1435
          Trace("si-prt") << "...ground single invocation" << std::endl;
310
        }
311
      }
312
      else
313
      {
314
107
        Trace("si-prt") << "...not single invocation." << std::endl;
315
107
        singleInvocation = false;
316
        // rename bound variables with maximal overlap with si_vars
317
214
        std::unordered_set<Node, NodeHashFunction> fvs;
318
107
        expr::getFreeVariables(cr, fvs);
319
214
        std::vector<Node> termsNs;
320
214
        std::vector<Node> subsNs;
321
762
        for (const Node& v : fvs)
322
        {
323
1310
          TypeNode tn = v.getType();
324
1310
          Trace("si-prt-debug")
325
655
              << "Fit bound var: " << v << " with si." << std::endl;
326
4827
          for (unsigned k = 0; k < d_si_vars.size(); k++)
327
          {
328
4548
            if (tn == d_arg_types[k])
329
            {
330
8673
              if (std::find(subsNs.begin(), subsNs.end(), d_si_vars[k])
331
8673
                  == subsNs.end())
332
              {
333
376
                termsNs.push_back(v);
334
376
                subsNs.push_back(d_si_vars[k]);
335
752
                Trace("si-prt-debug") << "  ...use " << d_si_vars[k]
336
376
                                      << std::endl;
337
376
                break;
338
              }
339
            }
340
          }
341
        }
342
107
        Assert(termsNs.size() == subsNs.size());
343
107
        cr = cr.substitute(
344
            termsNs.begin(), termsNs.end(), subsNs.begin(), subsNs.end());
345
      }
346
1571
      cr = Rewriter::rewrite(cr);
347
3142
      Trace("si-prt") << ".....got si=" << singleInvocation
348
1571
                      << ", result : " << cr << std::endl;
349
1571
      d_conjuncts[2].push_back(cr);
350
3142
      std::unordered_set<Node, NodeHashFunction> fvs;
351
1571
      expr::getFreeVariables(cr, fvs);
352
1571
      d_all_vars.insert(fvs.begin(), fvs.end());
353
1571
      if (singleInvocation)
354
      {
355
        // replace with single invocation formulation
356
1435
        Assert(si_terms.size() == si_subs.size());
357
1435
        cr = cr.substitute(
358
            si_terms.begin(), si_terms.end(), si_subs.begin(), si_subs.end());
359
1435
        cr = Rewriter::rewrite(cr);
360
1435
        Trace("si-prt") << ".....si version=" << cr << std::endl;
361
1435
        d_conjuncts[0].push_back(cr);
362
      }
363
      else
364
      {
365
136
        d_conjuncts[1].push_back(cr);
366
136
        if (ngroundSingleInvocation)
367
        {
368
29
          d_conjuncts[3].push_back(cr);
369
        }
370
      }
371
    }
372
  }
373
  else
374
  {
375
5
    Trace("si-prt") << "...failed." << std::endl;
376
5
    return false;
377
  }
378
488
  return true;
379
}
380
381
1931
bool SingleInvocationPartition::collectConjuncts(Node n,
382
                                                 bool pol,
383
                                                 std::vector<Node>& conj)
384
{
385
1931
  if ((!pol && n.getKind() == OR) || (pol && n.getKind() == AND))
386
  {
387
1560
    for (unsigned i = 0; i < n.getNumChildren(); i++)
388
    {
389
1324
      if (!collectConjuncts(n[i], pol, conj))
390
      {
391
5
        return false;
392
      }
393
    }
394
  }
395
1690
  else if (n.getKind() == NOT)
396
  {
397
114
    return collectConjuncts(n[0], !pol, conj);
398
  }
399
1576
  else if (n.getKind() == FORALL)
400
  {
401
5
    return false;
402
  }
403
  else
404
  {
405
1571
    if (!pol)
406
    {
407
112
      n = TermUtil::simpleNegate(n);
408
    }
409
1571
    Trace("si-prt") << "Conjunct : " << n << std::endl;
410
1571
    conj.push_back(n);
411
  }
412
1807
  return true;
413
}
414
415
30127
bool SingleInvocationPartition::processConjunct(Node n,
416
                                                std::map<Node, bool>& visited,
417
                                                std::vector<Node>& args,
418
                                                std::vector<Node>& terms,
419
                                                std::vector<Node>& subs)
420
{
421
30127
  std::map<Node, bool>::iterator it = visited.find(n);
422
30127
  if (it != visited.end())
423
  {
424
12157
    return true;
425
  }
426
  else
427
  {
428
17970
    bool ret = true;
429
46526
    for (unsigned i = 0; i < n.getNumChildren(); i++)
430
    {
431
28556
      if (!processConjunct(n[i], visited, args, terms, subs))
432
      {
433
256
        ret = false;
434
      }
435
    }
436
17970
    if (ret)
437
    {
438
35452
      Node f;
439
17726
      bool success = false;
440
17726
      if (d_has_input_funcs)
441
      {
442
17726
        f = n.hasOperator() ? n.getOperator() : n;
443
53178
        if (std::find(d_input_funcs.begin(), d_input_funcs.end(), f)
444
53178
            != d_input_funcs.end())
445
        {
446
2086
          success = true;
447
        }
448
      }
449
      else
450
      {
451
        if (n.getKind() == kind::APPLY_UF)
452
        {
453
          f = n.getOperator();
454
          success = true;
455
        }
456
      }
457
17726
      if (success)
458
      {
459
2086
        if (std::find(terms.begin(), terms.end(), n) == terms.end())
460
        {
461
          // check if it matches the type requirement
462
2086
          if (isAntiSkolemizableType(f))
463
          {
464
2078
            if (args.empty())
465
            {
466
              // record arguments
467
5047
              for (unsigned i = 0; i < n.getNumChildren(); i++)
468
              {
469
3481
                args.push_back(n[i]);
470
              }
471
            }
472
            else
473
            {
474
              // arguments must be the same as those already recorded
475
1682
              for (unsigned i = 0; i < n.getNumChildren(); i++)
476
              {
477
1281
                if (args[i] != n[i])
478
                {
479
222
                  Trace("si-prt-debug") << "...bad invocation : " << n
480
111
                                        << " at arg " << i << "." << std::endl;
481
111
                  ret = false;
482
111
                  break;
483
                }
484
              }
485
            }
486
2078
            if (ret)
487
            {
488
1967
              terms.push_back(n);
489
1967
              subs.push_back(d_func_inv[f]);
490
            }
491
          }
492
          else
493
          {
494
16
            Trace("si-prt-debug") << "... " << f << " is a bad operator."
495
8
                                  << std::endl;
496
8
            ret = false;
497
          }
498
        }
499
      }
500
    }
501
    //}
502
17970
    visited[n] = ret;
503
17970
    return ret;
504
  }
505
}
506
507
2086
bool SingleInvocationPartition::isAntiSkolemizableType(Node f)
508
{
509
2086
  std::map<Node, bool>::iterator it = d_funcs.find(f);
510
2086
  if (it != d_funcs.end())
511
  {
512
1204
    return it->second;
513
  }
514
  else
515
  {
516
1764
    TypeNode tn = f.getType();
517
882
    bool ret = false;
518
2558
    if (((tn.isFunction() && tn.getNumChildren() == d_arg_types.size() + 1)
519
970
         || (d_arg_types.empty() && tn.getNumChildren() == 0)))
520
    {
521
874
      ret = true;
522
1748
      std::vector<Node> children;
523
874
      children.push_back(f);
524
      // TODO: permutations of arguments
525
3115
      for (unsigned i = 0; i < d_arg_types.size(); i++)
526
      {
527
2241
        children.push_back(d_si_vars[i]);
528
2241
        if (tn[i] != d_arg_types[i])
529
        {
530
          ret = false;
531
          break;
532
        }
533
      }
534
874
      if (ret)
535
      {
536
1748
        Node t;
537
874
        if (children.size() > 1)
538
        {
539
794
          t = NodeManager::currentNM()->mkNode(kind::APPLY_UF, children);
540
        }
541
        else
542
        {
543
80
          t = children[0];
544
        }
545
874
        d_func_inv[f] = t;
546
1748
        std::stringstream ss;
547
874
        ss << "F_" << f;
548
1748
        TypeNode rt;
549
874
        if (d_arg_types.empty())
550
        {
551
80
          rt = tn;
552
        }
553
        else
554
        {
555
794
          rt = tn.getRangeType();
556
        }
557
1748
        Node v = NodeManager::currentNM()->mkBoundVar(ss.str(), rt);
558
874
        d_func_fo_var[f] = v;
559
874
        d_fo_var_to_func[v] = f;
560
874
        d_func_vars.push_back(v);
561
874
        d_all_funcs.push_back(f);
562
      }
563
    }
564
882
    d_funcs[f] = ret;
565
882
    return ret;
566
  }
567
}
568
569
134
Node SingleInvocationPartition::getConjunct(int index)
570
{
571
134
  return d_conjuncts[index].empty() ? NodeManager::currentNM()->mkConst(true)
572
134
                                    : (d_conjuncts[index].size() == 1
573
79
                                           ? d_conjuncts[index][0]
574
                                           : NodeManager::currentNM()->mkNode(
575
347
                                                 AND, d_conjuncts[index]));
576
}
577
578
488
void SingleInvocationPartition::debugPrint(const char* c)
579
{
580
488
  Trace(c) << "Single invocation variables : ";
581
1643
  for (unsigned i = 0; i < d_si_vars.size(); i++)
582
  {
583
1155
    Trace(c) << d_si_vars[i] << " ";
584
  }
585
488
  Trace(c) << std::endl;
586
488
  Trace(c) << "Functions : " << std::endl;
587
1370
  for (std::map<Node, bool>::iterator it = d_funcs.begin(); it != d_funcs.end();
588
       ++it)
589
  {
590
882
    Trace(c) << "  " << it->first << " : ";
591
882
    if (it->second)
592
    {
593
1748
      Trace(c) << d_func_inv[it->first] << " " << d_func_fo_var[it->first]
594
874
               << std::endl;
595
    }
596
    else
597
    {
598
8
      Trace(c) << "not incorporated." << std::endl;
599
    }
600
  }
601
2440
  for (unsigned i = 0; i < 4; i++)
602
  {
603
3416
    Trace(c) << (i == 0 ? "Single invocation"
604
2440
                        : (i == 1 ? "Non-single invocation"
605
976
                                  : (i == 2 ? "All"
606
                                            : "Non-ground single invocation")));
607
1952
    Trace(c) << " conjuncts: " << std::endl;
608
5123
    for (unsigned j = 0; j < d_conjuncts[i].size(); j++)
609
    {
610
3171
      Trace(c) << "  " << (j + 1) << " : " << d_conjuncts[i][j] << std::endl;
611
    }
612
  }
613
488
  Trace(c) << std::endl;
614
488
}
615
616
} /* namespace CVC4::theory::quantifiers */
617
} /* namespace CVC4::theory */
618
26685
} /* namespace CVC4 */