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-2018 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
23 #include <unordered_map>
25 #include "context/cdhashset.h"
26 #include "context/cdlist.h"
27 #include "expr/attribute.h"
28 #include "options/quantifiers_modes.h"
29 #include "theory/quantifiers/inst_match.h"
30 #include "theory/quantifiers/quant_util.h"
31 #include "theory/theory.h"
32 #include "util/hash.h"
33 #include "util/statistics_registry.h"
41 class QuantifiersEngine
;
43 namespace quantifiers
{
44 //TODO: organize this more/review this, github issue #1163
45 //TODO: include these instead of doing forward declarations? #1307
53 class TermEnumeration
;
54 class FirstOrderModel
;
55 class QuantAttributes
;
61 class EqualityInference
;
62 class EqualityQueryQuantifiersEngine
;
63 //modules, these are "subsolvers" of the quantifiers theory.
64 class InstantiationEngine
;
66 class BoundedIntegers
;
67 class QuantConflictFind
;
70 class ConjectureGenerator
;
71 class CegInstantiation
;
73 class AlphaEquivalence
;
74 class InstStrategyEnum
;
75 class InstStrategyCbqi
;
76 class InstStrategyCegqi
;
78 class QuantAntiSkolem
;
79 class EqualityInference
;
80 }/* CVC4::theory::quantifiers */
84 }/* CVC4::theory::inst */
87 class QuantifiersEngine
{
88 typedef context::CDHashMap
< Node
, bool, NodeHashFunction
> BoolMap
;
89 typedef context::CDList
<Node
> NodeList
;
90 typedef context::CDList
<bool> BoolList
;
91 typedef context::CDHashSet
<Node
, NodeHashFunction
> NodeSet
;
94 QuantifiersEngine(context::Context
* c
, context::UserContext
* u
, TheoryEngine
* te
);
96 //---------------------- external interface
97 /** get theory engine */
98 TheoryEngine
* getTheoryEngine() const { return d_te
; }
99 /** get default sat context for quantifiers engine */
100 context::Context
* getSatContext();
101 /** get default sat context for quantifiers engine */
102 context::UserContext
* getUserContext();
103 /** get default output channel for the quantifiers engine */
104 OutputChannel
& getOutputChannel();
105 /** get default valuation for the quantifiers engine */
106 Valuation
& getValuation();
107 /** get the logic info for the quantifiers engine */
108 const LogicInfo
& getLogicInfo() const;
109 //---------------------- end external interface
110 //---------------------- utilities
111 /** get equality query */
112 EqualityQuery
* getEqualityQuery() const;
113 /** get the equality inference */
114 quantifiers::EqualityInference
* getEqualityInference() const;
115 /** get relevant domain */
116 quantifiers::RelevantDomain
* getRelevantDomain() const;
117 /** get the BV inverter utility */
118 quantifiers::BvInverter
* getBvInverter() const;
119 /** get quantifier relevance */
120 quantifiers::QuantRelevance
* getQuantifierRelevance() const;
121 /** get the model builder */
122 quantifiers::QModelBuilder
* getModelBuilder() const;
123 /** get utility for EPR */
124 quantifiers::QuantEPR
* getQuantEPR() const;
126 quantifiers::FirstOrderModel
* getModel() const;
127 /** get term database */
128 quantifiers::TermDb
* getTermDatabase() const;
129 /** get term database sygus */
130 quantifiers::TermDbSygus
* getTermDatabaseSygus() const;
131 /** get term utilities */
132 quantifiers::TermUtil
* getTermUtil() const;
133 /** get term canonizer */
134 quantifiers::TermCanonize
* getTermCanonize() const;
135 /** get quantifiers attributes */
136 quantifiers::QuantAttributes
* getQuantAttributes() const;
137 /** get instantiate utility */
138 quantifiers::Instantiate
* getInstantiate() const;
139 /** get skolemize utility */
140 quantifiers::Skolemize
* getSkolemize() const;
141 /** get term enumeration utility */
142 quantifiers::TermEnumeration
* getTermEnumeration() const;
143 /** get trigger database */
144 inst::TriggerTrie
* getTriggerDatabase() const;
145 //---------------------- end utilities
146 //---------------------- modules
147 /** get bounded integers utility */
148 quantifiers::BoundedIntegers
* getBoundedIntegers() const;
149 /** Conflict find mechanism for quantifiers */
150 quantifiers::QuantConflictFind
* getConflictFind() const;
151 /** rewrite rules utility */
152 quantifiers::RewriteEngine
* getRewriteEngine() const;
153 /** ceg instantiation */
154 quantifiers::CegInstantiation
* getCegInstantiation() const;
155 /** get full saturation */
156 quantifiers::InstStrategyEnum
* getInstStrategyEnum() const;
157 /** get inst strategy cbqi */
158 quantifiers::InstStrategyCbqi
* getInstStrategyCbqi() const;
159 //---------------------- end modules
161 /** owner of quantified formulas */
162 std::map
< Node
, QuantifiersModule
* > d_owner
;
163 std::map
< Node
, int > d_owner_priority
;
166 QuantifiersModule
* getOwner( Node q
);
168 void setOwner( Node q
, QuantifiersModule
* m
, int priority
= 0 );
170 bool hasOwnership( Node q
, QuantifiersModule
* m
= NULL
);
171 /** is finite bound */
172 bool isFiniteBound( Node q
, Node v
);
176 /** notify preprocessed assertion */
177 void ppNotifyAssertions(const std::vector
<Node
>& assertions
);
178 /** check at level */
179 void check( Theory::Effort e
);
180 /** notify that theories were combined */
181 void notifyCombineTheories();
182 /** preRegister quantifier
184 * This function is called after registerQuantifier for quantified formulas
185 * that are pre-registered to the quantifiers theory.
187 void preRegisterQuantifier(Node q
);
188 /** register quantifier */
189 void registerPattern( std::vector
<Node
> & pattern
);
190 /** assert universal quantifier */
191 void assertQuantifier( Node q
, bool pol
);
192 /** get next decision request */
193 Node
getNextDecisionRequest( unsigned& priority
);
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
);
216 bool addEPRAxiom( TypeNode tn
);
217 /** mark relevant quantified formula, this will indicate it should be checked before the others */
218 void markRelevant( Node q
);
219 /** has added lemma */
220 bool hasAddedLemma() { return !d_lemmas_waiting
.empty() || d_hasAddedLemma
; }
221 /** is in conflict */
222 bool inConflict() { return d_conflict
; }
225 /** get current q effort */
226 QuantifiersModule::QEffort
getCurrentQEffort() { return d_curr_effort_level
; }
227 /** get number of waiting lemmas */
228 unsigned getNumLemmasWaiting() { return d_lemmas_waiting
.size(); }
229 /** get needs check */
230 bool getInstWhenNeedsCheck( Theory::Effort e
);
231 /** get user pat mode */
232 quantifiers::UserPatMode
getInstUserPatMode();
234 /** add term to database */
235 void addTermToDatabase( Node n
, bool withinQuant
= false, bool withinInstClosure
= false );
236 /** notification when master equality engine is updated */
237 void eqNotifyNewClass(TNode t
);
238 void eqNotifyPreMerge(TNode t1
, TNode t2
);
239 void eqNotifyPostMerge(TNode t1
, TNode t2
);
240 void eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
);
241 /** get the master equality engine */
242 eq::EqualityEngine
* getMasterEqualityEngine();
243 /** get the active equality engine */
244 eq::EqualityEngine
* getActiveEqualityEngine();
245 /** use model equality engine */
246 bool usingModelEqualityEngine() const { return d_useModelEe
; }
247 /** debug print equality engine */
248 void debugPrintEqualityEngine( const char * c
);
249 /** get internal representative */
250 Node
getInternalRepresentative( Node a
, Node q
, int index
);
253 //----------user interface for instantiations (see quantifiers/instantiate.h)
254 /** print instantiations */
255 void printInstantiations(std::ostream
& out
);
256 /** print solution for synthesis conjectures */
257 void printSynthSolution(std::ostream
& out
);
258 /** get list of quantified formulas that were instantiated */
259 void getInstantiatedQuantifiedFormulas(std::vector
<Node
>& qs
);
260 /** get instantiations */
261 void getInstantiations(Node q
, std::vector
<Node
>& insts
);
262 void getInstantiations(std::map
<Node
, std::vector
<Node
> >& insts
);
263 /** get instantiation term vectors */
264 void getInstantiationTermVectors(Node q
,
265 std::vector
<std::vector
<Node
> >& tvecs
);
266 void getInstantiationTermVectors(
267 std::map
<Node
, std::vector
<std::vector
<Node
> > >& insts
);
268 /** get instantiated conjunction */
269 Node
getInstantiatedConjunction(Node q
);
270 /** get unsat core lemmas */
271 bool getUnsatCoreLemmas(std::vector
<Node
>& active_lemmas
);
272 bool getUnsatCoreLemmas(std::vector
<Node
>& active_lemmas
,
273 std::map
<Node
, Node
>& weak_imp
);
274 /** get explanation for instantiation lemmas */
275 void getExplanationForInstLemmas(const std::vector
<Node
>& lems
,
276 std::map
<Node
, Node
>& quant
,
277 std::map
<Node
, std::vector
<Node
> >& tvec
);
279 /** get synth solutions
281 * This function adds entries to sol_map that map functions-to-synthesize with
282 * their solutions, for all active conjectures. This should be called
283 * immediately after the solver answers unsat for sygus input.
285 * For details on what is added to sol_map, see
286 * CegConjecture::getSynthSolutions.
288 void getSynthSolutions(std::map
<Node
, Node
>& sol_map
);
290 //----------end user interface for instantiations
292 /** statistics class */
296 TimerStat d_qcf_time
;
297 TimerStat d_ematching_time
;
299 IntStat d_instantiation_rounds
;
300 IntStat d_instantiation_rounds_lc
;
302 IntStat d_simple_triggers
;
303 IntStat d_multi_triggers
;
304 IntStat d_multi_trigger_instantiations
;
305 IntStat d_red_alpha_equiv
;
306 IntStat d_instantiations_user_patterns
;
307 IntStat d_instantiations_auto_gen
;
308 IntStat d_instantiations_guess
;
309 IntStat d_instantiations_qcf
;
310 IntStat d_instantiations_qcf_prop
;
311 IntStat d_instantiations_fmf_exh
;
312 IntStat d_instantiations_fmf_mbqi
;
313 IntStat d_instantiations_cbqi
;
314 IntStat d_instantiations_rr
;
317 };/* class QuantifiersEngine::Statistics */
318 Statistics d_statistics
;
321 /** reference to theory engine object */
323 /** vector of utilities for quantifiers */
324 std::vector
<QuantifiersUtil
*> d_util
;
325 /** vector of modules for quantifiers */
326 std::vector
<QuantifiersModule
*> d_modules
;
327 //------------- quantifiers utilities
328 /** equality query class */
329 std::unique_ptr
<quantifiers::EqualityQueryQuantifiersEngine
> d_eq_query
;
330 /** equality inference class */
331 std::unique_ptr
<quantifiers::EqualityInference
> d_eq_inference
;
332 /** quantifiers instantiation propagtor */
333 std::unique_ptr
<quantifiers::InstPropagator
> d_inst_prop
;
334 /** all triggers will be stored in this trie */
335 std::unique_ptr
<inst::TriggerTrie
> d_tr_trie
;
336 /** extended model object */
337 std::unique_ptr
<quantifiers::FirstOrderModel
> d_model
;
338 /** for computing relevance of quantifiers */
339 std::unique_ptr
<quantifiers::QuantRelevance
> d_quant_rel
;
340 /** relevant domain */
341 std::unique_ptr
<quantifiers::RelevantDomain
> d_rel_dom
;
342 /** inversion utility for BV instantiation */
343 std::unique_ptr
<quantifiers::BvInverter
> d_bv_invert
;
345 std::unique_ptr
<quantifiers::QModelBuilder
> d_builder
;
346 /** utility for effectively propositional logic */
347 std::unique_ptr
<quantifiers::QuantEPR
> d_qepr
;
348 /** term utilities */
349 std::unique_ptr
<quantifiers::TermUtil
> d_term_util
;
350 /** term utilities */
351 std::unique_ptr
<quantifiers::TermCanonize
> d_term_canon
;
353 std::unique_ptr
<quantifiers::TermDb
> d_term_db
;
354 /** sygus term database */
355 std::unique_ptr
<quantifiers::TermDbSygus
> d_sygus_tdb
;
356 /** quantifiers attributes */
357 std::unique_ptr
<quantifiers::QuantAttributes
> d_quant_attr
;
358 /** instantiate utility */
359 std::unique_ptr
<quantifiers::Instantiate
> d_instantiate
;
360 /** skolemize utility */
361 std::unique_ptr
<quantifiers::Skolemize
> d_skolemize
;
362 /** term enumeration utility */
363 std::unique_ptr
<quantifiers::TermEnumeration
> d_term_enum
;
364 //------------- end quantifiers utilities
365 //------------- quantifiers modules
366 /** alpha equivalence */
367 std::unique_ptr
<quantifiers::AlphaEquivalence
> d_alpha_equiv
;
368 /** instantiation engine */
369 std::unique_ptr
<quantifiers::InstantiationEngine
> d_inst_engine
;
371 std::unique_ptr
<quantifiers::ModelEngine
> d_model_engine
;
372 /** bounded integers utility */
373 std::unique_ptr
<quantifiers::BoundedIntegers
> d_bint
;
374 /** Conflict find mechanism for quantifiers */
375 std::unique_ptr
<quantifiers::QuantConflictFind
> d_qcf
;
376 /** rewrite rules utility */
377 std::unique_ptr
<quantifiers::RewriteEngine
> d_rr_engine
;
378 /** subgoal generator */
379 std::unique_ptr
<quantifiers::ConjectureGenerator
> d_sg_gen
;
380 /** ceg instantiation */
381 std::unique_ptr
<quantifiers::CegInstantiation
> d_ceg_inst
;
382 /** lte partial instantiation */
383 std::unique_ptr
<quantifiers::LtePartialInst
> d_lte_part_inst
;
384 /** full saturation */
385 std::unique_ptr
<quantifiers::InstStrategyEnum
> d_fs
;
386 /** counterexample-based quantifier instantiation */
387 std::unique_ptr
<quantifiers::InstStrategyCbqi
> d_i_cbqi
;
388 /** quantifiers splitting */
389 std::unique_ptr
<quantifiers::QuantDSplit
> d_qsplit
;
390 /** quantifiers anti-skolemization */
391 std::unique_ptr
<quantifiers::QuantAntiSkolem
> d_anti_skolem
;
392 //------------- end quantifiers modules
393 //------------- temporary information during check
394 /** current effort level */
395 QuantifiersModule::QEffort d_curr_effort_level
;
396 /** are we in conflict */
398 context::CDO
<bool> d_conflict_c
;
399 /** has added lemma this round */
400 bool d_hasAddedLemma
;
401 /** whether to use model equality engine */
403 //------------- end temporary information during check
405 /** list of all quantifiers seen */
406 std::map
<Node
, bool> d_quants
;
407 /** quantifiers pre-registered */
408 NodeSet d_quants_prereg
;
409 /** quantifiers reduced */
410 BoolMap d_quants_red
;
411 std::map
<Node
, Node
> d_quants_red_lem
;
412 /** list of all lemmas produced */
413 // std::map< Node, bool > d_lemmas_produced;
414 BoolMap d_lemmas_produced_c
;
415 /** lemmas waiting */
416 std::vector
<Node
> d_lemmas_waiting
;
417 /** phase requirements waiting */
418 std::map
<Node
, bool> d_phase_req_waiting
;
419 /** inst round counters TODO: make context-dependent? */
420 context::CDO
<int> d_ierCounter_c
;
423 int d_ierCounterLastLc
;
424 int d_inst_when_phase
;
425 /** has presolve been called */
426 context::CDO
<bool> d_presolve
;
427 /** presolve cache */
428 NodeSet d_presolve_in
;
429 NodeList d_presolve_cache
;
430 BoolList d_presolve_cache_wq
;
431 BoolList d_presolve_cache_wic
;
432 };/* class QuantifiersEngine */
434 }/* CVC4::theory namespace */
435 }/* CVC4 namespace */
437 #endif /* __CVC4__THEORY__QUANTIFIERS_ENGINE_H */