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