1 /********************* */
2 /*! \file quantifiers_engine.h
4 ** Original author: ajreynol
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief Theory instantiator, Instantiation Engine classes
17 #include "cvc4_private.h"
19 #ifndef __CVC4__THEORY__QUANTIFIERS_ENGINE_H
20 #define __CVC4__THEORY__QUANTIFIERS_ENGINE_H
22 #include "theory/theory.h"
23 #include "util/hash.h"
24 #include "theory/quantifiers/inst_match.h"
25 #include "theory/rewriterules/rr_inst_match.h"
27 #include "util/stats.h"
29 #include <ext/hash_set>
39 class QuantifiersEngine
;
49 /** reference to the instantiation engine */
50 QuantifiersEngine
* d_quantEngine
;
52 /** giving priorities */
53 std::vector
< InstStrategy
* > d_priority_over
;
54 /** do not instantiate list */
55 std::vector
< Node
> d_no_instantiate
;
56 std::vector
< Node
> d_no_instantiate_temp
;
57 /** reset instantiation */
58 virtual void processResetInstantiationRound( Theory::Effort effort
) = 0;
60 virtual int process( Node f
, Theory::Effort effort
, int e
) = 0;
62 InstStrategy( QuantifiersEngine
* ie
) : d_quantEngine( ie
){}
63 virtual ~InstStrategy(){}
65 /** reset instantiation */
66 void resetInstantiationRound( Theory::Effort effort
);
67 /** do instantiation round method */
68 int doInstantiation( Node f
, Theory::Effort effort
, int e
);
70 static void updateStatus( int& currStatus
, int addStatus
){
71 if( addStatus
==STATUS_UNFINISHED
){
72 currStatus
= STATUS_UNFINISHED
;
73 }else if( addStatus
==STATUS_UNKNOWN
){
74 if( currStatus
==STATUS_SAT
){
75 currStatus
= STATUS_UNKNOWN
;
80 virtual std::string
identify() const { return std::string("Unknown"); }
83 void setPriorityOver( InstStrategy
* is
) { d_priority_over
.push_back( is
); }
84 /** set no instantiate */
85 void setNoInstantiate( Node n
) { d_no_instantiate
.push_back( n
); }
86 /** should instantiate */
87 bool shouldInstantiate( Node n
) {
88 return std::find( d_no_instantiate_temp
.begin(), d_no_instantiate_temp
.end(), n
)==d_no_instantiate_temp
.end();
90 };/* class InstStrategy */
92 class QuantifiersModule
{
94 QuantifiersEngine
* d_quantEngine
;
96 QuantifiersModule( QuantifiersEngine
* qe
) : d_quantEngine( qe
){}
97 ~QuantifiersModule(){}
98 //get quantifiers engine
99 QuantifiersEngine
* getQuantifiersEngine() { return d_quantEngine
; }
100 /* Call during check registerQuantifier has already been called */
101 virtual void check( Theory::Effort e
) = 0;
102 /* Called for new quantifiers */
103 virtual void registerQuantifier( Node n
) = 0;
104 virtual void assertNode( Node n
) = 0;
105 virtual void propagate( Theory::Effort level
) = 0;
106 virtual Node
explain(TNode n
) = 0;
107 };/* class QuantifiersModule */
109 namespace quantifiers
{
110 class InstantiationEngine
;
113 class FirstOrderModel
;
114 }/* CVC4::theory::quantifiers */
117 class QuantifiersEngine
{
118 friend class quantifiers::InstantiationEngine
;
119 friend class quantifiers::ModelEngine
;
120 friend class inst::InstMatch
;
122 typedef context::CDHashMap
< Node
, bool, NodeHashFunction
> BoolMap
;
123 /** reference to theory engine object */
125 /** vector of modules for quantifiers */
126 std::vector
< QuantifiersModule
* > d_modules
;
127 /** instantiation engine */
128 quantifiers::InstantiationEngine
* d_inst_engine
;
130 quantifiers::ModelEngine
* d_model_engine
;
131 /** equality query class */
132 EqualityQuery
* d_eq_query
;
134 /** list of all quantifiers (pre-rewrite) */
135 std::vector
< Node
> d_quants
;
136 /** list of all quantifiers (post-rewrite) */
137 std::vector
< Node
> d_r_quants
;
138 /** map from quantifiers to whether they are active */
140 /** lemmas produced */
141 std::map
< Node
, bool > d_lemmas_produced
;
142 /** lemmas waiting */
143 std::vector
< Node
> d_lemmas_waiting
;
144 /** has added lemma this round */
145 bool d_hasAddedLemma
;
146 /** inst matches produced for each quantifier */
147 std::map
< Node
, inst::InstMatchTrie
> d_inst_match_trie
;
148 /** owner of quantifiers */
149 std::map
< Node
, Theory
* > d_owner
;
151 quantifiers::TermDb
* d_term_db
;
152 /** extended model object */
153 quantifiers::FirstOrderModel
* d_model
;
154 /** has the model been set? */
156 /** universal quantifiers that have been rewritten */
157 std::map
< Node
, std::vector
< Node
> > d_quant_rewritten
;
158 /** map from rewritten universal quantifiers to the quantifier they are the consequence of */
159 std::map
< Node
, Node
> d_rewritten_quant
;
161 /** for computing relavance */
162 /** map from quantifiers to symbols they contain */
163 std::map
< Node
, std::vector
< Node
> > d_syms
;
164 /** map from symbols to quantifiers */
165 std::map
< Node
, std::vector
< Node
> > d_syms_quants
;
166 /** relevance for quantifiers and symbols */
167 std::map
< Node
, int > d_relevance
;
168 /** compute symbols */
169 void computeSymbols( Node n
, std::vector
< Node
>& syms
);
171 /** helper functions compute phase requirements */
172 static void computePhaseReqs2( Node n
, bool polarity
, std::map
< Node
, int >& phaseReqs
);
174 KEEP_STATISTIC(TimerStat
, d_time
, "theory::QuantifiersEngine::time");
177 QuantifiersEngine(context::Context
* c
, TheoryEngine
* te
);
178 ~QuantifiersEngine();
179 /** get instantiator for id */
180 Instantiator
* getInstantiator( theory::TheoryId id
);
181 /** get theory engine */
182 TheoryEngine
* getTheoryEngine() { return d_te
; }
183 /** get equality query object for the given type. The default is the
185 inst::EqualityQuery
* getEqualityQuery(TypeNode t
);
186 inst::EqualityQuery
* getEqualityQuery() {
189 /** get equality query object for the given type. The default is the
191 rrinst::CandidateGenerator
* getRRCanGenClasses(TypeNode t
);
192 rrinst::CandidateGenerator
* getRRCanGenClass(TypeNode t
);
193 /* generic candidate generator */
194 rrinst::CandidateGenerator
* getRRCanGenClasses();
195 rrinst::CandidateGenerator
* getRRCanGenClass();
196 /** get instantiation engine */
197 quantifiers::InstantiationEngine
* getInstantiationEngine() { return d_inst_engine
; }
198 /** get model engine */
199 quantifiers::ModelEngine
* getModelEngine() { return d_model_engine
; }
200 /** get default sat context for quantifiers engine */
201 context::Context
* getSatContext();
202 /** get default output channel for the quantifiers engine */
203 OutputChannel
& getOutputChannel();
204 /** get default valuation for the quantifiers engine */
205 Valuation
& getValuation();
207 /** check at level */
208 void check( Theory::Effort e
);
209 /** register (non-rewritten) quantifier */
210 void registerQuantifier( Node f
);
211 /** register (non-rewritten) quantifier */
212 void registerPattern( std::vector
<Node
> & pattern
);
213 /** assert (universal) quantifier */
214 void assertNode( Node f
);
216 void propagate( Theory::Effort level
);
217 /** reset instantiation round */
218 void resetInstantiationRound( Theory::Effort level
);
220 //create inst variable
221 std::vector
<Node
> createInstVariable( std::vector
<Node
> & vars
);
224 bool addLemma( Node lem
);
225 /** instantiate f with arguments terms */
226 bool addInstantiation( Node f
, std::vector
< Node
>& terms
);
227 /** do instantiation specified by m */
228 bool addInstantiation( Node f
, InstMatch
& m
);
229 /** split on node n */
230 bool addSplit( Node n
, bool reqPhase
= false, bool reqPhasePol
= true );
231 /** add split equality */
232 bool addSplitEquality( Node n1
, Node n2
, bool reqPhase
= false, bool reqPhasePol
= true );
233 /** has added lemma */
234 bool hasAddedLemma() { return !d_lemmas_waiting
.empty() || d_hasAddedLemma
; }
236 void flushLemmas( OutputChannel
* out
);
237 /** get number of waiting lemmas */
238 int getNumLemmasWaiting() { return (int)d_lemmas_waiting
.size(); }
240 /** get number of quantifiers */
241 int getNumQuantifiers() { return (int)d_quants
.size(); }
242 /** get quantifier */
243 Node
getQuantifier( int i
) { return d_quants
[i
]; }
245 void setActive( Node n
, bool val
) { d_active
[n
] = val
; }
247 bool getActive( Node n
) { return d_active
.find( n
)!=d_active
.end() && d_active
[n
]; }
249 /** phase requirements for each quantifier for each instantiation literal */
250 std::map
< Node
, std::map
< Node
, bool > > d_phase_reqs
;
251 std::map
< Node
, std::map
< Node
, bool > > d_phase_reqs_equality
;
252 std::map
< Node
, std::map
< Node
, Node
> > d_phase_reqs_equality_term
;
254 /** is phase required */
255 bool isPhaseReq( Node f
, Node lit
) { return d_phase_reqs
[f
].find( lit
)!=d_phase_reqs
[f
].end(); }
256 /** get phase requirement */
257 bool getPhaseReq( Node f
, Node lit
) { return d_phase_reqs
[f
].find( lit
)==d_phase_reqs
[f
].end() ? false : d_phase_reqs
[f
][ lit
]; }
258 /** get term req terms */
259 void getPhaseReqTerms( Node f
, std::vector
< Node
>& nodes
);
260 /** helper functions compute phase requirements */
261 static void computePhaseReqs( Node n
, bool polarity
, std::map
< Node
, bool >& phaseReqs
);
262 /** compute phase requirements */
263 void generatePhaseReqs( Node f
, Node n
);
266 bool hasOwner( Node f
) { return d_owner
.find( f
)!=d_owner
.end(); }
268 Theory
* getOwner( Node f
) { return d_owner
[f
]; }
270 void setOwner( Node f
, Theory
* t
) { d_owner
[f
] = t
; }
273 quantifiers::FirstOrderModel
* getModel() { return d_model
; }
274 /** get term database */
275 quantifiers::TermDb
* getTermDatabase() { return d_term_db
; }
276 /** add term to database */
277 void addTermToDatabase( Node n
, bool withinQuant
= false );
280 void setRelevance( Node s
, int r
);
283 int getRelevance( Node s
) { return d_relevance
.find( s
)==d_relevance
.end() ? -1 : d_relevance
[s
]; }
284 /** get number of quantifiers for symbol s */
285 int getNumQuantifiersForSymbol( Node s
) { return (int)d_syms_quants
[s
].size(); }
287 /** statistics class */
291 IntStat d_instantiation_rounds
;
292 IntStat d_instantiation_rounds_lc
;
293 IntStat d_instantiations
;
294 IntStat d_max_instantiation_level
;
296 IntStat d_total_inst_var
;
297 IntStat d_total_inst_var_unspec
;
298 IntStat d_inst_unspec
;
299 IntStat d_inst_duplicate
;
300 IntStat d_lit_phase_req
;
301 IntStat d_lit_phase_nreq
;
303 IntStat d_simple_triggers
;
304 IntStat d_multi_triggers
;
305 IntStat d_multi_trigger_instantiations
;
306 IntStat d_term_in_termdb
;
307 IntStat d_num_mono_candidates
;
308 IntStat d_num_mono_candidates_new_term
;
309 IntStat d_num_multi_candidates
;
310 IntStat d_mono_candidates_cache_hit
;
311 IntStat d_mono_candidates_cache_miss
;
312 IntStat d_multi_candidates_cache_hit
;
313 IntStat d_multi_candidates_cache_miss
;
316 };/* class QuantifiersEngine::Statistics */
317 Statistics d_statistics
;
320 bool d_optInstCheckDuplicate
;
321 bool d_optInstMakeRepresentative
;
322 bool d_optInstAddSplits
;
323 bool d_optMatchIgnoreModelBasis
;
324 bool d_optInstLimitActive
;
326 };/* class QuantifiersEngine */
330 /** equality query object using theory engine */
331 class EqualityQueryQuantifiersEngine
: public EqualityQuery
334 /** pointer to theory engine */
335 QuantifiersEngine
* d_qe
;
337 EqualityQueryQuantifiersEngine( QuantifiersEngine
* qe
) : d_qe( qe
){}
338 ~EqualityQueryQuantifiersEngine(){}
339 /** general queries about equality */
340 bool hasTerm( Node a
);
341 Node
getRepresentative( Node a
);
342 bool areEqual( Node a
, Node b
);
343 bool areDisequal( Node a
, Node b
);
344 Node
getInternalRepresentative( Node a
);
345 eq::EqualityEngine
* getEngine();
346 void getEquivalenceClass( Node a
, std::vector
< Node
>& eqc
);
347 }; /* EqualityQueryQuantifiersEngine */
349 }/* CVC4::theory namespace */
350 }/* CVC4 namespace */
352 #endif /* __CVC4__THEORY__QUANTIFIERS_ENGINE_H */