GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/cegis.cpp Lines: 323 344 93.9 %
Date: 2021-03-23 Branches: 612 1300 47.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file cegis.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Haniel Barbosa, 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 cegis
13
 **/
14
15
#include "theory/quantifiers/sygus/cegis.h"
16
#include "expr/node_algorithm.h"
17
#include "options/base_options.h"
18
#include "options/quantifiers_options.h"
19
#include "printer/printer.h"
20
#include "theory/quantifiers/sygus/example_min_eval.h"
21
#include "theory/quantifiers/sygus/synth_conjecture.h"
22
#include "theory/quantifiers/sygus/term_database_sygus.h"
23
#include "theory/quantifiers_engine.h"
24
#include "theory/rewriter.h"
25
26
using namespace std;
27
using namespace CVC4::kind;
28
using namespace CVC4::context;
29
30
namespace CVC4 {
31
namespace theory {
32
namespace quantifiers {
33
34
6570
Cegis::Cegis(QuantifiersEngine* qe,
35
             QuantifiersInferenceManager& qim,
36
6570
             SynthConjecture* p)
37
6570
    : SygusModule(qe, qim, p), d_eval_unfold(nullptr), d_usingSymCons(false)
38
{
39
6570
  d_eval_unfold = qe->getTermDatabaseSygus()->getEvalUnfold();
40
6570
}
41
42
308
bool Cegis::initialize(Node conj,
43
                       Node n,
44
                       const std::vector<Node>& candidates,
45
                       std::vector<Node>& lemmas)
46
{
47
308
  d_base_body = n;
48
308
  if (d_base_body.getKind() == NOT && d_base_body[0].getKind() == FORALL)
49
  {
50
1254
    for (const Node& v : d_base_body[0][0])
51
    {
52
1040
      d_base_vars.push_back(v);
53
    }
54
214
    d_base_body = d_base_body[0][1];
55
  }
56
57
  // assign the cegis sampler if applicable
58
5705
  if (options::cegisSample() != options::CegisSampleMode::NONE)
59
  {
60
14
    Trace("cegis-sample") << "Initialize sampler for " << d_base_body << "..."
61
7
                          << std::endl;
62
14
    TypeNode bt = d_base_body.getType();
63
7
    d_cegis_sampler.initialize(bt, d_base_vars, options::sygusSamples());
64
  }
65
308
  return processInitialize(conj, n, candidates, lemmas);
66
}
67
68
287
bool Cegis::processInitialize(Node conj,
69
                              Node n,
70
                              const std::vector<Node>& candidates,
71
                              std::vector<Node>& lemmas)
72
{
73
287
  Trace("cegis") << "Initialize cegis..." << std::endl;
74
287
  unsigned csize = candidates.size();
75
  // The role of enumerators is to be either the single solution or part of
76
  // a solution involving multiple enumerators.
77
287
  EnumeratorRole erole =
78
287
      csize == 1 ? ROLE_ENUM_SINGLE_SOLUTION : ROLE_ENUM_MULTI_SOLUTION;
79
  // initialize an enumerator for each candidate
80
652
  for (unsigned i = 0; i < csize; i++)
81
  {
82
365
    Trace("cegis") << "...register enumerator " << candidates[i];
83
    // We use symbolic constants if we are doing repair constants or if the
84
    // grammar construction was not simple.
85
730
    if (options::sygusRepairConst()
86
1325
        || options::sygusGrammarConsMode()
87
               != options::SygusGrammarConsMode::SIMPLE)
88
    {
89
42
      TypeNode ctn = candidates[i].getType();
90
21
      d_tds->registerSygusType(ctn);
91
21
      SygusTypeInfo& cti = d_tds->getTypeInfo(ctn);
92
21
      if (cti.hasSubtermSymbolicCons())
93
      {
94
        // remember that we are using symbolic constructors
95
21
        d_usingSymCons = true;
96
21
        Trace("cegis") << " (using symbolic constructors)";
97
      }
98
    }
99
365
    Trace("cegis") << std::endl;
100
365
    d_tds->registerEnumerator(candidates[i], candidates[i], d_parent, erole);
101
  }
102
287
  return true;
103
}
104
105
47273
void Cegis::getTermList(const std::vector<Node>& candidates,
106
                        std::vector<Node>& enums)
107
{
108
47273
  enums.insert(enums.end(), candidates.begin(), candidates.end());
109
47273
}
110
111
21249
bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
112
                          const std::vector<Node>& candidate_values,
113
                          std::vector<Node>& lems)
114
{
115
  // First, decide if this call will apply "conjecture-specific refinement".
116
  // In other words, in some settings, the following method will identify and
117
  // block a class of solutions {candidates -> S} that generalizes the current
118
  // one (given by {candidates -> candidate_values}), such that for each
119
  // candidate_values' in S, we have that {candidates -> candidate_values'} is
120
  // also not a solution for the given conjecture. We may not
121
  // apply this form of refinement if any (relevant) enumerator in candidates is
122
  // "actively generated" (see TermDbSygs::isPassiveEnumerator), since its
123
  // model values are themselves interpreted as classes of solutions.
124
21249
  bool doGen = true;
125
53545
  for (const Node& v : candidates)
126
  {
127
    // if it is relevant to refinement
128
46983
    if (d_refinement_lemma_vars.find(v) != d_refinement_lemma_vars.end())
129
    {
130
40516
      if (!d_tds->isPassiveEnumerator(v))
131
      {
132
14687
        doGen = false;
133
14687
        break;
134
      }
135
    }
136
  }
137
21249
  NodeManager* nm = NodeManager::currentNM();
138
21249
  bool addedEvalLemmas = false;
139
  // Refinement evaluation should not be done for grammars with symbolic
140
  // constructors.
141
21249
  if (!d_usingSymCons)
142
  {
143
42082
    Trace("sygus-engine") << "  *** Do refinement lemma evaluation"
144
42082
                          << (doGen ? " with conjecture-specific refinement"
145
21041
                                    : "")
146
21041
                          << "..." << std::endl;
147
    // see if any refinement lemma is refuted by evaluation
148
21041
    if (doGen)
149
    {
150
12714
      std::vector<Node> cre_lems;
151
6357
      getRefinementEvalLemmas(candidates, candidate_values, cre_lems);
152
6357
      if (!cre_lems.empty())
153
      {
154
2582
        lems.insert(lems.end(), cre_lems.begin(), cre_lems.end());
155
2582
        addedEvalLemmas = true;
156
2582
        if (Trace.isOn("cegqi-lemma"))
157
        {
158
          for (const Node& lem : cre_lems)
159
          {
160
            Trace("cegqi-lemma")
161
                << "Cegqi::Lemma : ref evaluation : " << lem << std::endl;
162
          }
163
        }
164
        /* we could, but do not return here. experimentally, it is better to
165
          add the lemmas below as well, in parallel. */
166
      }
167
    }
168
    else
169
    {
170
      // just check whether the refinement lemmas are satisfied, fail if not
171
14684
      if (checkRefinementEvalLemmas(candidates, candidate_values))
172
      {
173
28244
        Trace("sygus-engine") << "...(actively enumerated) candidate failed "
174
14122
                                 "refinement lemma evaluation."
175
14122
                              << std::endl;
176
14122
        return true;
177
      }
178
    }
179
  }
180
  // we only do evaluation unfolding for passive enumerators
181
608647
  bool doEvalUnfold = (doGen && options::sygusEvalUnfold()) || d_usingSymCons;
182
7127
  if (doEvalUnfold)
183
  {
184
6565
    Trace("sygus-engine") << "  *** Do evaluation unfolding..." << std::endl;
185
13130
    std::vector<Node> eager_terms, eager_vals, eager_exps;
186
38864
    for (unsigned i = 0, size = candidates.size(); i < size; ++i)
187
    {
188
64598
      Trace("cegqi-debug") << "  register " << candidates[i] << " -> "
189
32299
                           << candidate_values[i] << std::endl;
190
64598
      d_eval_unfold->registerModelValue(candidates[i],
191
32299
                                        candidate_values[i],
192
                                        eager_terms,
193
                                        eager_vals,
194
                                        eager_exps);
195
    }
196
13130
    Trace("cegqi-debug") << "...produced " << eager_terms.size()
197
6565
                         << " evaluation unfold lemmas.\n";
198
22304
    for (unsigned i = 0, size = eager_terms.size(); i < size; ++i)
199
    {
200
      Node lem = nm->mkNode(
201
31478
          OR, eager_exps[i].negate(), eager_terms[i].eqNode(eager_vals[i]));
202
15739
      lems.push_back(lem);
203
15739
      addedEvalLemmas = true;
204
31478
      Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation unfold : " << lem
205
15739
                           << std::endl;
206
    }
207
  }
208
7127
  return addedEvalLemmas;
209
}
210
211
136
Node Cegis::getRefinementLemmaFormula()
212
{
213
272
  std::vector<Node> conj;
214
136
  conj.insert(
215
272
      conj.end(), d_refinement_lemmas.begin(), d_refinement_lemmas.end());
216
  // get the propagated values
217
484
  for (unsigned i = 0, nprops = d_rl_eval_hds.size(); i < nprops; i++)
218
  {
219
348
    conj.push_back(d_rl_eval_hds[i].eqNode(d_rl_vals[i]));
220
  }
221
  // make the formula
222
136
  NodeManager* nm = NodeManager::currentNM();
223
136
  Node ret;
224
136
  if (conj.empty())
225
  {
226
2
    ret = nm->mkConst(true);
227
  }
228
  else
229
  {
230
134
    ret = conj.size() == 1 ? conj[0] : nm->mkNode(AND, conj);
231
  }
232
272
  return ret;
233
}
234
235
21394
bool Cegis::constructCandidates(const std::vector<Node>& enums,
236
                                const std::vector<Node>& enum_values,
237
                                const std::vector<Node>& candidates,
238
                                std::vector<Node>& candidate_values,
239
                                std::vector<Node>& lems)
240
{
241
21394
  if (Trace.isOn("cegis"))
242
  {
243
    Trace("cegis") << "  Enumerators :\n";
244
    for (unsigned i = 0, size = enums.size(); i < size; ++i)
245
    {
246
      Trace("cegis") << "    " << enums[i] << " -> ";
247
      TermDbSygus::toStreamSygus("cegis", enum_values[i]);
248
      Trace("cegis") << "\n";
249
    }
250
  }
251
  // if we are using grammar-based repair
252
21394
  if (d_usingSymCons && options::sygusRepairConst())
253
  {
254
239
    SygusRepairConst* src = d_parent->getRepairConst();
255
239
    Assert(src != nullptr);
256
    // check if any enum_values have symbolic terms that must be repaired
257
239
    bool mustRepair = false;
258
333
    for (const Node& c : enum_values)
259
    {
260
239
      if (SygusRepairConst::mustRepair(c))
261
      {
262
145
        mustRepair = true;
263
145
        break;
264
      }
265
    }
266
239
    Trace("cegis") << "...must repair is: " << mustRepair << std::endl;
267
    // if the solution contains a subterm that must be repaired
268
239
    if (mustRepair)
269
    {
270
290
      std::vector<Node> fail_cvs = enum_values;
271
145
      Assert(candidates.size() == fail_cvs.size());
272
      // try to solve entire problem?
273
145
      if (src->repairSolution(candidates, fail_cvs, candidate_values))
274
      {
275
9
        return true;
276
      }
277
272
      Node rl = getRefinementLemmaFormula();
278
      // try to solve for the refinement lemmas only
279
      bool ret =
280
136
          src->repairSolution(rl, candidates, fail_cvs, candidate_values);
281
      // Even if ret is true, we will exclude the skeleton as well; this means
282
      // that we have one chance to repair each skeleton. It is possible however
283
      // that we might want to repair the same skeleton multiple times.
284
272
      std::vector<Node> exp;
285
272
      for (unsigned i = 0, size = enums.size(); i < size; i++)
286
      {
287
408
        d_tds->getExplain()->getExplanationForEquality(
288
272
            enums[i], enum_values[i], exp);
289
      }
290
136
      Assert(!exp.empty());
291
136
      NodeManager* nm = NodeManager::currentNM();
292
272
      Node expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp);
293
      // must guard it
294
136
      expn = nm->mkNode(OR, d_parent->getGuard().negate(), expn.negate());
295
136
      lems.push_back(expn);
296
136
      return ret;
297
    }
298
  }
299
300
  // evaluate on refinement lemmas
301
21249
  bool addedEvalLemmas = addEvalLemmas(enums, enum_values, lems);
302
303
  // try to construct candidates
304
21249
  if (!processConstructCandidates(enums,
305
                                  enum_values,
306
                                  candidates,
307
                                  candidate_values,
308
21249
                                  !addedEvalLemmas,
309
21249
                                  lems))
310
  {
311
18691
    return false;
312
  }
313
314
2558
  if (options::cegisSample() != options::CegisSampleMode::NONE && lems.empty())
315
  {
316
    // if we didn't add a lemma, trying sampling to add a refinement lemma
317
    // that immediately refutes the candidate we just constructed
318
40
    if (sampleAddRefinementLemma(candidates, candidate_values, lems))
319
    {
320
9
      candidate_values.clear();
321
      // restart (should be guaranteed to add evaluation lemmas on this call)
322
      return constructCandidates(
323
9
          enums, enum_values, candidates, candidate_values, lems);
324
    }
325
  }
326
2549
  return true;
327
}
328
329
19525
bool Cegis::processConstructCandidates(const std::vector<Node>& enums,
330
                                       const std::vector<Node>& enum_values,
331
                                       const std::vector<Node>& candidates,
332
                                       std::vector<Node>& candidate_values,
333
                                       bool satisfiedRl,
334
                                       std::vector<Node>& lems)
335
{
336
19525
  if (satisfiedRl)
337
  {
338
2492
    candidate_values.insert(
339
4984
        candidate_values.end(), enum_values.begin(), enum_values.end());
340
2492
    return true;
341
  }
342
17033
  return false;
343
}
344
345
682
void Cegis::addRefinementLemma(Node lem)
346
{
347
682
  Trace("cegis-rl") << "Cegis::addRefinementLemma: " << lem << std::endl;
348
682
  d_refinement_lemmas.push_back(lem);
349
  // apply existing substitution
350
1364
  Node slem = lem;
351
682
  if (!d_rl_eval_hds.empty())
352
  {
353
179
    slem = lem.substitute(d_rl_eval_hds.begin(),
354
                          d_rl_eval_hds.end(),
355
                          d_rl_vals.begin(),
356
                          d_rl_vals.end());
357
  }
358
  // rewrite with extended rewriter
359
682
  slem = d_tds->getExtRewriter()->extendedRewrite(slem);
360
  // collect all variables in slem
361
682
  expr::getSymbols(slem, d_refinement_lemma_vars);
362
1364
  std::vector<Node> waiting;
363
682
  waiting.push_back(lem);
364
682
  unsigned wcounter = 0;
365
  // while we are not done adding lemmas
366
2700
  while (wcounter < waiting.size())
367
  {
368
    // add the conjunct, possibly propagating
369
1009
    addRefinementLemmaConjunct(wcounter, waiting);
370
1009
    wcounter++;
371
  }
372
682
}
373
374
1009
void Cegis::addRefinementLemmaConjunct(unsigned wcounter,
375
                                       std::vector<Node>& waiting)
376
{
377
1887
  Node lem = waiting[wcounter];
378
1009
  lem = Rewriter::rewrite(lem);
379
  // apply substitution and rewrite if applicable
380
1009
  if (lem.isConst())
381
  {
382
9
    if (!lem.getConst<bool>())
383
    {
384
      // conjecture is infeasible
385
    }
386
    else
387
    {
388
6
      return;
389
    }
390
  }
391
  // break into conjunctions
392
1003
  if (lem.getKind() == AND)
393
  {
394
426
    for (const Node& lc : lem)
395
    {
396
317
      waiting.push_back(lc);
397
    }
398
109
    return;
399
  }
400
  // does this correspond to a substitution?
401
894
  NodeManager* nm = NodeManager::currentNM();
402
1772
  TNode term;
403
1772
  TNode val;
404
894
  if (lem.getKind() == EQUAL)
405
  {
406
1147
    for (unsigned i = 0; i < 2; i++)
407
    {
408
862
      if (lem[i].isConst() && d_tds->isEvaluationPoint(lem[1 - i]))
409
      {
410
147
        term = lem[1 - i];
411
147
        val = lem[i];
412
147
        break;
413
      }
414
    }
415
  }
416
  else
417
  {
418
462
    term = lem.getKind() == NOT ? lem[0] : lem;
419
    // predicate case: the conjunct is a (negated) evaluation point
420
462
    if (d_tds->isEvaluationPoint(term))
421
    {
422
168
      val = nm->mkConst(lem.getKind() != NOT);
423
    }
424
  }
425
894
  if (!val.isNull())
426
  {
427
315
    if (d_refinement_lemma_unit.find(lem) != d_refinement_lemma_unit.end())
428
    {
429
      // already added
430
16
      return;
431
    }
432
598
    Trace("cegis-rl") << "* cegis-rl: propagate: " << term << " -> " << val
433
299
                      << std::endl;
434
299
    d_rl_eval_hds.push_back(term);
435
299
    d_rl_vals.push_back(val);
436
299
    d_refinement_lemma_unit.insert(lem);
437
438
    // apply to waiting lemmas beyond this one
439
452
    for (unsigned i = wcounter + 1, size = waiting.size(); i < size; i++)
440
    {
441
153
      waiting[i] = waiting[i].substitute(term, val);
442
    }
443
    // apply to all existing refinement lemmas
444
598
    std::vector<Node> to_rem;
445
407
    for (const Node& rl : d_refinement_lemma_conj)
446
    {
447
216
      Node srl = rl.substitute(term, val);
448
108
      if (srl != rl)
449
      {
450
20
        Trace("cegis-rl") << "* cegis-rl: replace: " << rl << " -> " << srl
451
10
                          << std::endl;
452
10
        waiting.push_back(srl);
453
10
        to_rem.push_back(rl);
454
      }
455
    }
456
309
    for (const Node& tr : to_rem)
457
    {
458
10
      d_refinement_lemma_conj.erase(tr);
459
    }
460
  }
461
  else
462
  {
463
579
    if (Trace.isOn("cegis-rl"))
464
    {
465
      if (d_refinement_lemma_conj.find(lem) == d_refinement_lemma_conj.end())
466
      {
467
        Trace("cegis-rl") << "cegis-rl: add: " << lem << std::endl;
468
      }
469
    }
470
579
    d_refinement_lemma_conj.insert(lem);
471
  }
472
}
473
474
627
void Cegis::registerRefinementLemma(const std::vector<Node>& vars,
475
                                    Node lem,
476
                                    std::vector<Node>& lems)
477
{
478
627
  addRefinementLemma(lem);
479
  // Make the refinement lemma and add it to lems.
480
  // This lemma is guarded by the parent's guard, which has the semantics
481
  // "this conjecture has a solution", hence this lemma states:
482
  // if the parent conjecture has a solution, it satisfies the specification
483
  // for the given concrete point.
484
  Node rlem =
485
1254
      NodeManager::currentNM()->mkNode(OR, d_parent->getGuard().negate(), lem);
486
627
  lems.push_back(rlem);
487
627
}
488
489
348
bool Cegis::usingRepairConst() { return true; }
490
6357
bool Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs,
491
                                    const std::vector<Node>& ms,
492
                                    std::vector<Node>& lems)
493
{
494
12714
  Trace("sygus-cref-eval") << "Cref eval : conjecture has "
495
12714
                           << d_refinement_lemma_unit.size() << " unit and "
496
12714
                           << d_refinement_lemma_conj.size()
497
6357
                           << " non-unit refinement lemma conjunctions."
498
6357
                           << std::endl;
499
6357
  Assert(vs.size() == ms.size());
500
501
6357
  NodeManager* nm = NodeManager::currentNM();
502
503
12714
  Node nfalse = nm->mkConst(false);
504
12714
  Node neg_guard = d_parent->getGuard().negate();
505
6357
  bool ret = false;
506
507
15630
  for (unsigned r = 0; r < 2; r++)
508
  {
509
11855
    std::unordered_set<Node, NodeHashFunction>& rlemmas =
510
        r == 0 ? d_refinement_lemma_unit : d_refinement_lemma_conj;
511
41115
    for (const Node& lem : rlemmas)
512
    {
513
29260
      Assert(!lem.isNull());
514
58520
      std::map<Node, Node> visited;
515
58520
      std::map<Node, std::vector<Node> > exp;
516
58520
      EvalSygusInvarianceTest vsit;
517
58520
      Trace("sygus-cref-eval") << "Check refinement lemma conjunct " << lem
518
29260
                               << " against current model." << std::endl;
519
58520
      Trace("sygus-cref-eval2") << "Check refinement lemma conjunct " << lem
520
29260
                                << " against current model." << std::endl;
521
58520
      Node cre_lem;
522
58520
      Node lemcs = lem.substitute(vs.begin(), vs.end(), ms.begin(), ms.end());
523
58520
      Trace("sygus-cref-eval2")
524
29260
          << "...under substitution it is : " << lemcs << std::endl;
525
58520
      Node lemcsu = vsit.doEvaluateWithUnfolding(d_tds, lemcs);
526
58520
      Trace("sygus-cref-eval2")
527
29260
          << "...after unfolding is : " << lemcsu << std::endl;
528
29260
      if (lemcsu.isConst() && !lemcsu.getConst<bool>())
529
      {
530
6061
        ret = true;
531
12122
        std::vector<Node> msu;
532
12122
        std::vector<Node> mexp;
533
6061
        msu.insert(msu.end(), ms.begin(), ms.end());
534
12122
        std::map<TypeNode, int> var_count;
535
18104
        for (unsigned k = 0; k < vs.size(); k++)
536
        {
537
12043
          vsit.setUpdatedTerm(msu[k]);
538
12043
          msu[k] = vs[k];
539
          // substitute for everything except this
540
          Node sconj =
541
24086
              lem.substitute(vs.begin(), vs.end(), msu.begin(), msu.end());
542
12043
          vsit.init(sconj, vs[k], nfalse);
543
          // get minimal explanation for this
544
24086
          Node ut = vsit.getUpdatedTerm();
545
24086
          Trace("sygus-cref-eval2-debug")
546
12043
              << "  compute min explain of : " << vs[k] << " = " << ut
547
12043
              << std::endl;
548
24086
          d_tds->getExplain()->getExplanationFor(
549
12043
              vs[k], ut, mexp, vsit, var_count, false);
550
12043
          Trace("sygus-cref-eval2-debug") << "exp now: " << mexp << std::endl;
551
12043
          msu[k] = vsit.getUpdatedTerm();
552
24086
          Trace("sygus-cref-eval2-debug")
553
12043
              << "updated term : " << msu[k] << std::endl;
554
        }
555
6061
        if (!mexp.empty())
556
        {
557
12122
          Node en = mexp.size() == 1 ? mexp[0] : nm->mkNode(kind::AND, mexp);
558
6061
          cre_lem = nm->mkNode(kind::OR, en.negate(), neg_guard);
559
        }
560
        else
561
        {
562
          cre_lem = neg_guard;
563
        }
564
6061
        if (std::find(lems.begin(), lems.end(), cre_lem) == lems.end())
565
        {
566
6962
          Trace("sygus-cref-eval") << "...produced lemma : " << cre_lem
567
3481
                                   << std::endl;
568
3481
          lems.push_back(cre_lem);
569
        }
570
      }
571
    }
572
11855
    if (!lems.empty())
573
    {
574
2582
      break;
575
    }
576
  }
577
12714
  return ret;
578
}
579
580
14684
bool Cegis::checkRefinementEvalLemmas(const std::vector<Node>& vs,
581
                                      const std::vector<Node>& ms)
582
{
583
  // Maybe we already evaluated some terms in refinement lemmas.
584
  // In particular, the example eval cache for f may have some evaluations
585
  // cached, which we add to evalVisited and pass to the evaluator below.
586
29368
  std::unordered_map<Node, Node, NodeHashFunction> evalVisited;
587
14684
  ExampleInfer* ei = d_parent->getExampleInfer();
588
29368
  for (unsigned i = 0, vsize = vs.size(); i < vsize; i++)
589
  {
590
29368
    Node f = vs[i];
591
14684
    ExampleEvalCache* eec = d_parent->getExampleEvalCache(f);
592
14684
    if (eec != nullptr)
593
    {
594
      // get the results we obtained through the example evaluation utility
595
6796
      std::vector<Node> vsProc;
596
6796
      std::vector<Node> msProc;
597
6796
      Node bmsi = d_tds->sygusToBuiltin(ms[i]);
598
3398
      ei->getExampleTerms(f, vsProc);
599
3398
      eec->evaluateVec(bmsi, msProc);
600
3398
      Assert(vsProc.size() == msProc.size());
601
34687
      for (unsigned j = 0, psize = vsProc.size(); j < psize; j++)
602
      {
603
31289
        evalVisited[vsProc[j]] = msProc[j];
604
31289
        Assert(vsProc[j].getType().isComparableTo(msProc[j].getType()));
605
      }
606
    }
607
  }
608
609
14684
  Evaluator* eval = d_tds->getEvaluator();
610
18970
  for (unsigned r = 0; r < 2; r++)
611
  {
612
18408
    std::unordered_set<Node, NodeHashFunction>& rlemmas =
613
        r == 0 ? d_refinement_lemma_unit : d_refinement_lemma_conj;
614
23937
    for (const Node& lem : rlemmas)
615
    {
616
      // We may have computed the evaluation of some function applications
617
      // via example-based symmetry breaking, stored in evalVisited.
618
25180
      Node lemcsu = eval->eval(lem, vs, ms, evalVisited);
619
19651
      if (lemcsu.isConst() && !lemcsu.getConst<bool>())
620
      {
621
14122
        return true;
622
      }
623
    }
624
  }
625
562
  return false;
626
}
627
628
40
bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates,
629
                                     const std::vector<Node>& vals,
630
                                     std::vector<Node>& lems)
631
{
632
40
  Trace("sygus-engine") << "  *** Do sample add refinement..." << std::endl;
633
40
  if (Trace.isOn("cegis-sample"))
634
  {
635
    Trace("cegis-sample") << "Check sampling for candidate solution"
636
                          << std::endl;
637
    for (unsigned i = 0, size = vals.size(); i < size; i++)
638
    {
639
      Trace("cegis-sample") << "  " << candidates[i] << " -> " << vals[i]
640
                            << std::endl;
641
    }
642
  }
643
40
  Assert(vals.size() == candidates.size());
644
  Node sbody = d_base_body.substitute(
645
80
      candidates.begin(), candidates.end(), vals.begin(), vals.end());
646
40
  Trace("cegis-sample-debug2") << "Sample " << sbody << std::endl;
647
  // do eager rewriting
648
40
  sbody = Rewriter::rewrite(sbody);
649
40
  Trace("cegis-sample") << "Sample (after rewriting): " << sbody << std::endl;
650
651
40
  NodeManager* nm = NodeManager::currentNM();
652
31002
  for (unsigned i = 0, size = d_cegis_sampler.getNumSamplePoints(); i < size;
653
       i++)
654
  {
655
30971
    if (d_cegis_sample_refine.find(i) == d_cegis_sample_refine.end())
656
    {
657
61895
      Node ev = d_cegis_sampler.evaluate(sbody, i);
658
61904
      Trace("cegis-sample-debug") << "...evaluate point #" << i << " to " << ev
659
30952
                                  << std::endl;
660
30952
      Assert(ev.isConst());
661
30952
      Assert(ev.getType().isBoolean());
662
30952
      if (!ev.getConst<bool>())
663
      {
664
9
        Trace("cegis-sample-debug") << "...false for point #" << i << std::endl;
665
        // mark this as a CEGIS point (no longer sampled)
666
9
        d_cegis_sample_refine.insert(i);
667
9
        std::vector<Node> pt;
668
9
        d_cegis_sampler.getSamplePoint(i, pt);
669
9
        Assert(d_base_vars.size() == pt.size());
670
        Node rlem = d_base_body.substitute(
671
9
            d_base_vars.begin(), d_base_vars.end(), pt.begin(), pt.end());
672
9
        rlem = Rewriter::rewrite(rlem);
673
27
        if (std::find(
674
9
                d_refinement_lemmas.begin(), d_refinement_lemmas.end(), rlem)
675
27
            == d_refinement_lemmas.end())
676
        {
677
9
          if (Trace.isOn("cegis-sample"))
678
          {
679
            Trace("cegis-sample") << "   false for point #" << i << " : ";
680
            for (const Node& cn : pt)
681
            {
682
              Trace("cegis-sample") << cn << " ";
683
            }
684
            Trace("cegis-sample") << std::endl;
685
          }
686
9
          Trace("sygus-engine") << "  *** Refine by sampling" << std::endl;
687
9
          addRefinementLemma(rlem);
688
          // if trust, we are not interested in sending out refinement lemmas
689
9
          if (options::cegisSample() != options::CegisSampleMode::TRUST)
690
          {
691
12
            Node lem = nm->mkNode(OR, d_parent->getGuard().negate(), rlem);
692
6
            lems.push_back(lem);
693
          }
694
9
          return true;
695
        }
696
        else
697
        {
698
          Trace("cegis-sample-debug") << "...duplicate." << std::endl;
699
        }
700
      }
701
    }
702
  }
703
31
  return false;
704
}
705
706
} /* CVC4::theory::quantifiers namespace */
707
} /* CVC4::theory namespace */
708
26685
} /* CVC4 namespace */