GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/cegis_unif.cpp Lines: 303 348 87.1 %
Date: 2021-03-23 Branches: 511 1388 36.8 %

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