GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/cegis_core_connective.cpp Lines: 403 455 88.6 %
Date: 2021-03-23 Branches: 796 1871 42.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file cegis_core_connective.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, Andres Noetzli
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Implementation of cegis core connective module.
13
 **/
14
15
#include "theory/quantifiers/sygus/cegis_core_connective.h"
16
17
#include "expr/dtype_cons.h"
18
#include "options/base_options.h"
19
#include "printer/printer.h"
20
#include "proof/unsat_core.h"
21
#include "smt/smt_engine.h"
22
#include "smt/smt_engine_scope.h"
23
#include "theory/datatypes/theory_datatypes_utils.h"
24
#include "theory/quantifiers/sygus/ce_guided_single_inv.h"
25
#include "theory/quantifiers/sygus/transition_inference.h"
26
#include "theory/quantifiers/term_util.h"
27
#include "theory/quantifiers_engine.h"
28
#include "theory/rewriter.h"
29
#include "theory/smt_engine_subsolver.h"
30
#include "util/random.h"
31
32
using namespace CVC4::kind;
33
34
namespace CVC4 {
35
namespace theory {
36
namespace quantifiers {
37
38
28
bool VariadicTrie::add(Node n, const std::vector<Node>& i)
39
{
40
28
  VariadicTrie* curr = this;
41
64
  for (const Node& ic : i)
42
  {
43
36
    curr = &(curr->d_children[ic]);
44
  }
45
28
  if (curr->d_data.isNull())
46
  {
47
28
    curr->d_data = n;
48
28
    return true;
49
  }
50
  return false;
51
}
52
53
668
bool VariadicTrie::hasSubset(const std::vector<Node>& is) const
54
{
55
668
  if (!d_data.isNull())
56
  {
57
288
    return true;
58
  }
59
1406
  for (const std::pair<const Node, VariadicTrie>& p : d_children)
60
  {
61
2366
    Node n = p.first;
62
1340
    if (std::find(is.begin(), is.end(), n) != is.end())
63
    {
64
318
      if (p.second.hasSubset(is))
65
      {
66
314
        return true;
67
      }
68
    }
69
  }
70
66
  return false;
71
}
72
73
2190
CegisCoreConnective::CegisCoreConnective(QuantifiersEngine* qe,
74
                                         QuantifiersInferenceManager& qim,
75
2190
                                         SynthConjecture* p)
76
2190
    : Cegis(qe, qim, p)
77
{
78
2190
  d_true = NodeManager::currentNM()->mkConst(true);
79
2190
  d_false = NodeManager::currentNM()->mkConst(false);
80
2190
}
81
82
10
bool CegisCoreConnective::processInitialize(Node conj,
83
                                            Node n,
84
                                            const std::vector<Node>& candidates,
85
                                            std::vector<Node>& lemmas)
86
{
87
10
  Trace("sygus-ccore-init") << "CegisCoreConnective::initialize" << std::endl;
88
10
  Trace("sygus-ccore-init") << "  conjecture : " << conj << std::endl;
89
10
  Trace("sygus-ccore-init") << "  candidates : " << candidates << std::endl;
90
10
  if (candidates.size() != 1)
91
  {
92
    Trace("sygus-ccore-init")
93
        << "...only applies to single candidate conjectures." << std::endl;
94
    return false;
95
  }
96
10
  d_candidate = candidates[0];
97
10
  Assert(conj.getKind() == FORALL);
98
10
  Assert(conj[0].getNumChildren() == 1);
99
20
  Node body = conj[1];
100
10
  if (body.getKind() == NOT && body[0].getKind() == FORALL)
101
  {
102
8
    body = body[0][1];
103
  }
104
  else
105
  {
106
2
    body = TermUtil::simpleNegate(body);
107
  }
108
10
  Trace("sygus-ccore-init") << "  body : " << body << std::endl;
109
110
20
  TransitionInference ti;
111
10
  ti.process(body, conj[0][0]);
112
113
10
  if (!ti.isComplete())
114
  {
115
    Trace("sygus-ccore-init") << "...could not infer predicate." << std::endl;
116
    return false;
117
  }
118
10
  if (ti.isTrivial())
119
  {
120
    // not necessary to use this class if the conjecture is trivial (does
121
    // not contain the function-to-synthesize).
122
2
    Trace("sygus-ccore-init") << "...conjecture is trivial." << std::endl;
123
2
    return false;
124
  }
125
16
  Node trans = ti.getTransitionRelation();
126
8
  Trace("sygus-ccore-init") << "  transition relation: " << trans << std::endl;
127
8
  if (!trans.isConst() || trans.getConst<bool>())
128
  {
129
    Trace("sygus-ccore-init")
130
        << "...does not apply conjectures with transition relations."
131
        << std::endl;
132
    return false;
133
  }
134
135
  // the grammar must allow AND / OR when applicable
136
16
  TypeNode gt = d_candidate.getType();
137
138
16
  Node f = ti.getFunction();
139
8
  Assert(!f.isNull());
140
8
  Trace("sygus-ccore-init") << "  predicate: " << f << std::endl;
141
8
  ti.getVariables(d_vars);
142
8
  Trace("sygus-ccore-init") << "  variables: " << d_vars << std::endl;
143
  // make the evaluation function
144
16
  std::vector<Node> echildren;
145
8
  echildren.push_back(d_candidate);
146
8
  echildren.insert(echildren.end(), d_vars.begin(), d_vars.end());
147
8
  d_eterm = NodeManager::currentNM()->mkNode(DT_SYGUS_EVAL, echildren);
148
8
  Trace("sygus-ccore-init") << "  evaluation term: " << d_eterm << std::endl;
149
150
16
  Node prePost[2];
151
8
  prePost[0] = ti.getPreCondition();
152
  // negate the post condition
153
8
  prePost[1] = TermUtil::simpleNegate(ti.getPostCondition());
154
8
  Trace("sygus-ccore-init") << "  precondition: " << prePost[0] << std::endl;
155
8
  Trace("sygus-ccore-init") << "  postcondition: " << prePost[1] << std::endl;
156
157
  // side condition?
158
16
  QAttributes qa;
159
8
  QuantAttributes::computeQuantAttributes(conj, qa);
160
16
  Node sc = qa.d_sygusSideCondition;
161
8
  if (!sc.isNull())
162
  {
163
8
    Trace("sygus-ccore-init") << "  side condition: " << sc << std::endl;
164
8
    if (sc.getKind() == EXISTS)
165
    {
166
8
      sc = sc[1];
167
    }
168
16
    Node scb = TermUtil::simpleNegate(sc);
169
16
    TransitionInference tisc;
170
8
    tisc.process(scb, conj[0][0]);
171
16
    Node scTrans = ti.getTransitionRelation();
172
16
    Trace("sygus-ccore-init")
173
8
        << "  transition relation of SC: " << scTrans << std::endl;
174
8
    if (tisc.isComplete() && scTrans.isConst() && !scTrans.getConst<bool>())
175
    {
176
16
      std::vector<Node> scVars;
177
8
      tisc.getVariables(scVars);
178
16
      Node scPre = tisc.getPreCondition();
179
8
      scPre = scPre.substitute(
180
          scVars.begin(), scVars.end(), d_vars.begin(), d_vars.end());
181
16
      Node scPost = TermUtil::simpleNegate(tisc.getPostCondition());
182
8
      scPost = scPost.substitute(
183
          scVars.begin(), scVars.end(), d_vars.begin(), d_vars.end());
184
16
      Trace("sygus-ccore-init")
185
8
          << "  precondition of SC: " << scPre << std::endl;
186
16
      Trace("sygus-ccore-init")
187
8
          << "  postcondition of SC: " << scPost << std::endl;
188
      // We are extracting the side condition to be used by this algorithm
189
      // from the side condition ascribed to the synthesis conjecture.
190
      // A sygus conjecture of the form, for predicate-to-synthesize I:
191
      //   exists I. forall x. P[I,x]
192
      // whose ascribed side condition is C[I], has the semantics:
193
      //   exists I. C[I] ^ forall x. P[I,x].
194
      // Notice that this side condition C may be an arbitrary formula over the
195
      // function to synthesize. However, the algorithm implemented by this
196
      // class is restricted to side conditions of the form:
197
      //   exists k. A[k] ^ I(k)
198
      // The above condition guards for this case, and runs this block of code,
199
      // where we use the TransitionInference utility to extract A[k] from
200
      // A[k] ^ I(k). In the end, we set d_sc to A[d_vars]; notice the variables
201
      // d_vars are those introduced by the TransitionInference utility
202
      // for normalization.
203
8
      d_sc = scPost;
204
    }
205
  }
206
207
  // We use the postcondition if it non-trivial and the grammar gt for our
208
  // candidate has the production rule gt -> AND( gt, gt ). Similarly for
209
  // precondition and OR.
210
8
  Assert(gt.isDatatype());
211
8
  const DType& gdt = gt.getDType();
212
8
  SygusTypeInfo& gti = d_tds->getTypeInfo(gt);
213
24
  for (unsigned r = 0; r < 2; r++)
214
  {
215
24
    Node node = prePost[r];
216
16
    if (node.isConst())
217
    {
218
      // this direction is trivial, ignore
219
8
      continue;
220
    }
221
8
    Component& c = r == 0 ? d_pre : d_post;
222
8
    Kind rk = r == 0 ? OR : AND;
223
8
    int i = gti.getKindConsNum(rk);
224
14
    if (i != -1 && gdt[i].getNumArgs() == 2
225
14
        && gdt[i].getArgType(0) == gt
226
14
        && gdt[i].getArgType(1) == gt)
227
    {
228
12
      Trace("sygus-ccore-init") << "  will do " << (r == 0 ? "pre" : "post")
229
6
                                << "condition." << std::endl;
230
12
      Node cons = gdt[i].getConstructor();
231
6
      c.initialize(node, cons);
232
      // Register the symmetry breaking lemma: do not do top-level solutions
233
      // with this constructor (e.g. we want to enumerate literals, not
234
      // conjunctions).
235
12
      Node tst = datatypes::utils::mkTester(d_candidate, i, gdt);
236
6
      Trace("sygus-ccore-init") << "Sym break lemma " << tst << std::endl;
237
6
      lemmas.push_back(tst.negate());
238
    }
239
  }
240
8
  if (!isActive())
241
  {
242
2
    return false;
243
  }
244
  // initialize the enumerator
245
6
  return Cegis::processInitialize(conj, n, candidates, lemmas);
246
}
247
248
90
bool CegisCoreConnective::processConstructCandidates(
249
    const std::vector<Node>& enums,
250
    const std::vector<Node>& enum_values,
251
    const std::vector<Node>& candidates,
252
    std::vector<Node>& candidate_values,
253
    bool satisfiedRl,
254
    std::vector<Node>& lems)
255
{
256
90
  Assert(isActive());
257
90
  bool ret = constructSolution(enums, enum_values, candidate_values);
258
259
  // exclude in the basic way if passive
260
90
  Assert(enums.size() == 1);
261
90
  NodeManager* nm = NodeManager::currentNM();
262
180
  for (unsigned i = 0, esize = enums.size(); i < esize; i++)
263
  {
264
180
    Node e = enums[i];
265
90
    if (!d_tds->isPassiveEnumerator(e))
266
    {
267
      continue;
268
    }
269
180
    Node v = enum_values[i];
270
180
    Node lem = d_tds->getExplain()->getExplanationForEquality(e, v).negate();
271
180
    Node g = d_tds->getActiveGuardForEnumerator(e);
272
90
    if (!g.isNull())
273
    {
274
      lem = nm->mkNode(OR, g.negate(), lem);
275
    }
276
90
    lems.push_back(lem);
277
  }
278
90
  return ret;
279
}
280
281
188
bool CegisCoreConnective::isActive() const
282
{
283
188
  return d_pre.isActive() || d_post.isActive();
284
}
285
286
90
bool CegisCoreConnective::constructSolution(
287
    const std::vector<Node>& candidates,
288
    const std::vector<Node>& candidate_values,
289
    std::vector<Node>& solv)
290
{
291
  // if the conjecture is not the right shape, no repair is possible
292
90
  if (!isActive())
293
  {
294
    return false;
295
  }
296
90
  Assert(candidates.size() == candidate_values.size());
297
180
  Trace("sygus-ccore-summary")
298
90
      << "CegisCoreConnective: construct solution..." << std::endl;
299
90
  if (Trace.isOn("sygus-ccore"))
300
  {
301
    Trace("sygus-ccore")
302
        << "CegisCoreConnective: Construct candidate solutions..." << std::endl;
303
    for (unsigned i = 0, size = candidates.size(); i < size; i++)
304
    {
305
      std::stringstream ss;
306
      TermDbSygus::toStreamSygus(ss, candidate_values[i]);
307
      Trace("sygus-ccore") << "  " << candidates[i] << " -> " << ss.str()
308
                           << std::endl;
309
    }
310
  }
311
90
  Assert(candidates.size() == 1 && candidates[0] == d_candidate);
312
180
  TNode cval = candidate_values[0];
313
180
  Node ets = d_eterm.substitute(d_candidate, cval);
314
180
  Node etsr = Rewriter::rewrite(ets);
315
90
  Trace("sygus-ccore-debug") << "...predicate is: " << etsr << std::endl;
316
90
  NodeManager* nm = NodeManager::currentNM();
317
264
  for (unsigned d = 0; d < 2; d++)
318
  {
319
180
    Component& ccheck = d == 0 ? d_pre : d_post;
320
180
    if (!ccheck.isActive())
321
    {
322
      // not trying this direction
323
180
      continue;
324
    }
325
90
    Component& cfilter = d == 0 ? d_post : d_pre;
326
    // In terms of the algorithm described in the h file, this gets the formula
327
    // A (or B, depending on the direction d).
328
174
    Node fpred = cfilter.getFormula();
329
90
    if (!fpred.isNull() && !fpred.isConst())
330
    {
331
      // check refinement points
332
      Node etsrn = d == 0 ? etsr : etsr.negate();
333
      std::unordered_set<Node, NodeHashFunction> visited;
334
      std::vector<Node> pt;
335
      Node rid = cfilter.getRefinementPt(this, etsrn, visited, pt);
336
      if (!rid.isNull())
337
      {
338
        // failed a refinement point
339
        continue;
340
      }
341
      Node fassert = nm->mkNode(AND, fpred, etsrn);
342
      Trace("sygus-ccore-debug")
343
          << "...check filter " << fassert << "..." << std::endl;
344
      std::vector<Node> mvs;
345
      Result r = checkSat(fassert, mvs);
346
      Trace("sygus-ccore-debug") << "...got " << r << std::endl;
347
      if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
348
      {
349
        // failed the filter, remember the refinement point
350
        if (r.asSatisfiabilityResult().isSat() == Result::SAT)
351
        {
352
          cfilter.addRefinementPt(fassert, mvs);
353
        }
354
        continue;
355
      }
356
    }
357
180
    Trace("sygus-ccore-debug")
358
90
        << "...add to pool in direction " << d << std::endl;
359
    // implements e.g. pool(B) += e_i.
360
90
    ccheck.addToPool(etsr, cval);
361
362
    // ----- get the pool of assertions and randomize it
363
174
    std::vector<Node> passerts;
364
90
    ccheck.getTermPool(passerts);
365
90
    std::shuffle(passerts.begin(), passerts.end(), Random::getRandom());
366
367
    // ----- check for entailment, adding based on models of failed points
368
174
    std::vector<Node> asserts;
369
174
    Node sol = constructSolutionFromPool(ccheck, asserts, passerts);
370
90
    if (!sol.isNull())
371
    {
372
6
      solv.push_back(sol);
373
6
      Trace("sygus-ccore-summary") << "...success" << std::endl;
374
6
      return true;
375
    }
376
84
    if (Trace.isOn("sygus-ccore-summary"))
377
    {
378
      std::stringstream ss;
379
      ccheck.debugPrintSummary(ss);
380
      Trace("sygus-ccore-summary")
381
          << "C[d=" << d << "] " << ss.str() << std::endl;
382
    }
383
  }
384
168
  Trace("sygus-ccore") << "CegisCoreConnective: failed to generate candidate"
385
84
                       << std::endl;
386
84
  Trace("sygus-ccore-summary") << "...failed" << std::endl;
387
84
  return false;
388
}
389
390
6
void CegisCoreConnective::Component::initialize(Node n, Node c)
391
{
392
6
  d_this = n;
393
6
  d_scons = c;
394
6
}
395
396
90
void CegisCoreConnective::Component::addToPool(Node n, Node s)
397
{
398
90
  d_cpool.push_back(n);
399
90
  d_cpoolToSol[n] = s;
400
90
}
401
402
6
Node CegisCoreConnective::Component::getSygusSolution(
403
    std::vector<Node>& conjs) const
404
{
405
6
  std::sort(conjs.begin(), conjs.end());
406
6
  Node sol;
407
6
  std::map<Node, Node>::const_iterator itu;
408
6
  NodeManager* nm = NodeManager::currentNM();
409
20
  for (const Node& u : conjs)
410
  {
411
14
    itu = d_cpoolToSol.find(u);
412
14
    Assert(itu != d_cpoolToSol.end());
413
28
    Node s = itu->second;
414
14
    Trace("sygus-ccore-debug-sy") << "  uc-s " << s << std::endl;
415
14
    if (sol.isNull())
416
    {
417
6
      sol = s;
418
    }
419
    else
420
    {
421
8
      sol = nm->mkNode(APPLY_CONSTRUCTOR, d_scons, s, sol);
422
    }
423
  }
424
6
  return sol;
425
}
426
void CegisCoreConnective::Component::debugPrintSummary(std::ostream& os) const
427
{
428
  os << "size(pool/pts/cores): " << d_cpool.size() << "/" << d_numRefPoints
429
     << "/" << d_numFalseCores;
430
}
431
432
20
void CegisCoreConnective::Component::addRefinementPt(
433
    Node id, const std::vector<Node>& pt)
434
{
435
20
  d_numRefPoints++;
436
20
  bool res = d_refinementPt.addTerm(id, pt);
437
  // this should always be a new point
438
20
  AlwaysAssert(res);
439
20
}
440
28
void CegisCoreConnective::Component::addFalseCore(Node id,
441
                                                  const std::vector<Node>& u)
442
{
443
28
  d_numFalseCores++;
444
28
  d_falseCores.add(id, u);
445
28
}
446
447
168
Node CegisCoreConnective::Component::getRefinementPt(
448
    CegisCoreConnective* p,
449
    Node n,
450
    std::unordered_set<Node, NodeHashFunction>& visited,
451
    std::vector<Node>& ss)
452
{
453
336
  std::vector<Node> ctx;
454
455
168
  unsigned depth = p->d_vars.size();
456
336
  std::map<NodeTrie*, std::map<Node, NodeTrie>::iterator> vt;
457
168
  std::map<NodeTrie*, std::map<Node, NodeTrie>::iterator>::iterator itvt;
458
168
  std::map<Node, NodeTrie>::iterator itv;
459
336
  std::vector<NodeTrie*> visit;
460
  NodeTrie* cur;
461
168
  visit.push_back(&d_refinementPt);
462
5170
  do
463
  {
464
5338
    cur = visit.back();
465
5338
    Trace("sygus-ccore-ref") << "process trie " << cur << std::endl;
466
5338
    if (ctx.size() == depth)
467
    {
468
232
      Trace("sygus-ccore-ref") << "...at depth " << std::endl;
469
      // at leaf
470
338
      Node id = cur->getData();
471
232
      Trace("sygus-ccore-ref") << "...data is " << id << std::endl;
472
232
      Assert(!id.isNull());
473
232
      AlwaysAssert(id.getType().isBoolean());
474
232
      if (visited.find(id) == visited.end())
475
      {
476
164
        visited.insert(id);
477
164
        Trace("sygus-ccore-ref") << "...eval " << std::endl;
478
        // check if it is true
479
202
        Node en = p->evaluate(n, id, ctx);
480
164
        if (en.isConst() && en.getConst<bool>())
481
        {
482
126
          ss = ctx;
483
126
          return id;
484
        }
485
      }
486
106
      visit.pop_back();
487
106
      ctx.pop_back();
488
    }
489
    else
490
    {
491
      // get the current child iterator for this node
492
5106
      itvt = vt.find(cur);
493
5106
      if (itvt == vt.end())
494
      {
495
3626
        Trace("sygus-ccore-ref") << "...initialize iterator " << std::endl;
496
        // initialize the iterator
497
3626
        itv = cur->d_data.begin();
498
3626
        vt[cur] = itv;
499
3626
        Trace("sygus-ccore-ref") << "...finished init" << std::endl;
500
      }
501
      else
502
      {
503
1480
        Trace("sygus-ccore-ref") << "...continue iterator " << std::endl;
504
1480
        itv = itvt->second;
505
      }
506
5106
      Trace("sygus-ccore-ref") << "...now check status" << std::endl;
507
      // are we done iterating children?
508
5106
      if (itv == cur->d_data.end())
509
      {
510
1416
        Trace("sygus-ccore-ref") << "...finished iterating " << std::endl;
511
        // yes, pop back
512
1416
        if (!ctx.empty())
513
        {
514
1374
          ctx.pop_back();
515
        }
516
1416
        visit.pop_back();
517
1416
        vt.erase(cur);
518
      }
519
      else
520
      {
521
3690
        Trace("sygus-ccore-ref") << "...recurse " << itv->first << std::endl;
522
        // recurse
523
3690
        ctx.push_back(itv->first);
524
3690
        visit.push_back(&(itv->second));
525
3690
        ++vt[cur];
526
      }
527
    }
528
529
5212
  } while (!visit.empty());
530
42
  return Node::null();
531
}
532
533
90
void CegisCoreConnective::Component::getTermPool(
534
    std::vector<Node>& passerts) const
535
{
536
90
  passerts.insert(passerts.end(), d_cpool.begin(), d_cpool.end());
537
90
}
538
539
146
bool CegisCoreConnective::Component::addToAsserts(CegisCoreConnective* p,
540
                                                  std::vector<Node>& passerts,
541
                                                  const std::vector<Node>& mvs,
542
                                                  Node mvId,
543
                                                  std::vector<Node>& asserts,
544
                                                  Node& an)
545
{
546
  // point should be valid
547
146
  Assert(!mvId.isNull());
548
292
  Node n;
549
146
  unsigned currIndex = 0;
550
288
  do
551
  {
552
    // select condition from passerts that evaluates to false on mvs
553
1664
    for (unsigned i = currIndex, psize = passerts.size(); i < psize; i++)
554
    {
555
2810
      Node cn = passerts[i];
556
2810
      Node cne = p->evaluate(cn, mvId, mvs);
557
1580
      if (cne.isConst() && !cne.getConst<bool>())
558
      {
559
350
        n = cn;
560
        // remove n from the pool
561
350
        passerts.erase(passerts.begin() + i, passerts.begin() + i + 1);
562
350
        currIndex = i;
563
350
        break;
564
      }
565
    }
566
434
    if (n.isNull())
567
    {
568
      // could not find any
569
84
      return false;
570
    }
571
350
    Trace("sygus-ccore-debug") << "...try adding " << n << "..." << std::endl;
572
350
    asserts.push_back(n);
573
    // is it already part of a false core?
574
350
    if (d_falseCores.hasSubset(asserts))
575
    {
576
576
      Trace("sygus-ccore-debug")
577
288
          << "..." << n << " was rejected due to previous false core"
578
288
          << std::endl;
579
288
      asserts.pop_back();
580
288
      n = Node::null();
581
    }
582
350
  } while (n.isNull());
583
124
  Trace("sygus-ccore") << "--- Insert " << n << " to falsify " << mvs
584
62
                       << std::endl;
585
  // success
586
62
  if (an.isConst())
587
  {
588
40
    Assert(an.getConst<bool>());
589
40
    an = n;
590
  }
591
  else
592
  {
593
22
    an = NodeManager::currentNM()->mkNode(AND, n, an);
594
  }
595
62
  return true;
596
}
597
598
20
void CegisCoreConnective::getModel(SmtEngine& smt,
599
                                   std::vector<Node>& vals) const
600
{
601
226
  for (const Node& v : d_vars)
602
  {
603
412
    Node mv = smt.getValue(v);
604
206
    Trace("sygus-ccore-model") << v << " -> " << mv << " ";
605
206
    vals.push_back(mv);
606
  }
607
20
}
608
609
50
bool CegisCoreConnective::getUnsatCore(
610
    SmtEngine& smt,
611
    const std::unordered_set<Node, NodeHashFunction>& queryAsserts,
612
    std::vector<Node>& uasserts) const
613
{
614
100
  UnsatCore uc = smt.getUnsatCore();
615
50
  bool hasQuery = false;
616
158
  for (UnsatCore::const_iterator i = uc.begin(); i != uc.end(); ++i)
617
  {
618
176
    Node uassert = *i;
619
108
    Trace("sygus-ccore-debug") << "  uc " << uassert << std::endl;
620
148
    if (queryAsserts.find(uassert) != queryAsserts.end())
621
    {
622
40
      hasQuery = true;
623
40
      continue;
624
    }
625
68
    uasserts.push_back(uassert);
626
  }
627
100
  return hasQuery;
628
}
629
630
Result CegisCoreConnective::checkSat(Node n, std::vector<Node>& mvs) const
631
{
632
  Trace("sygus-ccore-debug") << "...check-sat " << n << "..." << std::endl;
633
  Result r = checkWithSubsolver(n, d_vars, mvs);
634
  Trace("sygus-ccore-debug") << "...got " << r << std::endl;
635
  return r;
636
}
637
638
1804
Node CegisCoreConnective::evaluate(Node n,
639
                                   Node id,
640
                                   const std::vector<Node>& mvs)
641
{
642
1804
  Kind nk = n.getKind();
643
1804
  if (nk == AND || nk == OR)
644
  {
645
20
    NodeManager* nm = NodeManager::currentNM();
646
20
    bool expRes = nk == OR;
647
    // split AND/OR
648
60
    for (const Node& nc : n)
649
    {
650
80
      Node enc = evaluate(nc, id, mvs);
651
40
      Assert(enc.isConst());
652
40
      if (enc.getConst<bool>() == expRes)
653
      {
654
        return nm->mkConst(expRes);
655
      }
656
    }
657
20
    return nm->mkConst(!expRes);
658
  }
659
1784
  std::unordered_map<Node, Node, NodeHashFunction>& ec = d_eval_cache[n];
660
1784
  if (!id.isNull())
661
  {
662
1744
    std::unordered_map<Node, Node, NodeHashFunction>::iterator it = ec.find(id);
663
1744
    if (it != ec.end())
664
    {
665
1528
      return it->second;
666
    }
667
  }
668
  // use evaluator
669
512
  Node cn = d_eval.eval(n, d_vars, mvs);
670
256
  if (cn.isNull())
671
  {
672
    cn = n.substitute(d_vars.begin(), d_vars.end(), mvs.begin(), mvs.end());
673
    cn = Rewriter::rewrite(cn);
674
  }
675
256
  if (!id.isNull())
676
  {
677
216
    ec[id] = cn;
678
  }
679
256
  return cn;
680
}
681
682
118
Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
683
                                                    std::vector<Node>& asserts,
684
                                                    std::vector<Node>& passerts)
685
{
686
  // In terms of Variant #2 from the header file, the set D is represented by
687
  // asserts. The available set of prediates pool(B) is represented by passerts.
688
118
  NodeManager* nm = NodeManager::currentNM();
689
118
  Trace("sygus-ccore") << "------ Get initial candidate..." << std::endl;
690
118
  Node an = asserts.empty()
691
                ? d_true
692
236
                : (asserts.size() == 1 ? asserts[0] : nm->mkNode(AND, asserts));
693
236
  std::vector<Node> mvs;
694
236
  std::unordered_set<Node, NodeHashFunction> visited;
695
118
  bool addSuccess = true;
696
  // Ensure that the current conjunction evaluates to false on all refinement
697
  // points. We get refinement points until we have exhausted.
698
  // In terms of Variant #2, this is inner while loop that adds points to D
699
  // while there exists a point in pts(B) such that D is true.
700
236
  Node mvId;
701
50
  do
702
  {
703
168
    mvs.clear();
704
168
    Trace("sygus-ccore-debug") << "...get refinement pt..." << std::endl;
705
    // In terms of Variant #2, this implements the line:
706
    //   "D[v] is true for some v in pts(B)",
707
    // where v is stored in mvs.
708
168
    mvId = ccheck.getRefinementPt(this, an, visited, mvs);
709
168
    if (!mvId.isNull())
710
    {
711
126
      Trace("sygus-ccore-debug") << "...got " << mvs << std::endl;
712
      // In terms of Variant #2, this checks the conditions:
713
      //   "d'[v] is false for some d' in pool(B)" and
714
      //   "no element of cores(B) is a subset of D ++ { d' }"
715
      // and adds d' to D (asserts) if possible.
716
126
      addSuccess = ccheck.addToAsserts(this, passerts, mvs, mvId, asserts, an);
717
252
      Trace("sygus-ccore-debug")
718
126
          << "...add success is " << addSuccess << std::endl;
719
    }
720
    else
721
    {
722
42
      Trace("sygus-ccore-debug") << "...failed" << std::endl;
723
    }
724
168
  } while (!mvId.isNull() && addSuccess);
725
118
  if (!addSuccess)
726
  {
727
152
    Trace("sygus-ccore") << ">>> Failed to generate initial candidate"
728
76
                         << std::endl;
729
76
    return Node::null();
730
  }
731
42
  Trace("sygus-ccore") << "----- Initial candidate is " << an << std::endl;
732
733
  // We now have constructed an initial candidate for D. In terms of Variant #2,
734
  // we now enter the block code within "if D is false for all v in pts(B)".
735
  // Further refinements to D are made as the following do-while loop proceeds.
736
20
  do
737
  {
738
54
    addSuccess = false;
739
    // try a new core
740
74
    std::unique_ptr<SmtEngine> checkSol;
741
54
    initializeSubsolver(checkSol);
742
54
    Trace("sygus-ccore") << "----- Check candidate " << an << std::endl;
743
74
    std::vector<Node> rasserts = asserts;
744
54
    rasserts.push_back(d_sc);
745
54
    rasserts.push_back(ccheck.getFormula());
746
54
    std::shuffle(rasserts.begin(), rasserts.end(), Random::getRandom());
747
74
    Node query = rasserts.size() == 1 ? rasserts[0] : nm->mkNode(AND, rasserts);
748
252
    for (const Node& a : rasserts)
749
    {
750
198
      checkSol->assertFormula(a);
751
    }
752
74
    Result r = checkSol->checkSat();
753
54
    Trace("sygus-ccore") << "----- check-sat returned " << r << std::endl;
754
    // In terms of Variant #2, this is the check "if (S ^ D) => B"
755
54
    if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
756
    {
757
      // it entails the postcondition, now get the unsat core
758
      // In terms of Variant #2, this is the line
759
      //   "Let U be a subset of D such that S ^ U ^ ~B is unsat."
760
      // and uasserts is set to U.
761
68
      std::vector<Node> uasserts;
762
68
      std::unordered_set<Node, NodeHashFunction> queryAsserts;
763
34
      queryAsserts.insert(ccheck.getFormula());
764
34
      queryAsserts.insert(d_sc);
765
34
      bool hasQuery = getUnsatCore(*checkSol, queryAsserts, uasserts);
766
      // now, check the side condition
767
34
      bool falseCore = false;
768
34
      if (!d_sc.isNull())
769
      {
770
34
        if (!hasQuery)
771
        {
772
          // Already know it trivially rewrites to false, don't need
773
          // to use unsat cores.
774
12
          falseCore = true;
775
        }
776
        else
777
        {
778
          // In terms of Variant #2, this is the check "if S ^ U is unsat"
779
22
          Trace("sygus-ccore") << "----- Check side condition" << std::endl;
780
44
          std::unique_ptr<SmtEngine> checkSc;
781
22
          initializeSubsolver(checkSc);
782
44
          std::vector<Node> scasserts;
783
22
          scasserts.insert(scasserts.end(), uasserts.begin(), uasserts.end());
784
22
          scasserts.push_back(d_sc);
785
22
          std::shuffle(scasserts.begin(), scasserts.end(), Random::getRandom());
786
76
          for (const Node& sca : scasserts)
787
          {
788
54
            checkSc->assertFormula(sca);
789
          }
790
44
          Result rsc = checkSc->checkSat();
791
44
          Trace("sygus-ccore")
792
22
              << "----- check-sat returned " << rsc << std::endl;
793
22
          if (rsc.asSatisfiabilityResult().isSat() == Result::UNSAT)
794
          {
795
            // In terms of Variant #2, this is the line
796
            //   "Let W be a subset of D such that S ^ W is unsat."
797
            // and uasserts is set to W.
798
16
            uasserts.clear();
799
32
            std::unordered_set<Node, NodeHashFunction> queryAsserts2;
800
16
            queryAsserts2.insert(d_sc);
801
16
            getUnsatCore(*checkSc, queryAsserts2, uasserts);
802
16
            falseCore = true;
803
          }
804
        }
805
      }
806
807
34
      if (!falseCore)
808
      {
809
        // In terms of Variant #2, this is the line:
810
        //   "return u_1 AND ... AND u_m where U = { u_1, ..., u_m }".
811
6
        Trace("sygus-ccore") << ">>> Solution : " << uasserts << std::endl;
812
        // We convert the builtin solution to a sygus datatype to
813
        // communicate with the sygus solver.
814
12
        Node sol = ccheck.getSygusSolution(uasserts);
815
6
        Trace("sygus-ccore-sy") << "Sygus solution : " << sol << std::endl;
816
6
        return sol;
817
      }
818
      else
819
      {
820
28
        Assert(!uasserts.empty());
821
56
        Node xu = uasserts[0];
822
56
        Trace("sygus-ccore")
823
28
            << "--- Add false core : " << uasserts << std::endl;
824
        // notice that a singleton false core could be removed from pool
825
        // in the case that (uasserts.size() == 1).
826
28
        std::sort(uasserts.begin(), uasserts.end());
827
        // In terms of Variant #2, this is "cores(B) += W".
828
28
        ccheck.addFalseCore(query, uasserts);
829
        // remove and continue
830
        // In terms of Variant #2, this is "remove some d'' in W from D".
831
        std::vector<Node>::iterator ita =
832
28
            std::find(asserts.begin(), asserts.end(), xu);
833
28
        Assert(ita != asserts.end());
834
28
        asserts.erase(ita);
835
        // Start over, since now we don't know which points are required to
836
        // falsify.
837
28
        return constructSolutionFromPool(ccheck, asserts, passerts);
838
      }
839
    }
840
20
    else if (r.asSatisfiabilityResult().isSat() == Result::SAT)
841
    {
842
      // it does not entail the postcondition, add an assertion that blocks
843
      // the current point
844
20
      mvs.clear();
845
20
      getModel(*checkSol, mvs);
846
      // should evaluate to true
847
40
      Node ean = evaluate(an, Node::null(), mvs);
848
20
      Assert(ean.isConst() && ean.getConst<bool>());
849
20
      Trace("sygus-ccore") << "--- Add refinement point " << mvs << std::endl;
850
      // In terms of Variant #2, this is the line:
851
      //   "pts(B) += { v } where { x -> v } is a model for D ^ ~B".
852
20
      ccheck.addRefinementPt(query, mvs);
853
20
      Trace("sygus-ccore-debug") << "...get new assertion..." << std::endl;
854
      // In terms of Variant #2, this rechecks the condition of the inner while
855
      // loop and attempts to add a new assertion to D.
856
20
      addSuccess = ccheck.addToAsserts(this, passerts, mvs, query, asserts, an);
857
20
      Trace("sygus-ccore-debug") << "...success is " << addSuccess << std::endl;
858
    }
859
  } while (addSuccess);
860
8
  return Node::null();
861
}
862
863
}  // namespace quantifiers
864
}  // namespace theory
865
26685
}  // namespace CVC4