1 /********************* */
2 /*! \file quantifiers_engine.h
4 ** Original author: Morgan Deters
5 ** Major contributors: Andrew Reynolds
6 ** Minor contributors (to current version): Francois Bobot
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** 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 "theory/theory.h"
21 #include "util/hash.h"
22 #include "theory/quantifiers/inst_match.h"
23 #include "theory/rewriterules/rr_inst_match.h"
24 #include "theory/quantifiers/quant_util.h"
26 #include "util/statistics_registry.h"
28 #include <ext/hash_set>
38 class QuantifiersEngine
;
40 class QuantifiersModule
{
42 QuantifiersEngine
* d_quantEngine
;
44 QuantifiersModule( QuantifiersEngine
* qe
) : d_quantEngine( qe
){}
45 virtual ~QuantifiersModule(){}
46 //get quantifiers engine
47 QuantifiersEngine
* getQuantifiersEngine() { return d_quantEngine
; }
49 virtual void finishInit() {}
50 /* whether this module needs to check this round */
51 virtual bool needsCheck( Theory::Effort e
) { return e
>=Theory::EFFORT_LAST_CALL
; }
52 /* Call during quantifier engine's check */
53 virtual void check( Theory::Effort e
) = 0;
54 /* Called for new quantifiers */
55 virtual void registerQuantifier( Node q
) = 0;
56 virtual void assertNode( Node n
) = 0;
57 virtual void propagate( Theory::Effort level
){}
58 virtual Node
getNextDecisionRequest() { return TNode::null(); }
59 virtual Node
explain(TNode n
) { return TNode::null(); }
60 };/* class QuantifiersModule */
62 namespace quantifiers
{
64 class FirstOrderModel
;
66 class InstantiationEngine
;
68 class BoundedIntegers
;
69 class QuantConflictFind
;
71 }/* CVC4::theory::quantifiers */
75 }/* CVC4::theory::inst */
79 }/* CVC4::theory::inst */
81 class EfficientEMatcher
;
82 class EqualityQueryQuantifiersEngine
;
84 class QuantifiersEngine
{
85 friend class quantifiers::InstantiationEngine
;
86 friend class quantifiers::ModelEngine
;
87 friend class quantifiers::RewriteEngine
;
88 friend class inst::InstMatch
;
90 typedef context::CDHashMap
< Node
, bool, NodeHashFunction
> BoolMap
;
91 /** reference to theory engine object */
93 /** vector of modules for quantifiers */
94 std::vector
< QuantifiersModule
* > d_modules
;
95 /** equality query class */
96 EqualityQueryQuantifiersEngine
* d_eq_query
;
97 /** for computing relevance of quantifiers */
98 QuantRelevance d_quant_rel
;
99 /** phase requirements for each quantifier for each instantiation literal */
100 std::map
< Node
, QuantPhaseReq
* > d_phase_reqs
;
101 /** efficient e-matcher */
102 EfficientEMatcher
* d_eem
;
103 /** instantiation engine */
104 quantifiers::InstantiationEngine
* d_inst_engine
;
106 quantifiers::ModelEngine
* d_model_engine
;
107 /** bounded integers utility */
108 quantifiers::BoundedIntegers
* d_bint
;
109 /** Conflict find mechanism for quantifiers */
110 quantifiers::QuantConflictFind
* d_qcf
;
111 /** rewrite rules utility */
112 quantifiers::RewriteEngine
* d_rr_engine
;
114 /** list of all quantifiers seen */
115 std::vector
< Node
> d_quants
;
116 /** list of all lemmas produced */
117 //std::map< Node, bool > d_lemmas_produced;
118 BoolMap d_lemmas_produced_c
;
119 /** lemmas waiting */
120 std::vector
< Node
> d_lemmas_waiting
;
121 /** has added lemma this round */
122 bool d_hasAddedLemma
;
123 /** list of all instantiations produced for each quantifier */
124 std::map
< Node
, inst::CDInstMatchTrie
* > d_inst_match_trie
;
126 quantifiers::TermDb
* d_term_db
;
127 /** all triggers will be stored in this trie */
128 inst::TriggerTrie
* d_tr_trie
;
129 /** all triggers for rewrite rules will be stored in this trie */
130 rrinst::TriggerTrie
* d_rr_tr_trie
;
131 /** extended model object */
132 quantifiers::FirstOrderModel
* d_model
;
133 /** statistics for debugging */
134 std::map
< Node
, int > d_total_inst_debug
;
135 std::map
< Node
, int > d_temp_inst_debug
;
136 int d_total_inst_count_debug
;
138 KEEP_STATISTIC(TimerStat
, d_time
, "theory::QuantifiersEngine::time");
140 QuantifiersEngine(context::Context
* c
, context::UserContext
* u
, TheoryEngine
* te
);
141 ~QuantifiersEngine();
142 /** get instantiator for id */
143 //Instantiator* getInstantiator( theory::TheoryId id );
144 /** get theory engine */
145 TheoryEngine
* getTheoryEngine() { return d_te
; }
146 /** get equality query object for the given type. The default is the
148 EqualityQueryQuantifiersEngine
* getEqualityQuery();
149 /** get instantiation engine */
150 quantifiers::InstantiationEngine
* getInstantiationEngine() { return d_inst_engine
; }
151 /** get model engine */
152 quantifiers::ModelEngine
* getModelEngine() { return d_model_engine
; }
153 /** get default sat context for quantifiers engine */
154 context::Context
* getSatContext();
155 /** get default sat context for quantifiers engine */
156 context::Context
* getUserContext();
157 /** get default output channel for the quantifiers engine */
158 OutputChannel
& getOutputChannel();
159 /** get default valuation for the quantifiers engine */
160 Valuation
& getValuation();
161 /** get quantifier relevance */
162 QuantRelevance
* getQuantifierRelevance() { return &d_quant_rel
; }
163 /** get phase requirement information */
164 QuantPhaseReq
* getPhaseRequirements( Node f
) { return d_phase_reqs
.find( f
)==d_phase_reqs
.end() ? NULL
: d_phase_reqs
[f
]; }
165 /** get phase requirement terms */
166 void getPhaseReqTerms( Node f
, std::vector
< Node
>& nodes
);
167 /** get efficient e-matching utility */
168 EfficientEMatcher
* getEfficientEMatcher() { return d_eem
; }
169 /** get bounded integers utility */
170 quantifiers::BoundedIntegers
* getBoundedIntegers() { return d_bint
; }
171 /** Conflict find mechanism for quantifiers */
172 quantifiers::QuantConflictFind
* getConflictFind() { return d_qcf
; }
176 /** check at level */
177 void check( Theory::Effort e
);
178 /** register quantifier */
179 void registerQuantifier( Node f
);
180 /** register quantifier */
181 void registerPattern( std::vector
<Node
> & pattern
);
182 /** assert universal quantifier */
183 void assertNode( Node f
);
185 void propagate( Theory::Effort level
);
186 /** get next decision request */
187 Node
getNextDecisionRequest();
189 /** compute term vector */
190 void computeTermVector( Node f
, InstMatch
& m
, std::vector
< Node
>& vars
, std::vector
< Node
>& terms
);
191 /** instantiate f with arguments terms */
192 bool addInstantiation( Node f
, std::vector
< Node
>& vars
, std::vector
< Node
>& terms
);
193 /** set instantiation level attr */
194 void setInstantiationLevelAttr( Node n
, uint64_t level
);
195 /** do substitution */
196 Node
doSubstitute( Node n
, std::vector
< Node
>& terms
);
198 /** get instantiation */
199 Node
getInstantiation( Node f
, std::vector
< Node
>& vars
, std::vector
< Node
>& terms
);
200 /** get instantiation */
201 Node
getInstantiation( Node f
, InstMatch
& m
);
202 /** get instantiation */
203 Node
getInstantiation( Node f
, std::vector
< Node
>& terms
);
204 /** exist instantiation ? */
205 bool existsInstantiation( Node f
, InstMatch
& m
, bool modEq
= true, bool modInst
= false );
207 bool addLemma( Node lem
);
208 /** do instantiation specified by m */
209 bool addInstantiation( Node f
, InstMatch
& m
, bool modEq
= true, bool modInst
= false, bool mkRep
= true );
210 /** split on node n */
211 bool addSplit( Node n
, bool reqPhase
= false, bool reqPhasePol
= true );
212 /** add split equality */
213 bool addSplitEquality( Node n1
, Node n2
, bool reqPhase
= false, bool reqPhasePol
= true );
214 /** has added lemma */
215 bool hasAddedLemma() { return !d_lemmas_waiting
.empty() || d_hasAddedLemma
; }
217 void flushLemmas( OutputChannel
* out
= NULL
);
218 /** get number of waiting lemmas */
219 int getNumLemmasWaiting() { return (int)d_lemmas_waiting
.size(); }
221 /** get number of quantifiers */
222 int getNumQuantifiers() { return (int)d_quants
.size(); }
223 /** get quantifier */
224 Node
getQuantifier( int i
) { return d_quants
[i
]; }
227 quantifiers::FirstOrderModel
* getModel() { return d_model
; }
228 /** get term database */
229 quantifiers::TermDb
* getTermDatabase() { return d_term_db
; }
230 /** get trigger database */
231 inst::TriggerTrie
* getTriggerDatabase() { return d_tr_trie
; }
232 /** get rewrite trigger database */
233 rrinst::TriggerTrie
* getRRTriggerDatabase() { return d_rr_tr_trie
; }
234 /** add term to database */
235 void addTermToDatabase( Node n
, bool withinQuant
= false );
236 /** get the master equality engine */
237 eq::EqualityEngine
* getMasterEqualityEngine() ;
239 /** statistics class */
243 IntStat d_instantiation_rounds
;
244 IntStat d_instantiation_rounds_lc
;
245 IntStat d_instantiations
;
246 IntStat d_inst_duplicate
;
247 IntStat d_inst_duplicate_eq
;
248 IntStat d_lit_phase_req
;
249 IntStat d_lit_phase_nreq
;
251 IntStat d_simple_triggers
;
252 IntStat d_multi_triggers
;
253 IntStat d_multi_trigger_instantiations
;
254 IntStat d_term_in_termdb
;
255 IntStat d_num_mono_candidates
;
256 IntStat d_num_mono_candidates_new_term
;
257 IntStat d_num_multi_candidates
;
258 IntStat d_mono_candidates_cache_hit
;
259 IntStat d_mono_candidates_cache_miss
;
260 IntStat d_multi_candidates_cache_hit
;
261 IntStat d_multi_candidates_cache_miss
;
264 };/* class QuantifiersEngine::Statistics */
265 Statistics d_statistics
;
268 bool d_optInstCheckDuplicate
;
269 bool d_optInstMakeRepresentative
;
270 bool d_optInstAddSplits
;
271 bool d_optMatchIgnoreModelBasis
;
272 bool d_optInstLimitActive
;
274 };/* class QuantifiersEngine */
278 /** equality query object using theory engine */
279 class EqualityQueryQuantifiersEngine
: public EqualityQuery
282 /** pointer to theory engine */
283 QuantifiersEngine
* d_qe
;
284 /** internal representatives */
285 std::map
< Node
, Node
> d_int_rep
;
287 std::map
< Node
, int > d_rep_score
;
294 Node
getInstance( Node n
, std::vector
< Node
>& eqc
);
296 int getRepScore( Node n
, Node f
, int index
);
298 EqualityQueryQuantifiersEngine( QuantifiersEngine
* qe
) : d_qe( qe
), d_reset_count( 0 ), d_liberal( false ){}
299 ~EqualityQueryQuantifiersEngine(){}
302 /** general queries about equality */
303 bool hasTerm( Node a
);
304 Node
getRepresentative( Node a
);
305 bool areEqual( Node a
, Node b
);
306 bool areDisequal( Node a
, Node b
);
307 eq::EqualityEngine
* getEngine();
308 void getEquivalenceClass( Node a
, std::vector
< Node
>& eqc
);
309 /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria.
310 If cbqi is active, this will return a term in the equivalence class of "a" that does
311 not contain instantiation constants, if such a term exists.
313 Node
getInternalRepresentative( Node a
, Node f
, int index
);
314 /** flatten representatives */
315 void flattenRepresentatives( std::map
< TypeNode
, std::vector
< Node
> >& reps
);
317 void setLiberal( bool l
) { d_liberal
= l
; }
318 }; /* EqualityQueryQuantifiersEngine */
320 }/* CVC4::theory namespace */
321 }/* CVC4 namespace */
323 #endif /* __CVC4__THEORY__QUANTIFIERS_ENGINE_H */