1 /********************* */
2 /*! \file instantiate.h
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-2019 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
15 #include "cvc4_private.h"
17 #ifndef CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H
18 #define CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H
22 #include "expr/node.h"
23 #include "theory/quantifiers/inst_match_trie.h"
24 #include "theory/quantifiers/quant_util.h"
25 #include "util/statistics_registry.h"
30 class QuantifiersEngine
;
32 namespace quantifiers
{
37 /** instantiation notify
39 * This class is a listener for all instantiations generated with quantifiers.
40 * By default, no notify classes are used. For an example of an instantiation
41 * notify class, see quantifiers/inst_propagate.h, which has a notify class
42 * that recognizes when the set of enqueued instantiations form a conflict.
44 class InstantiationNotify
47 InstantiationNotify() {}
48 virtual ~InstantiationNotify() {}
49 /** notify instantiation
51 * This is called when an instantiation of quantified formula q is
52 * instantiated by a substitution whose range is terms at quantifier effort
53 * quant_e. Furthermore:
54 * body is the substituted, preprocessed body of the quantified formula,
55 * lem is the instantiation lemma ( ~q V body ) after rewriting.
57 virtual bool notifyInstantiation(QuantifiersModule::QEffort quant_e
,
60 std::vector
<Node
>& terms
,
62 /** filter instantiations
64 * This is called just before the quantifiers engine flushes its lemmas to the
65 * output channel. During this call, the instantiation notify object may
66 * call, e.g. QuantifiersEngine::getInstantiate()->removeInstantiation
67 * to remove instantiations that should not be sent on the output channel.
69 virtual void filterInstantiations() = 0;
72 /** Instantiation rewriter
74 * This class is used for cases where instantiation lemmas can be rewritten by
75 * external utilities. Examples of this include virtual term substitution and
76 * nested quantifier elimination techniques.
78 class InstantiationRewriter
81 InstantiationRewriter() {}
82 virtual ~InstantiationRewriter() {}
84 /** rewrite instantiation
86 * The node inst is the instantiation of quantified formula q for terms.
87 * This method returns the rewritten form of the instantiation.
89 * The flag doVts is whether we must apply virtual term substitution to the
92 virtual Node
rewriteInstantiation(Node q
,
93 std::vector
<Node
>& terms
,
100 * This class is used for generating instantiation lemmas. It maintains an
101 * instantiation trie, which is represented by a different data structure
102 * depending on whether incremental solving is enabled (see d_inst_match_trie
103 * and d_c_inst_match_trie).
105 * Below, we say an instantiation lemma for q = forall x. F under substitution
106 * { x -> t } is the formula:
107 * ( ~forall x. F V F * { x -> t } )
108 * where * is application of substitution.
110 * Its main interface is ::addInstantiation(...), which is called by many of
111 * the quantifiers modules, which enqueues instantiation lemmas in quantifiers
112 * engine via calls to QuantifiersEngine::addLemma.
114 * It also has utilities for constructing instantiations, and interfaces for
115 * getting the results of the instantiations produced during check-sat calls.
117 class Instantiate
: public QuantifiersUtil
120 Instantiate(QuantifiersEngine
* qe
, context::UserContext
* u
);
124 bool reset(Theory::Effort e
) override
;
125 /** register quantifier */
126 void registerQuantifier(Node q
) override
;
128 std::string
identify() const override
{ return "Instantiate"; }
129 /** check incomplete */
130 bool checkComplete() override
;
132 //--------------------------------------notify/rewrite objects
133 /** add instantiation notify
135 * Adds an instantiation notify class to listen to the instantiations reported
138 void addNotify(InstantiationNotify
* in
);
139 /** get number of instantiation notify added to this class */
140 bool hasNotify() const { return !d_inst_notify
.empty(); }
141 /** add instantiation rewriter */
142 void addRewriter(InstantiationRewriter
* ir
);
143 /** notify flush lemmas
145 * This is called just before the quantifiers engine flushes its lemmas to
146 * the output channel.
148 void notifyFlushLemmas();
149 //--------------------------------------end notify objects
151 /** do instantiation specified by m
153 * This function returns true if the instantiation lemma for quantified
154 * formula q for the substitution specified by m is successfully enqueued
155 * via a call to QuantifiersEngine::addLemma.
156 * mkRep : whether to take the representatives of the terms in the range of
157 * the substitution m,
158 * modEq : whether to check for duplication modulo equality in instantiation
159 * tries (for performance),
160 * doVts : whether we must apply virtual term substitution to the
161 * instantiation lemma.
163 * This call may fail if it can be determined that the instantiation is not
164 * relevant or legal in the current context. This happens if:
165 * (1) The substitution is not well-typed,
166 * (2) The substitution involves terms whose instantiation level is above the
168 * (3) The resulting instantiation is entailed in the current context using a
169 * fast entailment check (see TermDb::isEntailed),
170 * (4) The range of the substitution is a duplicate of that of a previously
171 * added instantiation,
172 * (5) The instantiation lemma is a duplicate of previously added lemma.
175 bool addInstantiation(Node q
,
180 /** add instantiation
182 * Same as above, but the substitution we are considering maps the variables
183 * of q to the vector terms, in order.
185 bool addInstantiation(Node q
,
186 std::vector
<Node
>& terms
,
190 /** remove pending instantiation
192 * Removes the instantiation lemma lem from the instantiation trie.
194 bool removeInstantiation(Node q
, Node lem
, std::vector
<Node
>& terms
);
195 /** record instantiation
197 * Explicitly record that q has been instantiated with terms. This is the
198 * same as addInstantiation, but does not enqueue an instantiation lemma.
200 bool recordInstantiation(Node q
,
201 std::vector
<Node
>& terms
,
203 bool addedLem
= true);
204 /** exists instantiation
206 * Returns true if and only if the instantiation already was added or
207 * recorded by this class.
208 * modEq : whether to check for duplication modulo equality
210 bool existsInstantiation(Node q
,
211 std::vector
<Node
>& terms
,
213 //--------------------------------------general utilities
214 /** get instantiation
216 * Returns the instantiation lemma for q under substitution { vars -> terms }.
217 * doVts is whether to apply virtual term substitution to its body.
219 Node
getInstantiation(Node q
,
220 std::vector
<Node
>& vars
,
221 std::vector
<Node
>& terms
,
223 /** get instantiation
225 * Same as above, but with vars/terms specified by InstMatch m.
227 Node
getInstantiation(Node q
, InstMatch
& m
, bool doVts
= false);
228 /** get instantiation
230 * Same as above but with vars equal to the bound variables of q.
232 Node
getInstantiation(Node q
, std::vector
<Node
>& terms
, bool doVts
= false);
233 /** get term for type
235 * This returns an arbitrary term for type tn.
236 * This term is chosen heuristically to be the best
237 * term for instantiation. Currently, this
238 * heuristic enumerates the first term of the
239 * type if the type is closed enumerable, otherwise
240 * an existing ground term from the term database if
241 * one exists, or otherwise a fresh variable.
243 Node
getTermForType(TypeNode tn
);
244 //--------------------------------------end general utilities
246 /** debug print, called once per instantiation round. */
248 /** debug print model, called once, before we terminate with sat/unknown. */
249 void debugPrintModel();
251 //--------------------------------------user-level interface utilities
252 /** print instantiations
254 * Print all instantiations for all quantified formulas on out,
255 * returns true if at least one instantiation was printed.
257 bool printInstantiations(std::ostream
& out
);
258 /** get instantiated quantified formulas
260 * Get the list of quantified formulas that were instantiated in the current
261 * user context, store them in qs.
263 void getInstantiatedQuantifiedFormulas(std::vector
<Node
>& qs
);
264 /** get instantiations
266 * Get the body of all instantiation lemmas added in the current user context
267 * for quantified formula q, store them in insts.
269 void getInstantiations(Node q
, std::vector
<Node
>& insts
);
270 /** get instantiations
272 * Get the body of all instantiation lemmas added in the current user context
273 * for all quantified formulas stored in the domain of insts, store them in
274 * the range of insts.
276 void getInstantiations(std::map
<Node
, std::vector
<Node
> >& insts
);
277 /** get instantiation term vectors
279 * Get term vectors corresponding to for all instantiations lemmas added in
280 * the current user context for quantified formula q, store them in tvecs.
282 void getInstantiationTermVectors(Node q
,
283 std::vector
<std::vector
<Node
> >& tvecs
);
284 /** get instantiation term vectors
286 * Get term vectors for all instantiations lemmas added in the current user
287 * context for quantified formula q, store them in tvecs.
289 void getInstantiationTermVectors(
290 std::map
<Node
, std::vector
<std::vector
<Node
> > >& insts
);
291 /** get instantiated conjunction
293 * This gets a conjunction of the bodies of instantiation lemmas added in the
294 * current user context for quantified formula q. For example, if we added:
295 * ~forall x. P( x ) V P( a )
296 * ~forall x. P( x ) V P( b )
297 * Then, this method returns P( a ) ^ P( b ).
299 Node
getInstantiatedConjunction(Node q
);
300 /** get unsat core lemmas
302 * If this method returns true, then it appends to active_lemmas all lemmas
303 * that are in the unsat core that originated from the theory of quantifiers.
304 * This method returns false if the unsat core is not available.
306 bool getUnsatCoreLemmas(std::vector
<Node
>& active_lemmas
);
307 /** get unsat core lemmas
309 * If this method returns true, then it appends to active_lemmas all lemmas
310 * that are in the unsat core that originated from the theory of quantifiers.
311 * This method returns false if the unsat core is not available.
313 * It also computes a weak implicant for each of these lemmas. For each lemma
314 * L in active_lemmas, this is a formula L' such that:
316 * and replacing L by L' in the unsat core results in a set that is still
317 * unsatisfiable. The map weak_imp stores this formula for each formula in
320 bool getUnsatCoreLemmas(std::vector
<Node
>& active_lemmas
,
321 std::map
<Node
, Node
>& weak_imp
);
322 /** get explanation for instantiation lemmas
326 void getExplanationForInstLemmas(const std::vector
<Node
>& lems
,
327 std::map
<Node
, Node
>& quant
,
328 std::map
<Node
, std::vector
<Node
> >& tvec
);
329 //--------------------------------------end user-level interface utilities
333 * This tracks statistics on the number of instantiations successfully
334 * enqueued on the quantifiers output channel, and the number of redundant
335 * instantiations encountered by various criteria.
340 IntStat d_instantiations
;
341 IntStat d_inst_duplicate
;
342 IntStat d_inst_duplicate_eq
;
343 IntStat d_inst_duplicate_ent
;
344 IntStat d_inst_duplicate_model_true
;
347 }; /* class Instantiate::Statistics */
348 Statistics d_statistics
;
351 /** record instantiation, return true if it was not a duplicate
353 * addedLem : whether an instantiation lemma was added for the vector we are
354 * recording. If this is false, we bookkeep the vector.
355 * modEq : whether to check for duplication modulo equality in instantiation
356 * tries (for performance),
358 bool recordInstantiationInternal(Node q
,
359 std::vector
<Node
>& terms
,
361 bool addedLem
= true);
362 /** remove instantiation from the cache */
363 bool removeInstantiationInternal(Node q
, std::vector
<Node
>& terms
);
365 /** pointer to the quantifiers engine */
366 QuantifiersEngine
* d_qe
;
367 /** cache of term database for quantifiers engine */
369 /** cache of term util for quantifiers engine */
370 TermUtil
* d_term_util
;
371 /** instantiation notify classes */
372 std::vector
<InstantiationNotify
*> d_inst_notify
;
373 /** instantiation rewriter classes */
374 std::vector
<InstantiationRewriter
*> d_instRewrite
;
376 /** statistics for debugging total instantiation */
377 int d_total_inst_count_debug
;
378 /** statistics for debugging total instantiations per quantifier */
379 std::map
<Node
, int> d_total_inst_debug
;
380 /** statistics for debugging total instantiations per quantifier per round */
381 std::map
<Node
, int> d_temp_inst_debug
;
383 /** list of all instantiations produced for each quantifier
385 * We store context (dependent, independent) versions. If incremental solving
386 * is disabled, we use d_inst_match_trie for performance reasons.
388 std::map
<Node
, inst::InstMatchTrie
> d_inst_match_trie
;
389 std::map
<Node
, inst::CDInstMatchTrie
*> d_c_inst_match_trie
;
391 * The list of quantified formulas for which the domain of d_c_inst_match_trie
394 context::CDHashSet
<Node
, NodeHashFunction
> d_c_inst_match_trie_dom
;
396 /** explicitly recorded instantiations
398 * Sometimes an instantiation is recorded internally but not sent out as a
399 * lemma, for instance, for partial quantifier elimination. This is a map
400 * of these instantiations, for each quantified formula.
402 std::vector
<std::pair
<Node
, std::vector
<Node
> > > d_recorded_inst
;
405 } /* CVC4::theory::quantifiers namespace */
406 } /* CVC4::theory namespace */
407 } /* CVC4 namespace */
409 #endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H */