GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/ce_guided_single_inv.cpp Lines: 272 281 96.8 %
Date: 2021-03-23 Branches: 576 1266 45.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file ce_guided_single_inv.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, Tim King
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 utility for processing single invocation synthesis conjectures
13
 **
14
 **/
15
#include "theory/quantifiers/sygus/ce_guided_single_inv.h"
16
17
#include "options/quantifiers_options.h"
18
#include "smt/logic_exception.h"
19
#include "smt/smt_engine.h"
20
#include "smt/smt_engine_scope.h"
21
#include "smt/smt_statistics_registry.h"
22
#include "theory/arith/arith_msum.h"
23
#include "theory/quantifiers/quantifiers_attributes.h"
24
#include "theory/quantifiers/quantifiers_rewriter.h"
25
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
26
#include "theory/quantifiers/sygus/sygus_utils.h"
27
#include "theory/quantifiers/sygus/term_database_sygus.h"
28
#include "theory/quantifiers/term_enumeration.h"
29
#include "theory/quantifiers/term_util.h"
30
#include "theory/quantifiers_engine.h"
31
#include "theory/rewriter.h"
32
#include "theory/smt_engine_subsolver.h"
33
34
using namespace CVC4::kind;
35
36
namespace CVC4 {
37
namespace theory {
38
namespace quantifiers {
39
40
2190
CegSingleInv::CegSingleInv(QuantifiersEngine* qe)
41
    : d_qe(qe),
42
2190
      d_sip(new SingleInvocationPartition),
43
2190
      d_sol(new CegSingleInvSol(qe)),
44
      d_isSolved(false),
45
6570
      d_single_invocation(false)
46
{
47
48
2190
}
49
50
4376
CegSingleInv::~CegSingleInv()
51
{
52
2188
  delete d_sol;  // (new CegSingleInvSol(qe)),
53
2188
  delete d_sip;  // d_sip(new SingleInvocationPartition),
54
2188
}
55
56
506
void CegSingleInv::initialize(Node q)
57
{
58
  // can only register one quantified formula with this
59
506
  Assert(d_quant.isNull());
60
506
  d_quant = q;
61
506
  d_simp_quant = q;
62
506
  Trace("sygus-si") << "CegSingleInv::initialize : " << q << std::endl;
63
64
  // decompose the conjecture
65
506
  SygusUtils::decomposeSygusConjecture(d_quant, d_funs, d_unsolvedf, d_solvedf);
66
67
506
  Trace("sygus-si") << "functions: " << d_funs << std::endl;
68
506
  Trace("sygus-si") << " unsolved: " << d_unsolvedf << std::endl;
69
506
  Trace("sygus-si") << "   solved: " << d_solvedf << std::endl;
70
71
  // infer single invocation-ness
72
73
  // get the variables
74
984
  std::map<Node, std::vector<Node> > progVars;
75
1289
  for (const Node& sf : q[0])
76
  {
77
    // get its argument list
78
783
    SygusUtils::getSygusArgumentListForSynthFun(sf, progVars[sf]);
79
  }
80
  // compute single invocation partition
81
984
  Node qq;
82
506
  if (q[1].getKind() == NOT && q[1][0].getKind() == FORALL)
83
  {
84
293
    qq = q[1][0][1];
85
  }
86
  else
87
  {
88
213
    qq = TermUtil::simpleNegate(q[1]);
89
  }
90
  // process the single invocation-ness of the property
91
506
  if (!d_sip->init(d_unsolvedf, qq))
92
  {
93
56
    Trace("sygus-si") << "...not single invocation (type mismatch)"
94
28
                      << std::endl;
95
28
    return;
96
  }
97
956
  Trace("sygus-si") << "- Partitioned to single invocation parts : "
98
478
                    << std::endl;
99
478
  d_sip->debugPrint("sygus-si");
100
101
  // map from program to bound variables
102
956
  std::vector<Node> funcs;
103
478
  d_sip->getFunctions(funcs);
104
1102
  for (unsigned j = 0, size = funcs.size(); j < size; j++)
105
  {
106
624
    Assert(std::find(d_funs.begin(), d_funs.end(), funcs[j]) != d_funs.end());
107
624
    d_prog_to_sol_index[funcs[j]] = j;
108
  }
109
110
  // check if it is single invocation
111
478
  if (d_sip->isPurelySingleInvocation())
112
  {
113
    // We are fully single invocation, set single invocation if we haven't
114
    // disabled single invocation techniques.
115
369
    if (options::cegqiSingleInvMode() != options::CegqiSingleInvMode::NONE)
116
    {
117
297
      d_single_invocation = true;
118
    }
119
  }
120
}
121
122
506
void CegSingleInv::finishInit(bool syntaxRestricted)
123
{
124
506
  Trace("sygus-si-debug") << "Single invocation: finish init" << std::endl;
125
  // do not do single invocation if grammar is restricted and
126
  // options::CegqiSingleInvMode::ALL is not enabled
127
1012
  if (options::cegqiSingleInvMode() == options::CegqiSingleInvMode::USE
128
506
      && d_single_invocation && syntaxRestricted)
129
  {
130
167
    d_single_invocation = false;
131
167
    Trace("sygus-si") << "...grammar is restricted, do not use single invocation techniques." << std::endl;
132
  }
133
134
  // we now have determined whether we will do single invocation techniques
135
506
  if (!d_single_invocation)
136
  {
137
376
    d_single_inv = Node::null();
138
376
    Trace("sygus-si") << "Formula is not single invocation." << std::endl;
139
760
    if (options::cegqiSingleInvAbort())
140
    {
141
      std::stringstream ss;
142
      ss << "Property is not handled by single invocation." << std::endl;
143
      throw LogicException(ss.str());
144
    }
145
752
    return;
146
  }
147
130
  NodeManager* nm = NodeManager::currentNM();
148
130
  d_single_inv = d_sip->getSingleInvocation();
149
130
  d_single_inv = TermUtil::simpleNegate(d_single_inv);
150
260
  std::vector<Node> func_vars;
151
130
  d_sip->getFunctionVariables(func_vars);
152
130
  if (!func_vars.empty())
153
  {
154
236
    Node pbvl = nm->mkNode(BOUND_VAR_LIST, func_vars);
155
    // make the single invocation conjecture
156
118
    d_single_inv = nm->mkNode(FORALL, pbvl, d_single_inv);
157
  }
158
  // now, introduce the skolems
159
260
  std::vector<Node> sivars;
160
130
  d_sip->getSingleInvocationVariables(sivars);
161
320
  for (unsigned i = 0, size = sivars.size(); i < size; i++)
162
  {
163
    Node v = NodeManager::currentNM()->mkSkolem(
164
380
        "a", sivars[i].getType(), "single invocation arg");
165
190
    d_single_inv_arg_sk.push_back(v);
166
  }
167
260
  d_single_inv = d_single_inv.substitute(sivars.begin(),
168
                                         sivars.end(),
169
                                         d_single_inv_arg_sk.begin(),
170
130
                                         d_single_inv_arg_sk.end());
171
260
  Trace("sygus-si") << "Single invocation formula is : " << d_single_inv
172
130
                    << std::endl;
173
  // check whether we can handle this quantified formula
174
130
  CegHandledStatus status = CEG_HANDLED;
175
130
  if (d_single_inv.getKind() == FORALL)
176
  {
177
    // if the conjecture is trivially solvable, set the solution
178
118
    if (solveTrivial(d_single_inv))
179
    {
180
32
      setSolution();
181
    }
182
    else
183
    {
184
86
      status = CegInstantiator::isCbqiQuant(d_single_inv);
185
    }
186
  }
187
130
  Trace("sygus-si") << "CegHandledStatus is " << status << std::endl;
188
130
  if (status < CEG_HANDLED)
189
  {
190
20
    Trace("sygus-si") << "...do not invoke single invocation techniques since "
191
                         "the quantified formula does not have a handled "
192
10
                         "counterexample-guided instantiation strategy!"
193
10
                      << std::endl;
194
10
    d_single_invocation = false;
195
10
    d_single_inv = Node::null();
196
  }
197
}
198
199
110
bool CegSingleInv::solve()
200
{
201
110
  if (d_single_inv.isNull())
202
  {
203
    // not using single invocation techniques
204
    return false;
205
  }
206
110
  if (d_isSolved)
207
  {
208
    // already solved, probably via a call to solveTrivial.
209
32
    return true;
210
  }
211
78
  Trace("sygus-si") << "Solve using single invocation..." << std::endl;
212
78
  NodeManager* nm = NodeManager::currentNM();
213
  // Mark the quantified formula with the quantifier elimination attribute to
214
  // ensure its structure is preserved in the query below.
215
156
  Node siq = d_single_inv;
216
78
  if (siq.getKind() == FORALL)
217
  {
218
    Node n_attr =
219
        nm->mkSkolem("qe_si",
220
132
                     nm->booleanType(),
221
264
                     "Auxiliary variable for qe attr for single invocation.");
222
    QuantElimAttribute qea;
223
66
    n_attr.setAttribute(qea, true);
224
66
    n_attr = nm->mkNode(INST_ATTRIBUTE, n_attr);
225
66
    n_attr = nm->mkNode(INST_PATTERN_LIST, n_attr);
226
66
    siq = nm->mkNode(FORALL, siq[0], siq[1], n_attr);
227
  }
228
  // solve the single invocation conjecture using a fresh copy of SMT engine
229
156
  std::unique_ptr<SmtEngine> siSmt;
230
78
  initializeSubsolver(siSmt);
231
78
  siSmt->assertFormula(siq);
232
156
  Result r = siSmt->checkSat();
233
78
  Trace("sygus-si") << "Result: " << r << std::endl;
234
78
  if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
235
  {
236
    // conjecture is infeasible or unknown
237
11
    return false;
238
  }
239
  // now, get the instantiations
240
134
  std::vector<Node> qs;
241
67
  siSmt->getInstantiatedQuantifiedFormulas(qs);
242
67
  Assert(qs.size() <= 1);
243
  // track the instantiations, as solution construction is based on this
244
134
  Trace("sygus-si") << "#instantiated quantified formulas=" << qs.size()
245
67
                    << std::endl;
246
67
  d_inst.clear();
247
67
  d_instConds.clear();
248
67
  if (!qs.empty())
249
  {
250
126
    Node q = qs[0];
251
63
    Assert(q.getKind() == FORALL);
252
63
    siSmt->getInstantiationTermVectors(q, d_inst);
253
126
    Trace("sygus-si") << "#instantiations of " << q << "=" << d_inst.size()
254
63
                      << std::endl;
255
    // We use the original synthesis conjecture siq, since q may contain
256
    // internal symbols e.g. termITE skolem after preprocessing.
257
126
    std::vector<Node> vars;
258
265
    for (const Node& v : siq[0])
259
    {
260
202
      vars.push_back(v);
261
    }
262
126
    Node body = siq[1];
263
229
    for (unsigned i = 0, ninsts = d_inst.size(); i < ninsts; i++)
264
    {
265
      // note we do not convert to witness form here, since we could be
266
      // an internal subsolver
267
166
      std::vector<Node>& inst = d_inst[i];
268
166
      Trace("sygus-si") << "  Instantiation: " << inst << std::endl;
269
      // instantiation should have same arity since we are not allowed to
270
      // eliminate variables from quantifiers marked with QuantElimAttribute.
271
166
      Assert(inst.size() == vars.size());
272
      Node ilem =
273
332
          body.substitute(vars.begin(), vars.end(), inst.begin(), inst.end());
274
166
      ilem = Rewriter::rewrite(ilem);
275
166
      d_instConds.push_back(ilem);
276
166
      Trace("sygus-si") << "  Instantiation Lemma: " << ilem << std::endl;
277
    }
278
  }
279
  // set the solution
280
67
  setSolution();
281
67
  return true;
282
}
283
284
//TODO: use term size?
285
struct sortSiInstanceIndices {
286
  CegSingleInv* d_ccsi;
287
  int d_i;
288
196
  bool operator() (unsigned i, unsigned j) {
289
196
    if( d_ccsi->d_inst[i][d_i].isConst() && !d_ccsi->d_inst[j][d_i].isConst() ){
290
18
      return true;
291
    }else{
292
178
      return false;
293
    }
294
  }
295
};
296
297
147
Node CegSingleInv::getSolution(size_t sol_index,
298
                               TypeNode stn,
299
                               int& reconstructed,
300
                               bool rconsSygus)
301
{
302
147
  Assert(sol_index < d_quant[0].getNumChildren());
303
294
  Node f = d_quant[0][sol_index];
304
147
  Trace("csi-sol") << "CegSingleInv::getSolution " << f << std::endl;
305
  // maybe it is in the solved map already?
306
147
  if (d_solvedf.contains(f))
307
  {
308
    // notice that we ignore d_solutions for solved functions
309
    Trace("csi-sol") << "...return solution from annotation" << std::endl;
310
    return d_solvedf.apply(f);
311
  }
312
147
  Trace("csi-sol") << "...get solution from vector" << std::endl;
313
314
294
  Node s = d_solutions[sol_index];
315
294
  Node sol = s.getKind() == LAMBDA ? s[1] : s;
316
  // must substitute to be proper variables
317
147
  const DType& dt = stn.getDType();
318
294
  Node varList = dt.getSygusVarList();
319
147
  d_sol->d_varList.clear();
320
147
  Assert(d_single_inv_arg_sk.size() == varList.getNumChildren());
321
294
  std::vector< Node > vars;
322
408
  for (size_t i = 0, nvars = d_single_inv_arg_sk.size(); i < nvars; i++)
323
  {
324
261
    Trace("csi-sol") << d_single_inv_arg_sk[i] << " ";
325
261
    vars.push_back(d_single_inv_arg_sk[i]);
326
261
    d_sol->d_varList.push_back(varList[i]);
327
  }
328
147
  Trace("csi-sol") << std::endl;
329
147
  Assert(vars.size() == d_sol->d_varList.size());
330
294
  sol = sol.substitute(vars.begin(),
331
                       vars.end(),
332
147
                       d_sol->d_varList.begin(),
333
147
                       d_sol->d_varList.end());
334
147
  sol = reconstructToSyntax(sol, stn, reconstructed, rconsSygus);
335
147
  return s.getKind() == LAMBDA
336
             ? NodeManager::currentNM()->mkNode(LAMBDA, s[0], sol)
337
147
             : sol;
338
}
339
340
243
Node CegSingleInv::getSolutionFromInst(size_t index)
341
{
342
243
  Assert(d_sol != NULL);
343
486
  Node prog = d_quant[0][index];
344
486
  Node s;
345
  // If it is unconstrained: either the variable does not appear in the
346
  // conjecture or the conjecture can be solved without a single instantiation.
347
486
  if (d_prog_to_sol_index.find(prog) == d_prog_to_sol_index.end()
348
243
      || d_inst.empty())
349
  {
350
8
    TypeNode ptn = prog.getType();
351
4
    if (ptn.isFunction())
352
    {
353
      ptn = ptn.getRangeType();
354
    }
355
4
    Trace("csi-sol") << "Get solution for (unconstrained) " << prog << std::endl;
356
4
    s = d_qe->getTermEnumeration()->getEnumerateTerm(ptn, 0);
357
  }
358
  else
359
  {
360
239
    Trace("csi-sol") << "Get solution for " << prog << ", with skolems : ";
361
239
    size_t sol_index = d_prog_to_sol_index[prog];
362
363
    //construct the solution
364
239
    Trace("csi-sol") << "Sort solution return values " << sol_index << std::endl;
365
478
    std::vector< unsigned > indices;
366
947
    for (unsigned i = 0, ninst = d_inst.size(); i < ninst; i++)
367
    {
368
708
      indices.push_back(i);
369
    }
370
239
    Assert(!indices.empty());
371
    // We are constructing an ITE based on the list of instantiations. We
372
    // sort this list based on heuristic. Currently, we do all constant values
373
    // first since this leads to simpler conditions. Notice that we only allow
374
    // sorting if we have a single variable, since the correctness of
375
    // Proposition 1 of Reynolds et al CAV 2015 for the case of multiple
376
    // functions-to-synthesize requires that the instantiations come in the
377
    // same order for all functions. Thus, we cannot decide on an order for
378
    // instantiations independently, since this may lead to incorrect solutions.
379
239
    bool allowSort = (d_quant[0].getNumChildren() == 1);
380
239
    if (allowSort)
381
    {
382
      sortSiInstanceIndices ssii;
383
77
      ssii.d_ccsi = this;
384
77
      ssii.d_i = sol_index;
385
77
      std::sort(indices.begin(), indices.end(), ssii);
386
    }
387
239
    Trace("csi-sol") << "Construct solution" << std::endl;
388
239
    std::reverse(indices.begin(), indices.end());
389
239
    s = d_inst[indices[0]][sol_index];
390
    // it is an ITE chain whose conditions are the instantiations
391
239
    NodeManager* nm = NodeManager::currentNM();
392
708
    for (unsigned j = 1, nindices = indices.size(); j < nindices; j++)
393
    {
394
469
      unsigned uindex = indices[j];
395
938
      Node cond = d_instConds[uindex];
396
469
      cond = TermUtil::simpleNegate(cond);
397
469
      s = nm->mkNode(ITE, cond, d_inst[uindex][sol_index], s);
398
    }
399
  }
400
  //simplify the solution using the extended rewriter
401
243
  Trace("csi-sol") << "Solution (pre-simplification): " << s << std::endl;
402
243
  s = d_qe->getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(s);
403
243
  Trace("csi-sol") << "Solution (post-simplification): " << s << std::endl;
404
  // wrap into lambda, as needed
405
486
  return SygusUtils::wrapSolutionForSynthFun(prog, s);
406
}
407
408
99
void CegSingleInv::setSolution()
409
{
410
  // construct the solutions based on the instantiations
411
99
  d_solutions.clear();
412
99
  d_rcSolutions.clear();
413
198
  Subs finalSol;
414
342
  for (size_t i = 0, nvars = d_quant[0].getNumChildren(); i < nvars; i++)
415
  {
416
    // Note this is a dummy solution for solved functions, which are given
417
    // solutions in the annotation but do not appear in the conjecture.
418
486
    Node sol = getSolutionFromInst(i);
419
243
    d_solutions.push_back(sol);
420
    // haven't reconstructed to syntax yet
421
243
    d_rcSolutions.push_back(Node::null());
422
243
    finalSol.add(d_quant[0][i], sol);
423
  }
424
99
  d_isSolved = true;
425
99
  if (!d_solvedf.empty())
426
  {
427
    // replace the final solution into the solved functions
428
    finalSol.applyToRange(d_solvedf, true);
429
  }
430
99
}
431
432
164
Node CegSingleInv::reconstructToSyntax(Node s,
433
                                       TypeNode stn,
434
                                       int& reconstructed,
435
                                       bool rconsSygus)
436
{
437
  // extract the lambda body
438
328
  Node sol = s;
439
164
  const DType& dt = stn.getDType();
440
441
  //reconstruct the solution into sygus if necessary
442
164
  reconstructed = 0;
443
527
  if (options::cegqiSingleInvReconstruct()
444
          != options::CegqiSingleInvRconsMode::NONE
445
164
      && !dt.getSygusAllowAll() && !stn.isNull() && rconsSygus)
446
  {
447
16
    d_sol->preregisterConjecture( d_orig_conjecture );
448
16
    int enumLimit = -1;
449
32
    if (options::cegqiSingleInvReconstruct()
450
16
        == options::CegqiSingleInvRconsMode::TRY)
451
    {
452
1
      enumLimit = 0;
453
    }
454
30
    else if (options::cegqiSingleInvReconstruct()
455
15
             == options::CegqiSingleInvRconsMode::ALL_LIMIT)
456
    {
457
30
      enumLimit = options::cegqiSingleInvReconstructLimit();
458
    }
459
16
    sol = d_sol->reconstructSolution(s, stn, reconstructed, enumLimit);
460
16
    if( reconstructed==1 ){
461
32
      Trace("csi-sol") << "Solution (post-reconstruction into Sygus): " << sol
462
16
                       << std::endl;
463
    }
464
  }else{
465
148
    Trace("csi-sol") << "Post-process solution..." << std::endl;
466
296
    Node prev = sol;
467
148
    sol = d_qe->getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(sol);
468
148
    if (prev != sol)
469
    {
470
14
      Trace("csi-sol") << "Solution (after post process) : " << sol
471
7
                       << std::endl;
472
    }
473
  }
474
475
164
  if (reconstructed == -1)
476
  {
477
    return Node::null();
478
  }
479
164
  return sol;
480
}
481
482
508
void CegSingleInv::preregisterConjecture(Node q) { d_orig_conjecture = q; }
483
484
118
bool CegSingleInv::solveTrivial(Node q)
485
{
486
118
  Assert(!d_isSolved);
487
118
  Assert(d_inst.empty());
488
118
  Assert(q.getKind() == FORALL);
489
  // If the conjecture is forall x1...xn. ~(x1 = t1 ^ ... xn = tn), it is
490
  // trivially solvable.
491
236
  std::vector<Node> args(q[0].begin(), q[0].end());
492
  // keep solving for variables until a fixed point is reached
493
236
  std::vector<Node> vars;
494
236
  std::vector<Node> subs;
495
236
  Node body = q[1];
496
236
  Node prev;
497
428
  while (prev != body && !args.empty())
498
  {
499
155
    prev = body;
500
501
310
    std::vector<Node> varsTmp;
502
310
    std::vector<Node> subsTmp;
503
155
    QuantifiersRewriter::getVarElim(body, false, args, varsTmp, subsTmp);
504
    // if we eliminated a variable, update body and reprocess
505
155
    if (!varsTmp.empty())
506
    {
507
72
      Assert(varsTmp.size() == subsTmp.size());
508
      // remake with eliminated nodes
509
72
      body = body.substitute(
510
          varsTmp.begin(), varsTmp.end(), subsTmp.begin(), subsTmp.end());
511
72
      body = Rewriter::rewrite(body);
512
      // apply to subs
513
      // this ensures we behave correctly if we solve x before y in
514
      // x = y+1 ^ y = 2.
515
93
      for (size_t i = 0, ssize = subs.size(); i < ssize; i++)
516
      {
517
21
        subs[i] = subs[i].substitute(
518
            varsTmp.begin(), varsTmp.end(), subsTmp.begin(), subsTmp.end());
519
21
        subs[i] = Rewriter::rewrite(subs[i]);
520
      }
521
72
      vars.insert(vars.end(), varsTmp.begin(), varsTmp.end());
522
72
      subs.insert(subs.end(), subsTmp.begin(), subsTmp.end());
523
    }
524
  }
525
  // if we solved all arguments
526
118
  if (args.empty() && body.isConst() && !body.getConst<bool>())
527
  {
528
64
    Trace("sygus-si-trivial-solve")
529
32
        << q << " is trivially solvable by substitution " << vars << " -> "
530
32
        << subs << std::endl;
531
64
    std::map<Node, Node> imap;
532
69
    for (size_t j = 0, vsize = vars.size(); j < vsize; j++)
533
    {
534
37
      imap[vars[j]] = subs[j];
535
    }
536
64
    std::vector<Node> inst;
537
69
    for (const Node& v : q[0])
538
    {
539
37
      Assert(imap.find(v) != imap.end());
540
37
      inst.push_back(imap[v]);
541
    }
542
32
    d_inst.push_back(inst);
543
32
    d_instConds.push_back(NodeManager::currentNM()->mkConst(true));
544
32
    return true;
545
  }
546
172
  Trace("sygus-si-trivial-solve")
547
86
      << q << " is not trivially solvable." << std::endl;
548
549
86
  return false;
550
}
551
552
}  // namespace quantifiers
553
}  // namespace theory
554
27283
}  // namespace CVC4