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-2016 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
20 #include <ext/hash_set>
24 #include "context/cdchunk_list.h"
25 #include "context/cdhashset.h"
26 #include "expr/attribute.h"
27 #include "options/quantifiers_modes.h"
28 #include "theory/quantifiers/inst_match.h"
29 #include "theory/quantifiers/quant_util.h"
30 #include "theory/theory.h"
31 #include "util/hash.h"
32 #include "util/statistics_registry.h"
40 class QuantifiersEngine
;
42 class InstantiationNotify
{
44 InstantiationNotify(){}
45 virtual ~InstantiationNotify() {}
46 virtual bool notifyInstantiation( unsigned quant_e
, Node q
, Node lem
, std::vector
< Node
>& terms
, Node body
) = 0;
47 virtual void filterInstantiations() = 0;
50 namespace quantifiers
{
53 class FirstOrderModel
;
55 class InstantiationEngine
;
57 class BoundedIntegers
;
58 class QuantConflictFind
;
62 class ConjectureGenerator
;
63 class CegInstantiation
;
65 class AlphaEquivalence
;
67 class QuantEqualityEngine
;
69 class InstStrategyCbqi
;
70 class InstStrategyCegqi
;
72 class QuantAntiSkolem
;
73 class EqualityInference
;
75 }/* CVC4::theory::quantifiers */
79 }/* CVC4::theory::inst */
81 //class EfficientEMatcher;
82 class EqualityQueryQuantifiersEngine
;
84 class QuantifiersEngine
{
85 friend class quantifiers::InstantiationEngine
;
86 friend class quantifiers::InstStrategyCbqi
;
87 friend class quantifiers::InstStrategyCegqi
;
88 friend class quantifiers::ModelEngine
;
89 friend class quantifiers::RewriteEngine
;
90 friend class quantifiers::QuantConflictFind
;
91 friend class inst::InstMatch
;
92 typedef context::CDHashMap
< Node
, bool, NodeHashFunction
> BoolMap
;
93 typedef context::CDChunkList
<Node
> NodeList
;
94 typedef context::CDChunkList
<bool> BoolList
;
95 typedef context::CDHashSet
<Node
, NodeHashFunction
> NodeSet
;
97 /** reference to theory engine object */
99 /** vector of utilities for quantifiers */
100 std::vector
< QuantifiersUtil
* > d_util
;
101 /** vector of modules for quantifiers */
102 std::vector
< QuantifiersModule
* > d_modules
;
103 /** instantiation notify */
104 std::vector
< InstantiationNotify
* > d_inst_notify
;
105 /** equality query class */
106 EqualityQueryQuantifiersEngine
* d_eq_query
;
107 /** for computing relevance of quantifiers */
108 QuantRelevance
* d_quant_rel
;
109 /** relevant domain */
110 quantifiers::RelevantDomain
* d_rel_dom
;
111 /** alpha equivalence */
112 quantifiers::AlphaEquivalence
* d_alpha_equiv
;
114 quantifiers::QModelBuilder
* d_builder
;
115 /** utility for effectively propositional logic */
118 /** instantiation engine */
119 quantifiers::InstantiationEngine
* d_inst_engine
;
121 quantifiers::ModelEngine
* d_model_engine
;
122 /** bounded integers utility */
123 quantifiers::BoundedIntegers
* d_bint
;
124 /** Conflict find mechanism for quantifiers */
125 quantifiers::QuantConflictFind
* d_qcf
;
126 /** rewrite rules utility */
127 quantifiers::RewriteEngine
* d_rr_engine
;
128 /** subgoal generator */
129 quantifiers::ConjectureGenerator
* d_sg_gen
;
130 /** ceg instantiation */
131 quantifiers::CegInstantiation
* d_ceg_inst
;
132 /** lte partial instantiation */
133 quantifiers::LtePartialInst
* d_lte_part_inst
;
134 /** function definitions engine */
135 quantifiers::FunDefEngine
* d_fun_def_engine
;
136 /** quantifiers equality engine */
137 quantifiers::QuantEqualityEngine
* d_uee
;
138 /** full saturation */
139 quantifiers::FullSaturation
* d_fs
;
140 /** counterexample-based quantifier instantiation */
141 quantifiers::InstStrategyCbqi
* d_i_cbqi
;
142 /** quantifiers splitting */
143 quantifiers::QuantDSplit
* d_qsplit
;
144 /** quantifiers anti-skolemization */
145 quantifiers::QuantAntiSkolem
* d_anti_skolem
;
146 /** quantifiers instantiation propagtor */
147 quantifiers::InstPropagator
* d_inst_prop
;
148 public: //effort levels
157 private: //this information is reset during check
158 /** current effort level */
159 unsigned d_curr_effort_level
;
160 /** are we in conflict */
162 context::CDO
< bool > d_conflict_c
;
163 /** has added lemma this round */
164 bool d_hasAddedLemma
;
165 /** whether to use model equality engine */
168 /** list of all quantifiers seen */
169 std::map
< Node
, bool > d_quants
;
170 /** quantifiers reduced */
171 BoolMap d_quants_red
;
172 std::map
< Node
, Node
> d_quants_red_lem
;
173 /** list of all lemmas produced */
174 //std::map< Node, bool > d_lemmas_produced;
175 BoolMap d_lemmas_produced_c
;
176 /** lemmas waiting */
177 std::vector
< Node
> d_lemmas_waiting
;
178 /** phase requirements waiting */
179 std::map
< Node
, bool > d_phase_req_waiting
;
180 /** list of all instantiations produced for each quantifier */
181 std::map
< Node
, inst::InstMatchTrie
> d_inst_match_trie
;
182 std::map
< Node
, inst::CDInstMatchTrie
* > d_c_inst_match_trie
;
183 /** recorded instantiations */
184 std::vector
< std::pair
< Node
, std::vector
< Node
> > > d_recorded_inst
;
185 /** quantifiers that have been skolemized */
186 BoolMap d_skolemized
;
188 quantifiers::TermDb
* d_term_db
;
189 /** all triggers will be stored in this trie */
190 inst::TriggerTrie
* d_tr_trie
;
191 /** extended model object */
192 quantifiers::FirstOrderModel
* d_model
;
193 /** statistics for debugging */
194 std::map
< Node
, int > d_total_inst_debug
;
195 std::map
< Node
, int > d_temp_inst_debug
;
196 int d_total_inst_count_debug
;
197 /** inst round counters TODO: make context-dependent? */
198 context::CDO
< int > d_ierCounter_c
;
201 int d_ierCounterLastLc
;
202 int d_inst_when_phase
;
203 /** has presolve been called */
204 context::CDO
< bool > d_presolve
;
205 /** presolve cache */
206 NodeSet d_presolve_in
;
207 NodeList d_presolve_cache
;
208 BoolList d_presolve_cache_wq
;
209 BoolList d_presolve_cache_wic
;
212 QuantifiersEngine(context::Context
* c
, context::UserContext
* u
, TheoryEngine
* te
);
213 ~QuantifiersEngine();
214 /** get theory engine */
215 TheoryEngine
* getTheoryEngine() { return d_te
; }
216 /** get equality query */
217 EqualityQueryQuantifiersEngine
* getEqualityQuery();
218 /** get default sat context for quantifiers engine */
219 context::Context
* getSatContext();
220 /** get default sat context for quantifiers engine */
221 context::UserContext
* getUserContext();
222 /** get default output channel for the quantifiers engine */
223 OutputChannel
& getOutputChannel();
224 /** get default valuation for the quantifiers engine */
225 Valuation
& getValuation();
226 /** get relevant domain */
227 quantifiers::RelevantDomain
* getRelevantDomain() { return d_rel_dom
; }
228 /** get quantifier relevance */
229 QuantRelevance
* getQuantifierRelevance() { return d_quant_rel
; }
230 /** get the model builder */
231 quantifiers::QModelBuilder
* getModelBuilder() { return d_builder
; }
232 /** get utility for EPR */
233 QuantEPR
* getQuantEPR() { return d_qepr
; }
235 /** get instantiation engine */
236 quantifiers::InstantiationEngine
* getInstantiationEngine() { return d_inst_engine
; }
237 /** get model engine */
238 quantifiers::ModelEngine
* getModelEngine() { return d_model_engine
; }
239 /** get bounded integers utility */
240 quantifiers::BoundedIntegers
* getBoundedIntegers() { return d_bint
; }
241 /** Conflict find mechanism for quantifiers */
242 quantifiers::QuantConflictFind
* getConflictFind() { return d_qcf
; }
243 /** rewrite rules utility */
244 quantifiers::RewriteEngine
* getRewriteEngine() { return d_rr_engine
; }
245 /** subgoal generator */
246 quantifiers::ConjectureGenerator
* getConjectureGenerator() { return d_sg_gen
; }
247 /** ceg instantiation */
248 quantifiers::CegInstantiation
* getCegInstantiation() { return d_ceg_inst
; }
249 /** local theory ext partial inst */
250 quantifiers::LtePartialInst
* getLtePartialInst() { return d_lte_part_inst
; }
251 /** function definition engine */
252 quantifiers::FunDefEngine
* getFunDefEngine() { return d_fun_def_engine
; }
253 /** quantifiers equality engine */
254 quantifiers::QuantEqualityEngine
* getQuantEqualityEngine() { return d_uee
; }
255 /** get full saturation */
256 quantifiers::FullSaturation
* getFullSaturation() { return d_fs
; }
257 /** get inst strategy cbqi */
258 quantifiers::InstStrategyCbqi
* getInstStrategyCbqi() { return d_i_cbqi
; }
259 /** get quantifiers splitting */
260 quantifiers::QuantDSplit
* getQuantDSplit() { return d_qsplit
; }
261 /** get quantifiers anti-skolemization */
262 quantifiers::QuantAntiSkolem
* getQuantAntiSkolem() { return d_anti_skolem
; }
264 /** owner of quantified formulas */
265 std::map
< Node
, QuantifiersModule
* > d_owner
;
266 std::map
< Node
, int > d_owner_priority
;
269 QuantifiersModule
* getOwner( Node q
);
271 void setOwner( Node q
, QuantifiersModule
* m
, int priority
= 0 );
273 bool hasOwnership( Node q
, QuantifiersModule
* m
= NULL
);
274 /** is finite bound */
275 bool isFiniteBound( Node q
, Node v
);
281 /** notify preprocessed assertion */
282 void ppNotifyAssertions(const std::vector
<Node
>& assertions
);
283 /** check at level */
284 void check( Theory::Effort e
);
285 /** notify that theories were combined */
286 void notifyCombineTheories();
287 /** register quantifier */
288 bool registerQuantifier( Node f
);
289 /** register quantifier */
290 void registerPattern( std::vector
<Node
> & pattern
);
291 /** assert universal quantifier */
292 void assertQuantifier( Node q
, bool pol
);
294 void propagate( Theory::Effort level
);
295 /** get next decision request */
296 Node
getNextDecisionRequest( unsigned& priority
);
298 /** reduceQuantifier, return true if reduced */
299 bool reduceQuantifier( Node q
);
300 /** compute term vector */
301 void computeTermVector( Node f
, InstMatch
& m
, std::vector
< Node
>& vars
, std::vector
< Node
>& terms
);
302 /** record instantiation, return true if it was non-duplicate */
303 bool recordInstantiationInternal( Node q
, std::vector
< Node
>& terms
, bool modEq
= false, bool addedLem
= true );
304 /** remove instantiation */
305 bool removeInstantiationInternal( Node q
, std::vector
< Node
>& terms
);
306 /** set instantiation level attr */
307 static void setInstantiationLevelAttr( Node n
, Node qn
, uint64_t level
);
311 /** get instantiation */
312 Node
getInstantiation( Node q
, std::vector
< Node
>& vars
, std::vector
< Node
>& terms
, bool doVts
= false );
313 /** get instantiation */
314 Node
getInstantiation( Node q
, InstMatch
& m
, bool doVts
= false );
315 /** get instantiation */
316 Node
getInstantiation( Node q
, std::vector
< Node
>& terms
, bool doVts
= false );
317 /** do substitution */
318 Node
getSubstitute( Node n
, std::vector
< Node
>& terms
);
320 bool addLemma( Node lem
, bool doCache
= true, bool doRewrite
= true );
321 /** remove pending lemma */
322 bool removeLemma( Node lem
);
323 /** add require phase */
324 void addRequirePhase( Node lit
, bool req
);
325 /** do instantiation specified by m */
326 bool addInstantiation( Node q
, InstMatch
& m
, bool mkRep
= false, bool modEq
= false, bool doVts
= false );
327 /** add instantiation */
328 bool addInstantiation( Node q
, std::vector
< Node
>& terms
, bool mkRep
= false, bool modEq
= false, bool doVts
= false );
329 /** remove pending instantiation */
330 bool removeInstantiation( Node q
, Node lem
, std::vector
< Node
>& terms
);
331 /** split on node n */
332 bool addSplit( Node n
, bool reqPhase
= false, bool reqPhasePol
= true );
333 /** add split equality */
334 bool addSplitEquality( Node n1
, Node n2
, bool reqPhase
= false, bool reqPhasePol
= true );
336 bool addEPRAxiom( TypeNode tn
);
337 /** mark relevant quantified formula, this will indicate it should be checked before the others */
338 void markRelevant( Node q
);
339 /** has added lemma */
340 bool hasAddedLemma() { return !d_lemmas_waiting
.empty() || d_hasAddedLemma
; }
341 /** is in conflict */
342 bool inConflict() { return d_conflict
; }
345 /** get number of waiting lemmas */
346 unsigned getNumLemmasWaiting() { return d_lemmas_waiting
.size(); }
347 /** get needs check */
348 bool getInstWhenNeedsCheck( Theory::Effort e
);
349 /** get user pat mode */
350 quantifiers::UserPatMode
getInstUserPatMode();
351 /** set instantiation level attr */
352 static void setInstantiationLevelAttr( Node n
, uint64_t level
);
355 quantifiers::FirstOrderModel
* getModel() { return d_model
; }
356 /** get term database */
357 quantifiers::TermDb
* getTermDatabase() { return d_term_db
; }
358 /** get term database sygus */
359 quantifiers::TermDbSygus
* getTermDatabaseSygus();
360 /** get trigger database */
361 inst::TriggerTrie
* getTriggerDatabase() { return d_tr_trie
; }
362 /** add term to database */
363 void addTermToDatabase( Node n
, bool withinQuant
= false, bool withinInstClosure
= false );
364 /** notification when master equality engine is updated */
365 void eqNotifyNewClass(TNode t
);
366 void eqNotifyPreMerge(TNode t1
, TNode t2
);
367 void eqNotifyPostMerge(TNode t1
, TNode t2
);
368 void eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
);
369 /** get the master equality engine */
370 eq::EqualityEngine
* getMasterEqualityEngine();
371 /** get the active equality engine */
372 eq::EqualityEngine
* getActiveEqualityEngine();
373 /** debug print equality engine */
374 void debugPrintEqualityEngine( const char * c
);
375 /** get internal representative */
376 Node
getInternalRepresentative( Node a
, Node q
, int index
);
378 /** print instantiations */
379 void printInstantiations( std::ostream
& out
);
380 /** print solution for synthesis conjectures */
381 void printSynthSolution( std::ostream
& out
);
382 /** get list of quantified formulas that were instantiated */
383 void getInstantiatedQuantifiedFormulas( std::vector
< Node
>& qs
);
384 /** get instantiations */
385 void getInstantiations( Node q
, std::vector
< Node
>& insts
);
386 void getInstantiations( std::map
< Node
, std::vector
< Node
> >& insts
);
387 /** get instantiation term vectors */
388 void getInstantiationTermVectors( Node q
, std::vector
< std::vector
< Node
> >& tvecs
);
389 void getInstantiationTermVectors( std::map
< Node
, std::vector
< std::vector
< Node
> > >& insts
);
390 /** get instantiated conjunction */
391 Node
getInstantiatedConjunction( Node q
);
392 /** get unsat core lemmas */
393 bool getUnsatCoreLemmas( std::vector
< Node
>& active_lemmas
);
394 bool getUnsatCoreLemmas( std::vector
< Node
>& active_lemmas
, std::map
< Node
, Node
>& weak_imp
);
395 /** get inst for lemmas */
396 void getExplanationForInstLemmas( std::vector
< Node
>& lems
, std::map
< Node
, Node
>& quant
, std::map
< Node
, std::vector
< Node
> >& tvec
);
397 /** statistics class */
401 TimerStat d_qcf_time
;
402 TimerStat d_ematching_time
;
404 IntStat d_instantiation_rounds
;
405 IntStat d_instantiation_rounds_lc
;
406 IntStat d_instantiations
;
407 IntStat d_inst_duplicate
;
408 IntStat d_inst_duplicate_eq
;
409 IntStat d_inst_duplicate_ent
;
410 IntStat d_inst_duplicate_model_true
;
412 IntStat d_simple_triggers
;
413 IntStat d_multi_triggers
;
414 IntStat d_multi_trigger_instantiations
;
415 IntStat d_red_alpha_equiv
;
416 IntStat d_instantiations_user_patterns
;
417 IntStat d_instantiations_auto_gen
;
418 IntStat d_instantiations_guess
;
419 IntStat d_instantiations_qcf
;
420 IntStat d_instantiations_qcf_prop
;
421 IntStat d_instantiations_fmf_exh
;
422 IntStat d_instantiations_fmf_mbqi
;
423 IntStat d_instantiations_cbqi
;
424 IntStat d_instantiations_rr
;
427 };/* class QuantifiersEngine::Statistics */
428 Statistics d_statistics
;
429 };/* class QuantifiersEngine */
433 /** equality query object using theory engine */
434 class EqualityQueryQuantifiersEngine
: public EqualityQuery
437 /** pointer to theory engine */
438 QuantifiersEngine
* d_qe
;
439 /** quantifiers equality inference */
440 quantifiers::EqualityInference
* d_eq_inference
;
441 context::CDO
< unsigned > d_eqi_counter
;
442 /** internal representatives */
443 std::map
< TypeNode
, std::map
< Node
, Node
> > d_int_rep
;
445 std::map
< Node
, int > d_rep_score
;
449 /** processInferences : will merge equivalence classes in master equality engine, if possible */
450 bool processInferences( Theory::Effort e
);
452 Node
getInstance( Node n
, const std::vector
< Node
>& eqc
, std::hash_map
<TNode
, Node
, TNodeHashFunction
>& cache
);
454 int getRepScore( Node n
, Node f
, int index
, TypeNode v_tn
);
455 /** flatten representatives */
456 void flattenRepresentatives( std::map
< TypeNode
, std::vector
< Node
> >& reps
);
458 EqualityQueryQuantifiersEngine( context::Context
* c
, QuantifiersEngine
* qe
);
459 virtual ~EqualityQueryQuantifiersEngine();
461 bool reset( Theory::Effort e
);
463 std::string
identify() const { return "EqualityQueryQE"; }
464 /** general queries about equality */
465 bool hasTerm( Node a
);
466 Node
getRepresentative( Node a
);
467 bool areEqual( Node a
, Node b
);
468 bool areDisequal( Node a
, Node b
);
469 eq::EqualityEngine
* getEngine();
470 void getEquivalenceClass( Node a
, std::vector
< Node
>& eqc
);
471 TNode
getCongruentTerm( Node f
, std::vector
< TNode
>& args
);
472 /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria.
473 If cbqi is active, this will return a term in the equivalence class of "a" that does
474 not contain instantiation constants, if such a term exists.
476 Node
getInternalRepresentative( Node a
, Node f
, int index
);
477 /** get quantifiers equality inference */
478 quantifiers::EqualityInference
* getEqualityInference() { return d_eq_inference
; }
479 }; /* EqualityQueryQuantifiersEngine */
481 }/* CVC4::theory namespace */
482 }/* CVC4 namespace */
484 #endif /* __CVC4__THEORY__QUANTIFIERS_ENGINE_H */