GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/synth_conjecture.cpp Lines: 601 688 87.4 %
Date: 2021-03-22 Branches: 1283 3146 40.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file synth_conjecture.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 class that encapsulates techniques for a single
13
 ** (SyGuS) synthesis conjecture.
14
 **/
15
#include "theory/quantifiers/sygus/synth_conjecture.h"
16
17
#include "base/configuration.h"
18
#include "options/base_options.h"
19
#include "options/datatypes_options.h"
20
#include "options/quantifiers_options.h"
21
#include "printer/printer.h"
22
#include "smt/logic_exception.h"
23
#include "smt/smt_engine_scope.h"
24
#include "smt/smt_statistics_registry.h"
25
#include "theory/datatypes/sygus_datatype_utils.h"
26
#include "theory/quantifiers/first_order_model.h"
27
#include "theory/quantifiers/instantiate.h"
28
#include "theory/quantifiers/quantifiers_attributes.h"
29
#include "theory/quantifiers/sygus/enum_stream_substitution.h"
30
#include "theory/quantifiers/sygus/sygus_enumerator.h"
31
#include "theory/quantifiers/sygus/sygus_enumerator_basic.h"
32
#include "theory/quantifiers/sygus/synth_engine.h"
33
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
34
#include "theory/quantifiers/sygus/sygus_pbe.h"
35
#include "theory/quantifiers/sygus/term_database_sygus.h"
36
#include "theory/quantifiers/term_util.h"
37
#include "theory/quantifiers_engine.h"
38
#include "theory/rewriter.h"
39
#include "theory/smt_engine_subsolver.h"
40
41
using namespace CVC4::kind;
42
using namespace std;
43
44
namespace CVC4 {
45
namespace theory {
46
namespace quantifiers {
47
48
2190
SynthConjecture::SynthConjecture(QuantifiersEngine* qe,
49
                                 QuantifiersState& qs,
50
                                 QuantifiersInferenceManager& qim,
51
                                 QuantifiersRegistry& qr,
52
2190
                                 SygusStatistics& s)
53
    : d_qe(qe),
54
      d_qstate(qs),
55
      d_qim(qim),
56
      d_qreg(qr),
57
      d_stats(s),
58
2190
      d_tds(qe->getTermDatabaseSygus()),
59
      d_hasSolution(false),
60
2190
      d_ceg_si(new CegSingleInv(qe)),
61
2190
      d_templInfer(new SygusTemplateInfer),
62
2190
      d_ceg_proc(new SynthConjectureProcess(qe)),
63
2190
      d_ceg_gc(new CegGrammarConstructor(d_tds, this)),
64
2190
      d_sygus_rconst(new SygusRepairConst(qe)),
65
2190
      d_exampleInfer(new ExampleInfer(d_tds)),
66
2190
      d_ceg_pbe(new SygusPbe(qe, qim, this)),
67
2190
      d_ceg_cegis(new Cegis(qe, qim, this)),
68
2190
      d_ceg_cegisUnif(new CegisUnif(qe, qs, qim, this)),
69
2190
      d_sygus_ccore(new CegisCoreConnective(qe, qim, this)),
70
      d_master(nullptr),
71
      d_set_ce_sk_vars(false),
72
      d_repair_index(0),
73
      d_refine_count(0),
74
26280
      d_guarded_stream_exc(false)
75
{
76
2190
  if (options::sygusSymBreakPbe() || options::sygusUnifPbe())
77
  {
78
2190
    d_modules.push_back(d_ceg_pbe.get());
79
  }
80
2190
  if (options::sygusUnifPi() != options::SygusUnifPiMode::NONE)
81
  {
82
75
    d_modules.push_back(d_ceg_cegisUnif.get());
83
  }
84
2190
  if (options::sygusCoreConnective())
85
  {
86
126
    d_modules.push_back(d_sygus_ccore.get());
87
  }
88
2190
  d_modules.push_back(d_ceg_cegis.get());
89
2190
}
90
91
2188
SynthConjecture::~SynthConjecture() {}
92
93
2156
void SynthConjecture::presolve()
94
{
95
  // we don't have a solution yet
96
2156
  d_hasSolution = false;
97
2156
}
98
99
506
void SynthConjecture::assign(Node q)
100
{
101
506
  Assert(d_embed_quant.isNull());
102
506
  Assert(q.getKind() == FORALL);
103
506
  Trace("cegqi") << "SynthConjecture : assign : " << q << std::endl;
104
506
  d_quant = q;
105
506
  NodeManager* nm = NodeManager::currentNM();
106
107
  // initialize the guard
108
506
  d_feasible_guard = nm->mkSkolem("G", nm->booleanType());
109
506
  d_feasible_guard = Rewriter::rewrite(d_feasible_guard);
110
506
  d_feasible_guard = d_qstate.getValuation().ensureLiteral(d_feasible_guard);
111
506
  AlwaysAssert(!d_feasible_guard.isNull());
112
113
  // pre-simplify the quantified formula based on the process utility
114
506
  d_simp_quant = d_ceg_proc->preSimplify(d_quant);
115
116
  // compute its attributes
117
1009
  QAttributes qa;
118
506
  QuantAttributes::computeQuantAttributes(q, qa);
119
120
1009
  std::map<Node, Node> templates;
121
1009
  std::map<Node, Node> templates_arg;
122
  // register with single invocation if applicable
123
506
  if (qa.d_sygus)
124
  {
125
506
    d_ceg_si->initialize(d_simp_quant);
126
506
    d_simp_quant = d_ceg_si->getSimplifiedConjecture();
127
506
    if (!d_ceg_si->isSingleInvocation())
128
    {
129
506
      d_templInfer->initialize(d_simp_quant);
130
    }
131
    // carry the templates
132
1289
    for (const Node& v : q[0])
133
    {
134
1566
      Node templ = d_templInfer->getTemplate(v);
135
783
      if (!templ.isNull())
136
      {
137
47
        templates[v] = templ;
138
47
        templates_arg[v] = d_templInfer->getTemplateArg(v);
139
      }
140
    }
141
  }
142
143
  // post-simplify the quantified formula based on the process utility
144
506
  d_simp_quant = d_ceg_proc->postSimplify(d_simp_quant);
145
146
  // finished simplifying the quantified formula at this point
147
148
  // convert to deep embedding and finalize single invocation here
149
506
  d_embed_quant = d_ceg_gc->process(d_simp_quant, templates, templates_arg);
150
1012
  Trace("cegqi") << "SynthConjecture : converted to embedding : "
151
506
                 << d_embed_quant << std::endl;
152
153
1009
  Node sc = qa.d_sygusSideCondition;
154
506
  if (!sc.isNull())
155
  {
156
    // convert to deep embedding
157
22
    d_embedSideCondition = d_ceg_gc->convertToEmbedding(sc);
158
44
    Trace("cegqi") << "SynthConjecture : side condition : "
159
22
                   << d_embedSideCondition << std::endl;
160
  }
161
162
  // we now finalize the single invocation module, based on the syntax
163
  // restrictions
164
506
  if (qa.d_sygus)
165
  {
166
506
    d_ceg_si->finishInit(d_ceg_gc->isSyntaxRestricted());
167
  }
168
169
506
  Assert(d_candidates.empty());
170
1009
  std::vector<Node> vars;
171
1289
  for (unsigned i = 0; i < d_embed_quant[0].getNumChildren(); i++)
172
  {
173
783
    vars.push_back(d_embed_quant[0][i]);
174
    Node e =
175
1566
        NodeManager::currentNM()->mkSkolem("e", d_embed_quant[0][i].getType());
176
783
    d_candidates.push_back(e);
177
  }
178
1012
  Trace("cegqi") << "Base quantified formula is : " << d_embed_quant
179
506
                 << std::endl;
180
  // construct base instantiation
181
1012
  d_base_inst = Rewriter::rewrite(d_qe->getInstantiate()->getInstantiation(
182
506
      d_embed_quant, vars, d_candidates));
183
506
  if (!d_embedSideCondition.isNull())
184
  {
185
44
    d_embedSideCondition = d_embedSideCondition.substitute(
186
22
        vars.begin(), vars.end(), d_candidates.begin(), d_candidates.end());
187
  }
188
506
  Trace("cegqi") << "Base instantiation is :      " << d_base_inst << std::endl;
189
190
  // initialize the sygus constant repair utility
191
506
  if (options::sygusRepairConst())
192
  {
193
13
    d_sygus_rconst->initialize(d_base_inst.negate(), d_candidates);
194
26
    if (options::sygusConstRepairAbort())
195
    {
196
      if (!d_sygus_rconst->isActive())
197
      {
198
        // no constant repair is possible: abort
199
        std::stringstream ss;
200
        ss << "Grammar does not allow repair constants." << std::endl;
201
        throw LogicException(ss.str());
202
      }
203
    }
204
  }
205
  // initialize the example inference utility
206
506
  if (!d_exampleInfer->initialize(d_base_inst, d_candidates))
207
  {
208
    // there is a contradictory example pair, the conjecture is infeasible.
209
6
    Node infLem = d_feasible_guard.negate();
210
3
    d_qim.lemma(infLem, InferenceId::QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA);
211
    // we don't need to continue initialization in this case
212
3
    return;
213
  }
214
215
  // register this term with sygus database and other utilities that impact
216
  // the enumerative sygus search
217
1006
  std::vector<Node> guarded_lemmas;
218
503
  if (!isSingleInvocation())
219
  {
220
383
    d_ceg_proc->initialize(d_base_inst, d_candidates);
221
691
    for (unsigned i = 0, size = d_modules.size(); i < size; i++)
222
    {
223
1382
      if (d_modules[i]->initialize(
224
691
              d_simp_quant, d_base_inst, d_candidates, guarded_lemmas))
225
      {
226
383
        d_master = d_modules[i];
227
383
        break;
228
      }
229
    }
230
383
    Assert(d_master != nullptr);
231
  }
232
233
503
  Assert(d_qreg.getQuantAttributes().isSygus(q));
234
  // if the base instantiation is an existential, store its variables
235
503
  if (d_base_inst.getKind() == NOT && d_base_inst[0].getKind() == FORALL)
236
  {
237
1489
    for (const Node& v : d_base_inst[0][0])
238
    {
239
1199
      d_inner_vars.push_back(v);
240
    }
241
  }
242
243
  // register the strategy
244
1509
  d_feasible_strategy.reset(
245
      new DecisionStrategySingleton("sygus_feasible",
246
                                    d_feasible_guard,
247
503
                                    d_qstate.getSatContext(),
248
1006
                                    d_qstate.getValuation()));
249
503
  d_qe->getDecisionManager()->registerStrategy(
250
      DecisionManager::STRAT_QUANT_SYGUS_FEASIBLE, d_feasible_strategy.get());
251
  // this must be called, both to ensure that the feasible guard is
252
  // decided on with true polariy, but also to ensure that output channel
253
  // has been used on this call to check.
254
503
  d_qim.requirePhase(d_feasible_guard, true);
255
256
1006
  Node gneg = d_feasible_guard.negate();
257
509
  for (unsigned i = 0; i < guarded_lemmas.size(); i++)
258
  {
259
12
    Node lem = nm->mkNode(OR, gneg, guarded_lemmas[i]);
260
12
    Trace("cegqi-lemma") << "Cegqi::Lemma : initial (guarded) lemma : " << lem
261
6
                         << std::endl;
262
6
    d_qim.lemma(lem, InferenceId::UNKNOWN);
263
  }
264
265
1006
  Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation()
266
503
                 << std::endl;
267
}
268
269
7172
Node SynthConjecture::getGuard() const { return d_feasible_guard; }
270
271
59208
bool SynthConjecture::isSingleInvocation() const
272
{
273
59208
  return d_ceg_si->isSingleInvocation();
274
}
275
276
8489
bool SynthConjecture::needsCheck()
277
{
278
  bool value;
279
8489
  Assert(!d_feasible_guard.isNull());
280
  // non or fully single invocation : look at guard only
281
8489
  if (d_qstate.getValuation().hasSatValue(d_feasible_guard, value))
282
  {
283
8489
    if (!value)
284
    {
285
12
      Trace("sygus-engine-debug") << "Conjecture is infeasible." << std::endl;
286
12
      return false;
287
    }
288
    else
289
    {
290
16954
      Trace("sygus-engine-debug") << "Feasible guard " << d_feasible_guard
291
8477
                                  << " assigned true." << std::endl;
292
    }
293
  }
294
  else
295
  {
296
    Trace("cegqi-warn") << "WARNING: Guard " << d_feasible_guard
297
                        << " is not assigned!" << std::endl;
298
    Assert(false);
299
  }
300
8477
  return true;
301
}
302
303
158072
bool SynthConjecture::needsRefinement() const { return d_set_ce_sk_vars; }
304
56333
bool SynthConjecture::doCheck(std::vector<Node>& lems)
305
{
306
56333
  if (isSingleInvocation())
307
  {
308
    // We now try to solve with the single invocation solver, which may or may
309
    // not succeed in solving the conjecture. In either case,  we are done and
310
    // return true.
311
110
    if (d_ceg_si->solve())
312
    {
313
99
      d_hasSolution = true;
314
      // the conjecture has a solution, so its negation holds
315
99
      lems.push_back(d_quant.negate());
316
    }
317
110
    return true;
318
  }
319
56223
  Assert(d_master != nullptr);
320
56223
  Assert(!d_hasSolution);
321
322
  // get the list of terms that the master strategy is interested in
323
112446
  std::vector<Node> terms;
324
56223
  d_master->getTermList(d_candidates, terms);
325
326
56223
  Assert(!d_candidates.empty());
327
328
112446
  Trace("cegqi-check") << "CegConjuncture : check, build candidates..."
329
56223
                       << std::endl;
330
112446
  std::vector<Node> candidate_values;
331
56223
  bool constructed_cand = false;
332
333
  // If a module is not trying to repair constants in solutions and the option
334
  // sygusRepairConst  is true, we use a default scheme for trying to repair
335
  // constants here.
336
  bool doRepairConst =
337
56223
      options::sygusRepairConst() && !d_master->usingRepairConst();
338
56223
  if (doRepairConst)
339
  {
340
    // have we tried to repair the previous solution?
341
    // if not, call the repair constant utility
342
    unsigned ninst = d_cinfo[d_candidates[0]].d_inst.size();
343
    if (d_repair_index < ninst)
344
    {
345
      std::vector<Node> fail_cvs;
346
      for (const Node& cprog : d_candidates)
347
      {
348
        Assert(d_repair_index < d_cinfo[cprog].d_inst.size());
349
        fail_cvs.push_back(d_cinfo[cprog].d_inst[d_repair_index]);
350
      }
351
      if (Trace.isOn("sygus-engine"))
352
      {
353
        Trace("sygus-engine") << "CegConjuncture : repair previous solution ";
354
        for (const Node& fc : fail_cvs)
355
        {
356
          std::stringstream ss;
357
          TermDbSygus::toStreamSygus(ss, fc);
358
          Trace("sygus-engine") << ss.str() << " ";
359
        }
360
        Trace("sygus-engine") << std::endl;
361
      }
362
      d_repair_index++;
363
      if (d_sygus_rconst->repairSolution(
364
              d_candidates, fail_cvs, candidate_values, true))
365
      {
366
        constructed_cand = true;
367
      }
368
    }
369
  }
370
371
112450
  bool printDebug = options::debugSygus();
372
56223
  if (!constructed_cand)
373
  {
374
    // get the model value of the relevant terms from the master module
375
78511
    std::vector<Node> enum_values;
376
56223
    bool activeIncomplete = false;
377
56223
    bool fullModel = getEnumeratedValues(terms, enum_values, activeIncomplete);
378
379
    // if the master requires a full model and the model is partial, we fail
380
56211
    if (!d_master->allowPartialModel() && !fullModel)
381
    {
382
      // we retain the values in d_ev_active_gen_waiting
383
27760
      Trace("sygus-engine-debug") << "...partial model, fail." << std::endl;
384
      // if we are partial due to an active enumerator, we may still succeed
385
      // on the next call
386
27760
      return !activeIncomplete;
387
    }
388
    // the waiting values are passed to the module below, clear
389
28451
    d_ev_active_gen_waiting.clear();
390
391
28451
    Assert(terms.size() == enum_values.size());
392
28451
    bool emptyModel = true;
393
83482
    for (unsigned i = 0, size = terms.size(); i < size; i++)
394
    {
395
55031
      if (!enum_values[i].isNull())
396
      {
397
48125
        emptyModel = false;
398
      }
399
    }
400
28451
    if (emptyModel)
401
    {
402
6175
      Trace("sygus-engine-debug") << "...empty model, fail." << std::endl;
403
6175
      return !activeIncomplete;
404
    }
405
    // Must separately compute whether trace is on due to compilation of
406
    // Trace.isOn.
407
22276
    bool traceIsOn = Trace.isOn("sygus-engine");
408
22276
    if (printDebug || traceIsOn)
409
    {
410
4
      Trace("sygus-engine") << "  * Value is : ";
411
8
      std::stringstream sygusEnumOut;
412
8
      for (unsigned i = 0, size = terms.size(); i < size; i++)
413
      {
414
8
        Node nv = enum_values[i];
415
8
        Node onv = nv.isNull() ? d_qe->getModel()->getValue(terms[i]) : nv;
416
8
        TypeNode tn = onv.getType();
417
8
        std::stringstream ss;
418
4
        TermDbSygus::toStreamSygus(ss, onv);
419
4
        if (printDebug)
420
        {
421
4
          sygusEnumOut << " " << ss.str();
422
        }
423
4
        Trace("sygus-engine") << terms[i] << " -> ";
424
4
        if (nv.isNull())
425
        {
426
          Trace("sygus-engine") << "[EXC: " << ss.str() << "] ";
427
        }
428
        else
429
        {
430
4
          Trace("sygus-engine") << ss.str() << " ";
431
4
          if (Trace.isOn("sygus-engine-rr"))
432
          {
433
            Node bv = d_tds->sygusToBuiltin(nv, tn);
434
            bv = Rewriter::rewrite(bv);
435
            Trace("sygus-engine-rr") << " -> " << bv << std::endl;
436
          }
437
        }
438
      }
439
4
      Trace("sygus-engine") << std::endl;
440
4
      if (printDebug)
441
      {
442
4
        Options& sopts = smt::currentSmtEngine()->getOptions();
443
4
        std::ostream& out = *sopts.getOut();
444
4
        out << "(sygus-enum" << sygusEnumOut.str() << ")" << std::endl;
445
      }
446
    }
447
22276
    Assert(candidate_values.empty());
448
44552
    constructed_cand = d_master->constructCandidates(
449
22276
        terms, enum_values, d_candidates, candidate_values, lems);
450
    // now clear the evaluation caches
451
29324
    for (std::pair<const Node, std::unique_ptr<ExampleEvalCache> >& ecp :
452
22276
         d_exampleEvalCache)
453
    {
454
29324
      ExampleEvalCache* eec = ecp.second.get();
455
29324
      if (eec != nullptr)
456
      {
457
5317
        eec->clearEvaluationAll();
458
      }
459
    }
460
  }
461
462
22276
  NodeManager* nm = NodeManager::currentNM();
463
464
  // check the side condition if we constructed a candidate
465
22276
  if (constructed_cand)
466
  {
467
2648
    if (!checkSideCondition(candidate_values))
468
    {
469
136
      excludeCurrentSolution(terms, candidate_values);
470
136
      Trace("sygus-engine") << "...failed side condition" << std::endl;
471
136
      return false;
472
    }
473
  }
474
475
  // must get a counterexample to the value of the current candidate
476
44280
  Node inst;
477
22140
  if (constructed_cand)
478
  {
479
2512
    if (Trace.isOn("cegqi-check"))
480
    {
481
      Trace("cegqi-check") << "CegConjuncture : check candidate : "
482
                           << std::endl;
483
      for (unsigned i = 0, size = candidate_values.size(); i < size; i++)
484
      {
485
        Trace("cegqi-check") << "  " << i << " : " << d_candidates[i] << " -> "
486
                             << candidate_values[i] << std::endl;
487
      }
488
    }
489
2512
    Assert(candidate_values.size() == d_candidates.size());
490
2512
    inst = d_base_inst.substitute(d_candidates.begin(),
491
                                  d_candidates.end(),
492
                                  candidate_values.begin(),
493
                                  candidate_values.end());
494
  }
495
  else
496
  {
497
19628
    inst = d_base_inst;
498
  }
499
500
22140
  if (!constructed_cand)
501
  {
502
19628
    return false;
503
  }
504
505
  // if we trust the sampling we ran, we terminate now
506
2512
  if (options::cegisSample() == options::CegisSampleMode::TRUST)
507
  {
508
    // we have that the current candidate passed a sample test
509
    // since we trust sampling in this mode, we assert there is no
510
    // counterexample to the conjecture here.
511
1
    lems.push_back(d_quant.negate());
512
1
    recordSolution(candidate_values);
513
1
    return true;
514
  }
515
2511
  Assert(!d_set_ce_sk_vars);
516
517
  // immediately skolemize inner existentials
518
5022
  Node query;
519
  // introduce the skolem variables
520
5022
  std::vector<Node> sks;
521
5022
  std::vector<Node> vars;
522
2511
  if (constructed_cand)
523
  {
524
2511
    if (printDebug)
525
    {
526
4
      Options& sopts = smt::currentSmtEngine()->getOptions();
527
4
      std::ostream& out = *sopts.getOut();
528
4
      out << "(sygus-candidate ";
529
4
      Assert(d_quant[0].getNumChildren() == candidate_values.size());
530
8
      for (unsigned i = 0, ncands = candidate_values.size(); i < ncands; i++)
531
      {
532
8
        Node v = candidate_values[i];
533
8
        std::stringstream ss;
534
4
        TermDbSygus::toStreamSygus(ss, v);
535
4
        out << "(" << d_quant[0][i] << " " << ss.str() << ")";
536
      }
537
4
      out << ")" << std::endl;
538
    }
539
2511
    if (inst.getKind() == NOT && inst[0].getKind() == FORALL)
540
    {
541
5117
      for (const Node& v : inst[0][0])
542
      {
543
8878
        Node sk = nm->mkSkolem("rsk", v.getType());
544
4439
        sks.push_back(sk);
545
4439
        vars.push_back(v);
546
8878
        Trace("cegqi-check-debug")
547
4439
            << "  introduce skolem " << sk << " for " << v << "\n";
548
      }
549
678
      query = inst[0][1].substitute(
550
          vars.begin(), vars.end(), sks.begin(), sks.end());
551
678
      query = query.negate();
552
    }
553
    else
554
    {
555
      // use the instance itself
556
1833
      query = inst;
557
    }
558
  }
559
2511
  d_ce_sk_vars.insert(d_ce_sk_vars.end(), sks.begin(), sks.end());
560
2511
  d_set_ce_sk_vars = true;
561
562
2511
  if (query.isNull())
563
  {
564
    // no lemma to check
565
    return false;
566
  }
567
568
  // simplify the lemma based on the term database sygus utility
569
2511
  query = d_tds->rewriteNode(query);
570
  // eagerly unfold applications of evaluation function
571
2511
  Trace("cegqi-debug") << "pre-unfold counterexample : " << query << std::endl;
572
  // Record the solution, which may be falsified below. We require recording
573
  // here since the result of the satisfiability test may be unknown.
574
2511
  recordSolution(candidate_values);
575
576
2511
  if (!query.isConst() || query.getConst<bool>())
577
  {
578
904
    Trace("sygus-engine") << "  *** Verify with subcall..." << std::endl;
579
1119
    Result r = checkWithSubsolver(query, d_ce_sk_vars, d_ce_sk_var_mvs);
580
904
    Trace("sygus-engine") << "  ...got " << r << std::endl;
581
904
    if (r.asSatisfiabilityResult().isSat() == Result::SAT)
582
    {
583
673
      if (Trace.isOn("sygus-engine"))
584
      {
585
        Trace("sygus-engine") << "  * Verification lemma failed for:\n   ";
586
        for (unsigned i = 0, size = d_ce_sk_vars.size(); i < size; i++)
587
        {
588
          Trace("sygus-engine")
589
              << d_ce_sk_vars[i] << " -> " << d_ce_sk_var_mvs[i] << " ";
590
        }
591
        Trace("sygus-engine") << std::endl;
592
      }
593
673
      if (Configuration::isAssertionBuild())
594
      {
595
        // the values for the query should be a complete model
596
        Node squery = query.substitute(d_ce_sk_vars.begin(),
597
                                       d_ce_sk_vars.end(),
598
                                       d_ce_sk_var_mvs.begin(),
599
1346
                                       d_ce_sk_var_mvs.end());
600
673
        Trace("cegqi-debug") << "...squery : " << squery << std::endl;
601
673
        squery = Rewriter::rewrite(squery);
602
673
        Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl;
603
673
        Assert(options::sygusRecFun()
604
               || (squery.isConst() && squery.getConst<bool>()));
605
      }
606
673
      return false;
607
    }
608
231
    else if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
609
    {
610
      // In the rare case that the subcall is unknown, we simply exclude the
611
      // solution, without adding a counterexample point. This should only
612
      // happen if the quantifier free logic is undecidable.
613
16
      excludeCurrentSolution(terms, candidate_values);
614
      // We should set incomplete, since a "sat" answer should not be
615
      // interpreted as "infeasible", which would make a difference in the rare
616
      // case where e.g. we had a finite grammar and exhausted the grammar.
617
16
      d_qim.setIncomplete();
618
16
      return false;
619
    }
620
    // otherwise we are unsat, and we will process the solution below
621
  }
622
  // now mark that we have a solution
623
1822
  d_hasSolution = true;
624
1822
  if (options::sygusStream())
625
  {
626
    // immediately print the current solution
627
1497
    printAndContinueStream(terms, candidate_values);
628
    // streaming means now we immediately are looking for a new solution
629
1497
    d_hasSolution = false;
630
1497
    return false;
631
  }
632
  // Use lemma to terminate with "unsat", this is justified by the verification
633
  // check above, which confirms the synthesis conjecture is solved.
634
325
  lems.push_back(d_quant.negate());
635
325
  return true;
636
}
637
638
2648
bool SynthConjecture::checkSideCondition(const std::vector<Node>& cvals) const
639
{
640
2648
  if (!d_embedSideCondition.isNull())
641
  {
642
    Node sc = d_embedSideCondition.substitute(
643
456
        d_candidates.begin(), d_candidates.end(), cvals.begin(), cvals.end());
644
296
    Trace("sygus-engine") << "Check side condition..." << std::endl;
645
296
    Trace("cegqi-debug") << "Check side condition : " << sc << std::endl;
646
456
    Result r = checkWithSubsolver(sc);
647
296
    Trace("cegqi-debug") << "...got side condition : " << r << std::endl;
648
296
    if (r == Result::UNSAT)
649
    {
650
136
      return false;
651
    }
652
160
    Trace("sygus-engine") << "...passed side condition" << std::endl;
653
  }
654
2512
  return true;
655
}
656
657
673
bool SynthConjecture::doRefine()
658
{
659
1346
  std::vector<Node> lems;
660
673
  Assert(d_set_ce_sk_vars);
661
662
  // first, make skolem substitution
663
1346
  Trace("cegqi-refine") << "doRefine : construct skolem substitution..."
664
673
                        << std::endl;
665
1346
  std::vector<Node> sk_vars;
666
1346
  std::vector<Node> sk_subs;
667
  // collect the substitution over all disjuncts
668
673
  if (!d_ce_sk_vars.empty())
669
  {
670
385
    Trace("cegqi-refine") << "Get model values for skolems..." << std::endl;
671
385
    Assert(d_inner_vars.size() == d_ce_sk_vars.size());
672
385
    if (d_ce_sk_var_mvs.empty())
673
    {
674
      std::vector<Node> model_values;
675
      for (const Node& v : d_ce_sk_vars)
676
      {
677
        Node mv = getModelValue(v);
678
        Trace("cegqi-refine") << "  " << v << " -> " << mv << std::endl;
679
        model_values.push_back(mv);
680
      }
681
      sk_subs.insert(sk_subs.end(), model_values.begin(), model_values.end());
682
    }
683
    else
684
    {
685
385
      Assert(d_ce_sk_var_mvs.size() == d_ce_sk_vars.size());
686
385
      sk_subs.insert(
687
770
          sk_subs.end(), d_ce_sk_var_mvs.begin(), d_ce_sk_var_mvs.end());
688
    }
689
385
    sk_vars.insert(sk_vars.end(), d_inner_vars.begin(), d_inner_vars.end());
690
  }
691
  else
692
  {
693
288
    Assert(d_inner_vars.empty());
694
  }
695
696
1346
  std::vector<Node> lem_c;
697
1346
  Trace("cegqi-refine") << "doRefine : Construct refinement lemma..."
698
673
                        << std::endl;
699
1346
  Trace("cegqi-refine-debug")
700
673
      << "  For counterexample skolems : " << d_ce_sk_vars << std::endl;
701
1346
  Node base_lem;
702
673
  if (d_base_inst.getKind() == NOT && d_base_inst[0].getKind() == FORALL)
703
  {
704
385
    base_lem = d_base_inst[0][1];
705
  }
706
  else
707
  {
708
288
    base_lem = d_base_inst.negate();
709
  }
710
711
673
  Assert(sk_vars.size() == sk_subs.size());
712
713
673
  Trace("cegqi-refine") << "doRefine : substitute..." << std::endl;
714
673
  base_lem = base_lem.substitute(
715
      sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end());
716
673
  Trace("cegqi-refine") << "doRefine : rewrite..." << std::endl;
717
673
  base_lem = d_tds->rewriteNode(base_lem);
718
1346
  Trace("cegqi-refine") << "doRefine : register refinement lemma " << base_lem
719
673
                        << "..." << std::endl;
720
673
  d_master->registerRefinementLemma(sk_vars, base_lem, lems);
721
673
  Trace("cegqi-refine") << "doRefine : finished" << std::endl;
722
673
  d_set_ce_sk_vars = false;
723
673
  d_ce_sk_vars.clear();
724
673
  d_ce_sk_var_mvs.clear();
725
726
  // now send the lemmas
727
673
  bool addedLemma = false;
728
1346
  for (const Node& lem : lems)
729
  {
730
1346
    Trace("cegqi-lemma") << "Cegqi::Lemma : candidate refinement : " << lem
731
673
                         << std::endl;
732
673
    bool res = d_qim.addPendingLemma(lem, InferenceId::UNKNOWN);
733
673
    if (res)
734
    {
735
445
      ++(d_stats.d_cegqi_lemmas_refine);
736
445
      d_refine_count++;
737
445
      addedLemma = true;
738
    }
739
    else
740
    {
741
228
      Trace("cegqi-warn") << "  ...FAILED to add refinement!" << std::endl;
742
    }
743
  }
744
673
  if (addedLemma)
745
  {
746
445
    Trace("sygus-engine-debug") << "  ...refine candidate." << std::endl;
747
  }
748
  else
749
  {
750
456
    Trace("sygus-engine-debug") << "  ...(warning) failed to refine candidate, "
751
228
                                   "manually exclude candidate."
752
228
                                << std::endl;
753
456
    std::vector<Node> cvals;
754
456
    for (const Node& c : d_candidates)
755
    {
756
228
      cvals.push_back(d_cinfo[c].d_inst.back());
757
    }
758
    // something went wrong, exclude the current candidate
759
228
    excludeCurrentSolution(d_candidates, cvals);
760
    // Note this happens when evaluation is incapable of disproving a candidate
761
    // for counterexample point c, but satisfiability checking happened to find
762
    // the the same point c is indeed a true counterexample. It is sound
763
    // to exclude the candidate in this case.
764
  }
765
1346
  return addedLemma;
766
}
767
768
508
void SynthConjecture::preregisterConjecture(Node q)
769
{
770
508
  d_ceg_si->preregisterConjecture(q);
771
508
}
772
773
56223
bool SynthConjecture::getEnumeratedValues(std::vector<Node>& n,
774
                                          std::vector<Node>& v,
775
                                          bool& activeIncomplete)
776
{
777
112446
  std::vector<Node> ncheck = n;
778
56223
  n.clear();
779
56223
  bool ret = true;
780
143169
  for (unsigned i = 0, size = ncheck.size(); i < size; i++)
781
  {
782
173886
    Node e = ncheck[i];
783
    // if it is not active, we return null
784
173886
    Node g = d_tds->getActiveGuardForEnumerator(e);
785
86958
    if (!g.isNull())
786
    {
787
98418
      Node gstatus = d_qstate.getValuation().getSatValue(g);
788
49254
      if (gstatus.isNull() || !gstatus.getConst<bool>())
789
      {
790
60
        Trace("sygus-engine-debug")
791
30
            << "Enumerator " << e << " is inactive." << std::endl;
792
30
        continue;
793
      }
794
    }
795
173856
    Node nv = getEnumeratedValue(e, activeIncomplete);
796
86916
    n.push_back(e);
797
86916
    v.push_back(nv);
798
86916
    ret = ret && !nv.isNull();
799
  }
800
112422
  return ret;
801
}
802
803
86928
Node SynthConjecture::getEnumeratedValue(Node e, bool& activeIncomplete)
804
{
805
86928
  bool isEnum = d_tds->isEnumerator(e);
806
807
86928
  if (isEnum && !e.getAttribute(SygusSymBreakOkAttribute()))
808
  {
809
    // if the current model value of e was not registered by the datatypes
810
    // sygus solver, or was excluded by symmetry breaking, then it does not
811
    // have a proper model value that we should consider, thus we return null.
812
6236
    Trace("sygus-engine-debug")
813
3118
        << "Enumerator " << e << " does not have proper model value."
814
3118
        << std::endl;
815
3118
    return Node::null();
816
  }
817
818
83810
  if (!isEnum || d_tds->isPassiveEnumerator(e))
819
  {
820
34839
    return getModelValue(e);
821
  }
822
823
  // management of actively generated enumerators goes here
824
825
  // initialize the enumerated value generator for e
826
  std::map<Node, std::unique_ptr<EnumValGenerator> >::iterator iteg =
827
48971
      d_evg.find(e);
828
48971
  if (iteg == d_evg.end())
829
  {
830
195
    if (d_tds->isVariableAgnosticEnumerator(e))
831
    {
832
2
      d_evg[e].reset(new EnumStreamConcrete(d_tds));
833
    }
834
    else
835
    {
836
      // Actively-generated enumerators are currently either variable agnostic
837
      // or basic. The auto mode always prefers the optimized enumerator over
838
      // the basic one.
839
193
      Assert(d_tds->isBasicEnumerator(e));
840
2090
      if (options::sygusActiveGenMode()
841
193
          == options::SygusActiveGenMode::ENUM_BASIC)
842
      {
843
        d_evg[e].reset(new EnumValGeneratorBasic(d_tds, e.getType()));
844
      }
845
      else
846
      {
847
193
        Assert(options::sygusActiveGenMode()
848
                   == options::SygusActiveGenMode::ENUM
849
               || options::sygusActiveGenMode()
850
                      == options::SygusActiveGenMode::AUTO);
851
193
        d_evg[e].reset(new SygusEnumerator(d_tds, this, d_stats));
852
      }
853
    }
854
390
    Trace("sygus-active-gen")
855
195
        << "Active-gen: initialize for " << e << std::endl;
856
195
    d_evg[e]->initialize(e);
857
195
    d_ev_curr_active_gen[e] = Node::null();
858
195
    iteg = d_evg.find(e);
859
195
    Trace("sygus-active-gen-debug") << "...finish" << std::endl;
860
  }
861
  // if we have a waiting value, return it
862
48971
  std::map<Node, Node>::iterator itw = d_ev_active_gen_waiting.find(e);
863
48971
  if (itw != d_ev_active_gen_waiting.end())
864
  {
865
    Trace("sygus-active-gen-debug")
866
        << "Active-gen: return waiting " << itw->second << std::endl;
867
    return itw->second;
868
  }
869
  // Check if there is an (abstract) value absE we were actively generating
870
  // values based on.
871
97942
  Node absE = d_ev_curr_active_gen[e];
872
48971
  bool firstTime = false;
873
48971
  if (absE.isNull())
874
  {
875
    // None currently exist. The next abstract value is the model value for e.
876
195
    absE = getModelValue(e);
877
195
    if (Trace.isOn("sygus-active-gen"))
878
    {
879
      Trace("sygus-active-gen") << "Active-gen: new abstract value : ";
880
      TermDbSygus::toStreamSygus("sygus-active-gen", e);
881
      Trace("sygus-active-gen") << " -> ";
882
      TermDbSygus::toStreamSygus("sygus-active-gen", absE);
883
      Trace("sygus-active-gen") << std::endl;
884
    }
885
195
    d_ev_curr_active_gen[e] = absE;
886
195
    iteg->second->addValue(absE);
887
195
    firstTime = true;
888
  }
889
48971
  bool inc = true;
890
48971
  if (!firstTime)
891
  {
892
48776
    inc = iteg->second->increment();
893
  }
894
97942
  Node v;
895
48971
  if (inc)
896
  {
897
48963
    v = iteg->second->getCurrent();
898
  }
899
97918
  Trace("sygus-active-gen-debug") << "...generated " << v
900
48959
                                  << ", with increment success : " << inc
901
48959
                                  << std::endl;
902
48959
  if (!inc)
903
  {
904
    // No more concrete values generated from absE.
905
8
    NodeManager* nm = NodeManager::currentNM();
906
8
    d_ev_curr_active_gen[e] = Node::null();
907
16
    std::vector<Node> exp;
908
    // If we are a basic enumerator, a single abstract value maps to *all*
909
    // concrete values of its type, thus we don't depend on the current
910
    // solution.
911
8
    if (!d_tds->isBasicEnumerator(e))
912
    {
913
      // We must block e = absE
914
2
      d_tds->getExplain()->getExplanationForEquality(e, absE, exp);
915
4
      for (unsigned i = 0, size = exp.size(); i < size; i++)
916
      {
917
2
        exp[i] = exp[i].negate();
918
      }
919
    }
920
16
    Node g = d_tds->getActiveGuardForEnumerator(e);
921
8
    if (!g.isNull())
922
    {
923
8
      if (d_ev_active_gen_first_val.find(e) == d_ev_active_gen_first_val.end())
924
      {
925
8
        exp.push_back(g.negate());
926
8
        d_ev_active_gen_first_val[e] = absE;
927
      }
928
    }
929
    else
930
    {
931
      Assert(false);
932
    }
933
16
    Node lem = exp.size() == 1 ? exp[0] : nm->mkNode(OR, exp);
934
16
    Trace("cegqi-lemma") << "Cegqi::Lemma : actively-generated enumerator "
935
8
                            "exclude current solution : "
936
8
                         << lem << std::endl;
937
8
    if (Trace.isOn("sygus-active-gen-debug"))
938
    {
939
      Trace("sygus-active-gen-debug") << "Active-gen: block ";
940
      TermDbSygus::toStreamSygus("sygus-active-gen-debug", absE);
941
      Trace("sygus-active-gen-debug") << std::endl;
942
    }
943
8
    d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_EXCLUDE_CURRENT);
944
  }
945
  else
946
  {
947
    // We are waiting to send e -> v to the module that requested it.
948
48951
    if (v.isNull())
949
    {
950
31774
      activeIncomplete = true;
951
    }
952
    else
953
    {
954
17177
      d_ev_active_gen_waiting[e] = v;
955
    }
956
48951
    if (Trace.isOn("sygus-active-gen"))
957
    {
958
      Trace("sygus-active-gen") << "Active-gen : " << e << " : ";
959
      TermDbSygus::toStreamSygus("sygus-active-gen", absE);
960
      Trace("sygus-active-gen") << " -> ";
961
      TermDbSygus::toStreamSygus("sygus-active-gen", v);
962
      Trace("sygus-active-gen") << std::endl;
963
    }
964
  }
965
966
48959
  return v;
967
}
968
969
43396
Node SynthConjecture::getModelValue(Node n)
970
{
971
43396
  Trace("cegqi-mv") << "getModelValue for : " << n << std::endl;
972
43396
  return d_qe->getModel()->getValue(n);
973
}
974
975
void SynthConjecture::debugPrint(const char* c)
976
{
977
  Trace(c) << "Synthesis conjecture : " << d_embed_quant << std::endl;
978
  Trace(c) << "  * Candidate programs : " << d_candidates << std::endl;
979
  Trace(c) << "  * Counterexample skolems : " << d_ce_sk_vars << std::endl;
980
}
981
982
1497
void SynthConjecture::printAndContinueStream(const std::vector<Node>& enums,
983
                                             const std::vector<Node>& values)
984
{
985
1497
  Assert(d_master != nullptr);
986
  // we have generated a solution, print it
987
  // get the current output stream
988
1497
  Options& sopts = smt::currentSmtEngine()->getOptions();
989
1497
  printSynthSolution(*sopts.getOut());
990
1497
  excludeCurrentSolution(enums, values);
991
1497
}
992
993
1877
void SynthConjecture::excludeCurrentSolution(const std::vector<Node>& enums,
994
                                             const std::vector<Node>& values)
995
{
996
3754
  Trace("cegqi-debug") << "Exclude current solution: " << enums << " / "
997
1877
                       << values << std::endl;
998
  // We will not refine the current candidate solution since it is a solution
999
  // thus, we clear information regarding the current refinement
1000
1877
  d_set_ce_sk_vars = false;
1001
1877
  d_ce_sk_vars.clear();
1002
1877
  d_ce_sk_var_mvs.clear();
1003
  // However, we need to exclude the current solution using an explicit
1004
  // blocking clause, so that we proceed to the next solution. We do this only
1005
  // for passively-generated enumerators (TermDbSygus::isPassiveEnumerator).
1006
3754
  std::vector<Node> exp;
1007
3802
  for (unsigned i = 0, tsize = enums.size(); i < tsize; i++)
1008
  {
1009
3850
    Node cprog = enums[i];
1010
1925
    Assert(d_tds->isEnumerator(cprog));
1011
1925
    if (d_tds->isPassiveEnumerator(cprog))
1012
    {
1013
164
      Node cval = values[i];
1014
      // add to explanation of exclusion
1015
82
      d_tds->getExplain()->getExplanationForEquality(cprog, cval, exp);
1016
    }
1017
  }
1018
1877
  if (!exp.empty())
1019
  {
1020
34
    if (!d_guarded_stream_exc)
1021
    {
1022
10
      d_guarded_stream_exc = true;
1023
10
      exp.push_back(d_feasible_guard);
1024
    }
1025
34
    Node exc_lem = exp.size() == 1
1026
                       ? exp[0]
1027
68
                       : NodeManager::currentNM()->mkNode(kind::AND, exp);
1028
34
    exc_lem = exc_lem.negate();
1029
68
    Trace("cegqi-lemma") << "Cegqi::Lemma : stream exclude current solution : "
1030
34
                         << exc_lem << std::endl;
1031
34
    d_qim.lemma(exc_lem, InferenceId::QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT);
1032
  }
1033
1877
}
1034
1035
1501
void SynthConjecture::printSynthSolution(std::ostream& out)
1036
{
1037
1501
  Trace("cegqi-sol-debug") << "Printing synth solution..." << std::endl;
1038
1501
  Assert(d_quant[0].getNumChildren() == d_embed_quant[0].getNumChildren());
1039
3002
  std::vector<Node> sols;
1040
3002
  std::vector<int> statuses;
1041
1501
  if (!getSynthSolutionsInternal(sols, statuses))
1042
  {
1043
    return;
1044
  }
1045
1501
  NodeManager* nm = NodeManager::currentNM();
1046
3002
  for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++)
1047
  {
1048
3002
    Node sol = sols[i];
1049
1501
    if (!sol.isNull())
1050
    {
1051
3002
      Node prog = d_embed_quant[0][i];
1052
1501
      int status = statuses[i];
1053
3002
      TypeNode tn = prog.getType();
1054
1501
      const DType& dt = tn.getDType();
1055
3002
      std::stringstream ss;
1056
1501
      ss << prog;
1057
3002
      std::string f(ss.str());
1058
1501
      f.erase(f.begin());
1059
1501
      ++(d_stats.d_solutions);
1060
1061
1501
      bool is_unique_term = true;
1062
1063
1501
      if (status != 0
1064
2990
          && (options::sygusRewSynth() || options::sygusQueryGen()
1065
124
              || options::sygusFilterSolMode()
1066
                     != options::SygusFilterSolMode::NONE))
1067
      {
1068
1489
        Trace("cegqi-sol-debug") << "Run expression mining..." << std::endl;
1069
        std::map<Node, ExpressionMinerManager>::iterator its =
1070
1489
            d_exprm.find(prog);
1071
1489
        if (its == d_exprm.end())
1072
        {
1073
36
          d_exprm[prog].initializeSygus(
1074
24
              d_qe, d_candidates[i], options::sygusSamples(), true);
1075
12
          if (options::sygusRewSynth())
1076
          {
1077
8
            d_exprm[prog].enableRewriteRuleSynth();
1078
          }
1079
12
          if (options::sygusQueryGen())
1080
          {
1081
            d_exprm[prog].enableQueryGeneration(options::sygusQueryGenThresh());
1082
          }
1083
24
          if (options::sygusFilterSolMode()
1084
12
              != options::SygusFilterSolMode::NONE)
1085
          {
1086
8
            if (options::sygusFilterSolMode()
1087
4
                == options::SygusFilterSolMode::STRONG)
1088
            {
1089
4
              d_exprm[prog].enableFilterStrongSolutions();
1090
            }
1091
            else if (options::sygusFilterSolMode()
1092
                     == options::SygusFilterSolMode::WEAK)
1093
            {
1094
              d_exprm[prog].enableFilterWeakSolutions();
1095
            }
1096
          }
1097
12
          its = d_exprm.find(prog);
1098
        }
1099
1489
        bool rew_print = false;
1100
1489
        is_unique_term = d_exprm[prog].addTerm(sol, out, rew_print);
1101
1489
        if (rew_print)
1102
        {
1103
146
          ++(d_stats.d_candidate_rewrites_print);
1104
        }
1105
1489
        if (!is_unique_term)
1106
        {
1107
369
          ++(d_stats.d_filtered_solutions);
1108
        }
1109
      }
1110
1501
      if (is_unique_term)
1111
      {
1112
1132
        out << "(define-fun " << f << " ";
1113
        // Only include variables that are truly bound variables of the
1114
        // function-to-synthesize. This means we exclude variables that encode
1115
        // external terms. This ensures that --sygus-stream prints
1116
        // solutions with no arguments on the predicate for responses to
1117
        // the get-abduct command.
1118
        // pvs stores the variables that will be printed in the argument list
1119
        // below.
1120
2264
        std::vector<Node> pvs;
1121
2264
        Node vl = dt.getSygusVarList();
1122
1132
        if (!vl.isNull())
1123
        {
1124
1130
          Assert(vl.getKind() == BOUND_VAR_LIST);
1125
          SygusVarToTermAttribute sta;
1126
3708
          for (const Node& v : vl)
1127
          {
1128
2578
            if (!v.hasAttribute(sta))
1129
            {
1130
2410
              pvs.push_back(v);
1131
            }
1132
          }
1133
        }
1134
1132
        if (pvs.empty())
1135
        {
1136
44
          out << "() ";
1137
        }
1138
        else
1139
        {
1140
1088
          vl = nm->mkNode(BOUND_VAR_LIST, pvs);
1141
1088
          out << vl << " ";
1142
        }
1143
1132
        out << dt.getSygusType() << " ";
1144
1132
        if (status == 0)
1145
        {
1146
          out << sol;
1147
        }
1148
        else
1149
        {
1150
2264
          Node bsol = datatypes::utils::sygusToBuiltin(sol, true);
1151
1132
          out << bsol;
1152
        }
1153
1132
        out << ")" << std::endl;
1154
      }
1155
    }
1156
  }
1157
}
1158
1159
246
bool SynthConjecture::getSynthSolutions(
1160
    std::map<Node, std::map<Node, Node> >& sol_map)
1161
{
1162
246
  NodeManager* nm = NodeManager::currentNM();
1163
492
  std::vector<Node> sols;
1164
492
  std::vector<int> statuses;
1165
246
  Trace("cegqi-debug") << "getSynthSolutions..." << std::endl;
1166
246
  if (!getSynthSolutionsInternal(sols, statuses))
1167
  {
1168
    Trace("cegqi-debug") << "...failed internal" << std::endl;
1169
    return false;
1170
  }
1171
  // we add it to the solution map, indexed by this conjecture
1172
246
  std::map<Node, Node>& smc = sol_map[d_quant];
1173
614
  for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++)
1174
  {
1175
736
    Node sol = sols[i];
1176
368
    int status = statuses[i];
1177
736
    Trace("cegqi-debug") << "...got " << i << ": " << sol
1178
368
                         << ", status=" << status << std::endl;
1179
    // get the builtin solution
1180
736
    Node bsol = sol;
1181
368
    if (status != 0)
1182
    {
1183
      // Convert sygus to builtin here.
1184
      // We must use the external representation to ensure bsol matches the
1185
      // grammar.
1186
220
      bsol = datatypes::utils::sygusToBuiltin(sol, true);
1187
    }
1188
    // convert to lambda
1189
736
    TypeNode tn = d_embed_quant[0][i].getType();
1190
368
    const DType& dt = tn.getDType();
1191
736
    Node fvar = d_quant[0][i];
1192
736
    Node bvl = dt.getSygusVarList();
1193
368
    if (!bvl.isNull())
1194
    {
1195
      // since we don't have function subtyping, this assertion should only
1196
      // check the return type
1197
285
      Assert(fvar.getType().isFunction());
1198
285
      Assert(fvar.getType().getRangeType().isComparableTo(bsol.getType()));
1199
285
      bsol = nm->mkNode(LAMBDA, bvl, bsol);
1200
    }
1201
    else
1202
    {
1203
83
      Assert(fvar.getType().isComparableTo(bsol.getType()));
1204
    }
1205
    // store in map
1206
368
    smc[fvar] = bsol;
1207
368
    Trace("cegqi-debug") << "...return " << bsol << std::endl;
1208
  }
1209
246
  return true;
1210
}
1211
1212
2512
void SynthConjecture::recordSolution(std::vector<Node>& vs)
1213
{
1214
2512
  Assert(vs.size() == d_candidates.size());
1215
2512
  d_cinfo.clear();
1216
5250
  for (unsigned i = 0; i < vs.size(); i++)
1217
  {
1218
2738
    d_cinfo[d_candidates[i]].d_inst.push_back(vs[i]);
1219
  }
1220
2512
}
1221
1222
1747
bool SynthConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
1223
                                                std::vector<int>& statuses)
1224
{
1225
1747
  if (!d_hasSolution)
1226
  {
1227
    return false;
1228
  }
1229
3616
  for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++)
1230
  {
1231
3738
    Node prog = d_embed_quant[0][i];
1232
1869
    Trace("cegqi-debug") << "  get solution for " << prog << std::endl;
1233
3738
    TypeNode tn = prog.getType();
1234
1869
    Assert(tn.isDatatype());
1235
    // get the solution
1236
3738
    Node sol;
1237
1869
    int status = -1;
1238
1869
    if (isSingleInvocation())
1239
    {
1240
147
      Assert(d_ceg_si != NULL);
1241
147
      sol = d_ceg_si->getSolution(i, tn, status, true);
1242
147
      if (sol.isNull())
1243
      {
1244
        return false;
1245
      }
1246
147
      sol = sol.getKind() == LAMBDA ? sol[1] : sol;
1247
    }
1248
    else
1249
    {
1250
3444
      Node cprog = d_candidates[i];
1251
1722
      if (!d_cinfo[cprog].d_inst.empty())
1252
      {
1253
        // the solution is just the last instantiated term
1254
1722
        sol = d_cinfo[cprog].d_inst.back();
1255
1722
        status = 1;
1256
1257
        // check if there was a template
1258
3444
        Node sf = d_quant[0][i];
1259
3444
        Node templ = d_templInfer->getTemplate(sf);
1260
1722
        if (!templ.isNull())
1261
        {
1262
34
          Trace("cegqi-inv-debug")
1263
17
              << sf << " used template : " << templ << std::endl;
1264
          // if it was not embedded into the grammar
1265
17
          if (!options::sygusTemplEmbedGrammar())
1266
          {
1267
34
            TNode templa = d_templInfer->getTemplateArg(sf);
1268
            // make the builtin version of the full solution
1269
17
            sol = d_tds->sygusToBuiltin(sol, sol.getType());
1270
34
            Trace("cegqi-inv") << "Builtin version of solution is : " << sol
1271
17
                               << ", type : " << sol.getType() << std::endl;
1272
34
            TNode tsol = sol;
1273
17
            sol = templ.substitute(templa, tsol);
1274
17
            Trace("cegqi-inv-debug") << "With template : " << sol << std::endl;
1275
17
            sol = Rewriter::rewrite(sol);
1276
17
            Trace("cegqi-inv-debug") << "Simplified : " << sol << std::endl;
1277
            // now, reconstruct to the syntax
1278
17
            sol = d_ceg_si->reconstructToSyntax(sol, tn, status, true);
1279
17
            sol = sol.getKind() == LAMBDA ? sol[1] : sol;
1280
34
            Trace("cegqi-inv-debug")
1281
17
                << "Reconstructed to syntax : " << sol << std::endl;
1282
          }
1283
          else
1284
          {
1285
            Trace("cegqi-inv-debug")
1286
                << "...was embedding into grammar." << std::endl;
1287
          }
1288
        }
1289
        else
1290
        {
1291
3410
          Trace("cegqi-inv-debug")
1292
1705
              << sf << " did not use template" << std::endl;
1293
        }
1294
      }
1295
      else
1296
      {
1297
        Trace("cegqi-warn") << "WARNING : No recorded instantiations for "
1298
                               "syntax-guided solution!"
1299
                            << std::endl;
1300
      }
1301
    }
1302
1869
    sols.push_back(sol);
1303
1869
    statuses.push_back(status);
1304
  }
1305
1747
  return true;
1306
}
1307
1308
15140
Node SynthConjecture::getSymmetryBreakingPredicate(
1309
    Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth)
1310
{
1311
30280
  std::vector<Node> sb_lemmas;
1312
1313
  // based on simple preprocessing
1314
  Node ppred =
1315
30280
      d_ceg_proc->getSymmetryBreakingPredicate(x, e, tn, tindex, depth);
1316
15140
  if (!ppred.isNull())
1317
  {
1318
    sb_lemmas.push_back(ppred);
1319
  }
1320
1321
  // other static conjecture-dependent symmetry breaking goes here
1322
1323
15140
  if (!sb_lemmas.empty())
1324
  {
1325
    return sb_lemmas.size() == 1
1326
               ? sb_lemmas[0]
1327
               : NodeManager::currentNM()->mkNode(kind::AND, sb_lemmas);
1328
  }
1329
  else
1330
  {
1331
15140
    return Node::null();
1332
  }
1333
}
1334
1335
24808
ExampleEvalCache* SynthConjecture::getExampleEvalCache(Node e)
1336
{
1337
  std::map<Node, std::unique_ptr<ExampleEvalCache> >::iterator it =
1338
24808
      d_exampleEvalCache.find(e);
1339
24808
  if (it != d_exampleEvalCache.end())
1340
  {
1341
24300
    return it->second.get();
1342
  }
1343
1016
  Node f = d_tds->getSynthFunForEnumerator(e);
1344
  // if f does not have examples, we don't construct the utility
1345
508
  if (!d_exampleInfer->hasExamples(f) || d_exampleInfer->getNumExamples(f) == 0)
1346
  {
1347
301
    d_exampleEvalCache[e].reset(nullptr);
1348
301
    return nullptr;
1349
  }
1350
207
  d_exampleEvalCache[e].reset(new ExampleEvalCache(d_tds, this, f, e));
1351
207
  return d_exampleEvalCache[e].get();
1352
}
1353
1354
}  // namespace quantifiers
1355
}  // namespace theory
1356
26676
} /* namespace CVC4 */