GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/cegis_unif.cpp Lines: 304 350 86.9 %
Date: 2021-11-07 Branches: 510 1384 36.8 %

Line Exec Source
1
/******************************************************************************
2
 * Top contributors (to current version):
3
 *   Andrew Reynolds, Haniel Barbosa, Mathias Preiner
4
 *
5
 * This file is part of the cvc5 project.
6
 *
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.
11
 * ****************************************************************************
12
 *
13
 * Implementation of class for cegis with unification techniques.
14
 */
15
16
#include "theory/quantifiers/sygus/cegis_unif.h"
17
18
#include "expr/skolem_manager.h"
19
#include "expr/sygus_datatype.h"
20
#include "options/quantifiers_options.h"
21
#include "printer/printer.h"
22
#include "theory/datatypes/sygus_datatype_utils.h"
23
#include "theory/quantifiers/sygus/sygus_unif_rl.h"
24
#include "theory/quantifiers/sygus/synth_conjecture.h"
25
#include "theory/quantifiers/sygus/term_database_sygus.h"
26
#include "util/rational.h"
27
28
using namespace cvc5::kind;
29
30
namespace cvc5 {
31
namespace theory {
32
namespace quantifiers {
33
34
1900
CegisUnif::CegisUnif(Env& env,
35
                     QuantifiersState& qs,
36
                     QuantifiersInferenceManager& qim,
37
                     TermDbSygus* tds,
38
1900
                     SynthConjecture* p)
39
    : Cegis(env, qs, qim, tds, p),
40
      d_sygus_unif(env, p),
41
1900
      d_u_enum_manager(env, qs, qim, tds, p)
42
{
43
1900
}
44
45
3792
CegisUnif::~CegisUnif() {}
46
17
bool CegisUnif::processInitialize(Node conj,
47
                                  Node n,
48
                                  const std::vector<Node>& candidates)
49
{
50
  // list of strategy points for unification candidates
51
34
  std::vector<Node> unif_candidate_pts;
52
  // map from strategy points to their conditions
53
34
  std::map<Node, Node> pt_to_cond;
54
  // strategy lemmas for each strategy point
55
34
  std::map<Node, std::vector<Node>> strategy_lemmas;
56
  // Initialize strategies for all functions-to-synthesize
57
  // The role of non-unification enumerators is to be either the single solution
58
  // or part of a solution involving multiple enumerators.
59
17
  EnumeratorRole eroleNonUnif = candidates.size() == 1
60
17
                                    ? ROLE_ENUM_SINGLE_SOLUTION
61
17
                                    : ROLE_ENUM_MULTI_SOLUTION;
62
40
  for (const Node& f : candidates)
63
  {
64
    // Init UNIF util for this candidate
65
46
    d_sygus_unif.initializeCandidate(
66
23
        d_tds, f, d_cand_to_strat_pt[f], strategy_lemmas);
67
23
    if (!d_sygus_unif.usingUnif(f))
68
    {
69
6
      Trace("cegis-unif") << "* non-unification candidate : " << f << std::endl;
70
6
      d_tds->registerEnumerator(f, f, d_parent, eroleNonUnif);
71
6
      d_non_unif_candidates.push_back(f);
72
    }
73
    else
74
    {
75
17
      d_unif_candidates.push_back(f);
76
34
      Trace("cegis-unif") << "* unification candidate : " << f
77
17
                          << " with strategy points:" << std::endl;
78
17
      std::vector<Node>& enums = d_cand_to_strat_pt[f];
79
17
      unif_candidate_pts.insert(
80
34
          unif_candidate_pts.end(), enums.begin(), enums.end());
81
      // map strategy point to its condition in pt_to_cond
82
34
      for (const Node& e : enums)
83
      {
84
34
        Node cond = d_sygus_unif.getConditionForEvaluationPoint(e);
85
17
        Assert(!cond.isNull());
86
34
        Trace("cegis-unif")
87
17
            << "  " << e << " with condition : " << cond << std::endl;
88
17
        pt_to_cond[e] = cond;
89
      }
90
    }
91
  }
92
  // initialize the enumeration manager
93
17
  d_u_enum_manager.initialize(unif_candidate_pts, pt_to_cond, strategy_lemmas);
94
34
  return true;
95
}
96
97
482
void CegisUnif::getTermList(const std::vector<Node>& candidates,
98
                            std::vector<Node>& enums)
99
{
100
  // Non-unif candidate are themselves the enumerators
101
482
  enums.insert(
102
964
      enums.end(), d_non_unif_candidates.begin(), d_non_unif_candidates.end());
103
964
  for (const Node& c : d_unif_candidates)
104
  {
105
    // Collect heads of candidates
106
2274
    for (const Node& hd : d_sygus_unif.getEvalPointHeads(c))
107
    {
108
3584
      Trace("cegis-unif-enum-debug")
109
1792
          << "......cand " << c << " with enum hd " << hd << "\n";
110
1792
      enums.push_back(hd);
111
    }
112
    // get unification enumerators
113
964
    for (const Node& e : d_cand_to_strat_pt[c])
114
    {
115
1446
      for (unsigned index = 0; index < 2; index++)
116
      {
117
1928
        std::vector<Node> uenums;
118
        // get the current unification enumerators
119
964
        d_u_enum_manager.getEnumeratorsForStrategyPt(e, uenums, index);
120
        // get the model value of each enumerator
121
964
        enums.insert(enums.end(), uenums.begin(), uenums.end());
122
      }
123
    }
124
  }
125
482
}
126
127
388
bool CegisUnif::getEnumValues(const std::vector<Node>& enums,
128
                              const std::vector<Node>& enum_values,
129
                              std::map<Node, std::vector<Node>>& unif_cenums,
130
                              std::map<Node, std::vector<Node>>& unif_cvalues)
131
{
132
388
  NodeManager* nm = NodeManager::currentNM();
133
776
  Node cost_lit = d_u_enum_manager.getAssertedLiteral();
134
776
  std::map<Node, std::vector<Node>> unif_renums, unif_rvalues;
135
  // build model value map
136
776
  std::map<Node, Node> mvMap;
137
2914
  for (unsigned i = 0, size = enums.size(); i < size; i++)
138
  {
139
2526
    mvMap[enums[i]] = enum_values[i];
140
  }
141
388
  bool addedUnifEnumSymBreakLemma = false;
142
  // populate maps between unification enumerators and their model values
143
776
  for (const Node& c : d_unif_candidates)
144
  {
145
    // for each decision tree strategy allocated for c (these are referenced
146
    // by strategy points in d_cand_to_strat_pt[c])
147
776
    for (const Node& e : d_cand_to_strat_pt[c])
148
    {
149
1164
      for (unsigned index = 0; index < 2; index++)
150
      {
151
1552
        std::vector<Node> es, vs;
152
1552
        Trace("cegis-unif")
153
1552
            << "  " << (index == 0 ? "Return values" : "Conditions") << " for "
154
776
            << e << ":\n";
155
        // get the current unification enumerators
156
776
        d_u_enum_manager.getEnumeratorsForStrategyPt(e, es, index);
157
        // set enums for condition enumerators
158
776
        if (index == 1)
159
        {
160
388
          if (usingConditionPool())
161
          {
162
            Assert(es.size() == 1);
163
            // whether valueus exhausted
164
            if (mvMap.find(es[0]) == mvMap.end())
165
            {
166
              Trace("cegis-unif") << "    " << es[0] << " -> N/A\n";
167
              es.clear();
168
            }
169
          }
170
388
          unif_cenums[e] = es;
171
        }
172
        // get the model value of each enumerator
173
1756
        for (const Node& eu : es)
174
        {
175
980
          Assert(mvMap.find(eu) != mvMap.end());
176
1960
          Node m_eu = mvMap[eu];
177
980
          if (Trace.isOn("cegis-unif"))
178
          {
179
            Trace("cegis-unif") << "    " << eu << " -> ";
180
            TermDbSygus::toStreamSygus("cegis-unif", m_eu);
181
            Trace("cegis-unif") << "\n";
182
          }
183
980
          vs.push_back(m_eu);
184
        }
185
        // set values for condition enumerators of e
186
776
        if (index == 1)
187
        {
188
388
          unif_cvalues[e] = vs;
189
        }
190
        // inter-enumerator symmetry breaking for return values
191
        else
192
        {
193
          // given a pool of unification enumerators eu_1, ..., eu_n,
194
          // CegisUnifEnumDecisionStrategy insists that size(eu_1) <= ... <=
195
          // size(eu_n). We additionally insist that M(eu_i) < M(eu_{i+1}) when
196
          // size(eu_i) = size(eu_{i+1}), where < is pointer comparison.
197
          // We enforce this below by adding symmetry breaking lemmas of the
198
          // form ~( eu_i = M(eu_i) ^ eu_{i+1} = M(eu_{i+1} ) )
199
          // when applicable.
200
          // we only do this for return value enumerators, since condition
201
          // enumerators cannot be ordered (their order is based on the
202
          // seperation resolution scheme during model construction).
203
654
          for (unsigned j = 1, nenum = vs.size(); j < nenum; j++)
204
          {
205
560
            Node prev_val = vs[j - 1];
206
560
            Node curr_val = vs[j];
207
            // compare the node values
208
294
            if (curr_val < prev_val)
209
            {
210
              // must have the same size
211
28
              unsigned prev_size = datatypes::utils::getSygusTermSize(prev_val);
212
28
              unsigned curr_size = datatypes::utils::getSygusTermSize(curr_val);
213
28
              Assert(prev_size <= curr_size);
214
28
              if (curr_size == prev_size)
215
              {
216
                Node slem =
217
112
                    nm->mkNode(
218
112
                          AND, es[j - 1].eqNode(vs[j - 1]), es[j].eqNode(vs[j]))
219
56
                        .negate();
220
56
                Trace("cegis-unif")
221
                    << "CegisUnif::lemma, inter-unif-enumerator "
222
28
                       "symmetry breaking lemma : "
223
28
                    << slem << "\n";
224
28
                d_qim.lemma(
225
                    slem, InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_INTER_ENUM_SB);
226
28
                addedUnifEnumSymBreakLemma = true;
227
28
                break;
228
              }
229
            }
230
          }
231
        }
232
      }
233
    }
234
  }
235
776
  return !addedUnifEnumSymBreakLemma;
236
}
237
238
880
bool CegisUnif::usingConditionPool() const
239
{
240
880
  return d_sygus_unif.usingConditionPool();
241
}
242
243
144
void CegisUnif::setConditions(
244
    const std::map<Node, std::vector<Node>>& unif_cenums,
245
    const std::map<Node, std::vector<Node>>& unif_cvalues)
246
{
247
288
  Node cost_lit = d_u_enum_manager.getAssertedLiteral();
248
144
  NodeManager* nm = NodeManager::currentNM();
249
  // set the conditions
250
288
  for (const Node& c : d_unif_candidates)
251
  {
252
288
    for (const Node& e : d_cand_to_strat_pt[c])
253
    {
254
144
      Assert(unif_cenums.find(e) != unif_cenums.end());
255
144
      Assert(unif_cvalues.find(e) != unif_cvalues.end());
256
      std::map<Node, std::vector<Node>>::const_iterator itc =
257
144
          unif_cenums.find(e);
258
      std::map<Node, std::vector<Node>>::const_iterator itv =
259
144
          unif_cvalues.find(e);
260
144
      d_sygus_unif.setConditions(e, cost_lit, itc->second, itv->second);
261
      // d_sygus_unif.setConditions(e, cost_lit, unif_cenums[e],
262
      // unif_cvalues[e]); if condition enumerator had value and it is being
263
      // passively generated, exclude this value
264
144
      if (usingConditionPool() && !itc->second.empty())
265
      {
266
        Node eu = itc->second[0];
267
        Assert(d_tds->isEnumerator(eu));
268
        Assert(!itv->second.empty());
269
        if (d_tds->isPassiveEnumerator(eu))
270
        {
271
          Node g = d_tds->getActiveGuardForEnumerator(eu);
272
          Node exp_exc = d_tds->getExplain()
273
                             ->getExplanationForEquality(eu, itv->second[0])
274
                             .negate();
275
          Node lem = nm->mkNode(OR, g.negate(), exp_exc);
276
          d_qim.addPendingLemma(
277
              lem, InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_COND_EXCLUDE);
278
        }
279
      }
280
    }
281
  }
282
144
}
283
284
388
bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums,
285
                                           const std::vector<Node>& enum_values,
286
                                           const std::vector<Node>& candidates,
287
                                           std::vector<Node>& candidate_values,
288
                                           bool satisfiedRl)
289
{
290
388
  if (d_unif_candidates.empty())
291
  {
292
    Assert(d_non_unif_candidates.size() == candidates.size());
293
    return Cegis::processConstructCandidates(
294
        enums, enum_values, candidates, candidate_values, satisfiedRl);
295
  }
296
388
  if (Trace.isOn("cegis-unif"))
297
  {
298
    for (const Node& c : d_unif_candidates)
299
    {
300
      // Collect heads of candidates
301
      Trace("cegis-unif") << "  Evaluation heads for " << c << " :\n";
302
      for (const Node& hd : d_sygus_unif.getEvalPointHeads(c))
303
      {
304
        bool isUnit = false;
305
        // d_rl_eval_hds accumulates eval apps, so need to look at operators
306
        for (const Node& hd_unit : d_rl_eval_hds)
307
        {
308
          if (hd == hd_unit[0])
309
          {
310
            isUnit = true;
311
            break;
312
          }
313
        }
314
        Trace("cegis-unif") << "    " << hd << (isUnit ? "*" : "") << " -> ";
315
        Assert(std::find(enums.begin(), enums.end(), hd) != enums.end());
316
        unsigned i = std::distance(enums.begin(),
317
                                   std::find(enums.begin(), enums.end(), hd));
318
        Assert(i >= 0 && i < enum_values.size());
319
        TermDbSygus::toStreamSygus("cegis-unif", enum_values[i]);
320
        Trace("cegis-unif") << "\n";
321
      }
322
    }
323
  }
324
  // the unification enumerators for conditions and their model values
325
776
  std::map<Node, std::vector<Node>> unif_cenums;
326
776
  std::map<Node, std::vector<Node>> unif_cvalues;
327
  // we only proceed to solution building if we are not introducing symmetry
328
  // breaking lemmas between return values and if we have not previously
329
  // introduced return values refinement lemmas
330
776
  if (!getEnumValues(enums, enum_values, unif_cenums, unif_cvalues)
331
388
      || !satisfiedRl)
332
  {
333
    // if condition values are being indepedently enumerated, they should be
334
    // communicated to the decision tree strategies indepedently of we
335
    // proceeding to attempt solution building
336
244
    if (usingConditionPool())
337
    {
338
      setConditions(unif_cenums, unif_cvalues);
339
    }
340
488
    Trace("cegis-unif") << (!satisfiedRl
341
488
                                ? "..added refinement lemmas"
342
244
                                : "..added unif enum symmetry breaking")
343
244
                        << "\n---CegisUnif Engine---\n";
344
    // if we didn't satisfy the specification, there is no way to repair
345
244
    return false;
346
  }
347
144
  setConditions(unif_cenums, unif_cvalues);
348
  // build solutions (for unif candidates a divide-and-conquer approach is used)
349
288
  std::vector<Node> sols;
350
288
  std::vector<Node> lemmas;
351
144
  if (d_sygus_unif.constructSolution(sols, lemmas))
352
  {
353
40
    candidate_values.insert(candidate_values.end(), sols.begin(), sols.end());
354
40
    if (Trace.isOn("cegis-unif"))
355
    {
356
      Trace("cegis-unif") << "* Candidate solutions are:\n";
357
      for (const Node& sol : sols)
358
      {
359
        Trace("cegis-unif")
360
            << "... " << d_tds->sygusToBuiltin(sol, sol.getType()) << "\n";
361
      }
362
      Trace("cegis-unif") << "---CegisUnif Engine---\n";
363
    }
364
40
    return true;
365
  }
366
367
  // TODO tie this to the lemma for getting a new condition value
368
104
  Assert(usingConditionPool() || !lemmas.empty());
369
208
  for (const Node& lem : lemmas)
370
  {
371
208
    Trace("cegis-unif-lemma")
372
104
        << "CegisUnif::lemma, separation lemma : " << lem << "\n";
373
104
    d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_SEPARATION);
374
  }
375
104
  Trace("cegis-unif") << "..failed to separate heads\n---CegisUnif Engine---\n";
376
104
  return false;
377
}
378
379
26
void CegisUnif::registerRefinementLemma(const std::vector<Node>& vars, Node lem)
380
{
381
  // Notify lemma to unification utility and get its purified form
382
52
  std::map<Node, std::vector<Node>> eval_pts;
383
52
  Node plem = d_sygus_unif.addRefLemma(lem, eval_pts);
384
26
  addRefinementLemma(plem);
385
52
  Trace("cegis-unif-lemma")
386
26
      << "CegisUnif::lemma, refinement lemma : " << plem << "\n";
387
  // Notify the enumeration manager if there are new evaluation points
388
52
  for (const std::pair<const Node, std::vector<Node>>& ep : eval_pts)
389
  {
390
26
    Assert(d_cand_to_strat_pt.find(ep.first) != d_cand_to_strat_pt.end());
391
    // Notify each strategy point of the respective candidate
392
52
    for (const Node& n : d_cand_to_strat_pt[ep.first])
393
    {
394
26
      d_u_enum_manager.registerEvalPts(ep.second, n);
395
    }
396
  }
397
  // Make the refinement lemma and add it to lems. This lemma is guarded by the
398
  // parent's guard, which has the semantics "this conjecture has a solution",
399
  // hence this lemma states: if the parent conjecture has a solution, it
400
  // satisfies the specification for the given concrete point.
401
  Node rlem =
402
52
      NodeManager::currentNM()->mkNode(OR, d_parent->getGuard().negate(), plem);
403
26
  d_qim.addPendingLemma(rlem,
404
                        InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_REFINEMENT);
405
26
}
406
407
1900
CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy(
408
    Env& env,
409
    QuantifiersState& qs,
410
    QuantifiersInferenceManager& qim,
411
    TermDbSygus* tds,
412
1900
    SynthConjecture* parent)
413
1900
    : DecisionStrategyFmf(env, qs.getValuation()),
414
      d_qim(qim),
415
      d_tds(tds),
416
3800
      d_parent(parent)
417
{
418
1900
  d_initialized = false;
419
1900
  options::SygusUnifPiMode mode = options::sygusUnifPi();
420
1900
  d_useCondPool = mode == options::SygusUnifPiMode::CENUM
421
1900
                  || mode == options::SygusUnifPiMode::CENUM_IGAIN;
422
1900
}
423
424
29
Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n)
425
{
426
29
  NodeManager* nm = NodeManager::currentNM();
427
29
  SkolemManager* sm = nm->getSkolemManager();
428
29
  Node newLit = sm->mkDummySkolem("G_cost", nm->booleanType());
429
29
  unsigned new_size = n + 1;
430
431
  // allocate an enumerator for each candidate
432
58
  for (std::pair<const Node, StrategyPtInfo>& ci : d_ce_info)
433
  {
434
58
    Node c = ci.first;
435
58
    TypeNode ct = c.getType();
436
58
    Node eu = sm->mkDummySkolem("eu", ct);
437
58
    Node ceu;
438
29
    if (!d_useCondPool && !ci.second.d_enums[0].empty())
439
    {
440
      // make a new conditional enumerator as well, starting the
441
      // second type around
442
12
      ceu = sm->mkDummySkolem("cu", ci.second.d_ce_type);
443
    }
444
    // register the new enumerators
445
87
    for (unsigned index = 0; index < 2; index++)
446
    {
447
99
      Node e = index == 0 ? eu : ceu;
448
58
      if (e.isNull())
449
      {
450
17
        continue;
451
      }
452
41
      setUpEnumerator(e, ci.second, index);
453
    }
454
  }
455
  // register the evaluation points at the new value
456
58
  for (std::pair<const Node, StrategyPtInfo>& ci : d_ce_info)
457
  {
458
58
    Node c = ci.first;
459
65
    for (const Node& ei : ci.second.d_eval_points)
460
    {
461
72
      Trace("cegis-unif-enum") << "...increasing enum number for hd " << ei
462
36
                               << " to new size " << new_size << "\n";
463
36
      registerEvalPtAtSize(c, ei, newLit, new_size);
464
    }
465
  }
466
  // enforce fairness between number of enumerators and enumerator size
467
29
  if (new_size > 1)
468
  {
469
    // construct the "virtual enumerator"
470
12
    if (d_virtual_enum.isNull())
471
    {
472
      // we construct the default integer grammar with no variables, e.g.:
473
      //   A -> 1 | A+A
474
20
      TypeNode intTn = nm->integerType();
475
      // use a null variable list
476
20
      Node bvl;
477
20
      std::string veName("_virtual_enum_grammar");
478
20
      SygusDatatype sdt(veName);
479
20
      TypeNode u = nm->mkSort(veName, NodeManager::SORT_FLAG_PLACEHOLDER);
480
20
      std::set<TypeNode> unresolvedTypes;
481
10
      unresolvedTypes.insert(u);
482
20
      std::vector<TypeNode> cargsEmpty;
483
20
      Node cr = nm->mkConst(Rational(1));
484
10
      sdt.addConstructor(cr, "1", cargsEmpty);
485
20
      std::vector<TypeNode> cargsPlus;
486
10
      cargsPlus.push_back(u);
487
10
      cargsPlus.push_back(u);
488
10
      sdt.addConstructor(PLUS, cargsPlus);
489
10
      sdt.initializeDatatype(nm->integerType(), bvl, false, false);
490
20
      std::vector<DType> datatypes;
491
10
      datatypes.push_back(sdt.getDatatype());
492
      std::vector<TypeNode> dtypes = nm->mkMutualDatatypeTypes(
493
20
          datatypes, unresolvedTypes, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
494
10
      d_virtual_enum = sm->mkDummySkolem("_ve", dtypes[0]);
495
20
      d_tds->registerEnumerator(
496
20
          d_virtual_enum, Node::null(), d_parent, ROLE_ENUM_CONSTRAINED);
497
    }
498
    // if new_size is a power of two, then isPow2 returns log2(new_size)+1
499
    // otherwise, this returns 0. In the case it returns 0, we don't care
500
    // since the floor( log2( i ) ) = floor( log2( i - 1 ) ) and we do not
501
    // increase our size bound.
502
12
    unsigned pow_two = Integer(new_size).isPow2();
503
12
    if (pow_two > 0)
504
    {
505
20
      Node size_ve = nm->mkNode(DT_SIZE, d_virtual_enum);
506
      Node fair_lemma =
507
20
          nm->mkNode(GEQ, size_ve, nm->mkConst(Rational(pow_two - 1)));
508
10
      fair_lemma = nm->mkNode(OR, newLit, fair_lemma);
509
20
      Trace("cegis-unif-enum-lemma")
510
10
          << "CegisUnifEnum::lemma, fairness size:" << fair_lemma << "\n";
511
      // this lemma relates the number of conditions we enumerate and the
512
      // maximum size of a term that is part of our solution. It is of the
513
      // form:
514
      //   G_uq_i => size(ve) >= log_2( i-1 )
515
      // In other words, if we use i conditions, then we allow terms in our
516
      // solution whose size is at most log_2(i-1).
517
10
      d_qim.lemma(fair_lemma, InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_FAIR_SIZE);
518
    }
519
  }
520
521
29
  return newLit;
522
}
523
524
17
void CegisUnifEnumDecisionStrategy::initialize(
525
    const std::vector<Node>& es,
526
    const std::map<Node, Node>& e_to_cond,
527
    const std::map<Node, std::vector<Node>>& strategy_lemmas)
528
{
529
17
  Assert(!d_initialized);
530
17
  d_initialized = true;
531
17
  if (es.empty())
532
  {
533
    return;
534
  }
535
  // initialize type information for candidates
536
17
  NodeManager* nm = NodeManager::currentNM();
537
17
  SkolemManager* sm = nm->getSkolemManager();
538
34
  for (const Node& e : es)
539
  {
540
17
    Trace("cegis-unif-enum-debug") << "...adding strategy point " << e << "\n";
541
    // currently, we allocate the same enumerators for candidates of the same
542
    // type
543
17
    d_ce_info[e].d_pt = e;
544
17
    std::map<Node, Node>::const_iterator itcc = e_to_cond.find(e);
545
17
    Assert(itcc != e_to_cond.end());
546
34
    Node cond = itcc->second;
547
34
    Trace("cegis-unif-enum-debug")
548
17
        << "...its condition strategy point is " << cond << "\n";
549
17
    d_ce_info[e].d_ce_type = cond.getType();
550
    // initialize the symmetry breaking lemma templates
551
51
    for (unsigned index = 0; index < 2; index++)
552
    {
553
34
      Assert(d_ce_info[e].d_sbt_lemma_tmpl[index].first.isNull());
554
65
      Node sp = index == 0 ? e : cond;
555
      std::map<Node, std::vector<Node>>::const_iterator it =
556
34
          strategy_lemmas.find(sp);
557
34
      if (it == strategy_lemmas.end())
558
      {
559
3
        continue;
560
      }
561
      // collect lemmas for removing redundant ops for this candidate's type
562
      Node d_sbt_lemma =
563
62
          it->second.size() == 1 ? it->second[0] : nm->mkNode(AND, it->second);
564
62
      Trace("cegis-unif-enum-debug")
565
31
          << "...adding lemma template to remove redundant operators for " << sp
566
31
          << " --> lambda " << sp << ". " << d_sbt_lemma << "\n";
567
62
      d_ce_info[e].d_sbt_lemma_tmpl[index] =
568
93
          std::pair<Node, Node>(d_sbt_lemma, sp);
569
    }
570
  }
571
572
  // register this strategy
573
17
  d_qim.getDecisionManager()->registerStrategy(
574
      DecisionManager::STRAT_QUANT_CEGIS_UNIF_NUM_ENUMS, this);
575
576
  // create single condition enumerator for each decision tree strategy
577
17
  if (d_useCondPool)
578
  {
579
    // allocate a condition enumerator for each candidate
580
    for (std::pair<const Node, StrategyPtInfo>& ci : d_ce_info)
581
    {
582
      Node ceu = sm->mkDummySkolem("cu", ci.second.d_ce_type);
583
      setUpEnumerator(ceu, ci.second, 1);
584
    }
585
  }
586
}
587
588
1740
void CegisUnifEnumDecisionStrategy::getEnumeratorsForStrategyPt(
589
    Node e, std::vector<Node>& es, unsigned index) const
590
{
591
  // the number of active enumerators is related to the current cost value
592
1740
  unsigned num_enums = 0;
593
1740
  bool has_num_enums = getAssertedLiteralIndex(num_enums);
594
1740
  AlwaysAssert(has_num_enums);
595
1740
  num_enums = num_enums + 1;
596
1740
  if (index == 1)
597
  {
598
    // we always use (cost-1) conditions, or 1 if in the indepedent case
599
870
    num_enums = !d_useCondPool ? num_enums - 1 : 1;
600
  }
601
1740
  if (num_enums > 0)
602
  {
603
1386
    std::map<Node, StrategyPtInfo>::const_iterator itc = d_ce_info.find(e);
604
1386
    Assert(itc != d_ce_info.end());
605
1386
    Assert(num_enums <= itc->second.d_enums[index].size());
606
4158
    es.insert(es.end(),
607
1386
              itc->second.d_enums[index].begin(),
608
6930
              itc->second.d_enums[index].begin() + num_enums);
609
  }
610
1740
}
611
612
41
void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e,
613
                                                    StrategyPtInfo& si,
614
                                                    unsigned index)
615
{
616
41
  NodeManager* nm = NodeManager::currentNM();
617
  // instantiate template for removing redundant operators
618
41
  if (!si.d_sbt_lemma_tmpl[index].first.isNull())
619
  {
620
82
    Node templ = si.d_sbt_lemma_tmpl[index].first;
621
82
    TNode templ_var = si.d_sbt_lemma_tmpl[index].second;
622
82
    Node sym_break_red_ops = templ.substitute(templ_var, e);
623
82
    Trace("cegis-unif-enum-lemma")
624
41
        << "CegisUnifEnum::lemma, remove redundant ops of " << e << " : "
625
41
        << sym_break_red_ops << "\n";
626
41
    d_qim.lemma(sym_break_red_ops,
627
                InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_REM_OPS);
628
  }
629
  // symmetry breaking between enumerators
630
41
  if (!si.d_enums[index].empty() && index == 0)
631
  {
632
24
    Node e_prev = si.d_enums[index].back();
633
24
    Node size_e = nm->mkNode(DT_SIZE, e);
634
24
    Node size_e_prev = nm->mkNode(DT_SIZE, e_prev);
635
24
    Node sym_break = nm->mkNode(GEQ, size_e, size_e_prev);
636
24
    Trace("cegis-unif-enum-lemma")
637
12
        << "CegisUnifEnum::lemma, enum sym break:" << sym_break << "\n";
638
12
    d_qim.lemma(sym_break, InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_ENUM_SB);
639
  }
640
  // register the enumerator
641
41
  si.d_enums[index].push_back(e);
642
41
  EnumeratorRole erole = ROLE_ENUM_CONSTRAINED;
643
  // if we are using a single independent enumerator for conditions, then we
644
  // allocate an active guard, and are eligible to use variable-agnostic
645
  // enumeration.
646
41
  if (d_useCondPool && index == 1)
647
  {
648
    erole = ROLE_ENUM_POOL;
649
  }
650
82
  Trace("cegis-unif-enum") << "* Registering new enumerator " << e
651
41
                           << " to strategy point " << si.d_pt << "\n";
652
41
  d_tds->registerEnumerator(e, si.d_pt, d_parent, erole);
653
41
}
654
655
26
void CegisUnifEnumDecisionStrategy::registerEvalPts(
656
    const std::vector<Node>& eis, Node e)
657
{
658
  // candidates of the same type are managed
659
26
  std::map<Node, StrategyPtInfo>::iterator it = d_ce_info.find(e);
660
26
  Assert(it != d_ce_info.end());
661
52
  it->second.d_eval_points.insert(
662
52
      it->second.d_eval_points.end(), eis.begin(), eis.end());
663
  // register at all already allocated sizes
664
72
  for (const Node& ei : eis)
665
  {
666
46
    Assert(ei.getType() == e.getType());
667
106
    for (unsigned j = 0, size = d_literals.size(); j < size; j++)
668
    {
669
120
      Trace("cegis-unif-enum") << "...for cand " << e << " adding hd " << ei
670
60
                               << " at size " << j << "\n";
671
60
      registerEvalPtAtSize(e, ei, d_literals[j], j + 1);
672
    }
673
  }
674
26
}
675
676
96
void CegisUnifEnumDecisionStrategy::registerEvalPtAtSize(Node e,
677
                                                         Node ei,
678
                                                         Node guq_lit,
679
                                                         unsigned n)
680
{
681
  // must be equal to one of the first n enums
682
96
  std::map<Node, StrategyPtInfo>::iterator itc = d_ce_info.find(e);
683
96
  Assert(itc != d_ce_info.end());
684
96
  Assert(itc->second.d_enums[0].size() >= n);
685
192
  std::vector<Node> disj;
686
96
  disj.push_back(guq_lit.negate());
687
252
  for (unsigned i = 0; i < n; i++)
688
  {
689
156
    disj.push_back(ei.eqNode(itc->second.d_enums[0][i]));
690
  }
691
192
  Node lem = NodeManager::currentNM()->mkNode(OR, disj);
692
192
  Trace("cegis-unif-enum-lemma")
693
96
      << "CegisUnifEnum::lemma, domain:" << lem << "\n";
694
96
  d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_DOMAIN);
695
96
}
696
697
}  // namespace quantifiers
698
}  // namespace theory
699
31137
}  // namespace cvc5