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