GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/cegqi/ceg_instantiator.h Lines: 43 57 75.4 %
Date: 2021-03-23 Branches: 16 28 57.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file ceg_instantiator.h
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 counterexample-guided quantifier instantiation
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H
18
#define CVC4__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H
19
20
#include <vector>
21
22
#include "expr/node.h"
23
#include "util/statistics_registry.h"
24
25
namespace CVC4 {
26
namespace theory {
27
28
class QuantifiersEngine;
29
30
namespace quantifiers {
31
32
class Instantiator;
33
class InstantiatorPreprocess;
34
class InstStrategyCegqi;
35
class QuantifiersState;
36
37
/**
38
 * Descriptions of the types of constraints that a term was solved for in.
39
 */
40
enum CegTermType
41
{
42
  // invalid
43
  CEG_TT_INVALID,
44
  // term was the result of solving an equality
45
  CEG_TT_EQUAL,
46
  // term was the result of solving a non-strict lower bound x >= t
47
  CEG_TT_LOWER,
48
  // term was the result of solving a strict lower bound x > t
49
  CEG_TT_LOWER_STRICT,
50
  // term was the result of solving a non-strict upper bound x <= t
51
  CEG_TT_UPPER,
52
  // term was the result of solving a strict upper bound x < t
53
  CEG_TT_UPPER_STRICT,
54
};
55
/** make (non-strict term type) c a strict term type */
56
CegTermType mkStrictCTT(CegTermType c);
57
/** negate c (lower/upper bounds are swapped) */
58
CegTermType mkNegateCTT(CegTermType c);
59
/** is c a strict term type? */
60
bool isStrictCTT(CegTermType c);
61
/** is c a lower bound? */
62
bool isLowerBoundCTT(CegTermType c);
63
/** is c an upper bound? */
64
bool isUpperBoundCTT(CegTermType c);
65
66
/** Term Properties
67
 *
68
 * Stores properties for a variable to solve for in counterexample-guided
69
 * instantiation.
70
 *
71
 * For LIA, this includes the coefficient of the variable, and the bound type
72
 * for the variable.
73
 */
74
834703
class TermProperties {
75
 public:
76
338896
  TermProperties() : d_type(CEG_TT_EQUAL) {}
77
1173547
  virtual ~TermProperties() {}
78
79
  /**
80
   * Type for the solution term. For arithmetic this corresponds to bound type
81
   * of the constraint that the constraint the term was solved for in.
82
   */
83
  CegTermType d_type;
84
  // for arithmetic
85
  Node d_coeff;
86
  // get cache node
87
  // we consider terms + TermProperties that are unique up to their cache node
88
  // (see constructInstantiationInc)
89
18872
  virtual Node getCacheNode() const { return d_coeff; }
90
  // is non-basic
91
55412
  virtual bool isBasic() const { return d_coeff.isNull(); }
92
  // get modified term
93
2029
  virtual Node getModifiedTerm( Node pv ) const {
94
2029
    if( !d_coeff.isNull() ){
95
221
      return NodeManager::currentNM()->mkNode( kind::MULT, d_coeff, pv );
96
    }else{
97
1808
      return pv;
98
    }
99
  }
100
  // compose property, should be such that:
101
  //   p.getModifiedTerm( this.getModifiedTerm( x ) ) = this_updated.getModifiedTerm( x )
102
  virtual void composeProperty(TermProperties& p);
103
};
104
105
/** Solved form
106
 *  This specifies a substitution:
107
 *  { d_props[i].getModifiedTerm(d_vars[i]) -> d_subs[i] | i = 0...|d_vars| }
108
 */
109
13084
class SolvedForm {
110
public:
111
  // list of variables
112
  std::vector< Node > d_vars;
113
  // list of terms that they are substituted to
114
  std::vector< Node > d_subs;
115
  // properties for each variable
116
  std::vector< TermProperties > d_props;
117
  // the variables that have non-basic information regarding how they are substituted
118
  //   an example is for linear arithmetic, we store "substitution with coefficients".
119
  std::vector<Node> d_non_basic;
120
  // push the substitution pv_prop.getModifiedTerm(pv) -> n
121
  void push_back(Node pv, Node n, TermProperties& pv_prop);
122
  // pop the substitution pv_prop.getModifiedTerm(pv) -> n
123
  void pop_back(Node pv, Node n, TermProperties& pv_prop);
124
  // is this solved form empty?
125
1581
  bool empty() { return d_vars.empty(); }
126
public:
127
  // theta values (for LIA, see Section 4 of Reynolds/King/Kuncak FMSD 2017)
128
  std::vector< Node > d_theta;
129
  // get the current value for theta (for LIA, see Section 4 of Reynolds/King/Kuncak FMSD 2017)
130
8963
  Node getTheta() {
131
8963
    if( d_theta.empty() ){
132
8737
      return Node::null();
133
    }else{
134
226
      return d_theta[d_theta.size()-1];
135
    }
136
  }
137
};
138
139
/** instantiation effort levels
140
 *
141
 * This effort is used to stratify the construction of
142
 * instantiations for some theories that may result to
143
 * using model value instantiations.
144
 */
145
enum CegInstEffort
146
{
147
  // uninitialized
148
  CEG_INST_EFFORT_NONE,
149
  // standard effort level
150
  CEG_INST_EFFORT_STANDARD,
151
  // standard effort level, but we have used model values
152
  CEG_INST_EFFORT_STANDARD_MV,
153
  // full effort level
154
  CEG_INST_EFFORT_FULL
155
};
156
157
std::ostream& operator<<(std::ostream& os, CegInstEffort e);
158
159
/** instantiation phase for variables
160
 *
161
 * This indicates the phase in which we constructed
162
 * a substitution for individual variables.
163
 */
164
enum CegInstPhase
165
{
166
  // uninitialized
167
  CEG_INST_PHASE_NONE,
168
  // instantiation constructed during traversal of equivalence classes
169
  CEG_INST_PHASE_EQC,
170
  // instantiation constructed during solving equalities
171
  CEG_INST_PHASE_EQUAL,
172
  // instantiation constructed by looking at theory assertions
173
  CEG_INST_PHASE_ASSERTION,
174
  // instantiation constructed by querying model value
175
  CEG_INST_PHASE_MVALUE,
176
};
177
178
std::ostream& operator<<(std::ostream& os, CegInstPhase phase);
179
180
/**
181
 * The handled status of a sort/term/quantified formula, indicating whether
182
 * counterexample-guided instantiation handles it.
183
 */
184
enum CegHandledStatus
185
{
186
  // the sort/term/quantified formula is unhandled by cegqi
187
  CEG_UNHANDLED,
188
  // the sort/term/quantified formula is partially handled by cegqi
189
  CEG_PARTIALLY_HANDLED,
190
  // the sort/term/quantified formula is handled by cegqi
191
  CEG_HANDLED,
192
  // the sort/term/quantified formula is handled by cegqi, regardless of
193
  // additional factors
194
  CEG_HANDLED_UNCONDITIONAL,
195
};
196
std::ostream& operator<<(std::ostream& os, CegHandledStatus status);
197
198
/** Ceg instantiator
199
 *
200
 * This class manages counterexample-guided quantifier instantiation
201
 * for a single quantified formula.
202
 *
203
 * For details on counterexample-guided quantifier instantiation
204
 * (for linear arithmetic), see Reynolds/King/Kuncak FMSD 2017.
205
 */
206
class CegInstantiator {
207
 public:
208
  /**
209
   * The instantiator will be constructing instantiations for quantified formula
210
   * q, parent is the owner of this object.
211
   */
212
  CegInstantiator(Node q, QuantifiersState& qs, InstStrategyCegqi* parent);
213
  virtual ~CegInstantiator();
214
  /** check
215
   * This adds instantiations based on the state of d_vars in current context
216
   * on the output channel d_out of this class.
217
   */
218
  bool check();
219
  /** Register the counterexample lemma
220
   *
221
   * @param lem contains the counterexample lemma of the quantified formula we
222
   * are processing. The counterexample lemma is the formula { ~phi[e/x] } in
223
   * Figure 1 of Reynolds et al. FMSD 2017.
224
   * @param ce_vars contains the variables e. Notice these are variables of
225
   * INST_CONSTANT kind, since we do not permit bound variables in assertions.
226
   * This method may add additional variables to this vector if it decides there
227
   * are additional auxiliary variables to solve for.
228
   * @param auxLems : if this method decides that additional lemmas should be
229
   * sent on the output channel, they are added to this vector, and sent out by
230
   * the caller of this method.
231
   */
232
  void registerCounterexampleLemma(Node lem,
233
                                   std::vector<Node>& ce_vars,
234
                                   std::vector<Node>& auxLems);
235
  //------------------------------interface for instantiators
236
  /** get quantifiers engine */
237
  QuantifiersEngine* getQuantifiersEngine() { return d_qe; }
238
  /** push stack variable
239
   * This adds a new variable to solve for in the stack
240
   * of variables we are processing. This stack is only
241
   * used for datatypes, where e.g. the DtInstantiator
242
   * solving for a list x may push the stack "variables"
243
   * head(x) and tail(x).
244
   */
245
  void pushStackVariable(Node v);
246
  /** pop stack variable */
247
  void popStackVariable();
248
  /** construct instantiation increment
249
   *
250
   * Adds the substitution { pv_prop.getModifiedTerm(pv) -> n } to the current
251
   * instantiation, specified by sf.
252
   *
253
   * This function returns true if a call to
254
   * QuantifiersEngine::addInstantiation(...)
255
   * was successfully made in a recursive call.
256
   *
257
   * The solved form sf is reverted to its original state if
258
   *   this function returns false, or
259
   *   revertOnSuccess is true and this function returns true.
260
   */
261
  bool constructInstantiationInc(Node pv,
262
                                 Node n,
263
                                 TermProperties& pv_prop,
264
                                 SolvedForm& sf,
265
                                 bool revertOnSuccess = false);
266
  /** get the current model value of term n */
267
  Node getModelValue(Node n);
268
  /** get bound variable for type
269
   *
270
   * This gets the next (canonical) bound variable of
271
   * type tn. This can be used for instance when
272
   * constructing instantiations that involve witness expressions.
273
   */
274
  Node getBoundVariable(TypeNode tn);
275
  /** has this assertion been marked as solved? */
276
  bool isSolvedAssertion(Node n) const;
277
  /** marked solved */
278
  void markSolved(Node n, bool solved = true);
279
  //------------------------------end interface for instantiators
280
281
  /**
282
   * Get the number of atoms in the counterexample lemma of the quantified
283
   * formula we are processing with this class.
284
   */
285
  unsigned getNumCEAtoms() { return d_ce_atoms.size(); }
286
  /**
287
   * Get the i^th atom of the counterexample lemma of the quantified
288
   * formula we are processing with this class.
289
   */
290
  Node getCEAtom(unsigned i) { return d_ce_atoms[i]; }
291
  /** is n a term that is eligible for instantiation? */
292
  bool isEligible(Node n);
293
  /** does n have variable pv? */
294
  bool hasVariable(Node n, Node pv);
295
  /** are we processing a nested quantified formula? */
296
1805
  bool hasNestedQuantification() const { return d_is_nested_quant; }
297
  /**
298
   * Are we allowed to instantiate the current quantified formula with n? This
299
   * includes restrictions such as if n is a variable, it must occur free in
300
   * the current quantified formula.
301
   */
302
  bool isEligibleForInstantiation(Node n) const;
303
  //------------------------------------ static queries
304
  /** Is k a kind for which counterexample-guided instantiation is possible?
305
   *
306
   * If this method returns CEG_UNHANDLED, then we prohibit cegqi for terms
307
   * involving this kind. If this method returns CEG_HANDLED, our approaches
308
   * for cegqi fully handle the kind.
309
   *
310
   * This typically corresponds to kinds that correspond to operators that
311
   * have total interpretations and are a part of the signature of
312
   * satisfaction complete theories (see Reynolds et al., CAV 2015).
313
   */
314
  static CegHandledStatus isCbqiKind(Kind k);
315
  /** is cbqi term?
316
   *
317
   * This method returns whether the term is handled by cegqi techniques, i.e.
318
   * whether all subterms of n have kinds that can be handled by cegqi.
319
   */
320
  static CegHandledStatus isCbqiTerm(Node n);
321
  /** is cbqi sort?
322
   *
323
   * This method returns whether the type tn is handled by cegqi techniques.
324
   * If the result is CEG_HANDLED_UNCONDITIONAL, then this indicates that a
325
   * variable of this type is handled regardless of the formula it appears in.
326
   *
327
   * The argument qe is used if handling sort tn is conditional on the
328
   * strategies initialized in qe. For example, uninterpreted sorts are
329
   * handled if dedicated support for EPR is enabled.
330
   */
331
  static CegHandledStatus isCbqiSort(TypeNode tn,
332
                                     QuantifiersEngine* qe = nullptr);
333
  /** is cbqi quantifier prefix
334
   *
335
   * This returns the minimum value of the above method for a bound variable
336
   * in the prefix of quantified formula q.
337
   */
338
  static CegHandledStatus isCbqiQuantPrefix(Node q,
339
                                            QuantifiersEngine* qe = nullptr);
340
  /** is cbqi quantified formula
341
   *
342
   * This returns whether quantified formula q can and should be handled by
343
   * counterexample-guided instantiation. If this function returns
344
   * a status CEG_HANDLED or above, then q is fully handled by counterexample
345
   * guided quantifier instantiation and need not be processed by any other
346
   * strategy for quantifiers (e.g. E-matching). Otherwise, if this function
347
   * returns CEG_PARTIALLY_HANDLED, then it may be worthwhile to handle the
348
   * quantified formula using cegqi, however other strategies should also be
349
   * tried.
350
   */
351
  static CegHandledStatus isCbqiQuant(Node q, QuantifiersEngine* qe = nullptr);
352
  //------------------------------------ end static queries
353
 private:
354
  /** The quantified formula of this instantiator */
355
  Node d_quant;
356
  /** Reference to the quantifiers state */
357
  QuantifiersState& d_qstate;
358
  /** The parent of this instantiator */
359
  InstStrategyCegqi* d_parent;
360
  /** quantified formula associated with this instantiator */
361
  QuantifiersEngine* d_qe;
362
363
  //-------------------------------globally cached
364
  /** cache from nodes to the set of variables it contains
365
    * (from the quantified formula we are instantiating).
366
    */
367
  std::unordered_map<Node,
368
                     std::unordered_set<Node, NodeHashFunction>,
369
                     NodeHashFunction>
370
      d_prog_var;
371
  /** cache of the set of terms that we have established are
372
   * ineligible for instantiation.
373
    */
374
  std::unordered_set<Node, NodeHashFunction> d_inelig;
375
  /** ensures n is in d_prog_var and d_inelig. */
376
  void computeProgVars(Node n);
377
  //-------------------------------end globally cached
378
379
  //-------------------------------cached per round
380
  /** current assertions per theory */
381
  std::map<TheoryId, std::vector<Node> > d_curr_asserts;
382
  /** map from representatives to the terms in their equivalence class */
383
  std::map<Node, std::vector<Node> > d_curr_eqc;
384
  /** map from types to representatives of that type */
385
  std::map<TypeNode, std::vector<Node> > d_curr_type_eqc;
386
  /** solved asserts */
387
  std::unordered_set<Node, NodeHashFunction> d_solved_asserts;
388
  /** process assertions
389
   * This is called once at the beginning of check to
390
   * set up all necessary information for constructing instantiations,
391
   * such as the above data structures.
392
   */
393
  void processAssertions();
394
  /** cache bound variables for type returned
395
   * by getBoundVariable(...).
396
   */
397
  std::unordered_map<TypeNode, std::vector<Node>, TypeNodeHashFunction>
398
      d_bound_var;
399
  /** current index of bound variables for type.
400
   * The next call to getBoundVariable(...) for
401
   * type tn returns the d_bound_var_index[tn]^th
402
   * element of d_bound_var[tn], or a fresh variable
403
   * if not in bounds.
404
   */
405
  std::unordered_map<TypeNode, unsigned, TypeNodeHashFunction>
406
      d_bound_var_index;
407
  //-------------------------------end cached per round
408
409
  //-------------------------------data per theory
410
  /** relevant theory ids
411
   * A list of theory ids that contain at least one
412
   * constraint in the body of the quantified formula we
413
   * are processing.
414
   */
415
  std::vector<TheoryId> d_tids;
416
  /** map from theory ids to instantiator preprocessors */
417
  std::map<TheoryId, InstantiatorPreprocess*> d_tipp;
418
  /** registers all theory ids associated with type tn
419
   *
420
   * This recursively calls registerTheoryId for typeOf(tn') for
421
   * all parameters and datatype subfields of type tn.
422
   * visited stores the types we have already visited.
423
   */
424
  void registerTheoryIds(TypeNode tn, std::map<TypeNode, bool>& visited);
425
  /** register theory id tid
426
   *
427
   * This is called when the quantified formula we are processing
428
   * with this class involves theory tid. In this case, we will
429
   * construct instantiations based on the assertion list of this theory.
430
   */
431
  void registerTheoryId(TheoryId tid);
432
  //-------------------------------end data per theory
433
434
  //-------------------------------the variables
435
  /** the variables we are instantiating
436
   *
437
   * This is a superset of the variables for the instantiations we are
438
   * generating and sending on the output channel of this class.
439
   */
440
  std::vector<Node> d_vars;
441
  /** set form of d_vars */
442
  std::unordered_set<Node, NodeHashFunction> d_vars_set;
443
  /** index of variables reported in instantiation */
444
  std::vector<unsigned> d_var_order_index;
445
  /** number of input variables
446
   *
447
   * These are the variables, in order, for the instantiations we are generating
448
   * and sending on the output channel of this class.
449
   */
450
  std::vector<Node> d_input_vars;
451
  /** register variable */
452
  void registerVariable(Node v);
453
  //-------------------------------the variables
454
455
  //-------------------------------quantified formula info
456
  /** are we processing a nested quantified formula? */
457
  bool d_is_nested_quant;
458
  /** the atoms of the CE lemma */
459
  std::vector<Node> d_ce_atoms;
460
  /** collect atoms */
461
  void collectCeAtoms(Node n, std::map<Node, bool>& visited);
462
  //-------------------------------end quantified formula info
463
464
  //-------------------------------current state
465
  /** the current effort level of the instantiator
466
   * This indicates the effort Instantiator objects
467
   * will put into the terms they return.
468
   */
469
  CegInstEffort d_effort;
470
  /** for each variable, the instantiator used for that variable */
471
  std::map<Node, Instantiator*> d_active_instantiators;
472
  /** map from variables to the index in the prefix of the quantified
473
   * formula we are processing.
474
   */
475
  std::map<Node, unsigned> d_curr_index;
476
  /** map from variables to the phase in which we instantiated them */
477
  std::map<Node, CegInstPhase> d_curr_iphase;
478
  /** cache of current substitutions tried between activate/deactivate */
479
  std::map<Node, std::map<Node, std::map<Node, bool> > > d_curr_subs_proc;
480
  /** stack of temporary variables we are solving for,
481
   * e.g. subfields of datatypes.
482
   */
483
  std::vector<Node> d_stack_vars;
484
  /** activate instantiation variable v at index
485
   *
486
   * This is called when variable (inst constant) v is activated
487
   * for the quantified formula we are processing.
488
   * This method initializes the instantiator class for
489
   * that variable if necessary, where this class is
490
   * determined by the type of v. It also initializes
491
   * the cache of values we have tried substituting for v
492
   * (in d_curr_subs_proc), and stores its index.
493
   */
494
  void activateInstantiationVariable(Node v, unsigned index);
495
  /** deactivate instantiation variable
496
   *
497
   * This is called when variable (inst constant) v is deactivated
498
   * for the quantified formula we are processing.
499
   */
500
  void deactivateInstantiationVariable(Node v);
501
  /**
502
   * Have we tried an instantiation for v after the last call to
503
   * activateInstantiationVariable.
504
   */
505
  bool hasTriedInstantiation(Node v);
506
  //-------------------------------end current state
507
508
  //---------------------------------for applying substitutions
509
  /** can use basic substitution */
510
  bool canApplyBasicSubstitution( Node n, std::vector< Node >& non_basic );
511
  /** apply substitution
512
  * We wish to process the substitution:
513
  *   ( pv = n * sf )
514
  * where pv is a variable with type tn, and * denotes application of substitution.
515
  * The return value "ret" and pv_prop is such that the above equality is equivalent to
516
  *   ( pv_prop.getModifiedTerm(pv) = ret )
517
  */
518
247774
  Node applySubstitution( TypeNode tn, Node n, SolvedForm& sf, TermProperties& pv_prop, bool try_coeff = true ) {
519
247774
    return applySubstitution( tn, n, sf.d_vars, sf.d_subs, sf.d_props, sf.d_non_basic, pv_prop, try_coeff );
520
  }
521
  /** apply substitution, with solved form expanded to subs/prop/non_basic/vars */
522
  Node applySubstitution( TypeNode tn, Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< TermProperties >& prop,
523
                          std::vector< Node >& non_basic, TermProperties& pv_prop, bool try_coeff = true );
524
  /** apply substitution to literal lit
525
  * The return value is equivalent to ( lit * sf )
526
  * where * denotes application of substitution.
527
  */
528
160537
  Node applySubstitutionToLiteral( Node lit, SolvedForm& sf ) {
529
160537
    return applySubstitutionToLiteral( lit, sf.d_vars, sf.d_subs, sf.d_props, sf.d_non_basic );
530
  }
531
  /** apply substitution to literal lit, with solved form expanded to subs/prop/non_basic/vars */
532
  Node applySubstitutionToLiteral( Node lit, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< TermProperties >& prop,
533
                                   std::vector< Node >& non_basic );
534
  //---------------------------------end for applying substitutions
535
536
  /** map from variables to their instantiators */
537
  std::map<Node, Instantiator*> d_instantiator;
538
539
  /** construct instantiation
540
   *
541
   * This method attempts to find a term for the i^th variable in d_vars to
542
   * include in the current instantiation, given by sf.
543
   *
544
   * It returns true if a successful call to the output channel's
545
   * doAddInstantiation was made.
546
   */
547
  bool constructInstantiation(SolvedForm& sf, unsigned i);
548
  /** construct instantiation
549
   *
550
   * Helper method for the above method. This method attempts to find a term for
551
   * variable pv to include in the current instantiation, given by sf based
552
   * on equality and theory-specific instantiation techniques. The latter is
553
   * managed by the instantiator object vinst. Prior to calling this method,
554
   * the variable pv has been activated by a call to
555
   * activateInstantiationVariable.
556
   */
557
  bool constructInstantiation(SolvedForm& sf, Instantiator* vinst, Node pv);
558
  /** do add instantiation
559
   * This method is called by the above function after we finalize the
560
   * variables/substitution and auxiliary lemmas.
561
   * It returns true if a successful call to the output channel's
562
   * doAddInstantiation was made.
563
   */
564
  bool doAddInstantiation(std::vector<Node>& vars,
565
                          std::vector<Node>& subs,
566
                          std::vector<Node>& lemmas);
567
568
  //------------------------------------ static queries
569
  /** is cbqi sort
570
   *
571
   * Helper function for isCbqiSort. This function recurses over the structure
572
   * of the type tn, where visited stores the types we have visited.
573
   */
574
  static CegHandledStatus isCbqiSort(
575
      TypeNode tn,
576
      std::map<TypeNode, CegHandledStatus>& visited,
577
      QuantifiersEngine* qe);
578
  //------------------------------------ end  static queries
579
};
580
581
/** Instantiator class
582
 *
583
 * This is a virtual class that is used for methods for constructing
584
 * substitutions for individual variables in counterexample-guided
585
 * instantiation techniques.
586
 *
587
 * This class contains a set of interface functions below, which are called
588
 * based on a fixed instantiation method implemented by CegInstantiator.
589
 * In these calls, the Instantiator in turn makes calls to methods in
590
 * CegInstanatior (primarily constructInstantiationInc).
591
 */
592
class Instantiator {
593
public:
594
 Instantiator(TypeNode tn);
595
3099
 virtual ~Instantiator() {}
596
 /** reset
597
  * This is called once, prior to any of the below methods are called.
598
  * This function sets up any initial information necessary for constructing
599
  * instantiations for pv based on the current context.
600
  */
601
2391
 virtual void reset(CegInstantiator* ci,
602
                    SolvedForm& sf,
603
                    Node pv,
604
                    CegInstEffort effort)
605
 {
606
2391
 }
607
608
  /** has process equal term
609
   *
610
   * Whether this instantiator implements processEqualTerm and
611
   * processEqualTerms.
612
   */
613
17765
  virtual bool hasProcessEqualTerm(CegInstantiator* ci,
614
                                   SolvedForm& sf,
615
                                   Node pv,
616
                                   CegInstEffort effort)
617
  {
618
17765
    return false;
619
  }
620
  /** process equal term
621
   *
622
   * This method is called when the entailment:
623
   *   E |= pv_prop.getModifiedTerm(pv) = n
624
   * holds in the current context E, and n is eligible for instantiation.
625
   *
626
   * Returns true if an instantiation was successfully added via a call to
627
   * CegInstantiator::constructInstantiationInc.
628
   */
629
  virtual bool processEqualTerm(CegInstantiator* ci,
630
                                SolvedForm& sf,
631
                                Node pv,
632
                                TermProperties& pv_prop,
633
                                Node n,
634
                                CegInstEffort effort);
635
  /** process equal terms
636
   *
637
   * This method is called after process equal term, where eqc is the list of
638
   * eligible terms in the equivalence class of pv.
639
   *
640
   * Returns true if an instantiation was successfully added via a call to
641
   * CegInstantiator::constructInstantiationInc.
642
   */
643
  virtual bool processEqualTerms(CegInstantiator* ci,
644
                                 SolvedForm& sf,
645
                                 Node pv,
646
                                 std::vector<Node>& eqc,
647
                                 CegInstEffort effort)
648
  {
649
    return false;
650
  }
651
652
  /** whether the instantiator implements processEquality */
653
5957
  virtual bool hasProcessEquality(CegInstantiator* ci,
654
                                  SolvedForm& sf,
655
                                  Node pv,
656
                                  CegInstEffort effort)
657
  {
658
5957
    return false;
659
  }
660
  /** process equality
661
   *  The input is such that term_props.size() = terms.size() = 2
662
   *  This method is called when the entailment:
663
   *    E ^ term_props[0].getModifiedTerm(x0) =
664
   *    terms[0] ^ term_props[1].getModifiedTerm(x1) = terms[1] |= x0 = x1
665
   *  holds in current context E for fresh variables xi, terms[i] are eligible,
666
   *  and at least one terms[i] contains pv for i = 0,1.
667
   *  Notice in the basic case, E |= terms[0] = terms[1].
668
   *
669
   *  Returns true if an instantiation was successfully added via a call to
670
   *  CegInstantiator::constructInstantiationInc.
671
   */
672
  virtual bool processEquality(CegInstantiator* ci,
673
                               SolvedForm& sf,
674
                               Node pv,
675
                               std::vector<TermProperties>& term_props,
676
                               std::vector<Node>& terms,
677
                               CegInstEffort effort)
678
  {
679
    return false;
680
  }
681
682
  /** whether the instantiator implements processAssertion for any literal */
683
2255
  virtual bool hasProcessAssertion(CegInstantiator* ci,
684
                                   SolvedForm& sf,
685
                                   Node pv,
686
                                   CegInstEffort effort)
687
  {
688
2255
    return false;
689
  }
690
  /** has process assertion
691
  *
692
  * This method is called when the entailment:
693
  *   E |= lit
694
  * holds in current context E. Typically, lit belongs to the list of current
695
  * assertions.
696
  *
697
  * This method is used to determine whether the instantiator implements
698
  * processAssertion for literal lit.
699
  *   If this method returns null, then this intantiator does not handle the
700
  *   literal lit. Otherwise, this method returns a literal lit' such that:
701
  *   (1) lit' is true in the current model,
702
  *   (2) lit' implies lit.
703
  *   where typically lit' = lit.
704
  */
705
  virtual Node hasProcessAssertion(CegInstantiator* ci,
706
                                   SolvedForm& sf,
707
                                   Node pv,
708
                                   Node lit,
709
                                   CegInstEffort effort)
710
  {
711
    return Node::null();
712
  }
713
  /** process assertion
714
   * This method processes the assertion slit for variable pv.
715
   * lit : the substituted form (under sf) of a literal returned by
716
   *       hasProcessAssertion
717
   * alit : the asserted literal, given as input to hasProcessAssertion
718
   *
719
   *  Returns true if an instantiation was successfully added via a call to
720
   *  CegInstantiator::constructInstantiationInc.
721
   */
722
  virtual bool processAssertion(CegInstantiator* ci,
723
                                SolvedForm& sf,
724
                                Node pv,
725
                                Node lit,
726
                                Node alit,
727
                                CegInstEffort effort)
728
  {
729
    return false;
730
  }
731
  /** process assertions
732
   *
733
   * Called after processAssertion is called for each literal asserted to the
734
   * instantiator.
735
   *
736
   * Returns true if an instantiation was successfully added via a call to
737
   * CegInstantiator::constructInstantiationInc.
738
   */
739
  virtual bool processAssertions(CegInstantiator* ci,
740
                                 SolvedForm& sf,
741
                                 Node pv,
742
                                 CegInstEffort effort)
743
  {
744
    return false;
745
  }
746
747
  /** do we use the model value as instantiation for pv?
748
   * This method returns true if we use model value instantiations
749
   * at the same effort level as those determined by this instantiator.
750
   */
751
1400
  virtual bool useModelValue(CegInstantiator* ci,
752
                             SolvedForm& sf,
753
                             Node pv,
754
                             CegInstEffort effort)
755
  {
756
1400
    return effort > CEG_INST_EFFORT_STANDARD;
757
  }
758
  /** do we allow the model value as instantiation for pv? */
759
6071
  virtual bool allowModelValue(CegInstantiator* ci,
760
                               SolvedForm& sf,
761
                               Node pv,
762
                               CegInstEffort effort)
763
  {
764
6071
    return d_closed_enum_type;
765
  }
766
767
  /** do we need to postprocess the solved form for pv? */
768
6627
  virtual bool needsPostProcessInstantiationForVariable(CegInstantiator* ci,
769
                                                        SolvedForm& sf,
770
                                                        Node pv,
771
                                                        CegInstEffort effort)
772
  {
773
6627
    return false;
774
  }
775
  /** postprocess the solved form for pv
776
   *
777
   * This method returns true if we successfully postprocessed the solved form.
778
   * lemmas is a set of lemmas we wish to return along with the instantiation.
779
   */
780
  virtual bool postProcessInstantiationForVariable(CegInstantiator* ci,
781
                                                   SolvedForm& sf,
782
                                                   Node pv,
783
                                                   CegInstEffort effort,
784
                                                   std::vector<Node>& lemmas)
785
  {
786
    return true;
787
  }
788
789
  /** Identify this module (for debugging) */
790
148
  virtual std::string identify() const { return "Default"; }
791
 protected:
792
  /** the type of the variable we are instantiating */
793
  TypeNode d_type;
794
  /** whether d_type is a closed enumerable type */
795
  bool d_closed_enum_type;
796
};
797
798
class ModelValueInstantiator : public Instantiator {
799
public:
800
179
 ModelValueInstantiator(TypeNode tn) : Instantiator(tn) {}
801
358
 virtual ~ModelValueInstantiator() {}
802
2099
 bool useModelValue(CegInstantiator* ci,
803
                    SolvedForm& sf,
804
                    Node pv,
805
                    CegInstEffort effort) override
806
 {
807
2099
   return true;
808
 }
809
2099
  std::string identify() const override { return "ModelValue"; }
810
};
811
812
/** instantiator preprocess
813
 *
814
 * This class implements techniques for preprocessing the counterexample lemma
815
 * generated for counterexample-guided quantifier instantiation.
816
 */
817
class InstantiatorPreprocess
818
{
819
 public:
820
718
  InstantiatorPreprocess() {}
821
718
  virtual ~InstantiatorPreprocess() {}
822
  /** register counterexample lemma
823
   * This implements theory-specific preprocessing and registration
824
   * of counterexample lemmas, with the same contract as
825
   * CegInstantiation::registerCounterexampleLemma.
826
   */
827
  virtual void registerCounterexampleLemma(Node lem,
828
                                           std::vector<Node>& ceVars,
829
                                           std::vector<Node>& auxLems)
830
  {
831
  }
832
};
833
834
} /* CVC4::theory::quantifiers namespace */
835
} /* CVC4::theory namespace */
836
} /* CVC4 namespace */
837
838
#endif