GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/term_database.h Lines: 3 3 100.0 %
Date: 2021-03-23 Branches: 2 4 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file term_database.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, 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 term database class
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H
18
#define CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H
19
20
#include <map>
21
#include <unordered_map>
22
23
#include "context/cdhashmap.h"
24
#include "context/cdhashset.h"
25
#include "expr/attribute.h"
26
#include "expr/node_trie.h"
27
#include "theory/quantifiers/quant_util.h"
28
#include "theory/theory.h"
29
#include "theory/type_enumerator.h"
30
31
namespace CVC4 {
32
namespace theory {
33
34
class QuantifiersEngine;
35
36
namespace quantifiers {
37
38
class QuantifiersState;
39
class QuantifiersInferenceManager;
40
class QuantifiersRegistry;
41
42
/** Context-dependent list of nodes */
43
148765
class DbList
44
{
45
 public:
46
148765
  DbList(context::Context* c) : d_list(c) {}
47
  /** The list */
48
  context::CDList<Node> d_list;
49
};
50
51
/** Term Database
52
 *
53
 * This class is a key utility used by
54
 * a number of approaches for quantifier instantiation,
55
 * including E-matching, conflict-based instantiation,
56
 * and model-based instantiation.
57
 *
58
 * The primary responsibilities for this class are to :
59
 * (1) Maintain a list of all ground terms that exist in the quantifier-free
60
 *     solvers, as notified through the master equality engine.
61
 * (2) Build TNodeTrie objects that index all ground terms, per operator.
62
 *
63
 * Like other utilities, its reset(...) function is called
64
 * at the beginning of full or last call effort checks.
65
 * This initializes the database for the round. However,
66
 * notice that TNodeTrie objects are computed
67
 * lazily for performance reasons.
68
 */
69
class TermDb : public QuantifiersUtil {
70
  friend class ::CVC4::theory::QuantifiersEngine;
71
  using NodeBoolMap = context::CDHashMap<Node, bool, NodeHashFunction>;
72
  using NodeList = context::CDList<Node>;
73
  using NodeSet = context::CDHashSet<Node, NodeHashFunction>;
74
  using TypeNodeDbListMap = context::
75
      CDHashMap<TypeNode, std::shared_ptr<DbList>, TypeNodeHashFunction>;
76
  using NodeDbListMap =
77
      context::CDHashMap<Node, std::shared_ptr<DbList>, NodeHashFunction>;
78
79
 public:
80
  TermDb(QuantifiersState& qs,
81
         QuantifiersRegistry& qr);
82
  ~TermDb();
83
  /** Finish init, which sets the inference manager */
84
  void finishInit(QuantifiersInferenceManager* qim);
85
  /** presolve (called once per user check-sat) */
86
  void presolve();
87
  /** reset (calculate which terms are active) */
88
  bool reset(Theory::Effort effort) override;
89
  /** register quantified formula */
90
  void registerQuantifier(Node q) override;
91
  /** identify */
92
28265
  std::string identify() const override { return "TermDb"; }
93
  /** get number of operators */
94
  size_t getNumOperators() const;
95
  /** get operator at index i */
96
  Node getOperator(size_t i) const;
97
  /** ground terms for operator
98
  * Get the number of ground terms with operator f that have been added to the
99
  * database
100
  */
101
  size_t getNumGroundTerms(Node f) const;
102
  /** get ground term for operator
103
  * Get the i^th ground term with operator f that has been added to the database
104
  */
105
  Node getGroundTerm(Node f, size_t i) const;
106
  /** get num type terms
107
  * Get the number of ground terms of tn that have been added to the database
108
  */
109
  size_t getNumTypeGroundTerms(TypeNode tn) const;
110
  /** get type ground term
111
  * Returns the i^th ground term of type tn
112
  */
113
  Node getTypeGroundTerm(TypeNode tn, size_t i) const;
114
  /** get or make ground term
115
   *
116
   * Returns the first ground term of type tn, or makes one if none exist. If
117
   * reqVar is true, then the ground term must be a variable.
118
   */
119
  Node getOrMakeTypeGroundTerm(TypeNode tn, bool reqVar = false);
120
  /** make fresh variable
121
  * Returns a fresh variable of type tn.
122
  * This will return only a single fresh
123
  * variable per type.
124
  */
125
  Node getOrMakeTypeFreshVariable(TypeNode tn);
126
  /**
127
   * Add a term to the database, which registers it as a term that may be
128
   * matched with via E-matching, and can be used in entailment tests below.
129
   */
130
  void addTerm(Node n);
131
  /** Get the currently added ground terms of the given type */
132
  DbList* getOrMkDbListForType(TypeNode tn);
133
  /** Get the currently added ground terms for the given operator */
134
  DbList* getOrMkDbListForOp(TNode op);
135
  /** get match operator for term n
136
  *
137
  * If n has a kind that we index, this function will
138
  * typically return n.getOperator().
139
  *
140
  * However, for parametric operators f, the match operator is an arbitrary
141
  * chosen f-application.  For example, consider array select:
142
  * A : (Array Int Int)
143
  * B : (Array Bool Int)
144
  * We require that terms like (select A 1) and (select B 2) are indexed in
145
  * separate
146
  * data structures despite the fact that
147
  *    (select A 1).getOperator()==(select B 2).getOperator().
148
  * Hence, for the above terms, we may return:
149
  * getMatchOperator( (select A 1) ) = (select A 1), and
150
  * getMatchOperator( (select B 2) ) = (select B 2).
151
  * The match operator is the first instance of an application of the parametric
152
  * operator of its type.
153
  *
154
  * If n has a kind that we do not index (like PLUS),
155
  * then this function returns Node::null().
156
  */
157
  Node getMatchOperator(Node n);
158
  /** get term arg index for all f-applications in the current context */
159
  TNodeTrie* getTermArgTrie(Node f);
160
  /** get the term arg trie for f-applications in the equivalence class of eqc.
161
   */
162
  TNodeTrie* getTermArgTrie(Node eqc, Node f);
163
  /** get congruent term
164
  * If possible, returns a term t such that:
165
  * (1) t is a term that is currently indexed by this database,
166
  * (2) t is of the form f( t1, ..., tk ) and n is of the form f( s1, ..., sk ),
167
  *     where ti is in the equivalence class of si for i=1...k.
168
  */
169
  TNode getCongruentTerm(Node f, Node n);
170
  /** get congruent term
171
  * If possible, returns a term t such that:
172
  * (1) t is a term that is currently indexed by this database,
173
  * (2) t is of the form f( t1, ..., tk ) where ti is in the
174
  *     equivalence class of args[i] for i=1...k.
175
  */
176
  TNode getCongruentTerm(Node f, std::vector<TNode>& args);
177
  /** in relevant domain
178
  * Returns true if there is at least one term t such that:
179
  * (1) t is a term that is currently indexed by this database,
180
  * (2) t is of the form f( t1, ..., tk ) and ti is in the
181
  *     equivalence class of r.
182
  */
183
  bool inRelevantDomain(TNode f, unsigned i, TNode r);
184
  /** evaluate term
185
   *
186
   * Returns a term n' such that n = n' is entailed based on the equality
187
   * information ee.  This function may generate new terms. In particular,
188
   * we typically rewrite subterms of n of maximal size to terms that exist in
189
   * the equality engine specified by ee.
190
   *
191
   * useEntailmentTests is whether to call the theory engine's entailmentTest
192
   * on literals n for which this call fails to find a term n' that is
193
   * equivalent to n, for increased precision. This is not frequently used.
194
   *
195
   * The vector exp stores the explanation for why n evaluates to that term,
196
   * that is, if this call returns a non-null node n', then:
197
   *   exp => n = n'
198
   *
199
   * If reqHasTerm, then we require that the returned term is a Boolean
200
   * combination of terms that exist in the equality engine used by this call.
201
   * If no such term is constructable, this call returns null. The motivation
202
   * for setting this to true is to "fail fast" if we require the return value
203
   * of this function to only involve existing terms. This is used e.g. in
204
   * the "propagating instances" portion of conflict-based instantiation
205
   * (quant_conflict_find.h).
206
   */
207
  Node evaluateTerm(TNode n,
208
                    std::vector<Node>& exp,
209
                    bool useEntailmentTests = false,
210
                    bool reqHasTerm = false);
211
  /** same as above, without exp */
212
  Node evaluateTerm(TNode n,
213
                    bool useEntailmentTests = false,
214
                    bool reqHasTerm = false);
215
  /** get entailed term
216
   *
217
   * If possible, returns a term n' such that:
218
   * (1) n' exists in the current equality engine (as specified by the state),
219
   * (2) n = n' is entailed in the current context.
220
   * It returns null if no such term can be found.
221
   * Wrt evaluateTerm, this version does not construct new terms, and
222
   * thus is less aggressive.
223
   */
224
  TNode getEntailedTerm(TNode n);
225
  /** get entailed term
226
   *
227
   * If possible, returns a term n' such that:
228
   * (1) n' exists in the current equality engine (as specified by the state),
229
   * (2) n * subs = n' is entailed in the current context, where * denotes
230
   * substitution application.
231
   * It returns null if no such term can be found.
232
   * subsRep is whether the substitution maps to terms that are representatives
233
   * according to the quantifiers state.
234
   * Wrt evaluateTerm, this version does not construct new terms, and
235
   * thus is less aggressive.
236
   */
237
  TNode getEntailedTerm(TNode n, std::map<TNode, TNode>& subs, bool subsRep);
238
  /** is entailed
239
   * Checks whether the current context entails n with polarity pol, based on
240
   * the equality information in the quantifiers state. Returns true if the
241
   * entailment can be successfully shown.
242
   */
243
  bool isEntailed(TNode n, bool pol);
244
  /** is entailed
245
   *
246
   * Checks whether the current context entails ( n * subs ) with polarity pol,
247
   * based on the equality information in the quantifiers state,
248
   * where * denotes substitution application.
249
   * subsRep is whether the substitution maps to terms that are representatives
250
   * according to in the quantifiers state.
251
   */
252
  bool isEntailed(TNode n,
253
                  std::map<TNode, TNode>& subs,
254
                  bool subsRep,
255
                  bool pol);
256
  /** is the term n active in the current context?
257
   *
258
  * By default, all terms are active. A term is inactive if:
259
  * (1) it is congruent to another term
260
  * (2) it is irrelevant based on the term database mode. This includes terms
261
  * that only appear in literals that are not relevant.
262
  * (3) it contains instantiation constants (used for CEGQI and cannot be used
263
  * in instantiation).
264
  * (4) it is explicitly set inactive by a call to setTermInactive(...).
265
  * We store whether a term is inactive in a SAT-context-dependent map.
266
  */
267
  bool isTermActive(Node n);
268
  /** set that term n is inactive in this context. */
269
  void setTermInactive(Node n);
270
  /** has term current
271
   *
272
   * This function is used in cases where we restrict which terms appear in the
273
   * database, such as for heuristics used in local theory extensions
274
   * and for --term-db-mode=relevant.
275
   * It returns whether the term n should be indexed in the current context.
276
   *
277
   * If the argument useMode is true, then this method returns a value based on
278
   * the option options::termDbMode().
279
   * Otherwise, it returns the lookup in the map d_has_map.
280
   */
281
  bool hasTermCurrent(Node n, bool useMode = true);
282
  /** is term eligble for instantiation? */
283
  bool isTermEligibleForInstantiation(TNode n, TNode f);
284
  /** get eligible term in equivalence class of r */
285
  Node getEligibleTermInEqc(TNode r);
286
  /** get higher-order type match predicate
287
   *
288
   * This predicate is used to force certain functions f of type tn to appear as
289
   * first-class representatives in the quantifier-free UF solver. For a typical
290
   * use case, we call getHoTypeMatchPredicate which returns a fresh predicate
291
   * P of type (tn -> Bool). Then, we add P( f ) as a lemma.
292
   */
293
  Node getHoTypeMatchPredicate(TypeNode tn);
294
295
 private:
296
  /** The quantifiers state object */
297
  QuantifiersState& d_qstate;
298
  /** Pointer to the quantifiers inference manager */
299
  QuantifiersInferenceManager* d_qim;
300
  /** The quantifiers registry */
301
  QuantifiersRegistry& d_qreg;
302
  /** A context for the data structures below, when not context-dependent */
303
  context::Context d_termsContext;
304
  /** The context we are using for the data structures below */
305
  context::Context* d_termsContextUse;
306
  /** terms processed */
307
  NodeSet d_processed;
308
  /** map from types to ground terms for that type */
309
  TypeNodeDbListMap d_typeMap;
310
  /** list of all operators */
311
  NodeList d_ops;
312
  /** map from operators to ground terms for that operator */
313
  NodeDbListMap d_opMap;
314
  /** select op map */
315
  std::map< Node, std::map< TypeNode, Node > > d_par_op_map;
316
  /** whether master equality engine is UF-inconsistent */
317
  bool d_consistent_ee;
318
  /** boolean terms */
319
  Node d_true;
320
  Node d_false;
321
  /** map from type nodes to a fresh variable we introduced */
322
  std::unordered_map<TypeNode, Node, TypeNodeHashFunction> d_type_fv;
323
  /** inactive map */
324
  NodeBoolMap d_inactive_map;
325
  /** count of the number of non-redundant ground terms per operator */
326
  std::map< Node, int > d_op_nonred_count;
327
  /** mapping from terms to representatives of their arguments */
328
  std::map< TNode, std::vector< TNode > > d_arg_reps;
329
  /** map from operators to trie */
330
  std::map<Node, TNodeTrie> d_func_map_trie;
331
  std::map<Node, TNodeTrie> d_func_map_eqc_trie;
332
  /** mapping from operators to their representative relevant domains */
333
  std::map< Node, std::map< unsigned, std::vector< Node > > > d_func_map_rel_dom;
334
  /** has map */
335
  std::map< Node, bool > d_has_map;
336
  /** map from reps to a term in eqc in d_has_map */
337
  std::map<Node, Node> d_term_elig_eqc;
338
  /**
339
   * Dummy predicate that states terms should be considered first-class members
340
   * of equality engine (for higher-order).
341
   */
342
  std::map<TypeNode, Node> d_ho_type_match_pred;
343
  /** set has term */
344
  void setHasTerm( Node n );
345
  /** helper for evaluate term */
346
  Node evaluateTerm2(TNode n,
347
                     std::map<TNode, Node>& visited,
348
                     std::vector<Node>& exp,
349
                     bool useEntailmentTests,
350
                     bool computeExp,
351
                     bool reqHasTerm);
352
  /** helper for get entailed term */
353
  TNode getEntailedTerm2(TNode n,
354
                         std::map<TNode, TNode>& subs,
355
                         bool subsRep,
356
                         bool hasSubs);
357
  /** helper for is entailed */
358
  bool isEntailed2(TNode n,
359
                   std::map<TNode, TNode>& subs,
360
                   bool subsRep,
361
                   bool hasSubs,
362
                   bool pol);
363
  /** compute uf eqc terms :
364
  * Ensure entries for f are in d_func_map_eqc_trie for all equivalence classes
365
  */
366
  void computeUfEqcTerms( TNode f );
367
  /** compute uf terms
368
  * Ensure that an entry for f is in d_func_map_trie
369
  */
370
  void computeUfTerms( TNode f );
371
  /** compute arg reps
372
  * Ensure that an entry for n is in d_arg_reps
373
  */
374
  void computeArgReps(TNode n);
375
  //------------------------------higher-order term indexing
376
  /**
377
   * Map from non-variable function terms to the operator used to purify it in
378
   * this database. For details, see addTermHo.
379
   */
380
  std::map<Node, Node> d_ho_fun_op_purify;
381
  /**
382
   * Map from terms to the term that they purified. For details, see addTermHo.
383
   */
384
  std::map<Node, Node> d_ho_purify_to_term;
385
  /**
386
   * Map from terms in the domain of the above map to an equality between that
387
   * term and its range in the above map.
388
   */
389
  std::map<Node, Node> d_ho_purify_to_eq;
390
  /** a map from matchable operators to their representative */
391
  std::map< TNode, TNode > d_ho_op_rep;
392
  /** for each representative matchable operator, the list of other matchable operators in their equivalence class */
393
  std::map<TNode, std::vector<TNode> > d_ho_op_slaves;
394
  /** add term higher-order
395
   *
396
   * This registers additional terms corresponding to (possibly multiple)
397
   * purifications of a higher-order term n.
398
   *
399
   * Consider the example:
400
   *    g : Int -> Int, f : Int x Int -> Int
401
   *    constraints: (@ f 0) = g, (f 0 1) = (@ (@ f 0) 1) = 3
402
   *    pattern: (g x)
403
   * where @ is HO_APPLY.
404
   * We have that (g x){ x -> 1 } is an E-match for (@ (@ f 0) 1).
405
   * With the standard registration in addTerm, we construct term indices for
406
   *   f, g, @ : Int x Int -> Int, @ : Int -> Int.
407
   * However, to match (g x) with (@ (@ f 0) 1), we require that
408
   *   [1] -> (@ (@ f 0) 1)
409
   * is an entry in the term index of g. To do this, we maintain a term
410
   * index for a fresh variable pfun, the purification variable for
411
   * (@ f 0). Thus, we register the term (pfun 1) in the call to this function
412
   * for (@ (@ f 0) 1). This ensures that, when processing the equality
413
   * (@ f 0) = g, we merge the term indices of g and pfun. Hence, the entry
414
   *   [1] -> (@ (@ f 0) 1)
415
   * is added to the term index of g, assuming g is the representative of
416
   * the equivalence class of g and pfun.
417
   *
418
   * Above, we set d_ho_fun_op_purify[(@ f 0)] = pfun, and
419
   * d_ho_purify_to_term[(pfun 1)] = (@ (@ f 0) 1).
420
   */
421
  void addTermHo(Node n);
422
  /** get operator representative */
423
  Node getOperatorRepresentative( TNode op ) const;
424
  //------------------------------end higher-order term indexing
425
};/* class TermDb */
426
427
}/* CVC4::theory::quantifiers namespace */
428
}/* CVC4::theory namespace */
429
}/* CVC4 namespace */
430
431
#endif /* CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */