GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/ematching/candidate_generator.h Lines: 11 11 100.0 %
Date: 2021-03-23 Branches: 1 2 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file candidate_generator.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tim King, Morgan Deters
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 Theory uf candidate generator
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H
18
#define CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H
19
20
#include "theory/theory.h"
21
#include "theory/uf/equality_engine.h"
22
23
namespace CVC4 {
24
namespace theory {
25
26
class QuantifiersEngine;
27
28
namespace inst {
29
30
/** Candidate generator
31
 *
32
 * This is the base class for generating a stream of candidate terms for
33
 * E-matching. Depending on the kind of trigger we are processing and its
34
 * overall context, we are interested in several different criteria for
35
 * terms. This includes:
36
 * - Generating a stream of all ground terms with a given operator,
37
 * - Generating a stream of all ground terms with a given operator in a
38
 * particular equivalence class,
39
 * - Generating a stream of all terms of a particular type,
40
 * - Generating all terms that are disequal from a fixed ground term,
41
 * and so on.
42
 *
43
 * A typical use case of an instance cg of this class is the following. Given
44
 * an equivalence class representative eqc:
45
 *
46
 *  cg->reset( eqc );
47
 *  do{
48
 *    Node cand = cg->getNextCandidate();
49
 *    ; ...if non-null, cand is a candidate...
50
 *  }while( !cand.isNull() );
51
 *
52
 */
53
class CandidateGenerator {
54
protected:
55
  QuantifiersEngine* d_qe;
56
public:
57
32673
  CandidateGenerator( QuantifiersEngine* qe ) : d_qe( qe ){}
58
32673
  virtual ~CandidateGenerator(){}
59
  /** reset instantiation round
60
   *
61
   * This is called at the beginning of each instantiation round.
62
   */
63
214077
  virtual void resetInstantiationRound() {}
64
  /** reset for equivalence class eqc
65
   *
66
   * This indicates that this class should generate a stream of candidate terms
67
   * based on its criteria that occur in the equivalence class of eqc, or
68
   * any equivalence class if eqc is null.
69
   */
70
  virtual void reset( Node eqc ) = 0;
71
  /** get the next candidate */
72
  virtual Node getNextCandidate() = 0;
73
public:
74
 /** is n a legal candidate? */
75
 bool isLegalCandidate(Node n);
76
};/* class CandidateGenerator */
77
78
/* the default candidate generator class
79
 *
80
 * This class may generate candidates for E-matching based on several modes:
81
 * (1) cand_term_db: iterate over all ground terms for the given operator,
82
 * (2) cand_term_ident: generate the given input term as a candidate,
83
 * (3) cand_term_eqc: iterate over all terms in an equivalence class, returning
84
 * those with the proper operator as candidates.
85
 */
86
62821
class CandidateGeneratorQE : public CandidateGenerator
87
{
88
  friend class CandidateGeneratorQEDisequal;
89
90
 public:
91
  CandidateGeneratorQE(QuantifiersEngine* qe, Node pat);
92
  /** reset */
93
  void reset(Node eqc) override;
94
  /** get next candidate */
95
  Node getNextCandidate() override;
96
  /** tell this class to exclude candidates from equivalence class r */
97
2069
  void excludeEqc(Node r) { d_exclude_eqc[r] = true; }
98
  /** is r an excluded equivalence class? */
99
471642
  bool isExcludedEqc(Node r)
100
  {
101
471642
    return d_exclude_eqc.find(r) != d_exclude_eqc.end();
102
  }
103
 protected:
104
  /** reset this class for matching operator op in equivalence class eqc */
105
  void resetForOperator(Node eqc, Node op);
106
  /** the default implementation of getNextCandidate. */
107
  Node getNextCandidateInternal();
108
  /** operator you are looking for */
109
  Node d_op;
110
  /** the equality class iterator (for cand_term_eqc) */
111
  eq::EqClassIterator d_eqc_iter;
112
  /** the TermDb index of the current ground term (for cand_term_db) */
113
  int d_term_iter;
114
  /** the TermDb index of the current ground term (for cand_term_db) */
115
  int d_term_iter_limit;
116
  /** the current equivalence class */
117
  Node d_eqc;
118
  /** candidate generation modes */
119
  enum {
120
    cand_term_db,
121
    cand_term_ident,
122
    cand_term_eqc,
123
    cand_term_none,
124
  };
125
  /** the current mode of this candidate generator */
126
  short d_mode;
127
  /** is n a legal candidate of the required operator? */
128
  virtual bool isLegalOpCandidate(Node n);
129
  /** the equivalence classes that we have excluded from candidate generation */
130
  std::map< Node, bool > d_exclude_eqc;
131
132
};
133
134
/**
135
 * Generate terms based on a disequality, that is, we match (= t[x] s[x])
136
 * with equalities (= g1 g2) in the equivalence class of false.
137
 */
138
14
class CandidateGeneratorQELitDeq : public CandidateGenerator
139
{
140
 public:
141
  /**
142
   * mpat is an equality that we are matching to equalities in the equivalence
143
   * class of false
144
   */
145
  CandidateGeneratorQELitDeq(QuantifiersEngine* qe, Node mpat);
146
  /** reset */
147
  void reset(Node eqc) override;
148
  /** get next candidate */
149
  Node getNextCandidate() override;
150
151
 private:
152
  /** the equality class iterator for false */
153
  eq::EqClassIterator d_eqc_false;
154
  /**
155
   * equality you are trying to match against ground equalities that are
156
   * assigned to false
157
   */
158
  Node d_match_pattern;
159
  /** type of the terms we are generating */
160
  TypeNode d_match_pattern_type;
161
};
162
163
/**
164
 * Generate all terms of the proper sort that occur in the current context.
165
 */
166
142
class CandidateGeneratorQEAll : public CandidateGenerator
167
{
168
 private:
169
  //the equality classes iterator
170
  eq::EqClassesIterator d_eq;
171
  //equality you are trying to match equalities for
172
  Node d_match_pattern;
173
  TypeNode d_match_pattern_type;
174
  // quantifier/index for the variable we are matching
175
  Node d_f;
176
  unsigned d_index;
177
  //first time
178
  bool d_firstTime;
179
180
 public:
181
  CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat );
182
  /** reset */
183
  void reset(Node eqc) override;
184
  /** get next candidate */
185
  Node getNextCandidate() override;
186
};
187
188
/** candidate generation constructor expand
189
 *
190
 * This modifies the candidates t1, ..., tn generated by CandidateGeneratorQE
191
 * so that they are "expansions" of a fixed datatype constructor C. Assuming
192
 * C has arity m, we instead return the stream:
193
 *   C(sel_1( t1 ), ..., sel_m( tn )) ... C(sel_1( t1 ), ..., C( sel_m( tn ))
194
 * where sel_1 ... sel_m are the selectors of C.
195
 */
196
4420
class CandidateGeneratorConsExpand : public CandidateGeneratorQE
197
{
198
 public:
199
  CandidateGeneratorConsExpand(QuantifiersEngine* qe, Node mpat);
200
  /** reset */
201
  void reset(Node eqc) override;
202
  /** get next candidate */
203
  Node getNextCandidate() override;
204
205
 protected:
206
  /** the (datatype) type of the input match pattern */
207
  TypeNode d_mpat_type;
208
  /** we don't care about the operator of n */
209
  bool isLegalOpCandidate(Node n) override;
210
};
211
212
/**
213
 * Candidate generator for selector applications, which considers both
214
 * internal terms corresponding to correctly and incorrectly applied selectors.
215
 */
216
318
class CandidateGeneratorSelector : public CandidateGeneratorQE
217
{
218
 public:
219
  CandidateGeneratorSelector(QuantifiersEngine* qe, Node mpat);
220
  /** reset */
221
  void reset(Node eqc) override;
222
  /**
223
   * Get next candidate, returns matching candidates that are ground terms
224
   * of the selector operator, followed by those that are applications of the
225
   * UF corresponding to an invocation of applying this selector to an
226
   * application of the wrong constructor.
227
   */
228
  Node getNextCandidate() override;
229
 protected:
230
  /** the selector operator */
231
  Node d_selOp;
232
  /** the UF operator */
233
  Node d_ufOp;
234
};
235
236
}/* CVC4::theory::inst namespace */
237
}/* CVC4::theory namespace */
238
}/* CVC4 namespace */
239
240
#endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */