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

Line Exec Source
1
/*********************                                                        */
2
/*! \file instantiate.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, 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 instantiate
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H
18
#define CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H
19
20
#include <map>
21
22
#include "context/cdhashset.h"
23
#include "expr/node.h"
24
#include "expr/proof.h"
25
#include "theory/inference_id.h"
26
#include "theory/quantifiers/inst_match_trie.h"
27
#include "theory/quantifiers/quant_util.h"
28
#include "util/statistics_registry.h"
29
30
namespace CVC4 {
31
32
class LazyCDProof;
33
34
namespace theory {
35
36
class QuantifiersEngine;
37
38
namespace quantifiers {
39
40
class TermDb;
41
class QuantifiersState;
42
class QuantifiersInferenceManager;
43
class QuantifiersRegistry;
44
45
/** Instantiation rewriter
46
 *
47
 * This class is used for cases where instantiation lemmas can be rewritten by
48
 * external utilities. Examples of this include virtual term substitution and
49
 * nested quantifier elimination techniques.
50
 */
51
class InstantiationRewriter
52
{
53
 public:
54
5975
  InstantiationRewriter() {}
55
5972
  virtual ~InstantiationRewriter() {}
56
57
  /** rewrite instantiation
58
   *
59
   * The node inst is the instantiation of quantified formula q for terms.
60
   * This method returns the rewritten form of the instantiation.
61
   *
62
   * The flag doVts is whether we must apply virtual term substitution to the
63
   * instantiation.
64
   *
65
   * Returns a TrustNode of kind REWRITE, corresponding to the rewrite of inst
66
   * and its proof generator.
67
   */
68
  virtual TrustNode rewriteInstantiation(Node q,
69
                                         std::vector<Node>& terms,
70
                                         Node inst,
71
                                         bool doVts) = 0;
72
};
73
74
/** Instantiate
75
 *
76
 * This class is used for generating instantiation lemmas.  It maintains an
77
 * instantiation trie, which is represented by a different data structure
78
 * depending on whether incremental solving is enabled (see d_inst_match_trie
79
 * and d_c_inst_match_trie).
80
 *
81
 * Below, we say an instantiation lemma for q = forall x. F under substitution
82
 * { x -> t } is the formula:
83
 *   ( ~forall x. F V F * { x -> t } )
84
 * where * is application of substitution.
85
 *
86
 * Its main interface is ::addInstantiation(...), which is called by many of
87
 * the quantifiers modules, which enqueues instantiation lemmas in quantifiers
88
 * engine via calls to QuantifiersInferenceManager::addPendingLemma.
89
 *
90
 * It also has utilities for constructing instantiations, and interfaces for
91
 * getting the results of the instantiations produced during check-sat calls.
92
 */
93
class Instantiate : public QuantifiersUtil
94
{
95
  typedef context::CDHashMap<Node, uint32_t, NodeHashFunction> NodeUIntMap;
96
97
 public:
98
  Instantiate(QuantifiersEngine* qe,
99
              QuantifiersState& qs,
100
              QuantifiersInferenceManager& qim,
101
              QuantifiersRegistry& qr,
102
              ProofNodeManager* pnm = nullptr);
103
  ~Instantiate();
104
105
  /** reset */
106
  bool reset(Theory::Effort e) override;
107
  /** register quantifier */
108
  void registerQuantifier(Node q) override;
109
  /** identify */
110
28252
  std::string identify() const override { return "Instantiate"; }
111
  /** check incomplete */
112
  bool checkComplete() override;
113
114
  //--------------------------------------rewrite objects
115
  /** add instantiation rewriter */
116
  void addRewriter(InstantiationRewriter* ir);
117
  /** notify flush lemmas
118
   *
119
   * This is called just before the quantifiers engine flushes its lemmas to
120
   * the output channel.
121
   */
122
  void notifyFlushLemmas();
123
  //--------------------------------------end rewrite objects
124
125
  /** do instantiation specified by m
126
   *
127
   * This function returns true if the instantiation lemma for quantified
128
   * formula q for the substitution specified by terms is successfully enqueued
129
   * via a call to QuantifiersInferenceManager::addPendingLemma.
130
   * @param q the quantified formula to instantiate
131
   * @param terms the terms to instantiate with
132
   * @param id the identifier of the instantiation lemma sent via the inference
133
   * manager
134
   * @param mkRep whether to take the representatives of the terms in the
135
   * range of the substitution m,
136
   * @param modEq whether to check for duplication modulo equality in
137
   * instantiation tries (for performance),
138
   * @param doVts whether we must apply virtual term substitution to the
139
   * instantiation lemma.
140
   *
141
   * This call may fail if it can be determined that the instantiation is not
142
   * relevant or legal in the current context. This happens if:
143
   * (1) The substitution is not well-typed,
144
   * (2) The substitution involves terms whose instantiation level is above the
145
   *     allowed limit,
146
   * (3) The resulting instantiation is entailed in the current context using a
147
   *     fast entailment check (see TermDb::isEntailed),
148
   * (4) The range of the substitution is a duplicate of that of a previously
149
   *     added instantiation,
150
   * (5) The instantiation lemma is a duplicate of previously added lemma.
151
   *
152
   */
153
  bool addInstantiation(Node q,
154
                        std::vector<Node>& terms,
155
                        InferenceId id,
156
                        bool mkRep = false,
157
                        bool modEq = false,
158
                        bool doVts = false);
159
  /**
160
   * Same as above, but we also compute a vector failMask indicating which
161
   * values in terms led to the instantiation not being added when this method
162
   * returns false.  For example, if q is the formula
163
   *   forall xy. x>5 => P(x,y)
164
   * If terms = { 4, 0 }, then this method will return false since
165
   *   4>5 => P(4,0)
166
   * is entailed true based on rewriting. This method may additionally set
167
   * failMask to "10", indicating that x's value was critical, but y's value
168
   * was not. In other words, all instantiations including { x -> 4 } will also
169
   * lead to this method returning false.
170
   *
171
   * The bits of failMask are computed in a greedy fashion, in reverse order.
172
   * That is, we check whether each variable is critical one at a time, starting
173
   * from the end.
174
   *
175
   * The parameter expFull is whether try to set all bits of the fail mask to
176
   * 0. If this argument is true, then we only try to set a suffix of the
177
   * bits in failMask to false. The motivation for expFull=false is for callers
178
   * of this method that are enumerating tuples in lexiocographic order. The
179
   * number of false bits in the suffix of failMask tells the caller how many
180
   * "decimal" places to increment their iterator.
181
   */
182
  bool addInstantiationExpFail(Node q,
183
                               std::vector<Node>& terms,
184
                               std::vector<bool>& failMask,
185
                               InferenceId id,
186
                               bool mkRep = false,
187
                               bool modEq = false,
188
                               bool doVts = false,
189
                               bool expFull = true);
190
  /** record instantiation
191
   *
192
   * Explicitly record that q has been instantiated with terms. This is the
193
   * same as addInstantiation, but does not enqueue an instantiation lemma.
194
   */
195
  bool recordInstantiation(Node q,
196
                           std::vector<Node>& terms,
197
                           bool modEq = false,
198
                           bool addedLem = true);
199
  /** exists instantiation
200
   *
201
   * Returns true if and only if the instantiation already was added or
202
   * recorded by this class.
203
   *   modEq : whether to check for duplication modulo equality
204
   */
205
  bool existsInstantiation(Node q,
206
                           std::vector<Node>& terms,
207
                           bool modEq = false);
208
  //--------------------------------------general utilities
209
  /** get instantiation
210
   *
211
   * Returns the instantiation lemma for q under substitution { vars -> terms }.
212
   * doVts is whether to apply virtual term substitution to its body.
213
   *
214
   * If provided, pf is a lazy proof for which we store a proof of the
215
   * returned formula with free assumption q. This typically stores a
216
   * single INSTANTIATE step concluding the instantiated body of q from q.
217
   */
218
  Node getInstantiation(Node q,
219
                        std::vector<Node>& vars,
220
                        std::vector<Node>& terms,
221
                        bool doVts = false,
222
                        LazyCDProof* pf = nullptr);
223
  /** get instantiation
224
   *
225
   * Same as above but with vars equal to the bound variables of q.
226
   */
227
  Node getInstantiation(Node q, std::vector<Node>& terms, bool doVts = false);
228
  /** get term for type
229
   *
230
   * This returns an arbitrary term for type tn.
231
   * This term is chosen heuristically to be the best
232
   * term for instantiation. Currently, this
233
   * heuristic enumerates the first term of the
234
   * type if the type is closed enumerable, otherwise
235
   * an existing ground term from the term database if
236
   * one exists, or otherwise a fresh variable.
237
   */
238
  Node getTermForType(TypeNode tn);
239
  //--------------------------------------end general utilities
240
241
  /**
242
   * Debug print, called once per instantiation round. This prints
243
   * instantiations added this round to trace inst-per-quant-round, if
244
   * applicable, and prints to out if the option debug-inst is enabled.
245
   */
246
  void debugPrint(std::ostream& out);
247
  /** debug print model, called once, before we terminate with sat/unknown. */
248
  void debugPrintModel();
249
250
  //--------------------------------------user-level interface utilities
251
  /** get instantiated quantified formulas
252
   *
253
   * Get the list of quantified formulas that were instantiated in the current
254
   * user context, store them in qs.
255
   */
256
  void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs);
257
  /** get instantiation term vectors
258
   *
259
   * Get term vectors corresponding to for all instantiations lemmas added in
260
   * the current user context for quantified formula q, store them in tvecs.
261
   */
262
  void getInstantiationTermVectors(Node q,
263
                                   std::vector<std::vector<Node> >& tvecs);
264
  /** get instantiation term vectors
265
   *
266
   * Get term vectors for all instantiations lemmas added in the current user
267
   * context for quantified formula q, store them in tvecs.
268
   */
269
  void getInstantiationTermVectors(
270
      std::map<Node, std::vector<std::vector<Node> > >& insts);
271
  //--------------------------------------end user-level interface utilities
272
273
  /** Are proofs enabled for this object? */
274
  bool isProofEnabled() const;
275
276
  /** statistics class
277
   *
278
   * This tracks statistics on the number of instantiations successfully
279
   * enqueued on the quantifiers output channel, and the number of redundant
280
   * instantiations encountered by various criteria.
281
   */
282
  class Statistics
283
  {
284
   public:
285
    IntStat d_instantiations;
286
    IntStat d_inst_duplicate;
287
    IntStat d_inst_duplicate_eq;
288
    IntStat d_inst_duplicate_ent;
289
    Statistics();
290
    ~Statistics();
291
  }; /* class Instantiate::Statistics */
292
  Statistics d_statistics;
293
294
 private:
295
  /** record instantiation, return true if it was not a duplicate
296
   *
297
   * addedLem : whether an instantiation lemma was added for the vector we are
298
   *            recording. If this is false, we bookkeep the vector.
299
   * modEq : whether to check for duplication modulo equality in instantiation
300
   *         tries (for performance),
301
   */
302
  bool recordInstantiationInternal(Node q,
303
                                   std::vector<Node>& terms,
304
                                   bool modEq = false,
305
                                   bool addedLem = true);
306
  /** remove instantiation from the cache */
307
  bool removeInstantiationInternal(Node q, std::vector<Node>& terms);
308
  /**
309
   * Ensure that n has type tn, return a term equivalent to it for that type
310
   * if possible.
311
   */
312
  static Node ensureType(Node n, TypeNode tn);
313
314
  /** pointer to the quantifiers engine */
315
  QuantifiersEngine* d_qe;
316
  /** Reference to the quantifiers state */
317
  QuantifiersState& d_qstate;
318
  /** Reference to the quantifiers inference manager */
319
  QuantifiersInferenceManager& d_qim;
320
  /** The quantifiers registry */
321
  QuantifiersRegistry& d_qreg;
322
  /** pointer to the proof node manager */
323
  ProofNodeManager* d_pnm;
324
  /** cache of term database for quantifiers engine */
325
  TermDb* d_term_db;
326
  /** instantiation rewriter classes */
327
  std::vector<InstantiationRewriter*> d_instRewrite;
328
329
  /** statistics for debugging total instantiations per quantifier */
330
  NodeUIntMap d_total_inst_debug;
331
  /** statistics for debugging total instantiations per quantifier per round */
332
  std::map<Node, uint32_t> d_temp_inst_debug;
333
334
  /** list of all instantiations produced for each quantifier
335
   *
336
   * We store context (dependent, independent) versions. If incremental solving
337
   * is disabled, we use d_inst_match_trie for performance reasons.
338
   */
339
  std::map<Node, inst::InstMatchTrie> d_inst_match_trie;
340
  std::map<Node, inst::CDInstMatchTrie*> d_c_inst_match_trie;
341
  /**
342
   * The list of quantified formulas for which the domain of d_c_inst_match_trie
343
   * is valid.
344
   */
345
  context::CDHashSet<Node, NodeHashFunction> d_c_inst_match_trie_dom;
346
347
  /** explicitly recorded instantiations
348
   *
349
   * Sometimes an instantiation is recorded internally but not sent out as a
350
   * lemma, for instance, for partial quantifier elimination. This is a map
351
   * of these instantiations, for each quantified formula.
352
   */
353
  std::vector<std::pair<Node, std::vector<Node> > > d_recorded_inst;
354
  /**
355
   * A CDProof storing instantiation steps.
356
   */
357
  std::unique_ptr<CDProof> d_pfInst;
358
};
359
360
} /* CVC4::theory::quantifiers namespace */
361
} /* CVC4::theory namespace */
362
} /* CVC4 namespace */
363
364
#endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H */