1 /********************* */
2 /*! \file quantifiers_engine.h
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Morgan Deters, Haniel Barbosa
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
12 ** \brief Theory instantiator, Instantiation Engine classes
15 #include "cvc4_private.h"
17 #ifndef CVC4__THEORY__QUANTIFIERS_ENGINE_H
18 #define CVC4__THEORY__QUANTIFIERS_ENGINE_H
21 #include <unordered_map>
23 #include "context/cdhashset.h"
24 #include "context/cdlist.h"
25 #include "expr/attribute.h"
26 #include "expr/term_canonize.h"
27 #include "theory/quantifiers/ematching/trigger.h"
28 #include "theory/quantifiers/equality_infer.h"
29 #include "theory/quantifiers/equality_query.h"
30 #include "theory/quantifiers/first_order_model.h"
31 #include "theory/quantifiers/fmf/model_builder.h"
32 #include "theory/quantifiers/instantiate.h"
33 #include "theory/quantifiers/quant_epr.h"
34 #include "theory/quantifiers/quant_util.h"
35 #include "theory/quantifiers/quantifiers_attributes.h"
36 #include "theory/quantifiers/relevant_domain.h"
37 #include "theory/quantifiers/skolemize.h"
38 #include "theory/quantifiers/sygus/synth_engine.h"
39 #include "theory/quantifiers/sygus/term_database_sygus.h"
40 #include "theory/quantifiers/term_database.h"
41 #include "theory/quantifiers/term_enumeration.h"
42 #include "theory/quantifiers/term_util.h"
43 #include "util/statistics_registry.h"
51 class QuantifiersEnginePrivate
;
53 // TODO: organize this more/review this, github issue #1163
54 class QuantifiersEngine
{
55 typedef context::CDHashMap
< Node
, bool, NodeHashFunction
> BoolMap
;
56 typedef context::CDList
<Node
> NodeList
;
57 typedef context::CDList
<bool> BoolList
;
58 typedef context::CDHashSet
<Node
, NodeHashFunction
> NodeSet
;
61 QuantifiersEngine(context::Context
* c
, context::UserContext
* u
, TheoryEngine
* te
);
63 //---------------------- external interface
64 /** get theory engine */
65 TheoryEngine
* getTheoryEngine() const { return d_te
; }
66 /** get default sat context for quantifiers engine */
67 context::Context
* getSatContext();
68 /** get default sat context for quantifiers engine */
69 context::UserContext
* getUserContext();
70 /** get default output channel for the quantifiers engine */
71 OutputChannel
& getOutputChannel();
72 /** get default valuation for the quantifiers engine */
73 Valuation
& getValuation();
74 /** get the logic info for the quantifiers engine */
75 const LogicInfo
& getLogicInfo() const;
76 //---------------------- end external interface
77 //---------------------- utilities
78 /** get the master equality engine */
79 eq::EqualityEngine
* getMasterEqualityEngine() const;
80 /** get the active equality engine */
81 eq::EqualityEngine
* getActiveEqualityEngine() const;
82 /** get equality query */
83 EqualityQuery
* getEqualityQuery() const;
84 /** get the model builder */
85 quantifiers::QModelBuilder
* getModelBuilder() const;
86 /** get utility for EPR */
87 quantifiers::QuantEPR
* getQuantEPR() const;
89 quantifiers::FirstOrderModel
* getModel() const;
90 /** get term database */
91 quantifiers::TermDb
* getTermDatabase() const;
92 /** get term database sygus */
93 quantifiers::TermDbSygus
* getTermDatabaseSygus() const;
94 /** get term utilities */
95 quantifiers::TermUtil
* getTermUtil() const;
96 /** get term canonizer */
97 expr::TermCanonize
* getTermCanonize() const;
98 /** get quantifiers attributes */
99 quantifiers::QuantAttributes
* getQuantAttributes() const;
100 /** get instantiate utility */
101 quantifiers::Instantiate
* getInstantiate() const;
102 /** get skolemize utility */
103 quantifiers::Skolemize
* getSkolemize() const;
104 /** get term enumeration utility */
105 quantifiers::TermEnumeration
* getTermEnumeration() const;
106 /** get trigger database */
107 inst::TriggerTrie
* getTriggerDatabase() const;
108 //---------------------- end utilities
109 //---------------------- utilities (TODO move these utilities #1163)
110 /** get the equality inference */
111 quantifiers::EqualityInference
* getEqualityInference() const;
112 /** get relevant domain */
113 quantifiers::RelevantDomain
* getRelevantDomain() const;
114 //---------------------- end utilities
115 //---------------------- modules (TODO remove these #1163)
116 /** ceg instantiation */
117 quantifiers::SynthEngine
* getSynthEngine() const;
118 //---------------------- end modules
121 * Maps quantified formulas to the module that owns them, if any module has
122 * specifically taken ownership of it.
124 std::map
< Node
, QuantifiersModule
* > d_owner
;
126 * The priority value associated with the ownership of quantified formulas
127 * in the domain of the above map, where higher values take higher
130 std::map
< Node
, int > d_owner_priority
;
133 QuantifiersModule
* getOwner( Node q
);
135 * Set owner of quantified formula q to module m with given priority. If
136 * the quantified formula has previously been assigned an owner with
137 * lower priority, that owner is overwritten.
139 void setOwner( Node q
, QuantifiersModule
* m
, int priority
= 0 );
140 /** set owner of quantified formula q based on its attributes qa. */
141 void setOwner(Node q
, quantifiers::QAttributes
& qa
);
143 bool hasOwnership( Node q
, QuantifiersModule
* m
= NULL
);
144 /** does variable v of quantified formula q have a finite bound? */
145 bool isFiniteBound(Node q
, Node v
) const;
146 /** get bound var type
148 * This returns the type of bound that was inferred for variable v of
149 * quantified formula q.
151 BoundVarType
getBoundVarType(Node q
, Node v
) const;
153 * Get the indices of bound variables, in the order they should be processed
154 * in a RepSetIterator.
156 * For details, see BoundedIntegers::getBoundVarIndices.
158 void getBoundVarIndices(Node q
, std::vector
<unsigned>& indices
) const;
162 * This gets the (finite) enumeration of the range of variable v of quantified
163 * formula q and adds it into the vector elements in the context of the
164 * iteration being performed by rsi. It returns true if it could successfully
165 * determine this range.
167 * For details, see BoundedIntegers::getBoundElements.
169 bool getBoundElements(RepSetIterator
* rsi
,
173 std::vector
<Node
>& elements
) const;
178 /** notify preprocessed assertion */
179 void ppNotifyAssertions(const std::vector
<Node
>& assertions
);
180 /** check at level */
181 void check( Theory::Effort e
);
182 /** notify that theories were combined */
183 void notifyCombineTheories();
184 /** preRegister quantifier
186 * This function is called after registerQuantifier for quantified formulas
187 * that are pre-registered to the quantifiers theory.
189 void preRegisterQuantifier(Node q
);
190 /** register quantifier */
191 void registerPattern( std::vector
<Node
> & pattern
);
192 /** assert universal quantifier */
193 void assertQuantifier( Node q
, bool pol
);
195 /** (context-indepentent) register quantifier internal
197 * This is called when a quantified formula q is pre-registered to the
198 * quantifiers theory, and updates the modules in this class with
199 * context-independent information about how to handle q. This includes basic
200 * information such as which module owns q.
202 void registerQuantifierInternal(Node q
);
203 /** reduceQuantifier, return true if reduced */
204 bool reduceQuantifier(Node q
);
210 bool addLemma( Node lem
, bool doCache
= true, bool doRewrite
= true );
211 /** remove pending lemma */
212 bool removeLemma( Node lem
);
213 /** add require phase */
214 void addRequirePhase( Node lit
, bool req
);
215 /** mark relevant quantified formula, this will indicate it should be checked before the others */
216 void markRelevant( Node q
);
217 /** has added lemma */
218 bool hasAddedLemma() { return !d_lemmas_waiting
.empty() || d_hasAddedLemma
; }
219 /** is in conflict */
220 bool inConflict() { return d_conflict
; }
223 /** get current q effort */
224 QuantifiersModule::QEffort
getCurrentQEffort() { return d_curr_effort_level
; }
225 /** get number of waiting lemmas */
226 unsigned getNumLemmasWaiting() { return d_lemmas_waiting
.size(); }
227 /** get needs check */
228 bool getInstWhenNeedsCheck( Theory::Effort e
);
229 /** get user pat mode */
230 quantifiers::UserPatMode
getInstUserPatMode();
232 /** add term to database */
233 void addTermToDatabase( Node n
, bool withinQuant
= false, bool withinInstClosure
= false );
234 /** notification when master equality engine is updated */
235 void eqNotifyNewClass(TNode t
);
236 void eqNotifyPreMerge(TNode t1
, TNode t2
);
237 void eqNotifyPostMerge(TNode t1
, TNode t2
);
238 void eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
);
239 /** use model equality engine */
240 bool usingModelEqualityEngine() const { return d_useModelEe
; }
241 /** debug print equality engine */
242 void debugPrintEqualityEngine( const char * c
);
243 /** get internal representative */
244 Node
getInternalRepresentative( Node a
, Node q
, int index
);
247 //----------user interface for instantiations (see quantifiers/instantiate.h)
248 /** print instantiations */
249 void printInstantiations(std::ostream
& out
);
250 /** print solution for synthesis conjectures */
251 void printSynthSolution(std::ostream
& out
);
252 /** get list of quantified formulas that were instantiated */
253 void getInstantiatedQuantifiedFormulas(std::vector
<Node
>& qs
);
254 /** get instantiations */
255 void getInstantiations(Node q
, std::vector
<Node
>& insts
);
256 void getInstantiations(std::map
<Node
, std::vector
<Node
> >& insts
);
257 /** get instantiation term vectors */
258 void getInstantiationTermVectors(Node q
,
259 std::vector
<std::vector
<Node
> >& tvecs
);
260 void getInstantiationTermVectors(
261 std::map
<Node
, std::vector
<std::vector
<Node
> > >& insts
);
262 /** get instantiated conjunction */
263 Node
getInstantiatedConjunction(Node q
);
264 /** get unsat core lemmas */
265 bool getUnsatCoreLemmas(std::vector
<Node
>& active_lemmas
);
266 bool getUnsatCoreLemmas(std::vector
<Node
>& active_lemmas
,
267 std::map
<Node
, Node
>& weak_imp
);
268 /** get explanation for instantiation lemmas */
269 void getExplanationForInstLemmas(const std::vector
<Node
>& lems
,
270 std::map
<Node
, Node
>& quant
,
271 std::map
<Node
, std::vector
<Node
> >& tvec
);
273 /** get synth solutions
275 * This function adds entries to sol_map that map functions-to-synthesize with
276 * their solutions, for all active conjectures. This should be called
277 * immediately after the solver answers unsat for sygus input.
279 * For details on what is added to sol_map, see
280 * CegConjecture::getSynthSolutions.
282 void getSynthSolutions(std::map
<Node
, Node
>& sol_map
);
284 //----------end user interface for instantiations
286 /** statistics class */
290 TimerStat d_qcf_time
;
291 TimerStat d_ematching_time
;
293 IntStat d_instantiation_rounds
;
294 IntStat d_instantiation_rounds_lc
;
296 IntStat d_simple_triggers
;
297 IntStat d_multi_triggers
;
298 IntStat d_multi_trigger_instantiations
;
299 IntStat d_red_alpha_equiv
;
300 IntStat d_instantiations_user_patterns
;
301 IntStat d_instantiations_auto_gen
;
302 IntStat d_instantiations_guess
;
303 IntStat d_instantiations_qcf
;
304 IntStat d_instantiations_qcf_prop
;
305 IntStat d_instantiations_fmf_exh
;
306 IntStat d_instantiations_fmf_mbqi
;
307 IntStat d_instantiations_cbqi
;
308 IntStat d_instantiations_rr
;
311 };/* class QuantifiersEngine::Statistics */
312 Statistics d_statistics
;
315 /** reference to theory engine object */
317 /** vector of utilities for quantifiers */
318 std::vector
<QuantifiersUtil
*> d_util
;
319 /** vector of modules for quantifiers */
320 std::vector
<QuantifiersModule
*> d_modules
;
321 //------------- quantifiers utilities
322 /** equality query class */
323 std::unique_ptr
<quantifiers::EqualityQueryQuantifiersEngine
> d_eq_query
;
324 /** equality inference class */
325 std::unique_ptr
<quantifiers::EqualityInference
> d_eq_inference
;
326 /** all triggers will be stored in this trie */
327 std::unique_ptr
<inst::TriggerTrie
> d_tr_trie
;
328 /** extended model object */
329 std::unique_ptr
<quantifiers::FirstOrderModel
> d_model
;
330 /** relevant domain */
331 std::unique_ptr
<quantifiers::RelevantDomain
> d_rel_dom
;
333 std::unique_ptr
<quantifiers::QModelBuilder
> d_builder
;
334 /** utility for effectively propositional logic */
335 std::unique_ptr
<quantifiers::QuantEPR
> d_qepr
;
336 /** term utilities */
337 std::unique_ptr
<quantifiers::TermUtil
> d_term_util
;
338 /** term utilities */
339 std::unique_ptr
<expr::TermCanonize
> d_term_canon
;
341 std::unique_ptr
<quantifiers::TermDb
> d_term_db
;
342 /** sygus term database */
343 std::unique_ptr
<quantifiers::TermDbSygus
> d_sygus_tdb
;
344 /** quantifiers attributes */
345 std::unique_ptr
<quantifiers::QuantAttributes
> d_quant_attr
;
346 /** instantiate utility */
347 std::unique_ptr
<quantifiers::Instantiate
> d_instantiate
;
348 /** skolemize utility */
349 std::unique_ptr
<quantifiers::Skolemize
> d_skolemize
;
350 /** term enumeration utility */
351 std::unique_ptr
<quantifiers::TermEnumeration
> d_term_enum
;
352 //------------- end quantifiers utilities
354 * The private utility, which contains all of the quantifiers modules.
356 std::unique_ptr
<QuantifiersEnginePrivate
> d_private
;
357 //------------- temporary information during check
358 /** current effort level */
359 QuantifiersModule::QEffort d_curr_effort_level
;
360 /** are we in conflict */
362 context::CDO
<bool> d_conflict_c
;
363 /** has added lemma this round */
364 bool d_hasAddedLemma
;
365 /** whether to use model equality engine */
367 //------------- end temporary information during check
369 /** list of all quantifiers seen */
370 std::map
<Node
, bool> d_quants
;
371 /** quantifiers pre-registered */
372 NodeSet d_quants_prereg
;
373 /** quantifiers reduced */
374 BoolMap d_quants_red
;
375 std::map
<Node
, Node
> d_quants_red_lem
;
376 /** list of all lemmas produced */
377 // std::map< Node, bool > d_lemmas_produced;
378 BoolMap d_lemmas_produced_c
;
379 /** lemmas waiting */
380 std::vector
<Node
> d_lemmas_waiting
;
381 /** phase requirements waiting */
382 std::map
<Node
, bool> d_phase_req_waiting
;
383 /** inst round counters TODO: make context-dependent? */
384 context::CDO
<int> d_ierCounter_c
;
387 int d_ierCounterLastLc
;
388 int d_inst_when_phase
;
389 /** has presolve been called */
390 context::CDO
<bool> d_presolve
;
391 /** presolve cache */
392 NodeSet d_presolve_in
;
393 NodeList d_presolve_cache
;
394 BoolList d_presolve_cache_wq
;
395 BoolList d_presolve_cache_wic
;
396 };/* class QuantifiersEngine */
398 }/* CVC4::theory namespace */
399 }/* CVC4 namespace */
401 #endif /* CVC4__THEORY__QUANTIFIERS_ENGINE_H */