1 /********************* */
2 /*! \file quantifiers_engine.h
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Morgan Deters, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 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/cdchunk_list.h"
26 #include "context/cdhashset.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 class InstantiationNotify
{
45 InstantiationNotify(){}
46 virtual ~InstantiationNotify() {}
47 virtual bool notifyInstantiation( unsigned quant_e
, Node q
, Node lem
, std::vector
< Node
>& terms
, Node body
) = 0;
48 virtual void filterInstantiations() = 0;
51 namespace quantifiers
{
52 //TODO: organize this more/review this, github issue #1163
57 class FirstOrderModel
;
58 class QuantAttributes
;
62 class EqualityInference
;
63 class EqualityQueryQuantifiersEngine
;
64 //modules, these are "subsolvers" of the quantifiers theory.
65 class InstantiationEngine
;
67 class BoundedIntegers
;
68 class QuantConflictFind
;
71 class ConjectureGenerator
;
72 class CegInstantiation
;
74 class AlphaEquivalence
;
76 class QuantEqualityEngine
;
78 class InstStrategyCbqi
;
79 class InstStrategyCegqi
;
81 class QuantAntiSkolem
;
82 class EqualityInference
;
83 }/* CVC4::theory::quantifiers */
87 }/* CVC4::theory::inst */
90 class QuantifiersEngine
{
91 friend class quantifiers::InstantiationEngine
;
92 friend class quantifiers::InstStrategyCbqi
;
93 friend class quantifiers::InstStrategyCegqi
;
94 friend class quantifiers::ModelEngine
;
95 friend class quantifiers::RewriteEngine
;
96 friend class quantifiers::QuantConflictFind
;
97 friend class inst::InstMatch
;
98 typedef context::CDHashMap
< Node
, bool, NodeHashFunction
> BoolMap
;
99 typedef context::CDChunkList
<Node
> NodeList
;
100 typedef context::CDChunkList
<bool> BoolList
;
101 typedef context::CDHashSet
<Node
, NodeHashFunction
> NodeSet
;
103 /** reference to theory engine object */
105 /** vector of utilities for quantifiers */
106 std::vector
< QuantifiersUtil
* > d_util
;
107 /** vector of modules for quantifiers */
108 std::vector
< QuantifiersModule
* > d_modules
;
109 /** instantiation notify */
110 std::vector
< InstantiationNotify
* > d_inst_notify
;
111 /** equality query class */
112 quantifiers::EqualityQueryQuantifiersEngine
* d_eq_query
;
113 /** equality inference class */
114 quantifiers::EqualityInference
* d_eq_inference
;
115 /** for computing relevance of quantifiers */
116 QuantRelevance
* d_quant_rel
;
117 /** relevant domain */
118 quantifiers::RelevantDomain
* d_rel_dom
;
119 /** inversion utility for BV instantiation */
120 quantifiers::BvInverter
* d_bv_invert
;
121 /** alpha equivalence */
122 quantifiers::AlphaEquivalence
* d_alpha_equiv
;
124 quantifiers::QModelBuilder
* d_builder
;
125 /** utility for effectively propositional logic */
128 quantifiers::TermDb
* d_term_db
;
129 /** sygus term database */
130 quantifiers::TermDbSygus
* d_sygus_tdb
;
131 /** term utilities */
132 quantifiers::TermUtil
* d_term_util
;
133 /** quantifiers attributes */
134 std::unique_ptr
<quantifiers::QuantAttributes
> d_quant_attr
;
137 /** instantiation engine */
138 quantifiers::InstantiationEngine
* d_inst_engine
;
140 quantifiers::ModelEngine
* d_model_engine
;
141 /** bounded integers utility */
142 quantifiers::BoundedIntegers
* d_bint
;
143 /** Conflict find mechanism for quantifiers */
144 quantifiers::QuantConflictFind
* d_qcf
;
145 /** rewrite rules utility */
146 quantifiers::RewriteEngine
* d_rr_engine
;
147 /** subgoal generator */
148 quantifiers::ConjectureGenerator
* d_sg_gen
;
149 /** ceg instantiation */
150 quantifiers::CegInstantiation
* d_ceg_inst
;
151 /** lte partial instantiation */
152 quantifiers::LtePartialInst
* d_lte_part_inst
;
153 /** function definitions engine */
154 quantifiers::FunDefEngine
* d_fun_def_engine
;
155 /** quantifiers equality engine */
156 quantifiers::QuantEqualityEngine
* d_uee
;
157 /** full saturation */
158 quantifiers::FullSaturation
* d_fs
;
159 /** counterexample-based quantifier instantiation */
160 quantifiers::InstStrategyCbqi
* d_i_cbqi
;
161 /** quantifiers splitting */
162 quantifiers::QuantDSplit
* d_qsplit
;
163 /** quantifiers anti-skolemization */
164 quantifiers::QuantAntiSkolem
* d_anti_skolem
;
165 /** quantifiers instantiation propagtor */
166 quantifiers::InstPropagator
* d_inst_prop
;
168 public: // effort levels (TODO : make an enum and use everywhere #1293)
177 private: //this information is reset during check
178 /** current effort level */
179 unsigned d_curr_effort_level
;
180 /** are we in conflict */
182 context::CDO
< bool > d_conflict_c
;
183 /** has added lemma this round */
184 bool d_hasAddedLemma
;
185 /** whether to use model equality engine */
188 /** list of all quantifiers seen */
189 std::map
< Node
, bool > d_quants
;
190 /** quantifiers reduced */
191 BoolMap d_quants_red
;
192 std::map
< Node
, Node
> d_quants_red_lem
;
193 /** list of all lemmas produced */
194 //std::map< Node, bool > d_lemmas_produced;
195 BoolMap d_lemmas_produced_c
;
196 /** lemmas waiting */
197 std::vector
< Node
> d_lemmas_waiting
;
198 /** phase requirements waiting */
199 std::map
< Node
, bool > d_phase_req_waiting
;
200 /** list of all instantiations produced for each quantifier */
201 std::map
< Node
, inst::InstMatchTrie
> d_inst_match_trie
;
202 std::map
< Node
, inst::CDInstMatchTrie
* > d_c_inst_match_trie
;
203 /** recorded instantiations */
204 std::vector
< std::pair
< Node
, std::vector
< Node
> > > d_recorded_inst
;
205 /** quantifiers that have been skolemized */
206 BoolMap d_skolemized
;
207 /** all triggers will be stored in this trie */
208 inst::TriggerTrie
* d_tr_trie
;
209 /** extended model object */
210 quantifiers::FirstOrderModel
* d_model
;
211 /** statistics for debugging */
212 std::map
< Node
, int > d_total_inst_debug
;
213 std::map
< Node
, int > d_temp_inst_debug
;
214 int d_total_inst_count_debug
;
215 /** inst round counters TODO: make context-dependent? */
216 context::CDO
< int > d_ierCounter_c
;
219 int d_ierCounterLastLc
;
220 int d_inst_when_phase
;
221 /** has presolve been called */
222 context::CDO
< bool > d_presolve
;
223 /** presolve cache */
224 NodeSet d_presolve_in
;
225 NodeList d_presolve_cache
;
226 BoolList d_presolve_cache_wq
;
227 BoolList d_presolve_cache_wic
;
230 QuantifiersEngine(context::Context
* c
, context::UserContext
* u
, TheoryEngine
* te
);
231 ~QuantifiersEngine();
232 /** get theory engine */
233 TheoryEngine
* getTheoryEngine() { return d_te
; }
234 /** get equality query */
235 EqualityQuery
* getEqualityQuery();
236 /** get the equality inference */
237 quantifiers::EqualityInference
* getEqualityInference() { return d_eq_inference
; }
238 /** get default sat context for quantifiers engine */
239 context::Context
* getSatContext();
240 /** get default sat context for quantifiers engine */
241 context::UserContext
* getUserContext();
242 /** get default output channel for the quantifiers engine */
243 OutputChannel
& getOutputChannel();
244 /** get default valuation for the quantifiers engine */
245 Valuation
& getValuation();
246 /** get relevant domain */
247 quantifiers::RelevantDomain
* getRelevantDomain() { return d_rel_dom
; }
248 /** get the BV inverter utility */
249 quantifiers::BvInverter
* getBvInverter() { return d_bv_invert
; }
250 /** get quantifier relevance */
251 QuantRelevance
* getQuantifierRelevance() { return d_quant_rel
; }
252 /** get the model builder */
253 quantifiers::QModelBuilder
* getModelBuilder() { return d_builder
; }
254 /** get utility for EPR */
255 QuantEPR
* getQuantEPR() { return d_qepr
; }
257 /** get instantiation engine */
258 quantifiers::InstantiationEngine
* getInstantiationEngine() { return d_inst_engine
; }
259 /** get model engine */
260 quantifiers::ModelEngine
* getModelEngine() { return d_model_engine
; }
261 /** get bounded integers utility */
262 quantifiers::BoundedIntegers
* getBoundedIntegers() { return d_bint
; }
263 /** Conflict find mechanism for quantifiers */
264 quantifiers::QuantConflictFind
* getConflictFind() { return d_qcf
; }
265 /** rewrite rules utility */
266 quantifiers::RewriteEngine
* getRewriteEngine() { return d_rr_engine
; }
267 /** subgoal generator */
268 quantifiers::ConjectureGenerator
* getConjectureGenerator() { return d_sg_gen
; }
269 /** ceg instantiation */
270 quantifiers::CegInstantiation
* getCegInstantiation() { return d_ceg_inst
; }
271 /** local theory ext partial inst */
272 quantifiers::LtePartialInst
* getLtePartialInst() { return d_lte_part_inst
; }
273 /** function definition engine */
274 quantifiers::FunDefEngine
* getFunDefEngine() { return d_fun_def_engine
; }
275 /** quantifiers equality engine */
276 quantifiers::QuantEqualityEngine
* getQuantEqualityEngine() { return d_uee
; }
277 /** get full saturation */
278 quantifiers::FullSaturation
* getFullSaturation() { return d_fs
; }
279 /** get inst strategy cbqi */
280 quantifiers::InstStrategyCbqi
* getInstStrategyCbqi() { return d_i_cbqi
; }
281 /** get quantifiers splitting */
282 quantifiers::QuantDSplit
* getQuantDSplit() { return d_qsplit
; }
283 /** get quantifiers anti-skolemization */
284 quantifiers::QuantAntiSkolem
* getQuantAntiSkolem() { return d_anti_skolem
; }
286 /** owner of quantified formulas */
287 std::map
< Node
, QuantifiersModule
* > d_owner
;
288 std::map
< Node
, int > d_owner_priority
;
291 QuantifiersModule
* getOwner( Node q
);
293 void setOwner( Node q
, QuantifiersModule
* m
, int priority
= 0 );
295 bool hasOwnership( Node q
, QuantifiersModule
* m
= NULL
);
296 /** is finite bound */
297 bool isFiniteBound( Node q
, Node v
);
303 /** notify preprocessed assertion */
304 void ppNotifyAssertions(const std::vector
<Node
>& assertions
);
305 /** check at level */
306 void check( Theory::Effort e
);
307 /** notify that theories were combined */
308 void notifyCombineTheories();
309 /** register quantifier */
310 bool registerQuantifier( Node f
);
311 /** register quantifier */
312 void registerPattern( std::vector
<Node
> & pattern
);
313 /** assert universal quantifier */
314 void assertQuantifier( Node q
, bool pol
);
316 void propagate( Theory::Effort level
);
317 /** get next decision request */
318 Node
getNextDecisionRequest( unsigned& priority
);
320 /** reduceQuantifier, return true if reduced */
321 bool reduceQuantifier( Node q
);
322 /** compute term vector */
323 void computeTermVector( Node f
, InstMatch
& m
, std::vector
< Node
>& vars
, std::vector
< Node
>& terms
);
324 /** record instantiation, return true if it was non-duplicate */
325 bool recordInstantiationInternal( Node q
, std::vector
< Node
>& terms
, bool modEq
= false, bool addedLem
= true );
326 /** remove instantiation */
327 bool removeInstantiationInternal( Node q
, std::vector
< Node
>& terms
);
328 /** set instantiation level attr */
329 static void setInstantiationLevelAttr( Node n
, Node qn
, uint64_t level
);
333 /** get instantiation */
334 Node
getInstantiation( Node q
, std::vector
< Node
>& vars
, std::vector
< Node
>& terms
, bool doVts
= false );
335 /** get instantiation */
336 Node
getInstantiation( Node q
, InstMatch
& m
, bool doVts
= false );
337 /** get instantiation */
338 Node
getInstantiation( Node q
, std::vector
< Node
>& terms
, bool doVts
= false );
339 /** do substitution */
340 Node
getSubstitute( Node n
, std::vector
< Node
>& terms
, std::map
< Node
, Node
>& visited
);
342 bool addLemma( Node lem
, bool doCache
= true, bool doRewrite
= true );
343 /** remove pending lemma */
344 bool removeLemma( Node lem
);
345 /** add require phase */
346 void addRequirePhase( Node lit
, bool req
);
347 /** do instantiation specified by m */
348 bool addInstantiation( Node q
, InstMatch
& m
, bool mkRep
= false, bool modEq
= false, bool doVts
= false );
349 /** add instantiation */
350 bool addInstantiation( Node q
, std::vector
< Node
>& terms
, bool mkRep
= false, bool modEq
= false, bool doVts
= false );
351 /** remove pending instantiation */
352 bool removeInstantiation( Node q
, Node lem
, std::vector
< Node
>& terms
);
353 /** split on node n */
354 bool addSplit( Node n
, bool reqPhase
= false, bool reqPhasePol
= true );
355 /** add split equality */
356 bool addSplitEquality( Node n1
, Node n2
, bool reqPhase
= false, bool reqPhasePol
= true );
358 bool addEPRAxiom( TypeNode tn
);
359 /** mark relevant quantified formula, this will indicate it should be checked before the others */
360 void markRelevant( Node q
);
361 /** has added lemma */
362 bool hasAddedLemma() { return !d_lemmas_waiting
.empty() || d_hasAddedLemma
; }
363 /** is in conflict */
364 bool inConflict() { return d_conflict
; }
367 /** get number of waiting lemmas */
368 unsigned getNumLemmasWaiting() { return d_lemmas_waiting
.size(); }
369 /** get needs check */
370 bool getInstWhenNeedsCheck( Theory::Effort e
);
371 /** get user pat mode */
372 quantifiers::UserPatMode
getInstUserPatMode();
373 /** set instantiation level attr */
374 static void setInstantiationLevelAttr( Node n
, uint64_t level
);
377 quantifiers::FirstOrderModel
* getModel() { return d_model
; }
378 /** get term database */
379 quantifiers::TermDb
* getTermDatabase() { return d_term_db
; }
380 /** get term database sygus */
381 quantifiers::TermDbSygus
* getTermDatabaseSygus() { return d_sygus_tdb
; }
382 /** get term utilities */
383 quantifiers::TermUtil
* getTermUtil() { return d_term_util
; }
384 /** get quantifiers attributes */
385 quantifiers::QuantAttributes
* getQuantAttributes() {
386 return d_quant_attr
.get();
388 /** get trigger database */
389 inst::TriggerTrie
* getTriggerDatabase() { return d_tr_trie
; }
390 /** add term to database */
391 void addTermToDatabase( Node n
, bool withinQuant
= false, bool withinInstClosure
= false );
392 /** notification when master equality engine is updated */
393 void eqNotifyNewClass(TNode t
);
394 void eqNotifyPreMerge(TNode t1
, TNode t2
);
395 void eqNotifyPostMerge(TNode t1
, TNode t2
);
396 void eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
);
397 /** get the master equality engine */
398 eq::EqualityEngine
* getMasterEqualityEngine();
399 /** get the active equality engine */
400 eq::EqualityEngine
* getActiveEqualityEngine();
401 /** debug print equality engine */
402 void debugPrintEqualityEngine( const char * c
);
403 /** get internal representative */
404 Node
getInternalRepresentative( Node a
, Node q
, int index
);
406 /** print instantiations */
407 void printInstantiations( std::ostream
& out
);
408 /** print solution for synthesis conjectures */
409 void printSynthSolution( std::ostream
& out
);
410 /** get list of quantified formulas that were instantiated */
411 void getInstantiatedQuantifiedFormulas( std::vector
< Node
>& qs
);
412 /** get instantiations */
413 void getInstantiations( Node q
, std::vector
< Node
>& insts
);
414 void getInstantiations( std::map
< Node
, std::vector
< Node
> >& insts
);
415 /** get instantiation term vectors */
416 void getInstantiationTermVectors( Node q
, std::vector
< std::vector
< Node
> >& tvecs
);
417 void getInstantiationTermVectors( std::map
< Node
, std::vector
< std::vector
< Node
> > >& insts
);
418 /** get instantiated conjunction */
419 Node
getInstantiatedConjunction( Node q
);
420 /** get unsat core lemmas */
421 bool getUnsatCoreLemmas( std::vector
< Node
>& active_lemmas
);
422 bool getUnsatCoreLemmas( std::vector
< Node
>& active_lemmas
, std::map
< Node
, Node
>& weak_imp
);
423 /** get inst for lemmas */
424 void getExplanationForInstLemmas( std::vector
< Node
>& lems
, std::map
< Node
, Node
>& quant
, std::map
< Node
, std::vector
< Node
> >& tvec
);
425 /** statistics class */
429 TimerStat d_qcf_time
;
430 TimerStat d_ematching_time
;
432 IntStat d_instantiation_rounds
;
433 IntStat d_instantiation_rounds_lc
;
434 IntStat d_instantiations
;
435 IntStat d_inst_duplicate
;
436 IntStat d_inst_duplicate_eq
;
437 IntStat d_inst_duplicate_ent
;
438 IntStat d_inst_duplicate_model_true
;
440 IntStat d_simple_triggers
;
441 IntStat d_multi_triggers
;
442 IntStat d_multi_trigger_instantiations
;
443 IntStat d_red_alpha_equiv
;
444 IntStat d_instantiations_user_patterns
;
445 IntStat d_instantiations_auto_gen
;
446 IntStat d_instantiations_guess
;
447 IntStat d_instantiations_qcf
;
448 IntStat d_instantiations_qcf_prop
;
449 IntStat d_instantiations_fmf_exh
;
450 IntStat d_instantiations_fmf_mbqi
;
451 IntStat d_instantiations_cbqi
;
452 IntStat d_instantiations_rr
;
455 };/* class QuantifiersEngine::Statistics */
456 Statistics d_statistics
;
457 };/* class QuantifiersEngine */
459 }/* CVC4::theory namespace */
460 }/* CVC4 namespace */
462 #endif /* __CVC4__THEORY__QUANTIFIERS_ENGINE_H */