GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/sygus_unif_io.cpp Lines: 746 822 90.8 %
Date: 2021-03-22 Branches: 1344 3296 40.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_unif_io.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, Haniel Barbosa
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 sygus_unif_io
13
 **/
14
15
#include "theory/quantifiers/sygus/sygus_unif_io.h"
16
17
#include "options/quantifiers_options.h"
18
#include "theory/evaluator.h"
19
#include "theory/quantifiers/sygus/example_infer.h"
20
#include "theory/quantifiers/sygus/synth_conjecture.h"
21
#include "theory/quantifiers/sygus/term_database_sygus.h"
22
#include "theory/quantifiers/term_util.h"
23
#include "theory/quantifiers_engine.h"
24
#include "theory/rewriter.h"
25
#include "theory/strings/word.h"
26
#include "util/random.h"
27
28
#include <math.h>
29
30
using namespace CVC4::kind;
31
32
namespace CVC4 {
33
namespace theory {
34
namespace quantifiers {
35
36
84
UnifContextIo::UnifContextIo() : d_curr_role(role_invalid)
37
{
38
84
  d_true = NodeManager::currentNM()->mkConst(true);
39
84
  d_false = NodeManager::currentNM()->mkConst(false);
40
84
}
41
42
19812
NodeRole UnifContextIo::getCurrentRole() { return d_curr_role; }
43
44
1071
bool UnifContextIo::updateContext(SygusUnifIo* sui,
45
                                  std::vector<Node>& vals,
46
                                  bool pol)
47
{
48
1071
  Assert(d_vals.size() == vals.size());
49
1071
  bool changed = false;
50
2142
  Node poln = pol ? d_true : d_false;
51
22695
  for (size_t i = 0, vsize = vals.size(); i < vsize; i++)
52
  {
53
43248
    Node v = vals[i];
54
21624
    if (v.isNull())
55
    {
56
      // nothing can be inferred if the evaluation is unknown, e.g. if using
57
      // partial functions.
58
      continue;
59
    }
60
21624
    if (v != poln)
61
    {
62
10709
      if (d_vals[i] == d_true)
63
      {
64
8568
        d_vals[i] = d_false;
65
8568
        changed = true;
66
      }
67
    }
68
  }
69
1071
  if (changed)
70
  {
71
1067
    d_visit_role.clear();
72
  }
73
2142
  return changed;
74
}
75
76
2082
bool UnifContextIo::updateStringPosition(SygusUnifIo* sui,
77
                                         std::vector<size_t>& pos,
78
                                         NodeRole nrole)
79
{
80
2082
  Assert(pos.size() == d_str_pos.size());
81
2082
  bool changed = false;
82
25980
  for (unsigned i = 0; i < pos.size(); i++)
83
  {
84
23898
    if (pos[i] > 0)
85
    {
86
15462
      d_str_pos[i] += pos[i];
87
15462
      changed = true;
88
    }
89
  }
90
2082
  if (changed)
91
  {
92
2022
    d_visit_role.clear();
93
  }
94
2082
  d_curr_role = nrole;
95
2082
  return changed;
96
}
97
98
929
void UnifContextIo::initialize(SygusUnifIo* sui)
99
{
100
  // clear previous data
101
929
  d_vals.clear();
102
929
  d_str_pos.clear();
103
929
  d_curr_role = role_equal;
104
929
  d_visit_role.clear();
105
106
  // initialize with #examples
107
929
  unsigned sz = sui->d_examples.size();
108
15643
  for (unsigned i = 0; i < sz; i++)
109
  {
110
14714
    d_vals.push_back(d_true);
111
  }
112
113
929
  if (!sui->d_examples_out.empty())
114
  {
115
    // output type of the examples
116
1858
    TypeNode exotn = sui->d_examples_out[0].getType();
117
118
929
    if (exotn.isStringLike())
119
    {
120
7792
      for (unsigned i = 0; i < sz; i++)
121
      {
122
7352
        d_str_pos.push_back(0);
123
      }
124
    }
125
  }
126
929
  d_visit_role.clear();
127
929
}
128
129
5490
void UnifContextIo::getCurrentStrings(SygusUnifIo* sui,
130
                                      const std::vector<Node>& vals,
131
                                      std::vector<Node>& ex_vals)
132
{
133
5490
  bool isPrefix = d_curr_role == role_string_prefix;
134
10980
  Node dummy;
135
77652
  for (unsigned i = 0; i < vals.size(); i++)
136
  {
137
72162
    if (d_vals[i] == sui->d_true)
138
    {
139
52526
      Assert(vals[i].isConst());
140
52526
      unsigned pos_value = d_str_pos[i];
141
52526
      if (pos_value > 0)
142
      {
143
35392
        Assert(d_curr_role != role_invalid);
144
70784
        Node s = vals[i];
145
35392
        size_t sSize = strings::Word::getLength(s);
146
35392
        Assert(pos_value <= sSize);
147
35392
        ex_vals.push_back(isPrefix
148
70784
                              ? strings::Word::suffix(s, sSize - pos_value)
149
                              : strings::Word::prefix(s, sSize - pos_value));
150
      }
151
      else
152
      {
153
17134
        ex_vals.push_back(vals[i]);
154
      }
155
    }
156
    else
157
    {
158
      // irrelevant, add dummy
159
19636
      ex_vals.push_back(dummy);
160
    }
161
  }
162
5490
}
163
164
15154
bool UnifContextIo::getStringIncrement(SygusUnifIo* sui,
165
                                       bool isPrefix,
166
                                       const std::vector<Node>& ex_vals,
167
                                       const std::vector<Node>& vals,
168
                                       std::vector<size_t>& inc,
169
                                       size_t& tot)
170
{
171
62704
  for (unsigned j = 0; j < vals.size(); j++)
172
  {
173
60158
    size_t ival = 0;
174
60158
    if (d_vals[j] == sui->d_true)
175
    {
176
      // example is active in this context
177
33158
      if (!vals[j].isConst())
178
      {
179
        // the value is unknown, thus we cannot use it to increment the strings
180
        // position
181
12618
        return false;
182
      }
183
33148
      ival = strings::Word::getLength(vals[j]);
184
33148
      size_t exjLen = strings::Word::getLength(ex_vals[j]);
185
33148
      if (ival <= exjLen)
186
      {
187
104050
        if (!(isPrefix ? strings::Word::strncmp(ex_vals[j], vals[j], ival)
188
71636
                       : strings::Word::rstrncmp(ex_vals[j], vals[j], ival)))
189
        {
190
11864
          Trace("sygus-sui-dt-debug") << "X";
191
11864
          return false;
192
        }
193
      }
194
      else
195
      {
196
734
        Trace("sygus-sui-dt-debug") << "X";
197
734
        return false;
198
      }
199
20550
      Trace("sygus-sui-dt-debug") << ival;
200
20550
      tot += ival;
201
    }
202
    else
203
    {
204
      // inactive in this context
205
27000
      Trace("sygus-sui-dt-debug") << "-";
206
    }
207
47550
    inc.push_back(ival);
208
  }
209
2546
  return true;
210
}
211
16882
bool UnifContextIo::isStringSolved(SygusUnifIo* sui,
212
                                   const std::vector<Node>& ex_vals,
213
                                   const std::vector<Node>& vals)
214
{
215
50158
  for (unsigned j = 0; j < vals.size(); j++)
216
  {
217
50024
    if (d_vals[j] == sui->d_true)
218
    {
219
      // example is active in this context
220
17096
      if (!vals[j].isConst())
221
      {
222
        // value is unknown, thus it does not solve
223
14
        return false;
224
      }
225
17082
      if (ex_vals[j] != vals[j])
226
      {
227
16734
        return false;
228
      }
229
    }
230
  }
231
134
  return true;
232
}
233
234
// status : 0 : exact, -1 : vals is subset, 1 : vals is superset
235
26381
Node SubsumeTrie::addTermInternal(Node t,
236
                                  const std::vector<Node>& vals,
237
                                  bool pol,
238
                                  std::vector<Node>& subsumed,
239
                                  bool spol,
240
                                  unsigned index,
241
                                  int status,
242
                                  bool checkExistsOnly,
243
                                  bool checkSubsume)
244
{
245
26381
  if (index == vals.size())
246
  {
247
1433
    if (status == 0)
248
    {
249
      // set the term if checkExistsOnly = false
250
1026
      if (d_term.isNull() && !checkExistsOnly)
251
      {
252
721
        d_term = t;
253
      }
254
    }
255
407
    else if (status == 1)
256
    {
257
325
      Assert(checkSubsume);
258
      // found a subsumed term
259
325
      if (!d_term.isNull())
260
      {
261
325
        subsumed.push_back(d_term);
262
        // If we are only interested in feasibility, we could set d_term to null
263
        // here. However, d_term still could be useful, since it may be
264
        // smaller than t and suffice as a solution under some condition.
265
        // As a simple example, consider predicate synthesis and a case where we
266
        // enumerate a C that is correct for all I/O points whose output is
267
        // true. Then, C subsumes true. However, true may be preferred, e.g.
268
        // to generate a solution ite( C, true, D ) instead of ite( C, C, D ),
269
        // since true is conditionally correct under C, and is smaller than C.
270
      }
271
    }
272
    else
273
    {
274
82
      Assert(!checkExistsOnly && checkSubsume);
275
    }
276
1433
    return d_term;
277
  }
278
24948
  NodeManager* nm = NodeManager::currentNM();
279
  // the current value
280
24948
  Assert(pol || (vals[index].isConst() && vals[index].getType().isBoolean()));
281
49896
  Node cv = pol ? vals[index] : nm->mkConst(!vals[index].getConst<bool>());
282
  // if checkExistsOnly = false, check if the current value is subsumed if
283
  // checkSubsume = true, if so, don't add
284
24948
  if (!checkExistsOnly && checkSubsume)
285
  {
286
2254
    Assert(cv.isConst() && cv.getType().isBoolean());
287
4288
    std::vector<bool> check_subsumed_by;
288
2254
    if (status == 0)
289
    {
290
1750
      if (!cv.getConst<bool>())
291
      {
292
837
        check_subsumed_by.push_back(spol);
293
      }
294
    }
295
504
    else if (status == -1)
296
    {
297
196
      check_subsumed_by.push_back(spol);
298
196
      if (!cv.getConst<bool>())
299
      {
300
108
        check_subsumed_by.push_back(!spol);
301
      }
302
    }
303
    // check for subsumed nodes
304
3153
    for (unsigned i = 0, size = check_subsumed_by.size(); i < size; i++)
305
    {
306
1119
      bool csbi = check_subsumed_by[i];
307
2018
      Node csval = nm->mkConst(csbi);
308
      // check if subsumed
309
1119
      std::map<Node, SubsumeTrie>::iterator itc = d_children.find(csval);
310
1119
      if (itc != d_children.end())
311
      {
312
278
        Node ret = itc->second.addTermInternal(t,
313
                                               vals,
314
                                               pol,
315
                                               subsumed,
316
                                               spol,
317
                                               index + 1,
318
                                               -1,
319
                                               checkExistsOnly,
320
336
                                               checkSubsume);
321
        // ret subsumes t
322
278
        if (!ret.isNull())
323
        {
324
220
          return ret;
325
        }
326
      }
327
    }
328
  }
329
49456
  Node ret;
330
49456
  std::vector<bool> check_subsume;
331
24728
  if (status == 0)
332
  {
333
17252
    if (checkExistsOnly)
334
    {
335
      std::map<Node, SubsumeTrie>::iterator itc = d_children.find(cv);
336
      if (itc != d_children.end())
337
      {
338
        ret = itc->second.addTermInternal(t,
339
                                          vals,
340
                                          pol,
341
                                          subsumed,
342
                                          spol,
343
                                          index + 1,
344
                                          0,
345
                                          checkExistsOnly,
346
                                          checkSubsume);
347
      }
348
    }
349
    else
350
    {
351
17252
      Assert(spol);
352
17252
      ret = d_children[cv].addTermInternal(t,
353
                                           vals,
354
                                           pol,
355
                                           subsumed,
356
                                           spol,
357
                                           index + 1,
358
                                           0,
359
                                           checkExistsOnly,
360
                                           checkSubsume);
361
17252
      if (ret != t)
362
      {
363
        // we were subsumed by ret, return
364
5984
        return ret;
365
      }
366
    }
367
11268
    if (checkSubsume)
368
    {
369
1318
      Assert(cv.isConst() && cv.getType().isBoolean());
370
      // check for subsuming
371
1318
      if (cv.getConst<bool>())
372
      {
373
742
        check_subsume.push_back(!spol);
374
      }
375
    }
376
  }
377
7476
  else if (status == 1)
378
  {
379
7418
    Assert(checkSubsume);
380
7418
    Assert(cv.isConst() && cv.getType().isBoolean());
381
7418
    check_subsume.push_back(!spol);
382
7418
    if (cv.getConst<bool>())
383
    {
384
4453
      check_subsume.push_back(spol);
385
    }
386
  }
387
18744
  if (checkSubsume)
388
  {
389
    // check for subsumed terms
390
21407
    for (unsigned i = 0, size = check_subsume.size(); i < size; i++)
391
    {
392
25226
      Node csval = nm->mkConst<bool>(check_subsume[i]);
393
12613
      std::map<Node, SubsumeTrie>::iterator itc = d_children.find(csval);
394
12613
      if (itc != d_children.end())
395
      {
396
5965
        itc->second.addTermInternal(t,
397
                                    vals,
398
                                    pol,
399
                                    subsumed,
400
                                    spol,
401
                                    index + 1,
402
                                    1,
403
                                    checkExistsOnly,
404
                                    checkSubsume);
405
        // clean up
406
5965
        if (itc->second.isEmpty())
407
        {
408
          Assert(!checkExistsOnly);
409
          d_children.erase(csval);
410
        }
411
      }
412
    }
413
  }
414
18744
  return ret;
415
}
416
417
260
Node SubsumeTrie::addTerm(Node t,
418
                          const std::vector<Node>& vals,
419
                          bool pol,
420
                          std::vector<Node>& subsumed)
421
{
422
260
  return addTermInternal(t, vals, pol, subsumed, true, 0, 0, false, true);
423
}
424
425
848
Node SubsumeTrie::addCond(Node c, const std::vector<Node>& vals, bool pol)
426
{
427
1696
  std::vector<Node> subsumed;
428
1696
  return addTermInternal(c, vals, pol, subsumed, true, 0, 0, false, false);
429
}
430
431
void SubsumeTrie::getSubsumed(const std::vector<Node>& vals,
432
                              bool pol,
433
                              std::vector<Node>& subsumed)
434
{
435
  addTermInternal(Node::null(), vals, pol, subsumed, true, 0, 1, true, true);
436
}
437
438
1778
void SubsumeTrie::getSubsumedBy(const std::vector<Node>& vals,
439
                                bool pol,
440
                                std::vector<Node>& subsumed_by)
441
{
442
  // flip polarities
443
3556
  addTermInternal(
444
5334
      Node::null(), vals, !pol, subsumed_by, false, 0, 1, true, true);
445
1778
}
446
447
105357
void SubsumeTrie::getLeavesInternal(const std::vector<Node>& vals,
448
                                    bool pol,
449
                                    std::map<int, std::vector<Node> >& v,
450
                                    unsigned index,
451
                                    int status)
452
{
453
105357
  if (index == vals.size())
454
  {
455
    // by convention, if we did not test any points, then we consider the
456
    // evaluation along the current path to be always false.
457
5623
    int rstatus = status == -2 ? -1 : status;
458
5623
    Assert(!d_term.isNull());
459
5623
    Assert(std::find(v[rstatus].begin(), v[rstatus].end(), d_term)
460
           == v[rstatus].end());
461
5623
    v[rstatus].push_back(d_term);
462
  }
463
  else
464
  {
465
99734
    Assert(vals[index].isConst() && vals[index].getType().isBoolean());
466
99734
    bool curr_val_true = vals[index].getConst<bool>() == pol;
467
202865
    for (std::map<Node, SubsumeTrie>::iterator it = d_children.begin();
468
202865
         it != d_children.end();
469
         ++it)
470
    {
471
103131
      int new_status = status;
472
103131
      bool success = true;
473
      // If the current value is true, then this is a relevant point.
474
      // We must consider the value of this child.
475
103131
      if (curr_val_true)
476
      {
477
62403
        if (it->first.isNull())
478
        {
479
          // The value of this child is unknown on this point, hence we
480
          // do not recurse
481
57
          success = false;
482
        }
483
62346
        else if (status != 0)
484
        {
485
          // if the status is not zero (indicating that we have a mix of T/F),
486
          // then we must compute the new status.
487
46073
          Assert(it->first.getType().isBoolean());
488
46073
          Assert(it->first.isConst());
489
46073
          new_status = (it->first.getConst<bool>() ? 1 : -1);
490
46073
          if (status != -2 && new_status != status)
491
          {
492
1468
            new_status = 0;
493
          }
494
        }
495
      }
496
103131
      if (success)
497
      {
498
103074
        it->second.getLeavesInternal(vals, pol, v, index + 1, new_status);
499
      }
500
    }
501
  }
502
105357
}
503
504
2283
void SubsumeTrie::getLeaves(const std::vector<Node>& vals,
505
                            bool pol,
506
                            std::map<int, std::vector<Node> >& v)
507
{
508
2283
  getLeavesInternal(vals, pol, v, 0, -2);
509
2283
}
510
511
84
SygusUnifIo::SygusUnifIo(SynthConjecture* p)
512
    : d_parent(p),
513
      d_check_sol(false),
514
      d_cond_count(0),
515
      d_sol_term_size(0),
516
      d_sol_cons_nondet(false),
517
84
      d_solConsUsingInfoGain(false)
518
{
519
84
  d_true = NodeManager::currentNM()->mkConst(true);
520
84
  d_false = NodeManager::currentNM()->mkConst(false);
521
84
}
522
523
168
SygusUnifIo::~SygusUnifIo() {}
524
525
84
void SygusUnifIo::initializeCandidate(
526
    QuantifiersEngine* qe,
527
    Node f,
528
    std::vector<Node>& enums,
529
    std::map<Node, std::vector<Node>>& strategy_lemmas)
530
{
531
84
  d_candidate = f;
532
  // copy the examples from the parent
533
84
  ExampleInfer* ei = d_parent->getExampleInfer();
534
84
  d_examples.clear();
535
84
  d_examples_out.clear();
536
  // copy the examples
537
84
  if (ei->hasExamples(f))
538
  {
539
759
    for (unsigned i = 0, nex = ei->getNumExamples(f); i < nex; i++)
540
    {
541
1350
      std::vector<Node> input;
542
675
      ei->getExample(f, i, input);
543
1350
      Node output = ei->getExampleOut(f, i);
544
675
      d_examples.push_back(input);
545
675
      d_examples_out.push_back(output);
546
    }
547
  }
548
84
  d_ecache.clear();
549
84
  SygusUnif::initializeCandidate(qe, f, enums, strategy_lemmas);
550
  // learn redundant operators based on the strategy
551
84
  d_strategy[f].staticLearnRedundantOps(strategy_lemmas);
552
84
}
553
554
1006
void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
555
{
556
2012
  Trace("sygus-sui-enum") << "Notify enumeration for " << e << " : " << v
557
1006
                          << std::endl;
558
2012
  Node c = d_candidate;
559
1006
  Assert(!d_examples.empty());
560
1006
  Assert(d_examples.size() == d_examples_out.size());
561
562
1006
  EnumInfo& ei = d_strategy[c].getEnumInfo(e);
563
  // The explanation for why the current value should be excluded in future
564
  // iterations.
565
2012
  Node exp_exc;
566
567
2012
  std::vector<Node> base_results;
568
2012
  TypeNode xtn = e.getType();
569
2012
  Node bv = d_tds->sygusToBuiltin(v, xtn);
570
1006
  bv = d_tds->getExtRewriter()->extendedRewrite(bv);
571
1006
  Trace("sygus-sui-enum") << "PBE Compute Examples for " << bv << std::endl;
572
  // compte the results (should be cached)
573
1006
  ExampleEvalCache* eec = d_parent->getExampleEvalCache(e);
574
1006
  Assert(eec != nullptr);
575
  // Evaluate, which should be cached (assuming we have performed example-based
576
  // symmetry breaking on bv). Moreover don't cache the result in the case it
577
  // is not there already, since we won't need this evaluation anywhere outside
578
  // of this class.
579
1006
  eec->evaluateVec(bv, base_results);
580
  // get the results for each slave enumerator
581
2012
  std::map<Node, std::vector<Node>> srmap;
582
2916
  for (const Node& xs : ei.d_enum_slave)
583
  {
584
1910
    Assert(srmap.find(xs) == srmap.end());
585
1910
    EnumInfo& eiv = d_strategy[c].getEnumInfo(xs);
586
3820
    Node templ = eiv.d_template;
587
1910
    if (!templ.isNull())
588
    {
589
      // Substitute and evaluate, notice that the template skeleton may
590
      // involve the sygus variables e.g. (>= x _) where x is a sygus
591
      // variable, hence we must compute the substituted template before
592
      // calling the evaluator.
593
802
      TNode targ = eiv.d_template_arg;
594
802
      TNode tbv = bv;
595
802
      Node stempl = templ.substitute(targ, tbv);
596
802
      std::vector<Node> sresults;
597
401
      eec->evaluateVec(stempl, sresults);
598
401
      srmap[xs] = sresults;
599
    }
600
    else
601
    {
602
1509
      srmap[xs] = base_results;
603
    }
604
  }
605
606
  // is it excluded for domain-specific reason?
607
2012
  std::vector<Node> exp_exc_vec;
608
1006
  Assert(d_tds->isEnumerator(e));
609
1006
  bool isPassive = d_tds->isPassiveEnumerator(e);
610
1006
  if (getExplanationForEnumeratorExclude(e, v, base_results, exp_exc_vec))
611
  {
612
96
    if (isPassive)
613
    {
614
      Assert(!exp_exc_vec.empty());
615
      exp_exc = exp_exc_vec.size() == 1
616
                    ? exp_exc_vec[0]
617
                    : NodeManager::currentNM()->mkNode(AND, exp_exc_vec);
618
    }
619
192
    Trace("sygus-sui-enum")
620
96
        << "  ...fail : term is excluded (domain-specific)" << std::endl;
621
  }
622
  else
623
  {
624
    // notify all slaves
625
910
    Assert(!ei.d_enum_slave.empty());
626
    // explanation for why this value should be excluded
627
2580
    for (unsigned s = 0; s < ei.d_enum_slave.size(); s++)
628
    {
629
3340
      Node xs = ei.d_enum_slave[s];
630
1670
      EnumInfo& eiv = d_strategy[c].getEnumInfo(xs);
631
1670
      EnumCache& ecv = d_ecache[xs];
632
1670
      Trace("sygus-sui-enum") << "Process " << xs << " from " << s << std::endl;
633
      // bool prevIsCover = false;
634
1670
      if (eiv.getRole() == enum_io)
635
      {
636
822
        Trace("sygus-sui-enum") << "   IO-Eval of ";
637
        // prevIsCover = eiv.isFeasible();
638
      }
639
      else
640
      {
641
848
        Trace("sygus-sui-enum") << "Evaluation of ";
642
      }
643
1670
      Trace("sygus-sui-enum") << xs << " : ";
644
      // evaluate all input/output examples
645
3340
      std::vector<Node> results;
646
3340
      std::map<Node, bool> cond_vals;
647
1670
      std::map<Node, std::vector<Node>>::iterator itsr = srmap.find(xs);
648
1670
      Trace("sygus-sui-debug") << " {" << itsr->second << "} ";
649
1670
      Assert(itsr != srmap.end());
650
26810
      for (unsigned j = 0, size = itsr->second.size(); j < size; j++)
651
      {
652
50280
        Node res = itsr->second[j];
653
        // The value of this term for this example, or the truth value of
654
        // the I/O pair if the role of this enumerator is enum_io.
655
50280
        Node resb;
656
25140
        if (eiv.getRole() == enum_io)
657
        {
658
19112
          Node out = d_examples_out[j];
659
9556
          Assert(out.isConst());
660
          // If the result is not constant, then we assume that it does
661
          // not satisfy the example. This is a safe underapproximation
662
          // of the good behavior of the current term, that is, we only
663
          // produce solutions whose values are fully evaluatable on all input
664
          // points. Notice that terms may be used as leaves of decision
665
          // trees that are fully evaluatable on points in that branch, but
666
          // are not evaluatable on others, e.g. (head x) in the solution:
667
          //   (ite ((_ is cons) x) (head x) 5)
668
9556
          resb = (res.isConst() && res == out) ? d_true : d_false;
669
        }
670
        else
671
        {
672
          // We only set resb if it is constant, otherwise it remains null.
673
          // This indicates its value cannot be determined.
674
15584
          if (res.isConst())
675
          {
676
15536
            resb = res;
677
          }
678
        }
679
25140
        cond_vals[resb] = true;
680
25140
        results.push_back(resb);
681
25140
        if (Trace.isOn("sygus-sui-enum"))
682
        {
683
          if (resb.isNull())
684
          {
685
            Trace("sygus-sui-enum") << "_";
686
          }
687
          else if (resb.getType().isBoolean())
688
          {
689
            Trace("sygus-sui-enum") << (resb == d_true ? "1" : "0");
690
          }
691
          else
692
          {
693
            Trace("sygus-sui-enum") << "?";
694
          }
695
        }
696
      }
697
1670
      bool keep = false;
698
1670
      if (eiv.getRole() == enum_io)
699
      {
700
        // latter is the degenerate case of no examples
701
822
        if (cond_vals.find(d_true) != cond_vals.end() || cond_vals.empty())
702
        {
703
          // check subsumbed/subsuming
704
520
          std::vector<Node> subsume;
705
260
          if (cond_vals.find(d_false) == cond_vals.end())
706
          {
707
33
            Assert(cond_vals.size() == 1);
708
            // it is the entire solution, we are done
709
66
            Trace("sygus-sui-enum")
710
33
                << "  ...success, full solution added to PBE pool : "
711
33
                << d_tds->sygusToBuiltin(v) << std::endl;
712
33
            if (!ecv.isSolved())
713
            {
714
33
              ecv.setSolved(v);
715
              // it subsumes everything
716
33
              ecv.d_term_trie.clear();
717
33
              ecv.d_term_trie.addTerm(v, results, true, subsume);
718
            }
719
33
            keep = true;
720
          }
721
          else
722
          {
723
454
            Node val = ecv.d_term_trie.addTerm(v, results, true, subsume);
724
227
            if (val == v)
725
            {
726
110
              Trace("sygus-sui-enum") << "  ...success";
727
110
              if (!subsume.empty())
728
              {
729
30
                ecv.d_enum_subsume.insert(
730
60
                    ecv.d_enum_subsume.end(), subsume.begin(), subsume.end());
731
60
                Trace("sygus-sui-enum")
732
30
                    << " and subsumed " << subsume.size() << " terms";
733
              }
734
220
              Trace("sygus-sui-enum")
735
220
                  << "!   add to PBE pool : " << d_tds->sygusToBuiltin(v)
736
110
                  << std::endl;
737
110
              keep = true;
738
            }
739
            else
740
            {
741
117
              Assert(subsume.empty());
742
117
              Trace("sygus-sui-enum") << "  ...fail : subsumed" << std::endl;
743
            }
744
          }
745
        }
746
        else
747
        {
748
1124
          Trace("sygus-sui-enum")
749
562
              << "  ...fail : it does not satisfy examples." << std::endl;
750
        }
751
      }
752
      else
753
      {
754
        // must be unique up to examples
755
1696
        Node val = ecv.d_term_trie.addCond(v, results, true);
756
848
        if (val == v)
757
        {
758
1156
          Trace("sygus-sui-enum") << "  ...success!   add to PBE pool : "
759
578
                                  << d_tds->sygusToBuiltin(v) << std::endl;
760
578
          keep = true;
761
        }
762
        else
763
        {
764
540
          Trace("sygus-sui-enum")
765
270
              << "  ...fail : term is not unique" << std::endl;
766
        }
767
      }
768
1670
      if (keep)
769
      {
770
        // notify to retry the build of solution
771
721
        d_check_sol = true;
772
721
        d_cond_count++;
773
721
        ecv.addEnumValue(v, results);
774
      }
775
    }
776
  }
777
778
1006
  if (isPassive)
779
  {
780
    // exclude this value on subsequent iterations
781
14
    if (exp_exc.isNull())
782
    {
783
14
      Trace("sygus-sui-enum-lemma") << "Use basic exclusion." << std::endl;
784
      // if we did not already explain why this should be excluded, use default
785
14
      exp_exc = d_tds->getExplain()->getExplanationForEquality(e, v);
786
    }
787
14
    exp_exc = exp_exc.negate();
788
28
    Trace("sygus-sui-enum-lemma")
789
14
        << "SygusUnifIo : enumeration exclude lemma : " << exp_exc << std::endl;
790
14
    lemmas.push_back(exp_exc);
791
  }
792
1006
}
793
794
906
bool SygusUnifIo::constructSolution(std::vector<Node>& sols,
795
                                    std::vector<Node>& lemmas)
796
{
797
1812
  Node sol = constructSolutionNode(lemmas);
798
906
  if (!sol.isNull())
799
  {
800
93
    sols.push_back(sol);
801
93
    return true;
802
  }
803
813
  return false;
804
}
805
806
906
Node SygusUnifIo::constructSolutionNode(std::vector<Node>& lemmas)
807
{
808
1812
  Node c = d_candidate;
809
906
  if (!d_solution.isNull() && !options::sygusStream())
810
  {
811
    // already has a solution
812
10
    return d_solution;
813
  }
814
  // only check if an enumerator updated
815
896
  if (d_check_sol)
816
  {
817
1014
    Trace("sygus-pbe") << "Construct solution, #iterations = " << d_cond_count
818
507
                       << std::endl;
819
507
    d_check_sol = false;
820
931
    Node newSolution;
821
507
    d_solConsUsingInfoGain = false;
822
    // try multiple times if we have done multiple conditions, due to
823
    // non-determinism
824
989
    for (unsigned i = 0; i <= d_cond_count; i++)
825
    {
826
929
      Trace("sygus-pbe-dt") << "ConstructPBE for candidate: " << c << std::endl;
827
      // initialize a call to construct solution
828
929
      initializeConstructSol();
829
929
      initializeConstructSolFor(c);
830
      // call the virtual construct solution method
831
1411
      Node e = d_strategy[c].getRootEnumerator();
832
1411
      Node vcc = constructSol(c, e, role_equal, 1, lemmas);
833
      // if we constructed the solution, and we either did not previously have
834
      // a solution, or the new solution is better (smaller).
835
1858
      if (!vcc.isNull()
836
1958
          && (d_solution.isNull()
837
178
              || (!d_solution.isNull()
838
1107
                  && d_tds->getSygusTermSize(vcc) < d_sol_term_size)))
839
      {
840
100
        if (Trace.isOn("sygus-pbe"))
841
        {
842
          Trace("sygus-pbe") << "**** SygusUnif SOLVED : " << c << " = ";
843
          TermDbSygus::toStreamSygus("sygus-pbe", vcc);
844
          Trace("sygus-pbe") << std::endl;
845
          Trace("sygus-pbe") << "...solved at iteration " << i << std::endl;
846
        }
847
100
        d_solution = vcc;
848
100
        newSolution = vcc;
849
100
        d_sol_term_size = d_tds->getSygusTermSize(vcc);
850
200
        Trace("sygus-pbe-sol")
851
100
            << "PBE solution size: " << d_sol_term_size << std::endl;
852
        // We've determined its feasible, now, enable information gain and
853
        // retry. We do this since information gain comes with an overhead,
854
        // and we want testing feasibility to be fast.
855
100
        if (!d_solConsUsingInfoGain)
856
        {
857
          // we permanently enable information gain and minimality now
858
83
          d_solConsUsingInfoGain = true;
859
83
          d_enableMinimality = true;
860
83
          i = 0;
861
        }
862
      }
863
829
      else if (!d_sol_cons_nondet)
864
      {
865
447
        break;
866
      }
867
    }
868
507
    if (!newSolution.isNull())
869
    {
870
83
      return newSolution;
871
    }
872
424
    Trace("sygus-pbe") << "...failed to solve." << std::endl;
873
  }
874
813
  return Node::null();
875
}
876
877
// ------------------------------------ solution construction from enumeration
878
879
1006
bool SygusUnifIo::useStrContainsEnumeratorExclude(Node e)
880
{
881
2012
  TypeNode xbt = d_tds->sygusToBuiltinType(e.getType());
882
1006
  if (xbt.isStringLike())
883
  {
884
178
    std::map<Node, bool>::iterator itx = d_use_str_contains_eexc.find(e);
885
178
    if (itx != d_use_str_contains_eexc.end())
886
    {
887
146
      return itx->second;
888
    }
889
64
    Trace("sygus-sui-enum-debug")
890
32
        << "Is " << e << " is str.contains exclusion?" << std::endl;
891
32
    d_use_str_contains_eexc[e] = true;
892
64
    Node c = d_candidate;
893
32
    EnumInfo& ei = d_strategy[c].getEnumInfo(e);
894
120
    for (const Node& sn : ei.d_enum_slave)
895
    {
896
88
      EnumInfo& eis = d_strategy[c].getEnumInfo(sn);
897
88
      EnumRole er = eis.getRole();
898
88
      if (er != enum_io && er != enum_concat_term)
899
      {
900
        Trace("sygus-sui-enum-debug") << "  incompatible slave : " << sn
901
                                      << ", role = " << er << std::endl;
902
        d_use_str_contains_eexc[e] = false;
903
        return false;
904
      }
905
88
      d_use_str_contains_eexc_conditional[e] = false;
906
88
      if (eis.isConditional())
907
      {
908
8
        Trace("sygus-sui-enum-debug")
909
4
            << "  conditional slave : " << sn << std::endl;
910
4
        d_use_str_contains_eexc_conditional[e] = true;
911
      }
912
    }
913
64
    Trace("sygus-sui-enum-debug")
914
32
        << "...can use str.contains exclusion." << std::endl;
915
32
    return d_use_str_contains_eexc[e];
916
  }
917
828
  return false;
918
}
919
920
1006
bool SygusUnifIo::getExplanationForEnumeratorExclude(
921
    Node e,
922
    Node v,
923
    std::vector<Node>& results,
924
    std::vector<Node>& exp)
925
{
926
1006
  NodeManager* nm = NodeManager::currentNM();
927
1006
  if (useStrContainsEnumeratorExclude(e))
928
  {
929
    // This check whether the example evaluates to something that is larger than
930
    // the output for some input/output pair. If so, then this term is never
931
    // useful. We generalize its explanation below.
932
933
    // if the enumerator is in a conditional context, then we are stricter
934
    // about when to exclude
935
178
    bool isConditional = d_use_str_contains_eexc_conditional[e];
936
178
    if (Trace.isOn("sygus-sui-cterm-debug"))
937
    {
938
      Trace("sygus-sui-enum") << std::endl;
939
    }
940
    // check if all examples had longer length that the output
941
178
    Assert(d_examples_out.size() == results.size());
942
356
    Trace("sygus-sui-cterm-debug")
943
178
        << "Check enumerator exclusion for " << e << " -> "
944
178
        << d_tds->sygusToBuiltin(v) << " based on str.contains." << std::endl;
945
240
    std::vector<unsigned> cmp_indices;
946
7032
    for (unsigned i = 0, size = results.size(); i < size; i++)
947
    {
948
      // If the result is not constant, then it is worthless. It does not
949
      // impact whether the term is excluded.
950
6874
      if (results[i].isConst())
951
      {
952
6872
        Assert(d_examples_out[i].isConst());
953
13744
        Trace("sygus-sui-cterm-debug")
954
6872
            << "  " << results[i] << " <> " << d_examples_out[i];
955
13724
        Node cont = nm->mkNode(STRING_STRCTN, d_examples_out[i], results[i]);
956
13724
        Node contr = Rewriter::rewrite(cont);
957
6872
        if (contr == d_false)
958
        {
959
5348
          cmp_indices.push_back(i);
960
5348
          Trace("sygus-sui-cterm-debug") << "...not contained." << std::endl;
961
        }
962
        else
963
        {
964
1524
          Trace("sygus-sui-cterm-debug") << "...contained." << std::endl;
965
1524
          if (isConditional)
966
          {
967
20
            return false;
968
          }
969
        }
970
      }
971
    }
972
158
    if (!cmp_indices.empty())
973
    {
974
      // we check invariance with respect to a negative contains test
975
192
      NegContainsSygusInvarianceTest ncset;
976
96
      if (isConditional)
977
      {
978
6
        ncset.setUniversal();
979
      }
980
96
      ncset.init(e, d_examples, d_examples_out, cmp_indices);
981
      // construct the generalized explanation
982
96
      d_tds->getExplain()->getExplanationFor(e, v, exp, ncset);
983
192
      Trace("sygus-sui-cterm")
984
192
          << "PBE-cterm : enumerator exclude " << d_tds->sygusToBuiltin(v)
985
96
          << " due to negative containment." << std::endl;
986
96
      return true;
987
    }
988
  }
989
890
  return false;
990
}
991
992
721
void SygusUnifIo::EnumCache::addEnumValue(Node v, std::vector<Node>& results)
993
{
994
1442
  Trace("sygus-sui-debug") << "Add enum value " << this << " " << v << " : "
995
721
                           << results << std::endl;
996
  // should not have been enumerated before
997
721
  Assert(d_enum_val_to_index.find(v) == d_enum_val_to_index.end());
998
721
  d_enum_val_to_index[v] = d_enum_vals.size();
999
721
  d_enum_vals.push_back(v);
1000
721
  d_enum_vals_res.push_back(results);
1001
721
}
1002
1003
929
void SygusUnifIo::initializeConstructSol()
1004
{
1005
929
  d_context.initialize(this);
1006
929
  d_sol_cons_nondet = false;
1007
929
}
1008
1009
929
void SygusUnifIo::initializeConstructSolFor(Node f)
1010
{
1011
929
  Assert(d_candidate == f);
1012
929
}
1013
1014
6654
Node SygusUnifIo::constructSol(
1015
    Node f, Node e, NodeRole nrole, int ind, std::vector<Node>& lemmas)
1016
{
1017
6654
  Assert(d_candidate == f);
1018
6654
  UnifContextIo& x = d_context;
1019
13308
  TypeNode etn = e.getType();
1020
6654
  if (Trace.isOn("sygus-sui-dt-debug"))
1021
  {
1022
    indent("sygus-sui-dt-debug", ind);
1023
    Trace("sygus-sui-dt-debug") << "ConstructPBE: (" << e << ", " << nrole
1024
                                << ") for type " << etn << " in context ";
1025
    print_val("sygus-sui-dt-debug", x.d_vals);
1026
    NodeRole ctx_role = x.getCurrentRole();
1027
    Trace("sygus-sui-dt-debug") << ", context role [" << ctx_role;
1028
    if (ctx_role == role_string_prefix || ctx_role == role_string_suffix)
1029
    {
1030
      Trace("sygus-sui-dt-debug") << ", string pos : ";
1031
      for (unsigned i = 0, size = x.d_str_pos.size(); i < size; i++)
1032
      {
1033
        Trace("sygus-sui-dt-debug") << " " << x.d_str_pos[i];
1034
      }
1035
    }
1036
    Trace("sygus-sui-dt-debug") << "]";
1037
    Trace("sygus-sui-dt-debug") << std::endl;
1038
  }
1039
  // enumerator type info
1040
6654
  EnumTypeInfo& tinfo = d_strategy[f].getEnumTypeInfo(etn);
1041
1042
  // get the enumerator information
1043
6654
  EnumInfo& einfo = d_strategy[f].getEnumInfo(e);
1044
1045
6654
  EnumCache& ecache = d_ecache[e];
1046
1047
6654
  bool retValMod = x.isReturnValueModified();
1048
1049
6654
  Node ret_dt;
1050
13308
  Node cached_ret_dt;
1051
6654
  if (nrole == role_equal)
1052
  {
1053
3968
    if (!retValMod)
1054
    {
1055
1848
      if (ecache.isSolved())
1056
      {
1057
        // this type has a complete solution
1058
70
        ret_dt = ecache.getSolved();
1059
70
        indent("sygus-sui-dt", ind);
1060
140
        Trace("sygus-sui-dt") << "return PBE: success : solved "
1061
70
                              << d_tds->sygusToBuiltin(ret_dt) << std::endl;
1062
70
        Assert(!ret_dt.isNull());
1063
      }
1064
      else
1065
      {
1066
        // could be conditionally solved
1067
3556
        std::vector<Node> subsumed_by;
1068
1778
        ecache.d_term_trie.getSubsumedBy(x.d_vals, true, subsumed_by);
1069
1778
        if (!subsumed_by.empty())
1070
        {
1071
255
          ret_dt = constructBestSolvedTerm(e, subsumed_by);
1072
255
          indent("sygus-sui-dt", ind);
1073
510
          Trace("sygus-sui-dt") << "return PBE: success : conditionally solved "
1074
255
                                << d_tds->sygusToBuiltin(ret_dt) << std::endl;
1075
        }
1076
        else
1077
        {
1078
1523
          indent("sygus-sui-dt-debug", ind);
1079
3046
          Trace("sygus-sui-dt-debug")
1080
1523
              << "  ...not currently conditionally solved." << std::endl;
1081
        }
1082
      }
1083
    }
1084
3968
    if (ret_dt.isNull())
1085
    {
1086
3643
      if (d_tds->sygusToBuiltinType(e.getType()).isStringLike())
1087
      {
1088
        // check if a current value that closes all examples
1089
        // get the term enumerator for this type
1090
        std::map<EnumRole, Node>::iterator itnt =
1091
2804
            tinfo.d_enum.find(enum_concat_term);
1092
2804
        if (itnt != tinfo.d_enum.end())
1093
        {
1094
5608
          Node et = itnt->second;
1095
1096
2804
          EnumCache& ecachet = d_ecache[et];
1097
          // get the current examples
1098
5608
          std::vector<Node> ex_vals;
1099
2804
          x.getCurrentStrings(this, d_examples_out, ex_vals);
1100
2804
          Assert(ecache.d_enum_vals.size() == ecache.d_enum_vals_res.size());
1101
1102
          // test each example in the term enumerator for the type
1103
5608
          std::vector<Node> str_solved;
1104
19686
          for (unsigned i = 0, size = ecachet.d_enum_vals.size(); i < size; i++)
1105
          {
1106
16882
            if (x.isStringSolved(this, ex_vals, ecachet.d_enum_vals_res[i]))
1107
            {
1108
134
              str_solved.push_back(ecachet.d_enum_vals[i]);
1109
            }
1110
          }
1111
2804
          if (!str_solved.empty())
1112
          {
1113
134
            ret_dt = constructBestSolvedTerm(e, str_solved);
1114
134
            indent("sygus-sui-dt", ind);
1115
268
            Trace("sygus-sui-dt") << "return PBE: success : string solved "
1116
134
                                  << d_tds->sygusToBuiltin(ret_dt) << std::endl;
1117
          }
1118
          else
1119
          {
1120
2670
            indent("sygus-sui-dt-debug", ind);
1121
5340
            Trace("sygus-sui-dt-debug")
1122
2670
                << "  ...not currently string solved." << std::endl;
1123
          }
1124
        }
1125
      }
1126
    }
1127
    // maybe we can find one in the cache
1128
3968
    if (ret_dt.isNull() && !retValMod)
1129
    {
1130
1523
      bool firstTime = true;
1131
3046
      std::unordered_set<Node, NodeHashFunction> intersection;
1132
      std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>::iterator
1133
1523
          pit;
1134
5089
      for (size_t i = 0, nvals = x.d_vals.size(); i < nvals; i++)
1135
      {
1136
4844
        if (x.d_vals[i].getConst<bool>())
1137
        {
1138
2708
          pit = d_psolutions[i].find(etn);
1139
2708
          if (pit == d_psolutions[i].end())
1140
          {
1141
            // no cached solution
1142
1278
            intersection.clear();
1143
1278
            break;
1144
          }
1145
1430
          if (firstTime)
1146
          {
1147
255
            intersection = pit->second;
1148
255
            firstTime = false;
1149
          }
1150
          else
1151
          {
1152
2350
            std::vector<Node> rm;
1153
3955
            for (const Node& a : intersection)
1154
            {
1155
2780
              if (pit->second.find(a) == pit->second.end())
1156
              {
1157
110
                rm.push_back(a);
1158
              }
1159
            }
1160
1285
            for (const Node& a : rm)
1161
            {
1162
110
              intersection.erase(a);
1163
            }
1164
1175
            if (intersection.empty())
1165
            {
1166
              break;
1167
            }
1168
          }
1169
        }
1170
      }
1171
1523
      if (!intersection.empty())
1172
      {
1173
245
        if (d_enableMinimality)
1174
        {
1175
          // if we are enabling minimality, the minimal cached solution may
1176
          // still not be the best solution, thus we remember it and keep it if
1177
          // we don't construct a better one below
1178
350
          std::vector<Node> intervec;
1179
175
          intervec.insert(
1180
350
              intervec.begin(), intersection.begin(), intersection.end());
1181
175
          cached_ret_dt = getMinimalTerm(intervec);
1182
        }
1183
        else
1184
        {
1185
70
          ret_dt = *intersection.begin();
1186
        }
1187
245
        if (Trace.isOn("sygus-sui-dt"))
1188
        {
1189
          indent("sygus-sui-dt", ind);
1190
          Trace("sygus-sui-dt") << "ConstructPBE: found in cache: ";
1191
          Node csol = ret_dt;
1192
          if (d_enableMinimality)
1193
          {
1194
            csol = cached_ret_dt;
1195
            Trace("sygus-sui-dt") << "(minimal) ";
1196
          }
1197
          TermDbSygus::toStreamSygus("sygus-sui-dt", csol);
1198
          Trace("sygus-sui-dt") << std::endl;
1199
        }
1200
      }
1201
    }
1202
  }
1203
2686
  else if (nrole == role_string_prefix || nrole == role_string_suffix)
1204
  {
1205
    // check if each return value is a prefix/suffix of all open examples
1206
2686
    if (!retValMod || x.getCurrentRole() == nrole)
1207
    {
1208
5372
      std::map<Node, std::vector<size_t>> incr;
1209
2686
      bool isPrefix = nrole == role_string_prefix;
1210
5372
      std::map<Node, size_t> total_inc;
1211
5372
      std::vector<Node> inc_strs;
1212
      // make the value of the examples
1213
5372
      std::vector<Node> ex_vals;
1214
2686
      x.getCurrentStrings(this, d_examples_out, ex_vals);
1215
2686
      if (Trace.isOn("sygus-sui-dt-debug"))
1216
      {
1217
        indent("sygus-sui-dt-debug", ind);
1218
        Trace("sygus-sui-dt-debug") << "current strings : " << std::endl;
1219
        for (unsigned i = 0, size = ex_vals.size(); i < size; i++)
1220
        {
1221
          indent("sygus-sui-dt-debug", ind + 1);
1222
          Trace("sygus-sui-dt-debug") << ex_vals[i] << std::endl;
1223
        }
1224
      }
1225
1226
      // check if there is a value for which is a prefix/suffix of all active
1227
      // examples
1228
2686
      Assert(ecache.d_enum_vals.size() == ecache.d_enum_vals_res.size());
1229
1230
17840
      for (unsigned i = 0, size = ecache.d_enum_vals.size(); i < size; i++)
1231
      {
1232
30308
        Node val_t = ecache.d_enum_vals[i];
1233
15154
        Assert(incr.find(val_t) == incr.end());
1234
15154
        indent("sygus-sui-dt-debug", ind);
1235
15154
        Trace("sygus-sui-dt-debug") << "increment string values : ";
1236
15154
        TermDbSygus::toStreamSygus("sygus-sui-dt-debug", val_t);
1237
15154
        Trace("sygus-sui-dt-debug") << " : ";
1238
15154
        Assert(ecache.d_enum_vals_res[i].size() == d_examples_out.size());
1239
15154
        size_t tot = 0;
1240
15154
        bool exsuccess = x.getStringIncrement(this,
1241
                                              isPrefix,
1242
                                              ex_vals,
1243
15154
                                              ecache.d_enum_vals_res[i],
1244
15154
                                              incr[val_t],
1245
15154
                                              tot);
1246
15154
        if (!exsuccess)
1247
        {
1248
12608
          incr.erase(val_t);
1249
12608
          Trace("sygus-sui-dt-debug") << "...fail" << std::endl;
1250
        }
1251
        else
1252
        {
1253
2546
          total_inc[val_t] = tot;
1254
2546
          inc_strs.push_back(val_t);
1255
5092
          Trace("sygus-sui-dt-debug")
1256
2546
              << "...success, total increment = " << tot << std::endl;
1257
        }
1258
      }
1259
1260
2686
      if (!incr.empty())
1261
      {
1262
        // solution construction for strings concatenation is non-deterministic
1263
        // with respect to failure/success.
1264
2082
        d_sol_cons_nondet = true;
1265
2082
        ret_dt = constructBestStringToConcat(inc_strs, total_inc, incr);
1266
2082
        Assert(!ret_dt.isNull());
1267
2082
        indent("sygus-sui-dt", ind);
1268
4164
        Trace("sygus-sui-dt")
1269
2082
            << "PBE: CONCAT strategy : choose " << (isPrefix ? "pre" : "suf")
1270
2082
            << "fix value " << d_tds->sygusToBuiltin(ret_dt) << std::endl;
1271
        // update the context
1272
2082
        bool ret = x.updateStringPosition(this, incr[ret_dt], nrole);
1273
2082
        AlwaysAssert(ret == (total_inc[ret_dt] > 0));
1274
      }
1275
      else
1276
      {
1277
604
        indent("sygus-sui-dt", ind);
1278
1208
        Trace("sygus-sui-dt") << "PBE: failed CONCAT strategy, no values are "
1279
604
                              << (isPrefix ? "pre" : "suf")
1280
604
                              << "fix of all examples." << std::endl;
1281
      }
1282
    }
1283
    else
1284
    {
1285
      indent("sygus-sui-dt", ind);
1286
      Trace("sygus-sui-dt")
1287
          << "PBE: failed CONCAT strategy, prefix/suffix mismatch."
1288
          << std::endl;
1289
    }
1290
  }
1291
6654
  if (!ret_dt.isNull() || einfo.isTemplated())
1292
  {
1293
2665
    Assert(ret_dt.isNull() || ret_dt.getType() == e.getType());
1294
2665
    indent("sygus-sui-dt", ind);
1295
5330
    Trace("sygus-sui-dt") << "ConstructPBE: returned (pre-strategy) " << ret_dt
1296
2665
                          << std::endl;
1297
2665
    return ret_dt;
1298
  }
1299
  // we will try a single strategy
1300
3989
  EnumTypeInfoStrat* etis = nullptr;
1301
3989
  std::map<NodeRole, StrategyNode>::iterator itsn = tinfo.d_snodes.find(nrole);
1302
3989
  if (itsn == tinfo.d_snodes.end())
1303
  {
1304
    indent("sygus-sui-dt", ind);
1305
    Trace("sygus-sui-dt") << "ConstructPBE: returned (no-strategy) " << ret_dt
1306
                          << std::endl;
1307
    return ret_dt;
1308
  }
1309
  // strategy info
1310
3989
  StrategyNode& snode = itsn->second;
1311
3989
  if (x.d_visit_role[e].find(nrole) != x.d_visit_role[e].end())
1312
  {
1313
    // already visited and context not changed (notice d_visit_role is cleared
1314
    // when the context changes).
1315
286
    indent("sygus-sui-dt", ind);
1316
572
    Trace("sygus-sui-dt") << "ConstructPBE: returned (already visited) "
1317
286
                          << ret_dt << std::endl;
1318
286
    return ret_dt;
1319
  }
1320
3703
  x.d_visit_role[e][nrole] = true;
1321
  // try a random strategy
1322
3703
  if (snode.d_strats.size() > 1)
1323
  {
1324
2770
    std::shuffle(
1325
        snode.d_strats.begin(), snode.d_strats.end(), Random::getRandom());
1326
  }
1327
  // ITE always first if we have not yet solved
1328
  // the reasoning is that splitting on conditions only subdivides the problem
1329
  // and cannot be the source of failure, whereas the wrong choice for a
1330
  // concatenation term may lead to failure
1331
3703
  if (d_solution.isNull())
1332
  {
1333
4976
    for (unsigned i = 0; i < snode.d_strats.size(); i++)
1334
    {
1335
4326
      if (snode.d_strats[i]->d_this == strat_ITE)
1336
      {
1337
        // flip the two
1338
2038
        EnumTypeInfoStrat* etis_i = snode.d_strats[i];
1339
2038
        snode.d_strats[i] = snode.d_strats[0];
1340
2038
        snode.d_strats[0] = etis_i;
1341
2038
        break;
1342
      }
1343
    }
1344
  }
1345
1346
  // iterate over the strategies
1347
3703
  unsigned sindex = 0;
1348
3703
  bool did_recurse = false;
1349
15249
  while (ret_dt.isNull() && !did_recurse && sindex < snode.d_strats.size())
1350
  {
1351
5773
    if (snode.d_strats[sindex]->isValid(x))
1352
    {
1353
4861
      etis = snode.d_strats[sindex];
1354
4861
      Assert(etis != nullptr);
1355
4861
      StrategyType strat = etis->d_this;
1356
4861
      indent("sygus-sui-dt", ind + 1);
1357
9722
      Trace("sygus-sui-dt")
1358
4861
          << "...try STRATEGY " << strat << "..." << std::endl;
1359
1360
9722
      std::vector<Node> dt_children_cons;
1361
4861
      bool success = true;
1362
1363
      // for ITE
1364
9722
      Node split_cond_enum;
1365
4861
      unsigned split_cond_res_index = 0;
1366
4861
      CVC4_UNUSED bool set_split_cond_res_index = false;
1367
1368
9075
      for (unsigned sc = 0, size = etis->d_cenum.size(); sc < size; sc++)
1369
      {
1370
8008
        indent("sygus-sui-dt", ind + 1);
1371
16016
        Trace("sygus-sui-dt")
1372
8008
            << "construct PBE child #" << sc << "..." << std::endl;
1373
12222
        Node rec_c;
1374
1375
8008
        std::pair<Node, NodeRole>& cenum = etis->d_cenum[sc];
1376
1377
        // update the context
1378
12222
        std::vector<Node> prev;
1379
8008
        if (strat == strat_ITE && sc > 0)
1380
        {
1381
1071
          EnumCache& ecache_cond = d_ecache[split_cond_enum];
1382
1071
          Assert(set_split_cond_res_index);
1383
1071
          Assert(split_cond_res_index < ecache_cond.d_enum_vals_res.size());
1384
1071
          prev = x.d_vals;
1385
2142
          x.updateContext(this,
1386
1071
                          ecache_cond.d_enum_vals_res[split_cond_res_index],
1387
                          sc == 1);
1388
          // return value of above call may be false in corner cases where we
1389
          // must choose a non-separating condition to traverse to another
1390
          // strategy node
1391
        }
1392
1393
        // recurse
1394
8008
        if (strat == strat_ITE && sc == 0)
1395
        {
1396
4566
          Node ce = cenum.first;
1397
1398
2283
          EnumCache& ecache_child = d_ecache[ce];
1399
1400
          // get the conditionals in the current context : they must be
1401
          // distinguishable
1402
4566
          std::map<int, std::vector<Node> > possible_cond;
1403
4566
          std::map<Node, int> solved_cond;  // stores branch
1404
2283
          ecache_child.d_term_trie.getLeaves(x.d_vals, true, possible_cond);
1405
1406
          std::map<int, std::vector<Node>>::iterator itpc =
1407
2283
              possible_cond.find(0);
1408
2283
          if (itpc != possible_cond.end())
1409
          {
1410
735
            if (Trace.isOn("sygus-sui-dt-debug"))
1411
            {
1412
              indent("sygus-sui-dt-debug", ind + 1);
1413
              Trace("sygus-sui-dt-debug")
1414
                  << "PBE : We have " << itpc->second.size()
1415
                  << " distinguishable conditionals:" << std::endl;
1416
              for (Node& cond : itpc->second)
1417
              {
1418
                indent("sygus-sui-dt-debug", ind + 2);
1419
                Trace("sygus-sui-dt-debug")
1420
                    << d_tds->sygusToBuiltin(cond) << std::endl;
1421
              }
1422
            }
1423
735
            if (rec_c.isNull())
1424
            {
1425
735
              rec_c = constructBestConditional(ce, itpc->second);
1426
735
              Assert(!rec_c.isNull());
1427
735
              indent("sygus-sui-dt", ind);
1428
1470
              Trace("sygus-sui-dt")
1429
735
                  << "PBE: ITE strategy : choose best conditional "
1430
735
                  << d_tds->sygusToBuiltin(rec_c) << std::endl;
1431
            }
1432
          }
1433
          else
1434
          {
1435
            // if the branch types are different, it could still make a
1436
            // difference to recurse, for instance see issue #4790. We do this
1437
            // if either branch is a different type from the current type.
1438
3096
            TypeNode branchType1 = etis->d_cenum[1].first.getType();
1439
3096
            TypeNode branchType2 = etis->d_cenum[2].first.getType();
1440
1548
            bool childTypesEqual = branchType1 == etn && branchType2 == etn;
1441
1548
            if (!childTypesEqual)
1442
            {
1443
4
              if (!ecache_child.d_enum_vals.empty())
1444
              {
1445
                // take arbitrary
1446
4
                rec_c = constructBestConditional(ce, ecache_child.d_enum_vals);
1447
4
                indent("sygus-sui-dt", ind);
1448
8
                Trace("sygus-sui-dt")
1449
                    << "PBE: ITE strategy : choose arbitrary conditional due "
1450
4
                       "to disequal child types "
1451
4
                    << d_tds->sygusToBuiltin(rec_c) << std::endl;
1452
              }
1453
            }
1454
1548
            if (rec_c.isNull())
1455
            {
1456
1544
              indent("sygus-sui-dt", ind);
1457
3088
              Trace("sygus-sui-dt")
1458
                  << "return PBE: failed ITE strategy, "
1459
1544
                     "cannot find a distinguishable condition, childTypesEqual="
1460
1544
                  << childTypesEqual << std::endl;
1461
            }
1462
          }
1463
2283
          if (!rec_c.isNull())
1464
          {
1465
739
            Assert(ecache_child.d_enum_val_to_index.find(rec_c)
1466
                   != ecache_child.d_enum_val_to_index.end());
1467
739
            split_cond_res_index = ecache_child.d_enum_val_to_index[rec_c];
1468
739
            set_split_cond_res_index = true;
1469
739
            split_cond_enum = ce;
1470
739
            Assert(split_cond_res_index < ecache_child.d_enum_vals_res.size());
1471
2283
          }
1472
        }
1473
        else
1474
        {
1475
5725
          did_recurse = true;
1476
5725
          rec_c = constructSol(f, cenum.first, cenum.second, ind + 2, lemmas);
1477
        }
1478
        // undo update the context
1479
8008
        if (strat == strat_ITE && sc > 0)
1480
        {
1481
1071
          x.d_vals = prev;
1482
        }
1483
8008
        if (!rec_c.isNull())
1484
        {
1485
4214
          dt_children_cons.push_back(rec_c);
1486
        }
1487
        else
1488
        {
1489
3794
          success = false;
1490
3794
          break;
1491
        }
1492
      }
1493
4861
      if (success)
1494
      {
1495
1067
        Assert(dt_children_cons.size() == etis->d_sol_templ_args.size());
1496
        // ret_dt = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR,
1497
        // dt_children );
1498
1067
        ret_dt = etis->d_sol_templ;
1499
1067
        ret_dt = ret_dt.substitute(etis->d_sol_templ_args.begin(),
1500
                                   etis->d_sol_templ_args.end(),
1501
                                   dt_children_cons.begin(),
1502
                                   dt_children_cons.end());
1503
1067
        indent("sygus-sui-dt-debug", ind);
1504
2134
        Trace("sygus-sui-dt-debug")
1505
1067
            << "PBE: success : constructed for strategy " << strat << std::endl;
1506
      }
1507
      else
1508
      {
1509
3794
        indent("sygus-sui-dt-debug", ind);
1510
7588
        Trace("sygus-sui-dt-debug")
1511
3794
            << "PBE: failed for strategy " << strat << std::endl;
1512
      }
1513
    }
1514
    // increment
1515
5773
    sindex++;
1516
  }
1517
1518
  // if there was a cached solution, process it now
1519
3703
  if (!cached_ret_dt.isNull() && cached_ret_dt != ret_dt)
1520
  {
1521
127
    if (ret_dt.isNull())
1522
    {
1523
      // take the cached one if it is the only one
1524
58
      ret_dt = cached_ret_dt;
1525
    }
1526
69
    else if (d_enableMinimality)
1527
    {
1528
69
      Assert(ret_dt.getType() == cached_ret_dt.getType());
1529
      // take the cached one if it is smaller
1530
138
      std::vector<Node> retDts;
1531
69
      retDts.push_back(cached_ret_dt);
1532
69
      retDts.push_back(ret_dt);
1533
69
      ret_dt = getMinimalTerm(retDts);
1534
    }
1535
  }
1536
3703
  Assert(ret_dt.isNull() || ret_dt.getType() == e.getType());
1537
3703
  if (Trace.isOn("sygus-sui-dt"))
1538
  {
1539
    indent("sygus-sui-dt", ind);
1540
    Trace("sygus-sui-dt") << "ConstructPBE: returned ";
1541
    TermDbSygus::toStreamSygus("sygus-sui-dt", ret_dt);
1542
    Trace("sygus-sui-dt") << std::endl;
1543
  }
1544
  // remember the solution
1545
3703
  if (nrole == role_equal)
1546
  {
1547
3371
    if (!retValMod && !ret_dt.isNull())
1548
    {
1549
2285
      for (size_t i = 0, nvals = x.d_vals.size(); i < nvals; i++)
1550
      {
1551
2036
        if (x.d_vals[i].getConst<bool>())
1552
        {
1553
1694
          if (Trace.isOn("sygus-sui-cache"))
1554
          {
1555
            indent("sygus-sui-cache", ind);
1556
            Trace("sygus-sui-cache") << "Cache solution (#" << i << ") : ";
1557
            TermDbSygus::toStreamSygus("sygus-sui-cache", ret_dt);
1558
            Trace("sygus-sui-cache") << std::endl;
1559
          }
1560
1694
          d_psolutions[i][etn].insert(ret_dt);
1561
        }
1562
      }
1563
    }
1564
  }
1565
1566
3703
  return ret_dt;
1567
}
1568
1569
739
Node SygusUnifIo::constructBestConditional(Node ce,
1570
                                           const std::vector<Node>& conds)
1571
{
1572
739
  if (!d_solConsUsingInfoGain)
1573
  {
1574
594
    return SygusUnif::constructBestConditional(ce, conds);
1575
  }
1576
145
  UnifContextIo& x = d_context;
1577
  // use information gain heuristic
1578
145
  Trace("sygus-sui-dt-igain") << "Best information gain in context ";
1579
145
  print_val("sygus-sui-dt-igain", x.d_vals);
1580
145
  Trace("sygus-sui-dt-igain") << std::endl;
1581
  // set of indices that are active in this branch, i.e. x.d_vals[i] is true
1582
290
  std::vector<unsigned> activeIndices;
1583
  // map (j,t,s) -> n, such that the j^th condition in the vector conds
1584
  // evaluates to t (typically true/false) on n active I/O pairs with output s.
1585
290
  std::map<unsigned, std::map<Node, std::map<Node, unsigned>>> eval;
1586
  // map (j,t) -> m, such that the j^th condition in the vector conds
1587
  // evaluates to t (typically true/false) for m active I/O pairs.
1588
290
  std::map<unsigned, std::map<Node, unsigned>> evalCount;
1589
145
  unsigned nconds = conds.size();
1590
145
  EnumCache& ecache = d_ecache[ce];
1591
  // Get the index of conds[j] in the enumerator cache, this is to look up
1592
  // its evaluation on each point.
1593
290
  std::vector<unsigned> eindex;
1594
473
  for (unsigned j = 0; j < nconds; j++)
1595
  {
1596
328
    eindex.push_back(ecache.d_enum_val_to_index[conds[j]]);
1597
  }
1598
145
  unsigned activePoints = 0;
1599
2411
  for (unsigned i = 0, npoints = x.d_vals.size(); i < npoints; i++)
1600
  {
1601
2266
    if (x.d_vals[i].getConst<bool>())
1602
    {
1603
1540
      activePoints++;
1604
3080
      Node eo = d_examples_out[i];
1605
5694
      for (unsigned j = 0; j < nconds; j++)
1606
      {
1607
8308
        Node resn = ecache.d_enum_vals_res[eindex[j]][i];
1608
4154
        Assert(resn.isConst());
1609
4154
        eval[j][resn][eo]++;
1610
4154
        evalCount[j][resn]++;
1611
      }
1612
    }
1613
  }
1614
145
  AlwaysAssert(activePoints > 0);
1615
  // find the condition that leads to the lowest entropy
1616
  // initially set minEntropy to > 1.0.
1617
145
  double minEntropy = 2.0;
1618
145
  unsigned bestIndex = 0;
1619
145
  int numEqual = 1;
1620
473
  for (unsigned j = 0; j < nconds; j++)
1621
  {
1622
    // To compute the entropy for a condition C, for pair of terms (s, t), let
1623
    //   prob(t) be the probability C evaluates to t on an active point,
1624
    //   prob(s|t) be the probability that an active point on which C
1625
    //     evaluates to t has output s.
1626
    // Then, the entropy of C is:
1627
    //   sum{t}. prob(t)*( sum{s}. -prob(s|t)*log2(prob(s|t)) )
1628
    // where notice this is always between 0 and 1.
1629
328
    double entropySum = 0.0;
1630
328
    Trace("sygus-sui-dt-igain") << j << " : ";
1631
984
    for (std::pair<const Node, std::map<Node, unsigned>>& ej : eval[j])
1632
    {
1633
656
      unsigned ecount = evalCount[j][ej.first];
1634
656
      if (ecount > 0)
1635
      {
1636
656
        double probBranch = double(ecount) / double(activePoints);
1637
656
        Trace("sygus-sui-dt-igain") << ej.first << " -> ( ";
1638
4492
        for (std::pair<const Node, unsigned>& eej : ej.second)
1639
        {
1640
3836
          if (eej.second > 0)
1641
          {
1642
3836
            double probVal = double(eej.second) / double(ecount);
1643
7672
            Trace("sygus-sui-dt-igain")
1644
3836
                << eej.first << ":" << eej.second << " ";
1645
3836
            double factor = -probVal * log2(probVal);
1646
3836
            entropySum += probBranch * factor;
1647
          }
1648
        }
1649
656
        Trace("sygus-sui-dt-igain") << ") ";
1650
      }
1651
    }
1652
328
    Trace("sygus-sui-dt-igain") << "..." << entropySum << std::endl;
1653
    // either less, or equal and coin flip passes
1654
328
    bool doSet = false;
1655
328
    if (entropySum == minEntropy)
1656
    {
1657
41
      numEqual++;
1658
41
      if (Random::getRandom().pickWithProb(double(1) / double(numEqual)))
1659
      {
1660
22
        doSet = true;
1661
      }
1662
    }
1663
287
    else if (entropySum < minEntropy)
1664
    {
1665
66
      doSet = true;
1666
66
      numEqual = 1;
1667
    }
1668
328
    if (doSet)
1669
    {
1670
88
      minEntropy = entropySum;
1671
88
      bestIndex = j;
1672
    }
1673
  }
1674
1675
145
  Assert(!conds.empty());
1676
145
  return conds[bestIndex];
1677
}
1678
1679
} /* CVC4::theory::quantifiers namespace */
1680
} /* CVC4::theory namespace */
1681
26676
} /* CVC4 namespace */