GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/cegqi/ceg_instantiator.cpp Lines: 817 896 91.2 %
Date: 2021-03-22 Branches: 1652 3372 49.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file ceg_instantiator.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Piotr Trojanek, Mathias Preiner
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Implementation of counterexample-guided quantifier instantiation
13
 **/
14
15
#include "theory/quantifiers/cegqi/ceg_instantiator.h"
16
17
#include "theory/quantifiers/cegqi/ceg_arith_instantiator.h"
18
#include "theory/quantifiers/cegqi/ceg_bv_instantiator.h"
19
#include "theory/quantifiers/cegqi/ceg_dt_instantiator.h"
20
21
#include "expr/dtype.h"
22
#include "expr/dtype_cons.h"
23
#include "expr/node_algorithm.h"
24
#include "options/quantifiers_options.h"
25
#include "theory/arith/arith_msum.h"
26
#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
27
#include "theory/quantifiers/first_order_model.h"
28
#include "theory/quantifiers/quantifiers_attributes.h"
29
#include "theory/quantifiers/quantifiers_rewriter.h"
30
#include "theory/quantifiers/term_database.h"
31
#include "theory/quantifiers/term_util.h"
32
#include "theory/quantifiers_engine.h"
33
#include "theory/rewriter.h"
34
#include "theory/theory_engine.h"
35
36
using namespace std;
37
using namespace CVC4::kind;
38
39
namespace CVC4 {
40
namespace theory {
41
namespace quantifiers {
42
43
309
CegTermType mkStrictCTT(CegTermType c)
44
{
45
309
  Assert(!isStrictCTT(c));
46
309
  if (c == CEG_TT_LOWER)
47
  {
48
204
    return CEG_TT_LOWER_STRICT;
49
  }
50
105
  else if (c == CEG_TT_UPPER)
51
  {
52
105
    return CEG_TT_UPPER_STRICT;
53
  }
54
  return c;
55
}
56
57
1936
CegTermType mkNegateCTT(CegTermType c)
58
{
59
1936
  if (c == CEG_TT_LOWER)
60
  {
61
414
    return CEG_TT_UPPER;
62
  }
63
1522
  else if (c == CEG_TT_UPPER)
64
  {
65
1522
    return CEG_TT_LOWER;
66
  }
67
  else if (c == CEG_TT_LOWER_STRICT)
68
  {
69
    return CEG_TT_UPPER_STRICT;
70
  }
71
  else if (c == CEG_TT_UPPER_STRICT)
72
  {
73
    return CEG_TT_LOWER_STRICT;
74
  }
75
  return c;
76
}
77
309
bool isStrictCTT(CegTermType c)
78
{
79
309
  return c == CEG_TT_LOWER_STRICT || c == CEG_TT_UPPER_STRICT;
80
}
81
bool isLowerBoundCTT(CegTermType c)
82
{
83
  return c == CEG_TT_LOWER || c == CEG_TT_LOWER_STRICT;
84
}
85
9892
bool isUpperBoundCTT(CegTermType c)
86
{
87
9892
  return c == CEG_TT_UPPER || c == CEG_TT_UPPER_STRICT;
88
}
89
90
std::ostream& operator<<(std::ostream& os, CegInstEffort e)
91
{
92
  switch (e)
93
  {
94
    case CEG_INST_EFFORT_NONE: os << "?"; break;
95
    case CEG_INST_EFFORT_STANDARD: os << "STANDARD"; break;
96
    case CEG_INST_EFFORT_STANDARD_MV: os << "STANDARD_MV"; break;
97
    case CEG_INST_EFFORT_FULL: os << "FULL"; break;
98
    default: Unreachable();
99
  }
100
  return os;
101
}
102
103
std::ostream& operator<<(std::ostream& os, CegInstPhase phase)
104
{
105
  switch (phase)
106
  {
107
    case CEG_INST_PHASE_NONE: os << "?"; break;
108
    case CEG_INST_PHASE_EQC: os << "eqc"; break;
109
    case CEG_INST_PHASE_EQUAL: os << "eq"; break;
110
    case CEG_INST_PHASE_ASSERTION: os << "as"; break;
111
    case CEG_INST_PHASE_MVALUE: os << "mv"; break;
112
    default: Unreachable();
113
  }
114
  return os;
115
}
116
std::ostream& operator<<(std::ostream& os, CegHandledStatus status)
117
{
118
  switch (status)
119
  {
120
    case CEG_UNHANDLED: os << "unhandled"; break;
121
    case CEG_PARTIALLY_HANDLED: os << "partially_handled"; break;
122
    case CEG_HANDLED: os << "handled"; break;
123
    case CEG_HANDLED_UNCONDITIONAL: os << "handled_unc"; break;
124
    default: Unreachable();
125
  }
126
  return os;
127
}
128
129
2
void TermProperties::composeProperty(TermProperties& p)
130
{
131
2
  if (p.d_coeff.isNull())
132
  {
133
    return;
134
  }
135
2
  if (d_coeff.isNull())
136
  {
137
2
    d_coeff = p.d_coeff;
138
  }
139
  else
140
  {
141
    d_coeff = NodeManager::currentNM()->mkNode(MULT, d_coeff, p.d_coeff);
142
    d_coeff = Rewriter::rewrite(d_coeff);
143
  }
144
}
145
146
// push the substitution pv_prop.getModifiedTerm(pv) -> n
147
18868
void SolvedForm::push_back(Node pv, Node n, TermProperties& pv_prop)
148
{
149
18868
  d_vars.push_back(pv);
150
18868
  d_subs.push_back(n);
151
18868
  d_props.push_back(pv_prop);
152
18868
  if (pv_prop.isBasic())
153
  {
154
18756
    return;
155
  }
156
112
  d_non_basic.push_back(pv);
157
  // update theta value
158
224
  Node new_theta = getTheta();
159
112
  if (new_theta.isNull())
160
  {
161
106
    new_theta = pv_prop.d_coeff;
162
  }
163
  else
164
  {
165
6
    new_theta =
166
12
        NodeManager::currentNM()->mkNode(MULT, new_theta, pv_prop.d_coeff);
167
6
    new_theta = Rewriter::rewrite(new_theta);
168
  }
169
112
  d_theta.push_back(new_theta);
170
}
171
// pop the substitution pv_prop.getModifiedTerm(pv) -> n
172
4084
void SolvedForm::pop_back(Node pv, Node n, TermProperties& pv_prop)
173
{
174
4084
  d_vars.pop_back();
175
4084
  d_subs.pop_back();
176
4084
  d_props.pop_back();
177
4084
  if (pv_prop.isBasic())
178
  {
179
4048
    return;
180
  }
181
36
  d_non_basic.pop_back();
182
  // update theta value
183
36
  d_theta.pop_back();
184
}
185
186
1731
CegInstantiator::CegInstantiator(Node q,
187
                                 QuantifiersState& qs,
188
1731
                                 InstStrategyCegqi* parent)
189
    : d_quant(q),
190
      d_qstate(qs),
191
      d_parent(parent),
192
1731
      d_qe(parent->getQuantifiersEngine()),
193
      d_is_nested_quant(false),
194
3462
      d_effort(CEG_INST_EFFORT_NONE)
195
{
196
1731
}
197
198
5193
CegInstantiator::~CegInstantiator() {
199
4818
  for (std::pair<Node, Instantiator*> inst : d_instantiator)
200
  {
201
3087
    delete inst.second;
202
  }
203
2449
  for (std::pair<TheoryId, InstantiatorPreprocess*> instp : d_tipp)
204
  {
205
718
    delete instp.second;
206
  }
207
3462
}
208
209
1385870
void CegInstantiator::computeProgVars( Node n ){
210
1385870
  if( d_prog_var.find( n )==d_prog_var.end() ){
211
57879
    d_prog_var[n].clear();
212
57879
    if (n.getKind() == kind::WITNESS)
213
    {
214
610
      Assert(d_prog_var.find(n[0][0]) == d_prog_var.end());
215
610
      d_prog_var[n[0][0]].clear();
216
    }
217
57879
    if (d_vars_set.find(n) != d_vars_set.end())
218
    {
219
2776
      d_prog_var[n].insert(n);
220
    }
221
55103
    else if (!isEligibleForInstantiation(n))
222
    {
223
2676
      d_inelig.insert(n);
224
2676
      return;
225
    }
226
135087
    for( unsigned i=0; i<n.getNumChildren(); i++ ){
227
79884
      computeProgVars( n[i] );
228
79884
      if( d_inelig.find( n[i] )!=d_inelig.end() ){
229
13631
        d_inelig.insert(n);
230
      }
231
      // all variables in child are contained in this
232
79884
      d_prog_var[n].insert(d_prog_var[n[i]].begin(), d_prog_var[n[i]].end());
233
    }
234
    // selectors applied to program variables are also variables
235
110406
    if (n.getKind() == APPLY_SELECTOR_TOTAL
236
110406
        && d_prog_var[n].find(n[0]) != d_prog_var[n].end())
237
    {
238
34
      d_prog_var[n].insert(n);
239
    }
240
55203
    if (n.getKind() == kind::WITNESS)
241
    {
242
610
      d_prog_var.erase(n[0][0]);
243
    }
244
  }
245
}
246
247
451150
bool CegInstantiator::isEligible( Node n ) {
248
  //compute d_subs_fv, which program variables are contained in n, and determines if eligible
249
451150
  computeProgVars( n );
250
451150
  return d_inelig.find( n )==d_inelig.end();
251
}
252
253
47580
CegHandledStatus CegInstantiator::isCbqiKind(Kind k)
254
{
255
119802
  if (quantifiers::TermUtil::isBoolConnective(k) || k == PLUS || k == GEQ
256
12926
      || k == EQUAL || k == MULT || k == NONLINEAR_MULT || k == DIVISION
257
7897
      || k == DIVISION_TOTAL || k == INTS_DIVISION || k == INTS_DIVISION_TOTAL
258
7784
      || k == INTS_MODULUS || k == INTS_MODULUS_TOTAL || k == TO_INTEGER
259
55272
      || k == IS_INTEGER)
260
  {
261
39892
    return CEG_HANDLED;
262
  }
263
264
  // CBQI typically works for satisfaction-complete theories
265
7688
  TheoryId t = kindToTheoryId(k);
266
7688
  if (t == THEORY_BV || t == THEORY_FP || t == THEORY_DATATYPES
267
4606
      || t == THEORY_BOOL)
268
  {
269
3082
    return CEG_HANDLED;
270
  }
271
4606
  return CEG_UNHANDLED;
272
}
273
274
6430
CegHandledStatus CegInstantiator::isCbqiTerm(Node n)
275
{
276
6430
  CegHandledStatus ret = CEG_HANDLED;
277
12860
  std::unordered_set<TNode, TNodeHashFunction> visited;
278
12860
  std::vector<TNode> visit;
279
12860
  TNode cur;
280
6430
  visit.push_back(n);
281
88983
  do
282
  {
283
95413
    cur = visit.back();
284
95413
    visit.pop_back();
285
95413
    if (visited.find(cur) == visited.end())
286
    {
287
77913
      visited.insert(cur);
288
77913
      if (cur.getKind() != BOUND_VARIABLE && TermUtil::hasBoundVarAttr(cur))
289
      {
290
54298
        if (cur.getKind() == FORALL || cur.getKind() == WITNESS)
291
        {
292
6718
          visit.push_back(cur[1]);
293
        }
294
        else
295
        {
296
47580
          CegHandledStatus curr = isCbqiKind(cur.getKind());
297
47580
          if (curr < ret)
298
          {
299
4606
            ret = curr;
300
9212
            Trace("cegqi-debug2") << "Non-cbqi kind : " << cur.getKind()
301
4606
                                 << " in " << n << std::endl;
302
4606
            if (curr == CEG_UNHANDLED)
303
            {
304
4606
              return CEG_UNHANDLED;
305
            }
306
          }
307
134274
          for (const Node& nc : cur)
308
          {
309
91300
            visit.push_back(nc);
310
          }
311
        }
312
      }
313
    }
314
90807
  } while (!visit.empty());
315
1824
  return ret;
316
}
317
318
24320
CegHandledStatus CegInstantiator::isCbqiSort(TypeNode tn, QuantifiersEngine* qe)
319
{
320
48640
  std::map<TypeNode, CegHandledStatus> visited;
321
48640
  return isCbqiSort(tn, visited, qe);
322
}
323
324
28445
CegHandledStatus CegInstantiator::isCbqiSort(
325
    TypeNode tn,
326
    std::map<TypeNode, CegHandledStatus>& visited,
327
    QuantifiersEngine* qe)
328
{
329
28445
  std::map<TypeNode, CegHandledStatus>::iterator itv = visited.find(tn);
330
28445
  if (itv != visited.end())
331
  {
332
2399
    return itv->second;
333
  }
334
26046
  CegHandledStatus ret = CEG_UNHANDLED;
335
68846
  if (tn.isInteger() || tn.isReal() || tn.isBoolean() || tn.isBitVector()
336
40687
      || tn.isFloatingPoint())
337
  {
338
11418
    ret = CEG_HANDLED;
339
  }
340
14628
  else if (tn.isDatatype())
341
  {
342
    // recursive calls to this datatype are handlable
343
1921
    visited[tn] = CEG_HANDLED;
344
    // we initialize to handled, we remain handled as long as all subfields
345
    // of this datatype are not unhandled.
346
1921
    ret = CEG_HANDLED;
347
1921
    const DType& dt = tn.getDType();
348
3940
    for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
349
    {
350
      // get the constructor type
351
5290
      TypeNode consType;
352
3271
      if (dt.isParametric())
353
      {
354
        // if parametric, must instantiate the argument types
355
32
        consType = dt[i].getSpecializedConstructorType(tn);
356
      }
357
      else
358
      {
359
3239
        consType = dt[i].getConstructor().getType();
360
      }
361
6144
      for (const TypeNode& crange : consType)
362
      {
363
4125
        CegHandledStatus cret = isCbqiSort(crange, visited, qe);
364
4125
        if (cret == CEG_UNHANDLED)
365
        {
366
2504
          Trace("cegqi-debug2")
367
1252
              << "Non-cbqi sort : " << tn << " due to " << crange << std::endl;
368
1252
          visited[tn] = CEG_UNHANDLED;
369
1252
          return CEG_UNHANDLED;
370
        }
371
2873
        else if (cret < ret)
372
        {
373
          ret = cret;
374
        }
375
      }
376
    }
377
  }
378
  // sets, arrays, functions and others are not supported
379
24794
  visited[tn] = ret;
380
24794
  return ret;
381
}
382
383
19135
CegHandledStatus CegInstantiator::isCbqiQuantPrefix(Node q,
384
                                                    QuantifiersEngine* qe)
385
{
386
19135
  CegHandledStatus hmin = CEG_HANDLED_UNCONDITIONAL;
387
30693
  for (const Node& v : q[0])
388
  {
389
35821
    TypeNode tn = v.getType();
390
24263
    CegHandledStatus handled = isCbqiSort(tn, qe);
391
24263
    if (handled == CEG_UNHANDLED)
392
    {
393
12705
      return CEG_UNHANDLED;
394
    }
395
11558
    else if (handled < hmin)
396
    {
397
6708
      hmin = handled;
398
    }
399
  }
400
6430
  return hmin;
401
}
402
403
23401
CegHandledStatus CegInstantiator::isCbqiQuant(Node q, QuantifiersEngine* qe)
404
{
405
23401
  Assert(q.getKind() == FORALL);
406
  // compute attributes
407
46802
  QAttributes qa;
408
23401
  QuantAttributes::computeQuantAttributes(q, qa);
409
23401
  if (qa.d_quant_elim)
410
  {
411
96
    return CEG_HANDLED;
412
  }
413
23305
  if (qa.d_sygus)
414
  {
415
512
    return CEG_UNHANDLED;
416
  }
417
22793
  Assert(!qa.d_quant_elim_partial);
418
  // if has an instantiation pattern, don't do it
419
22793
  if (q.getNumChildren() == 3)
420
  {
421
4152
    for (const Node& pat : q[2])
422
    {
423
3931
      if (pat.getKind() == INST_PATTERN)
424
      {
425
3658
        return CEG_UNHANDLED;
426
      }
427
    }
428
  }
429
19135
  CegHandledStatus ret = CEG_HANDLED;
430
  // if quantifier has a non-handled variable, then do not use cbqi
431
  // if quantifier has an APPLY_UF term, then do not use cbqi unless EPR
432
19135
  CegHandledStatus ncbqiv = CegInstantiator::isCbqiQuantPrefix(q, qe);
433
38270
  Trace("cegqi-quant-debug") << "isCbqiQuantPrefix returned " << ncbqiv
434
19135
                            << std::endl;
435
19135
  if (ncbqiv == CEG_UNHANDLED)
436
  {
437
    // unhandled variable type
438
12705
    ret = CEG_UNHANDLED;
439
  }
440
  else
441
  {
442
6430
    CegHandledStatus cbqit = CegInstantiator::isCbqiTerm(q);
443
6430
    Trace("cegqi-quant-debug") << "isCbqiTerm returned " << cbqit << std::endl;
444
6430
    if (cbqit == CEG_UNHANDLED)
445
    {
446
4606
      if (ncbqiv == CEG_HANDLED_UNCONDITIONAL)
447
      {
448
        // all variables are fully handled, this implies this will be handlable
449
        // regardless of body (e.g. for EPR)
450
        //  so, try but not exclusively
451
        ret = CEG_PARTIALLY_HANDLED;
452
      }
453
      else
454
      {
455
        // cannot be handled
456
4606
        ret = CEG_UNHANDLED;
457
      }
458
    }
459
1824
    else if (cbqit == CEG_PARTIALLY_HANDLED)
460
    {
461
      ret = CEG_PARTIALLY_HANDLED;
462
    }
463
  }
464
19135
  if (ret == CEG_UNHANDLED && options::cegqiAll())
465
  {
466
    // try but not exclusively
467
11
    ret = CEG_PARTIALLY_HANDLED;
468
  }
469
19135
  return ret;
470
}
471
472
158725
bool CegInstantiator::hasVariable( Node n, Node pv ) {
473
158725
  computeProgVars( n );
474
158725
  return d_prog_var[n].find( pv )!=d_prog_var[n].end();
475
}
476
477
18932
void CegInstantiator::activateInstantiationVariable(Node v, unsigned index)
478
{
479
18932
  if( d_instantiator.find( v )==d_instantiator.end() ){
480
6174
    TypeNode tn = v.getType();
481
    Instantiator * vinst;
482
3087
    if( tn.isReal() ){
483
1663
      vinst = new ArithInstantiator(tn, d_parent->getVtsTermCache());
484
1424
    }else if( tn.isDatatype() ){
485
35
      vinst = new DtInstantiator(tn);
486
1389
    }else if( tn.isBitVector() ){
487
1198
      vinst = new BvInstantiator(tn, d_parent->getBvInverter());
488
191
    }else if( tn.isBoolean() ){
489
179
      vinst = new ModelValueInstantiator(tn);
490
    }else{
491
      //default
492
12
      vinst = new Instantiator(tn);
493
    }
494
3087
    d_instantiator[v] = vinst;
495
  }
496
18932
  d_curr_subs_proc[v].clear();
497
18932
  d_curr_index[v] = index;
498
18932
  d_curr_iphase[v] = CEG_INST_PHASE_NONE;
499
18932
}
500
501
4148
void CegInstantiator::deactivateInstantiationVariable(Node v)
502
{
503
4148
  d_curr_subs_proc.erase(v);
504
4148
  d_curr_index.erase(v);
505
4148
  d_curr_iphase.erase(v);
506
4148
}
507
508
31708
bool CegInstantiator::hasTriedInstantiation(Node v)
509
{
510
31708
  return !d_curr_subs_proc[v].empty();
511
}
512
513
4716
void CegInstantiator::registerTheoryIds(TypeNode tn,
514
                                        std::map<TypeNode, bool>& visited)
515
{
516
4716
  if (visited.find(tn) == visited.end())
517
  {
518
4675
    visited[tn] = true;
519
4675
    TheoryId tid = Theory::theoryOf(tn);
520
4675
    registerTheoryId(tid);
521
4675
    if (tn.isDatatype())
522
    {
523
43
      const DType& dt = tn.getDType();
524
120
      for (unsigned i = 0; i < dt.getNumConstructors(); i++)
525
      {
526
160
        for (unsigned j = 0; j < dt[i].getNumArgs(); j++)
527
        {
528
83
          registerTheoryIds(dt[i].getArgType(j), visited);
529
        }
530
      }
531
    }
532
  }
533
4716
}
534
535
6406
void CegInstantiator::registerTheoryId(TheoryId tid)
536
{
537
6406
  if (std::find(d_tids.begin(), d_tids.end(), tid) == d_tids.end())
538
  {
539
    // setup any theory-specific preprocessors here
540
3520
    if (tid == THEORY_BV)
541
    {
542
718
      d_tipp[tid] = new BvInstantiatorPreprocess;
543
    }
544
3520
    d_tids.push_back(tid);
545
  }
546
6406
}
547
548
4633
void CegInstantiator::registerVariable(Node v)
549
{
550
4633
  Assert(std::find(d_vars.begin(), d_vars.end(), v) == d_vars.end());
551
4633
  d_vars.push_back(v);
552
4633
  d_vars_set.insert(v);
553
9266
  TypeNode vtn = v.getType();
554
9266
  Trace("cegqi-proc-debug") << "Collect theory ids from type " << vtn << " of "
555
4633
                           << v << std::endl;
556
  // collect relevant theories for this variable
557
9266
  std::map<TypeNode, bool> visited;
558
4633
  registerTheoryIds(vtn, visited);
559
4633
}
560
561
23981
bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i)
562
{
563
23981
  if( i==d_vars.size() ){
564
    //solved for all variables, now construct instantiation
565
    bool needsPostprocess =
566
5049
        sf.d_vars.size() > d_input_vars.size() || !d_var_order_index.empty();
567
10098
    std::vector< Instantiator * > pp_inst;
568
10098
    std::map< Instantiator *, Node > pp_inst_to_var;
569
10098
    std::vector< Node > lemmas;
570
23917
    for( std::map< Node, Instantiator * >::iterator ita = d_active_instantiators.begin(); ita != d_active_instantiators.end(); ++ita ){
571
56604
      if (ita->second->needsPostProcessInstantiationForVariable(
572
37736
              this, sf, ita->first, d_effort))
573
      {
574
114
        needsPostprocess = true;
575
114
        pp_inst_to_var[ ita->second ] = ita->first;
576
      }
577
    }
578
5049
    if( needsPostprocess ){
579
      //must make copy so that backtracking reverts sf
580
2858
      SolvedForm sf_tmp = sf;
581
1429
      bool postProcessSuccess = true;
582
1513
      for( std::map< Instantiator *, Node >::iterator itp = pp_inst_to_var.begin(); itp != pp_inst_to_var.end(); ++itp ){
583
342
        if (!itp->first->postProcessInstantiationForVariable(
584
228
                this, sf_tmp, itp->second, d_effort, lemmas))
585
        {
586
30
          postProcessSuccess = false;
587
30
          break;
588
        }
589
      }
590
1429
      if( postProcessSuccess ){
591
1399
        return doAddInstantiation( sf_tmp.d_vars, sf_tmp.d_subs, lemmas );
592
      }else{
593
30
        return false;
594
      }
595
    }else{
596
3620
      return doAddInstantiation( sf.d_vars, sf.d_subs, lemmas );
597
    }
598
  }else{
599
18932
    bool is_sv = false;
600
37864
    Node pv;
601
18932
    if( d_stack_vars.empty() ){
602
18888
      pv = d_vars[i];
603
    }else{
604
44
      pv = d_stack_vars.back();
605
44
      is_sv = true;
606
44
      d_stack_vars.pop_back();
607
    }
608
18932
    activateInstantiationVariable(pv, i);
609
610
    //get the instantiator object
611
18932
    Assert(d_instantiator.find(pv) != d_instantiator.end());
612
18932
    Instantiator* vinst = d_instantiator[pv];
613
18932
    Assert(vinst != NULL);
614
18932
    d_active_instantiators[pv] = vinst;
615
18932
    vinst->reset(this, sf, pv, d_effort);
616
    // if d_effort is full, we must choose at least one model value
617
18932
    if ((i + 1) < d_vars.size() || d_effort != CEG_INST_EFFORT_FULL)
618
    {
619
      // First, try to construct an instantiation term for pv based on
620
      // equality and theory-specific instantiation techniques.
621
17804
      if (constructInstantiation(sf, vinst, pv))
622
      {
623
9971
        return true;
624
      }
625
    }
626
    // If the above call fails, resort to using value in model. We do so if:
627
    // - we have yet to try an instantiation this round (or we are trying
628
    //   multiple instantiations, indicated by options::cegqiMultiInst),
629
    // - the instantiator uses model values at this effort or
630
    //   if we are solving for a subfield of a datatype (is_sv), and
631
    // - the instantiator allows model values.
632
26803
    if ((options::cegqiMultiInst() || !hasTriedInstantiation(pv))
633
15228
        && (vinst->useModelValue(this, sf, pv, d_effort) || is_sv)
634
24005
        && vinst->allowModelValue(this, sf, pv, d_effort))
635
    {
636
7353
      Node mv = getModelValue( pv );
637
7353
      TermProperties pv_prop_m;
638
6083
      Trace("cegqi-inst-debug") << "[4] " << i << "...try model value " << mv << std::endl;
639
6083
      d_curr_iphase[pv] = CEG_INST_PHASE_MVALUE;
640
6083
      CegInstEffort prev = d_effort;
641
6083
      if (d_effort < CEG_INST_EFFORT_STANDARD_MV)
642
      {
643
        // update the effort level to indicate we have used a model value
644
1561
        d_effort = CEG_INST_EFFORT_STANDARD_MV;
645
      }
646
6083
      if (constructInstantiationInc(pv, mv, pv_prop_m, sf))
647
      {
648
4813
        return true;
649
      }
650
1270
      d_effort = prev;
651
    }
652
653
4148
    Trace("cegqi-inst-debug") << "[No instantiation found for " << pv << "]" << std::endl;
654
4148
    if (is_sv)
655
    {
656
      d_stack_vars.push_back( pv );
657
    }
658
4148
    d_active_instantiators.erase( pv );
659
4148
    deactivateInstantiationVariable(pv);
660
4148
    return false;
661
  }
662
}
663
664
17804
bool CegInstantiator::constructInstantiation(SolvedForm& sf,
665
                                             Instantiator* vinst,
666
                                             Node pv)
667
{
668
35608
  TypeNode pvtn = pv.getType();
669
35608
  TypeNode pvtnb = pvtn.getBaseType();
670
35608
  Node pvr = pv;
671
17804
  eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine();
672
17804
  if (ee->hasTerm(pv))
673
  {
674
12827
    pvr = ee->getRepresentative(pv);
675
  }
676
35608
  Trace("cegqi-inst-debug") << "[Find instantiation for " << pv
677
17804
                           << "], rep=" << pvr << ", instantiator is "
678
17804
                           << vinst->identify() << std::endl;
679
35608
  Node pv_value;
680
17804
  if (options::cegqiModel())
681
  {
682
17804
    pv_value = getModelValue(pv);
683
17804
    Trace("cegqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl;
684
  }
685
686
  //[1] easy case : pv is in the equivalence class as another term not
687
  // containing pv
688
17804
  if (vinst->hasProcessEqualTerm(this, sf, pv, d_effort))
689
  {
690
86
    Trace("cegqi-inst-debug")
691
43
        << "[1] try based on equivalence class." << std::endl;
692
43
    d_curr_iphase[pv] = CEG_INST_PHASE_EQC;
693
43
    std::map<Node, std::vector<Node> >::iterator it_eqc = d_curr_eqc.find(pvr);
694
43
    if (it_eqc != d_curr_eqc.end())
695
    {
696
      // std::vector< Node > eq_candidates;
697
86
      Trace("cegqi-inst-debug2")
698
43
          << "...eqc has size " << it_eqc->second.size() << std::endl;
699
100
      for (const Node& n : it_eqc->second)
700
      {
701
69
        if (n != pv)
702
        {
703
72
          Trace("cegqi-inst-debug")
704
36
              << "...try based on equal term " << n << std::endl;
705
          // must be an eligible term
706
36
          if (isEligible(n))
707
          {
708
60
            Node ns;
709
            // coefficient of pv in the equality we solve (null is 1)
710
60
            TermProperties pv_prop;
711
36
            bool proc = false;
712
36
            if (!d_prog_var[n].empty())
713
            {
714
24
              ns = applySubstitution(pvtn, n, sf, pv_prop, false);
715
24
              if (!ns.isNull())
716
              {
717
24
                computeProgVars(ns);
718
                // substituted version must be new and cannot contain pv
719
24
                proc = d_prog_var[ns].find(pv) == d_prog_var[ns].end();
720
              }
721
            }
722
            else
723
            {
724
12
              ns = n;
725
12
              proc = true;
726
            }
727
36
            if (proc)
728
            {
729
12
              if (vinst->processEqualTerm(this, sf, pv, pv_prop, ns, d_effort))
730
              {
731
12
                return true;
732
              }
733
              else if (!options::cegqiMultiInst() && hasTriedInstantiation(pv))
734
              {
735
                return false;
736
              }
737
              // Do not consider more than one equal term,
738
              // this helps non-monotonic strategies that may encounter
739
              // duplicate instantiations.
740
              break;
741
            }
742
          }
743
        }
744
      }
745
31
      if (vinst->processEqualTerms(this, sf, pv, it_eqc->second, d_effort))
746
      {
747
22
        return true;
748
      }
749
9
      else if (!options::cegqiMultiInst() && hasTriedInstantiation(pv))
750
      {
751
        return false;
752
      }
753
    }
754
    else
755
    {
756
      Trace("cegqi-inst-debug2") << "...eqc not found." << std::endl;
757
    }
758
  }
759
760
  //[2] : we can solve an equality for pv
761
  /// iterate over equivalence classes to find cases where we can solve for
762
  /// the variable
763
17770
  if (vinst->hasProcessEquality(this, sf, pv, d_effort))
764
  {
765
23626
    Trace("cegqi-inst-debug")
766
11813
        << "[2] try based on solving equalities." << std::endl;
767
11813
    d_curr_iphase[pv] = CEG_INST_PHASE_EQUAL;
768
11813
    std::vector<Node>& cteqc = d_curr_type_eqc[pvtnb];
769
770
183782
    for (const Node& r : cteqc)
771
    {
772
177220
      std::map<Node, std::vector<Node> >::iterator it_reqc = d_curr_eqc.find(r);
773
349189
      std::vector<Node> lhs;
774
349189
      std::vector<bool> lhs_v;
775
349189
      std::vector<TermProperties> lhs_prop;
776
177220
      Assert(it_reqc != d_curr_eqc.end());
777
600559
      for (const Node& n : it_reqc->second)
778
      {
779
428590
        Trace("cegqi-inst-debug2") << "...look at term " << n << std::endl;
780
        // must be an eligible term
781
428590
        if (isEligible(n))
782
        {
783
572755
          Node ns;
784
572755
          TermProperties pv_prop;
785
289003
          if (!d_prog_var[n].empty())
786
          {
787
247922
            ns = applySubstitution(pvtn, n, sf, pv_prop);
788
247922
            if (!ns.isNull())
789
            {
790
247914
              computeProgVars(ns);
791
            }
792
          }
793
          else
794
          {
795
41081
            ns = n;
796
          }
797
289003
          if (!ns.isNull())
798
          {
799
288995
            bool hasVar = d_prog_var[ns].find(pv) != d_prog_var[ns].end();
800
577990
            Trace("cegqi-inst-debug2") << "... " << ns << " has var " << pv
801
288995
                                      << " : " << hasVar << std::endl;
802
572739
            std::vector<TermProperties> term_props;
803
572739
            std::vector<Node> terms;
804
288995
            term_props.push_back(pv_prop);
805
288995
            terms.push_back(ns);
806
634851
            for (unsigned j = 0, size = lhs.size(); j < size; j++)
807
            {
808
              // if this term or the another has pv in it, try to solve for it
809
351107
              if (hasVar || lhs_v[j])
810
              {
811
33290
                Trace("cegqi-inst-debug") << "......try based on equality "
812
16645
                                         << lhs[j] << " = " << ns << std::endl;
813
16645
                term_props.push_back(lhs_prop[j]);
814
16645
                terms.push_back(lhs[j]);
815
16645
                if (vinst->processEquality(
816
16645
                        this, sf, pv, term_props, terms, d_effort))
817
                {
818
4277
                  return true;
819
                }
820
12368
                else if (!options::cegqiMultiInst() && hasTriedInstantiation(pv))
821
                {
822
974
                  return false;
823
                }
824
11394
                term_props.pop_back();
825
11394
                terms.pop_back();
826
              }
827
            }
828
283744
            lhs.push_back(ns);
829
283744
            lhs_v.push_back(hasVar);
830
283744
            lhs_prop.push_back(pv_prop);
831
          }
832
          else
833
          {
834
16
            Trace("cegqi-inst-debug2")
835
8
                << "... term " << n << " is ineligible after substitution."
836
8
                << std::endl;
837
          }
838
        }
839
        else
840
        {
841
279174
          Trace("cegqi-inst-debug2")
842
139587
              << "... term " << n << " is ineligible." << std::endl;
843
        }
844
      }
845
    }
846
  }
847
  //[3] directly look at assertions
848
12519
  if (!vinst->hasProcessAssertion(this, sf, pv, d_effort))
849
  {
850
2970
    return false;
851
  }
852
9549
  Trace("cegqi-inst-debug") << "[3] try based on assertions." << std::endl;
853
9549
  d_curr_iphase[pv] = CEG_INST_PHASE_ASSERTION;
854
19098
  std::unordered_set<Node, NodeHashFunction> lits;
855
28647
  for (unsigned r = 0; r < 2; r++)
856
  {
857
19098
    TheoryId tid = r == 0 ? Theory::theoryOf(pvtn) : THEORY_UF;
858
19098
    Trace("cegqi-inst-debug2") << "  look at assertions of " << tid << std::endl;
859
    std::map<TheoryId, std::vector<Node> >::iterator ita =
860
19098
        d_curr_asserts.find(tid);
861
19098
    if (ita != d_curr_asserts.end())
862
    {
863
183362
      for (const Node& lit : ita->second)
864
      {
865
169957
        if (lits.find(lit) == lits.end())
866
        {
867
161138
          lits.insert(lit);
868
322276
          Node plit;
869
322276
          if (options::cegqiRepeatLit() || !isSolvedAssertion(lit))
870
          {
871
159985
            plit = vinst->hasProcessAssertion(this, sf, pv, lit, d_effort);
872
          }
873
161138
          if (!plit.isNull())
874
          {
875
158787
            Trace("cegqi-inst-debug2") << "  look at " << lit;
876
158787
            if (plit != lit)
877
            {
878
3230
              Trace("cegqi-inst-debug2") << "...processed to : " << plit;
879
            }
880
158787
            Trace("cegqi-inst-debug2") << std::endl;
881
            // apply substitutions
882
317574
            Node slit = applySubstitutionToLiteral(plit, sf);
883
158787
            if (!slit.isNull())
884
            {
885
              // check if contains pv
886
158725
              if (hasVariable(slit, pv))
887
              {
888
21412
                Trace("cegqi-inst-debug")
889
10706
                    << "...try based on literal " << slit << "," << std::endl;
890
10706
                Trace("cegqi-inst-debug") << "...from " << lit << std::endl;
891
10706
                if (vinst->processAssertion(this, sf, pv, slit, lit, d_effort))
892
                {
893
                  return true;
894
                }
895
10706
                else if (!options::cegqiMultiInst() && hasTriedInstantiation(pv))
896
                {
897
                  return false;
898
                }
899
              }
900
            }
901
          }
902
        }
903
      }
904
    }
905
  }
906
9549
  if (vinst->processAssertions(this, sf, pv, d_effort))
907
  {
908
5660
    return true;
909
  }
910
3889
  return false;
911
}
912
913
44
void CegInstantiator::pushStackVariable( Node v ) {
914
44
  d_stack_vars.push_back( v );
915
44
}
916
917
void CegInstantiator::popStackVariable() {
918
  Assert(!d_stack_vars.empty());
919
  d_stack_vars.pop_back();
920
}
921
922
18872
bool CegInstantiator::constructInstantiationInc(Node pv,
923
                                                Node n,
924
                                                TermProperties& pv_prop,
925
                                                SolvedForm& sf,
926
                                                bool revertOnSuccess)
927
{
928
37744
  Node cnode = pv_prop.getCacheNode();
929
18872
  if( d_curr_subs_proc[pv][n].find( cnode )==d_curr_subs_proc[pv][n].end() ){
930
18868
    d_curr_subs_proc[pv][n][cnode] = true;
931
18868
    if( Trace.isOn("cegqi-inst-debug") ){
932
      for( unsigned j=0; j<sf.d_subs.size(); j++ ){
933
        Trace("cegqi-inst-debug") << " ";
934
      }
935
      Trace("cegqi-inst-debug") << sf.d_subs.size() << ": (" << d_curr_iphase[pv]
936
                         << ") ";
937
      Node mod_pv = pv_prop.getModifiedTerm( pv );
938
      Trace("cegqi-inst-debug") << mod_pv << " -> " << n << std::endl;
939
      Assert(n.getType().isSubtypeOf(pv.getType()));
940
    }
941
    //must ensure variables have been computed for n
942
18868
    computeProgVars( n );
943
18868
    Assert(d_inelig.find(n) == d_inelig.end());
944
945
    //substitute into previous substitutions, when applicable
946
37736
    std::vector< Node > a_var;
947
18868
    a_var.push_back( pv );
948
37736
    std::vector< Node > a_subs;
949
18868
    a_subs.push_back( n );
950
37736
    std::vector< TermProperties > a_prop;
951
18868
    a_prop.push_back( pv_prop );
952
37736
    std::vector< Node > a_non_basic;
953
18868
    if( !pv_prop.isBasic() ){
954
112
      a_non_basic.push_back( pv );
955
    }
956
18868
    bool success = true;
957
37736
    std::map< int, Node > prev_subs;
958
37736
    std::map< int, TermProperties > prev_prop;
959
37736
    std::map< int, Node > prev_sym_subs;
960
37736
    std::vector< Node > new_non_basic;
961
18868
    Trace("cegqi-inst-debug2") << "Applying substitutions to previous substitution terms..." << std::endl;
962
273265
    for( unsigned j=0; j<sf.d_subs.size(); j++ ){
963
254397
      Trace("cegqi-inst-debug2") << "  Apply for " << sf.d_subs[j]  << std::endl;
964
254397
      Assert(d_prog_var.find(sf.d_subs[j]) != d_prog_var.end());
965
254397
      if( d_prog_var[sf.d_subs[j]].find( pv )!=d_prog_var[sf.d_subs[j]].end() ){
966
11235
        prev_subs[j] = sf.d_subs[j];
967
22470
        TNode tv = pv;
968
22470
        TNode ts = n;
969
22470
        TermProperties a_pv_prop;
970
22470
        Node new_subs = applySubstitution( sf.d_vars[j].getType(), sf.d_subs[j], a_var, a_subs, a_prop, a_non_basic, a_pv_prop, true );
971
11235
        if( !new_subs.isNull() ){
972
11235
          sf.d_subs[j] = new_subs;
973
          // the substitution apply to this term resulted in a non-basic substitution relationship
974
11235
          if( !a_pv_prop.isBasic() ){
975
            // we are processing:
976
            //    sf.d_props[j].getModifiedTerm( sf.d_vars[j] ) = sf.d_subs[j] { pv_prop.getModifiedTerm( pv ) -> n }
977
978
            // based on the above substitution, we have:
979
            //   x = sf.d_subs[j] { pv_prop.getModifiedTerm( pv ) -> n }
980
            // is equivalent to
981
            //   a_pv_prop.getModifiedTerm( x ) = new_subs
982
983
            // thus we must compose substitutions:
984
            //   a_pv_prop.getModifiedTerm( sf.d_props[j].getModifiedTerm( sf.d_vars[j] ) ) = new_subs
985
986
2
            prev_prop[j] = sf.d_props[j];
987
2
            bool prev_basic = sf.d_props[j].isBasic();
988
989
            // now compose the property
990
2
            sf.d_props[j].composeProperty( a_pv_prop );
991
992
            // if previously was basic, becomes non-basic
993
2
            if( prev_basic && !sf.d_props[j].isBasic() ){
994
2
              Assert(std::find(sf.d_non_basic.begin(),
995
                               sf.d_non_basic.end(),
996
                               sf.d_vars[j])
997
                     == sf.d_non_basic.end());
998
2
              new_non_basic.push_back( sf.d_vars[j] );
999
2
              sf.d_non_basic.push_back( sf.d_vars[j] );
1000
            }
1001
          }
1002
11235
          if( sf.d_subs[j]!=prev_subs[j] ){
1003
11235
            computeProgVars( sf.d_subs[j] );
1004
11235
            Assert(d_inelig.find(sf.d_subs[j]) == d_inelig.end());
1005
          }
1006
11235
          Trace("cegqi-inst-debug2") << "Subs " << j << " " << sf.d_subs[j] << std::endl;
1007
        }else{
1008
          Trace("cegqi-inst-debug2") << "...failed to apply substitution to " << sf.d_subs[j] << std::endl;
1009
          success = false;
1010
          break;
1011
        }
1012
      }else{
1013
243162
        Trace("cegqi-inst-debug2") << "Skip " << j << " " << sf.d_subs[j] << std::endl;
1014
      }
1015
    }
1016
18868
    if( success ){
1017
18868
      Trace("cegqi-inst-debug2") << "Adding to vectors..." << std::endl;
1018
18868
      sf.push_back( pv, n, pv_prop );
1019
18868
      Trace("cegqi-inst-debug2") << "Recurse..." << std::endl;
1020
18868
      unsigned i = d_curr_index[pv];
1021
18868
      success = constructInstantiation(sf, d_stack_vars.empty() ? i + 1 : i);
1022
18868
      if (!success || revertOnSuccess)
1023
      {
1024
4084
        Trace("cegqi-inst-debug2") << "Removing from vectors..." << std::endl;
1025
4084
        sf.pop_back( pv, n, pv_prop );
1026
      }
1027
    }
1028
18868
    if (success && !revertOnSuccess)
1029
    {
1030
14784
      return true;
1031
    }else{
1032
4084
      Trace("cegqi-inst-debug2") << "Revert substitutions..." << std::endl;
1033
      //revert substitution information
1034
5643
      for (std::map<int, Node>::iterator it = prev_subs.begin();
1035
5643
           it != prev_subs.end();
1036
           ++it)
1037
      {
1038
1559
        sf.d_subs[it->first] = it->second;
1039
      }
1040
4084
      for (std::map<int, TermProperties>::iterator it = prev_prop.begin();
1041
4084
           it != prev_prop.end();
1042
           ++it)
1043
      {
1044
        sf.d_props[it->first] = it->second;
1045
      }
1046
4084
      for( unsigned i=0; i<new_non_basic.size(); i++ ){
1047
        sf.d_non_basic.pop_back();
1048
      }
1049
4084
      return success;
1050
    }
1051
  }else{
1052
    //already tried this substitution
1053
4
    return false;
1054
  }
1055
}
1056
1057
5019
bool CegInstantiator::doAddInstantiation( std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& lemmas ) {
1058
5019
  if (vars.size() > d_input_vars.size() || !d_var_order_index.empty())
1059
  {
1060
1399
    Trace("cegqi-inst-debug") << "Reconstructing instantiations...." << std::endl;
1061
2798
    std::map< Node, Node > subs_map;
1062
15982
    for( unsigned i=0; i<subs.size(); i++ ){
1063
14583
      subs_map[vars[i]] = subs[i];
1064
    }
1065
1399
    subs.clear();
1066
10372
    for (unsigned i = 0, size = d_input_vars.size(); i < size; ++i)
1067
    {
1068
8973
      std::map<Node, Node>::iterator it = subs_map.find(d_input_vars[i]);
1069
8973
      Assert(it != subs_map.end());
1070
17946
      Node n = it->second;
1071
17946
      Trace("cegqi-inst-debug") << "  " << d_input_vars[i] << " -> " << n
1072
8973
                               << std::endl;
1073
8973
      Assert(n.getType().isSubtypeOf(d_input_vars[i].getType()));
1074
8973
      subs.push_back( n );
1075
    }
1076
  }
1077
5019
  if (Trace.isOn("cegqi-inst"))
1078
  {
1079
    Trace("cegqi-inst") << "Ceg Instantiator produced : " << std::endl;
1080
    for (unsigned i = 0, size = d_input_vars.size(); i < size; ++i)
1081
    {
1082
      Node v = d_input_vars[i];
1083
      Trace("cegqi-inst") << i << " (" << d_curr_iphase[v] << ") : "
1084
                         << v << " -> " << subs[i] << std::endl;
1085
      Assert(subs[i].getType().isSubtypeOf(v.getType()));
1086
    }
1087
  }
1088
5019
  Trace("cegqi-inst-debug") << "Do the instantiation...." << std::endl;
1089
5019
  bool ret = d_parent->doAddInstantiation(subs);
1090
5019
  for (const Node& l : lemmas)
1091
  {
1092
    d_parent->addPendingLemma(l);
1093
  }
1094
5019
  return ret;
1095
}
1096
1097
55119
bool CegInstantiator::isEligibleForInstantiation(Node n) const
1098
{
1099
55119
  if (n.getKind() != INST_CONSTANT && n.getKind() != SKOLEM)
1100
  {
1101
51684
    return true;
1102
  }
1103
3435
  if (n.getAttribute(VirtualTermSkolemAttribute()))
1104
  {
1105
    // virtual terms are allowed
1106
66
    return true;
1107
  }
1108
  // only legal if current quantified formula contains n
1109
3369
  return expr::hasSubterm(d_quant, n);
1110
}
1111
1112
418070
bool CegInstantiator::canApplyBasicSubstitution( Node n, std::vector< Node >& non_basic ){
1113
418070
  Assert(d_prog_var.find(n) != d_prog_var.end());
1114
418070
  if( !non_basic.empty() ){
1115
2663
    for (std::unordered_set<Node, NodeHashFunction>::iterator it =
1116
2059
             d_prog_var[n].begin();
1117
4722
         it != d_prog_var[n].end();
1118
         ++it)
1119
    {
1120
3108
      if (std::find(non_basic.begin(), non_basic.end(), *it) != non_basic.end())
1121
      {
1122
445
        return false;
1123
      }
1124
    }
1125
  }
1126
417625
  return true;
1127
}
1128
1129
259283
Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< TermProperties >& prop,
1130
                                         std::vector< Node >& non_basic, TermProperties& pv_prop, bool try_coeff ) {
1131
259283
  n = Rewriter::rewrite(n);
1132
259283
  computeProgVars( n );
1133
259283
  bool is_basic = canApplyBasicSubstitution( n, non_basic );
1134
259283
  if( Trace.isOn("sygus-si-apply-subs-debug") ){
1135
    Trace("sygus-si-apply-subs-debug") << "is_basic = " << is_basic << "  " << tn << std::endl;
1136
    for( unsigned i=0; i<subs.size(); i++ ){
1137
      Trace("sygus-si-apply-subs-debug") << "  " << vars[i] << " -> " << subs[i] << "   types : " << vars[i].getType() << " -> " << subs[i].getType() << std::endl;
1138
      Assert(subs[i].getType().isSubtypeOf(vars[i].getType()));
1139
    }
1140
  }
1141
259283
  Node nret;
1142
259283
  if( is_basic ){
1143
259002
    nret = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
1144
  }else{
1145
281
    if( !tn.isInteger() ){
1146
      //can do basic substitution instead with divisions
1147
216
      std::vector< Node > nvars;
1148
216
      std::vector< Node > nsubs;
1149
704
      for( unsigned i=0; i<vars.size(); i++ ){
1150
596
        if( !prop[i].d_coeff.isNull() ){
1151
148
          Assert(vars[i].getType().isInteger());
1152
148
          Assert(prop[i].d_coeff.isConst());
1153
296
          Node nn = NodeManager::currentNM()->mkNode( MULT, subs[i], NodeManager::currentNM()->mkConst( Rational(1)/prop[i].d_coeff.getConst<Rational>() ) );
1154
148
          nn = NodeManager::currentNM()->mkNode( kind::TO_INTEGER, nn );
1155
148
          nn =  Rewriter::rewrite( nn );
1156
148
          nsubs.push_back( nn );
1157
        }else{
1158
448
          nsubs.push_back( subs[i] );
1159
        }
1160
      }
1161
108
      nret = n.substitute( vars.begin(), vars.end(), nsubs.begin(), nsubs.end() );
1162
173
    }else if( try_coeff ){
1163
      //must convert to monomial representation
1164
346
      std::map< Node, Node > msum;
1165
173
      if (ArithMSum::getMonomialSum(n, msum))
1166
      {
1167
346
        std::map< Node, Node > msum_coeff;
1168
346
        std::map< Node, Node > msum_term;
1169
1267
        for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
1170
          //check if in substitution
1171
1094
          std::vector< Node >::iterator its = std::find( vars.begin(), vars.end(), it->first );
1172
1094
          if( its!=vars.end() ){
1173
472
            int index = its-vars.begin();
1174
472
            if( prop[index].d_coeff.isNull() ){
1175
              //apply substitution
1176
307
              msum_term[it->first] = subs[index];
1177
            }else{
1178
              //apply substitution, multiply to ensure no divisibility conflict
1179
165
              msum_term[it->first] = subs[index];
1180
              //relative coefficient
1181
165
              msum_coeff[it->first] = prop[index].d_coeff;
1182
165
              if( pv_prop.d_coeff.isNull() ){
1183
165
                pv_prop.d_coeff = prop[index].d_coeff;
1184
              }else{
1185
                pv_prop.d_coeff = NodeManager::currentNM()->mkNode( MULT, pv_prop.d_coeff, prop[index].d_coeff );
1186
              }
1187
            }
1188
          }else{
1189
622
            msum_term[it->first] = it->first;
1190
          }
1191
        }
1192
        //make sum with normalized coefficient
1193
173
        if( !pv_prop.d_coeff.isNull() ){
1194
165
          pv_prop.d_coeff = Rewriter::rewrite( pv_prop.d_coeff );
1195
165
          Trace("sygus-si-apply-subs-debug") << "Combined coeff : " << pv_prop.d_coeff << std::endl;
1196
330
          std::vector< Node > children;
1197
1243
          for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
1198
2156
            Node c_coeff;
1199
1078
            if( !msum_coeff[it->first].isNull() ){
1200
165
              c_coeff = Rewriter::rewrite( NodeManager::currentNM()->mkConst( pv_prop.d_coeff.getConst<Rational>() / msum_coeff[it->first].getConst<Rational>() ) );
1201
            }else{
1202
913
              c_coeff = pv_prop.d_coeff;
1203
            }
1204
1078
            if( !it->second.isNull() ){
1205
955
              c_coeff = NodeManager::currentNM()->mkNode( MULT, c_coeff, it->second );
1206
            }
1207
1078
            Assert(!c_coeff.isNull());
1208
2156
            Node c;
1209
1078
            if( msum_term[it->first].isNull() ){
1210
36
              c = c_coeff;
1211
            }else{
1212
1042
              c = NodeManager::currentNM()->mkNode( MULT, c_coeff, msum_term[it->first] );
1213
            }
1214
1078
            children.push_back( c );
1215
1078
            Trace("sygus-si-apply-subs-debug") << "Add child : " << c << std::endl;
1216
          }
1217
330
          Node nretc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( PLUS, children );
1218
165
          nretc = Rewriter::rewrite( nretc );
1219
          //ensure that nret does not contain vars
1220
165
          if (!expr::hasSubterm(nretc, vars))
1221
          {
1222
            //result is ( nret / pv_prop.d_coeff )
1223
165
            nret = nretc;
1224
          }else{
1225
            Trace("sygus-si-apply-subs-debug") << "Failed, since result " << nretc << " contains free variable." << std::endl;
1226
          }
1227
        }else{
1228
          //implies that we have a monomial that has a free variable
1229
8
          Trace("sygus-si-apply-subs-debug") << "Failed to find coefficient during substitution, implies monomial with free variable." << std::endl;
1230
        }
1231
      }else{
1232
        Trace("sygus-si-apply-subs-debug") << "Failed to find monomial sum " << n << std::endl;
1233
      }
1234
    }
1235
  }
1236
259283
  if( n!=nret && !nret.isNull() ){
1237
132326
    nret = Rewriter::rewrite( nret );
1238
  }
1239
259283
  return nret;
1240
}
1241
1242
158787
Node CegInstantiator::applySubstitutionToLiteral( Node lit, std::vector< Node >& vars, std::vector< Node >& subs,
1243
                                                  std::vector< TermProperties >& prop, std::vector< Node >& non_basic ) {
1244
158787
  computeProgVars( lit );
1245
158787
  bool is_basic = canApplyBasicSubstitution( lit, non_basic );
1246
158787
  Node lret;
1247
158787
  if( is_basic ){
1248
158623
   lret = lit.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
1249
  }else{
1250
328
    Node atom = lit.getKind()==NOT ? lit[0] : lit;
1251
164
    bool pol = lit.getKind()!=NOT;
1252
    //arithmetic inequalities and disequalities
1253
164
    if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && atom[0].getType().isReal() ) ){
1254
102
      NodeManager* nm = NodeManager::currentNM();
1255
102
      Assert(atom.getKind() != GEQ || atom[1].isConst());
1256
204
      Node atom_lhs;
1257
204
      Node atom_rhs;
1258
102
      if( atom.getKind()==GEQ ){
1259
80
        atom_lhs = atom[0];
1260
80
        atom_rhs = atom[1];
1261
      }else{
1262
22
        atom_lhs = nm->mkNode(MINUS, atom[0], atom[1]);
1263
22
        atom_lhs = Rewriter::rewrite( atom_lhs );
1264
22
        atom_rhs = nm->mkConst(Rational(0));
1265
      }
1266
      //must be an eligible term
1267
102
      if( isEligible( atom_lhs ) ){
1268
        //apply substitution to LHS of atom
1269
204
        TermProperties atom_lhs_prop;
1270
102
        atom_lhs = applySubstitution(nm->realType(),
1271
                                     atom_lhs,
1272
                                     vars,
1273
                                     subs,
1274
                                     prop,
1275
                                     non_basic,
1276
                                     atom_lhs_prop);
1277
102
        if( !atom_lhs.isNull() ){
1278
102
          if( !atom_lhs_prop.d_coeff.isNull() ){
1279
            atom_rhs = nm->mkNode(MULT, atom_lhs_prop.d_coeff, atom_rhs);
1280
            atom_rhs = Rewriter::rewrite(atom_rhs);
1281
          }
1282
102
          lret = nm->mkNode(atom.getKind(), atom_lhs, atom_rhs);
1283
102
          if( !pol ){
1284
82
            lret = lret.negate();
1285
          }
1286
        }
1287
      }
1288
    }else{
1289
      // don't know how to apply substitution to literal
1290
    }
1291
  }
1292
158787
  if( lit!=lret && !lret.isNull() ){
1293
90604
    lret = Rewriter::rewrite( lret );
1294
  }
1295
158787
  return lret;
1296
}
1297
1298
3985
bool CegInstantiator::check() {
1299
3985
  processAssertions();
1300
5405
  for( unsigned r=0; r<2; r++ ){
1301
5113
    d_effort = r == 0 ? CEG_INST_EFFORT_STANDARD : CEG_INST_EFFORT_FULL;
1302
6533
    SolvedForm sf;
1303
5113
    d_stack_vars.clear();
1304
5113
    d_bound_var_index.clear();
1305
5113
    d_solved_asserts.clear();
1306
    //try to add an instantiation
1307
5113
    if (constructInstantiation(sf, 0))
1308
    {
1309
3693
      return true;
1310
    }
1311
  }
1312
292
  Trace("cegqi-engine") << "  WARNING : unable to find CEGQI single invocation instantiation." << std::endl;
1313
292
  return false;
1314
}
1315
1316
3985
void CegInstantiator::processAssertions() {
1317
7970
  Trace("cegqi-proc") << "--- Process assertions, #var = " << d_vars.size()
1318
3985
                     << std::endl;
1319
3985
  d_curr_asserts.clear();
1320
3985
  d_curr_eqc.clear();
1321
3985
  d_curr_type_eqc.clear();
1322
1323
  // must use master equality engine to avoid value instantiations
1324
3985
  eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine();
1325
1326
  //for each variable
1327
20299
  for( unsigned i=0; i<d_vars.size(); i++ ){
1328
32628
    Node pv = d_vars[i];
1329
32628
    TypeNode pvtn = pv.getType();
1330
16314
    Trace("cegqi-proc-debug") << "Collect theory ids from type " << pvtn << " of " << pv << std::endl;
1331
    //collect information about eqc
1332
16314
    if( ee->hasTerm( pv ) ){
1333
23540
      Node pvr = ee->getRepresentative( pv );
1334
11770
      if( d_curr_eqc.find( pvr )==d_curr_eqc.end() ){
1335
7855
        Trace("cegqi-proc") << "Collect equivalence class " << pvr << std::endl;
1336
7855
        eq::EqClassIterator eqc_i = eq::EqClassIterator( pvr, ee );
1337
37657
        while( !eqc_i.isFinished() ){
1338
14901
          d_curr_eqc[pvr].push_back( *eqc_i );
1339
14901
          ++eqc_i;
1340
        }
1341
      }
1342
    }
1343
  }
1344
  //collect assertions for relevant theories
1345
3985
  const LogicInfo& logicInfo = d_qstate.getLogicInfo();
1346
12148
  for (TheoryId tid : d_tids)
1347
  {
1348
8163
    if (!logicInfo.isTheoryEnabled(tid))
1349
    {
1350
1637
      continue;
1351
    }
1352
13052
    Trace("cegqi-proc") << "Collect assertions from theory " << tid
1353
6526
                        << std::endl;
1354
6526
    d_curr_asserts[tid].clear();
1355
    // collect all assertions from theory
1356
278393
    for (context::CDList<Assertion>::const_iterator
1357
6526
             it = d_qstate.factsBegin(tid),
1358
6526
             itEnd = d_qstate.factsEnd(tid);
1359
284919
         it != itEnd;
1360
         ++it)
1361
    {
1362
556786
      Node lit = (*it).d_assertion;
1363
556786
      Node atom = lit.getKind() == NOT ? lit[0] : lit;
1364
556786
      if (d_is_nested_quant
1365
823495
          || std::find(d_ce_atoms.begin(), d_ce_atoms.end(), atom)
1366
823495
                 != d_ce_atoms.end())
1367
      {
1368
22422
        d_curr_asserts[tid].push_back(lit);
1369
22422
        Trace("cegqi-proc-debug") << "...add : " << lit << std::endl;
1370
      }
1371
      else
1372
      {
1373
511942
        Trace("cegqi-proc")
1374
255971
            << "...do not consider literal " << tid << " : " << lit
1375
255971
            << " since it is not part of CE body." << std::endl;
1376
      }
1377
    }
1378
  }
1379
  //collect equivalence classes that correspond to relevant theories
1380
3985
  Trace("cegqi-proc-debug") << "...collect typed equivalence classes" << std::endl;
1381
3985
  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
1382
778491
  while( !eqcs_i.isFinished() ){
1383
774506
    Node r = *eqcs_i;
1384
774506
    TypeNode rtn = r.getType();
1385
387253
    TheoryId tid = Theory::theoryOf( rtn );
1386
    //if we care about the theory of this eqc
1387
387253
    if( std::find( d_tids.begin(), d_tids.end(), tid )!=d_tids.end() ){
1388
308568
      if( rtn.isInteger() || rtn.isReal() ){
1389
15646
        rtn = rtn.getBaseType();
1390
      }
1391
308568
      Trace("cegqi-proc-debug") << "...type eqc: " << r << std::endl;
1392
308568
      d_curr_type_eqc[rtn].push_back( r );
1393
308568
      if( d_curr_eqc.find( r )==d_curr_eqc.end() ){
1394
300713
        Trace("cegqi-proc") << "Collect equivalence class " << r << std::endl;
1395
300713
        Trace("cegqi-proc-debug") << "  ";
1396
300713
        eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
1397
966517
        while( !eqc_i.isFinished() ){
1398
332902
          Trace("cegqi-proc-debug") << *eqc_i << " ";
1399
332902
          d_curr_eqc[r].push_back( *eqc_i );
1400
332902
          ++eqc_i;
1401
        }
1402
300713
        Trace("cegqi-proc-debug") << std::endl;
1403
      }
1404
    }
1405
387253
    ++eqcs_i;
1406
  }
1407
1408
  //remove unecessary assertions
1409
10511
  for( std::map< TheoryId, std::vector< Node > >::iterator it = d_curr_asserts.begin(); it != d_curr_asserts.end(); ++it ){
1410
13052
    std::vector< Node > akeep;
1411
28948
    for( unsigned i=0; i<it->second.size(); i++ ){
1412
44844
      Node n = it->second[i];
1413
      //must be an eligible term
1414
22422
      if( isEligible( n ) ){
1415
        //must contain at least one variable
1416
17243
        if( !d_prog_var[n].empty() ){
1417
15249
          Trace("cegqi-proc") << "...literal[" << it->first << "] : " << n << std::endl;
1418
15249
          akeep.push_back( n );
1419
        }else{
1420
1994
          Trace("cegqi-proc") << "...remove literal from " << it->first << " : " << n << " since it contains no relevant variables." << std::endl;
1421
        }
1422
      }else{
1423
5179
        Trace("cegqi-proc") << "...remove literal from " << it->first << " : " << n << " since it contains ineligible terms." << std::endl;
1424
      }
1425
    }
1426
6526
    it->second.clear();
1427
6526
    it->second.insert( it->second.end(), akeep.begin(), akeep.end() );
1428
  }
1429
1430
  //remove duplicate terms from eqc
1431
312553
  for( std::map< Node, std::vector< Node > >::iterator it = d_curr_eqc.begin(); it != d_curr_eqc.end(); ++it ){
1432
617136
    std::vector< Node > new_eqc;
1433
656371
    for( unsigned i=0; i<it->second.size(); i++ ){
1434
347803
      if( std::find( new_eqc.begin(), new_eqc.end(), it->second[i] )==new_eqc.end() ){
1435
347803
        new_eqc.push_back( it->second[i] );
1436
      }
1437
    }
1438
308568
    it->second.clear();
1439
308568
    it->second.insert( it->second.end(), new_eqc.begin(), new_eqc.end() );
1440
  }
1441
3985
}
1442
1443
52216
Node CegInstantiator::getModelValue( Node n ) {
1444
52216
  return d_qe->getModel()->getValue( n );
1445
}
1446
1447
1224
Node CegInstantiator::getBoundVariable(TypeNode tn)
1448
{
1449
1224
  unsigned index = 0;
1450
  std::unordered_map<TypeNode, unsigned, TypeNodeHashFunction>::iterator itb =
1451
1224
      d_bound_var_index.find(tn);
1452
1224
  if (itb != d_bound_var_index.end())
1453
  {
1454
177
    index = itb->second;
1455
  }
1456
1224
  d_bound_var_index[tn] = index + 1;
1457
2232
  while (index >= d_bound_var[tn].size())
1458
  {
1459
1008
    std::stringstream ss;
1460
504
    ss << "x" << index;
1461
1008
    Node x = NodeManager::currentNM()->mkBoundVar(ss.str(), tn);
1462
504
    d_bound_var[tn].push_back(x);
1463
  }
1464
1224
  return d_bound_var[tn][index];
1465
}
1466
1467
162719
bool CegInstantiator::isSolvedAssertion(Node n) const
1468
{
1469
162719
  return d_solved_asserts.find(n) != d_solved_asserts.end();
1470
}
1471
1472
3162
void CegInstantiator::markSolved(Node n, bool solved)
1473
{
1474
3162
  if (solved)
1475
  {
1476
1581
    d_solved_asserts.insert(n);
1477
  }
1478
1581
  else if (isSolvedAssertion(n))
1479
  {
1480
1581
    d_solved_asserts.erase(n);
1481
  }
1482
3162
}
1483
1484
24215
void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited ) {
1485
24215
  if( n.getKind()==FORALL ){
1486
132
    d_is_nested_quant = true;
1487
24083
  }else if( visited.find( n )==visited.end() ){
1488
22096
    visited[n] = true;
1489
22096
    if( TermUtil::isBoolConnectiveTerm( n ) ){
1490
33838
      for( unsigned i=0; i<n.getNumChildren(); i++ ){
1491
22346
        collectCeAtoms( n[i], visited );
1492
      }
1493
    }else{
1494
10604
      if( std::find( d_ce_atoms.begin(), d_ce_atoms.end(), n )==d_ce_atoms.end() ){
1495
10604
        Trace("cegqi-ce-atoms") << "CE atoms : " << n << std::endl;
1496
10604
        d_ce_atoms.push_back( n );
1497
      }
1498
    }
1499
  }
1500
24215
}
1501
1502
1731
void CegInstantiator::registerCounterexampleLemma(Node lem,
1503
                                                  std::vector<Node>& ceVars,
1504
                                                  std::vector<Node>& auxLems)
1505
{
1506
1731
  Trace("cegqi-reg") << "Register counterexample lemma..." << std::endl;
1507
1731
  d_input_vars.clear();
1508
1731
  d_input_vars.insert(d_input_vars.end(), ceVars.begin(), ceVars.end());
1509
1510
  //Assert( d_vars.empty() );
1511
1731
  d_vars.clear();
1512
1731
  registerTheoryId(THEORY_UF);
1513
5165
  for (const Node& cv : ceVars)
1514
  {
1515
3434
    Trace("cegqi-reg") << "  register input variable : " << cv << std::endl;
1516
3434
    registerVariable(cv);
1517
  }
1518
1519
  // preprocess with all relevant instantiator preprocessors
1520
3462
  Trace("cegqi-debug") << "Preprocess based on theory-specific methods..."
1521
1731
                      << std::endl;
1522
3462
  std::vector<Node> pvars;
1523
1731
  pvars.insert(pvars.end(), d_vars.begin(), d_vars.end());
1524
2445
  for (std::pair<const TheoryId, InstantiatorPreprocess*>& p : d_tipp)
1525
  {
1526
714
    p.second->registerCounterexampleLemma(lem, pvars, auxLems);
1527
  }
1528
  // must register variables generated by preprocessors
1529
3462
  Trace("cegqi-debug") << "Register variables from theory-specific methods "
1530
3462
                      << d_input_vars.size() << " " << pvars.size() << " ..."
1531
1731
                      << std::endl;
1532
2009
  for (unsigned i = d_input_vars.size(), size = pvars.size(); i < size; ++i)
1533
  {
1534
556
    Trace("cegqi-reg") << "  register inst preprocess variable : " << pvars[i]
1535
278
                       << std::endl;
1536
278
    registerVariable(pvars[i]);
1537
  }
1538
1539
  // register variables that were introduced during TheoryEngine preprocessing
1540
3462
  std::unordered_set<Node, NodeHashFunction> ceSyms;
1541
1731
  expr::getSymbols(lem, ceSyms);
1542
3462
  std::unordered_set<Node, NodeHashFunction> qSyms;
1543
1731
  expr::getSymbols(d_quant, qSyms);
1544
  // all variables that are in counterexample lemma but not in quantified
1545
  // formula
1546
10855
  for (const Node& ces : ceSyms)
1547
  {
1548
9124
    if (qSyms.find(ces) != qSyms.end())
1549
    {
1550
      // a free symbol of the quantified formula.
1551
11096
      continue;
1552
    }
1553
6231
    if (std::find(d_vars.begin(), d_vars.end(), ces) != d_vars.end())
1554
    {
1555
      // already processed variable
1556
3409
      continue;
1557
    }
1558
    // must avoid selector symbols, and function skolems introduced by
1559
    // theory preprocessing
1560
3743
    TypeNode ct = ces.getType();
1561
2822
    if (ct.isBoolean() || ct.isFunctionLike())
1562
    {
1563
      // Boolean variables, including the counterexample literal, don't matter
1564
      // since they are always assigned a model value.
1565
1901
      continue;
1566
    }
1567
1842
    Trace("cegqi-reg") << "  register theory preprocess variable : " << ces
1568
921
                       << std::endl;
1569
    // register the variable, which was introduced by TheoryEngine's preprocess
1570
    // method, e.g. an ITE skolem.
1571
921
    registerVariable(ces);
1572
  }
1573
1574
  // determine variable order: must do Reals before Ints
1575
1731
  Trace("cegqi-debug") << "Determine variable order..." << std::endl;
1576
1731
  if (!d_vars.empty())
1577
  {
1578
3462
    std::map<Node, unsigned> voo;
1579
1731
    bool doSort = false;
1580
3462
    std::vector<Node> vars;
1581
3462
    std::map<TypeNode, std::vector<Node> > tvars;
1582
6364
    for (unsigned i = 0, size = d_vars.size(); i < size; i++)
1583
    {
1584
4633
      voo[d_vars[i]] = i;
1585
4633
      d_var_order_index.push_back(0);
1586
9266
      TypeNode tn = d_vars[i].getType();
1587
4633
      if (tn.isInteger())
1588
      {
1589
2444
        doSort = true;
1590
2444
        tvars[tn].push_back(d_vars[i]);
1591
      }
1592
      else
1593
      {
1594
2189
        vars.push_back(d_vars[i]);
1595
      }
1596
    }
1597
1731
    if (doSort)
1598
    {
1599
671
      Trace("cegqi-debug") << "Sort variables based on ordering." << std::endl;
1600
1342
      for (std::pair<const TypeNode, std::vector<Node> >& vs : tvars)
1601
      {
1602
671
        vars.insert(vars.end(), vs.second.begin(), vs.second.end());
1603
      }
1604
1605
671
      Trace("cegqi-debug") << "Consider variables in this order : " << std::endl;
1606
3339
      for (unsigned i = 0; i < vars.size(); i++)
1607
      {
1608
2668
        d_var_order_index[voo[vars[i]]] = i;
1609
5336
        Trace("cegqi-debug") << "  " << vars[i] << " : " << vars[i].getType()
1610
2668
                            << ", index was : " << voo[vars[i]] << std::endl;
1611
2668
        d_vars[i] = vars[i];
1612
      }
1613
671
      Trace("cegqi-debug") << std::endl;
1614
    }
1615
    else
1616
    {
1617
1060
      d_var_order_index.clear();
1618
    }
1619
  }
1620
1621
  // collect atoms from all lemmas: we will only solve for literals coming from
1622
  // the original body
1623
1731
  d_is_nested_quant = false;
1624
3462
  std::map< Node, bool > visited;
1625
1731
  collectCeAtoms(lem, visited);
1626
1869
  for (const Node& alem : auxLems)
1627
  {
1628
138
    collectCeAtoms(alem, visited);
1629
  }
1630
1731
}
1631
1632
3087
Instantiator::Instantiator(TypeNode tn) : d_type(tn)
1633
{
1634
3087
  d_closed_enum_type = tn.isClosedEnumerable();
1635
3087
}
1636
1637
12
bool Instantiator::processEqualTerm(CegInstantiator* ci,
1638
                                    SolvedForm& sf,
1639
                                    Node pv,
1640
                                    TermProperties& pv_prop,
1641
                                    Node n,
1642
                                    CegInstEffort effort)
1643
{
1644
12
  pv_prop.d_type = CEG_TT_EQUAL;
1645
12
  return ci->constructInstantiationInc(pv, n, pv_prop, sf);
1646
}
1647
1648
} /* CVC4::theory::quantifiers namespace */
1649
} /* CVC4::theory namespace */
1650
187814
} /* CVC4 namespace */