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/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
52 class TermEnumeration
;
53 class FirstOrderModel
;
54 class QuantAttributes
;
60 class EqualityInference
;
61 class EqualityQueryQuantifiersEngine
;
62 //modules, these are "subsolvers" of the quantifiers theory.
63 class InstantiationEngine
;
65 class BoundedIntegers
;
66 class QuantConflictFind
;
69 class ConjectureGenerator
;
70 class CegInstantiation
;
72 class AlphaEquivalence
;
74 class QuantEqualityEngine
;
75 class InstStrategyEnum
;
76 class InstStrategyCbqi
;
77 class InstStrategyCegqi
;
79 class QuantAntiSkolem
;
80 class EqualityInference
;
81 }/* CVC4::theory::quantifiers */
85 }/* CVC4::theory::inst */
88 class QuantifiersEngine
{
89 // TODO: remove these github issue #1163
90 friend class quantifiers::InstantiationEngine
;
91 friend class quantifiers::InstStrategyCbqi
;
92 friend class quantifiers::InstStrategyCegqi
;
93 friend class quantifiers::ModelEngine
;
94 friend class quantifiers::RewriteEngine
;
95 friend class quantifiers::QuantConflictFind
;
96 friend class inst::InstMatch
;
97 typedef context::CDHashMap
< Node
, bool, NodeHashFunction
> BoolMap
;
98 typedef context::CDList
<Node
> NodeList
;
99 typedef context::CDList
<bool> BoolList
;
100 typedef context::CDHashSet
<Node
, NodeHashFunction
> NodeSet
;
102 /** reference to theory engine object */
104 /** vector of utilities for quantifiers */
105 std::vector
< QuantifiersUtil
* > d_util
;
106 /** vector of modules for quantifiers */
107 std::vector
< QuantifiersModule
* > d_modules
;
108 /** equality query class */
109 quantifiers::EqualityQueryQuantifiersEngine
* d_eq_query
;
110 /** equality inference class */
111 quantifiers::EqualityInference
* d_eq_inference
;
112 /** for computing relevance of quantifiers */
113 quantifiers::QuantRelevance
* d_quant_rel
;
114 /** relevant domain */
115 quantifiers::RelevantDomain
* d_rel_dom
;
116 /** inversion utility for BV instantiation */
117 quantifiers::BvInverter
* d_bv_invert
;
118 /** alpha equivalence */
119 quantifiers::AlphaEquivalence
* d_alpha_equiv
;
121 quantifiers::QModelBuilder
* d_builder
;
122 /** utility for effectively propositional logic */
123 quantifiers::QuantEPR
* d_qepr
;
125 quantifiers::TermDb
* d_term_db
;
126 /** sygus term database */
127 quantifiers::TermDbSygus
* d_sygus_tdb
;
128 /** term utilities */
129 quantifiers::TermUtil
* d_term_util
;
130 /** quantifiers attributes */
131 std::unique_ptr
<quantifiers::QuantAttributes
> d_quant_attr
;
132 /** instantiate utility */
133 std::unique_ptr
<quantifiers::Instantiate
> d_instantiate
;
134 /** skolemize utility */
135 std::unique_ptr
<quantifiers::Skolemize
> d_skolemize
;
136 /** term enumeration utility */
137 std::unique_ptr
<quantifiers::TermEnumeration
> d_term_enum
;
138 /** instantiation engine */
139 quantifiers::InstantiationEngine
* d_inst_engine
;
141 quantifiers::ModelEngine
* d_model_engine
;
142 /** bounded integers utility */
143 quantifiers::BoundedIntegers
* d_bint
;
144 /** Conflict find mechanism for quantifiers */
145 quantifiers::QuantConflictFind
* d_qcf
;
146 /** rewrite rules utility */
147 quantifiers::RewriteEngine
* d_rr_engine
;
148 /** subgoal generator */
149 quantifiers::ConjectureGenerator
* d_sg_gen
;
150 /** ceg instantiation */
151 quantifiers::CegInstantiation
* d_ceg_inst
;
152 /** lte partial instantiation */
153 quantifiers::LtePartialInst
* d_lte_part_inst
;
154 /** function definitions engine */
155 quantifiers::FunDefEngine
* d_fun_def_engine
;
156 /** quantifiers equality engine */
157 quantifiers::QuantEqualityEngine
* d_uee
;
158 /** full saturation */
159 quantifiers::InstStrategyEnum
* d_fs
;
160 /** counterexample-based quantifier instantiation */
161 quantifiers::InstStrategyCbqi
* d_i_cbqi
;
162 /** quantifiers splitting */
163 quantifiers::QuantDSplit
* d_qsplit
;
164 /** quantifiers anti-skolemization */
165 quantifiers::QuantAntiSkolem
* d_anti_skolem
;
166 /** quantifiers instantiation propagtor */
167 quantifiers::InstPropagator
* d_inst_prop
;
169 private: //this information is reset during check
170 /** current effort level */
171 QuantifiersModule::QEffort d_curr_effort_level
;
172 /** are we in conflict */
174 context::CDO
<bool> d_conflict_c
;
175 /** has added lemma this round */
176 bool d_hasAddedLemma
;
177 /** whether to use model equality engine */
180 /** list of all quantifiers seen */
181 std::map
< Node
, bool > d_quants
;
182 /** quantifiers reduced */
183 BoolMap d_quants_red
;
184 std::map
< Node
, Node
> d_quants_red_lem
;
185 /** list of all lemmas produced */
186 //std::map< Node, bool > d_lemmas_produced;
187 BoolMap d_lemmas_produced_c
;
188 /** lemmas waiting */
189 std::vector
< Node
> d_lemmas_waiting
;
190 /** phase requirements waiting */
191 std::map
< Node
, bool > d_phase_req_waiting
;
192 /** all triggers will be stored in this trie */
193 inst::TriggerTrie
* d_tr_trie
;
194 /** extended model object */
195 quantifiers::FirstOrderModel
* d_model
;
196 /** inst round counters TODO: make context-dependent? */
197 context::CDO
< int > d_ierCounter_c
;
200 int d_ierCounterLastLc
;
201 int d_inst_when_phase
;
202 /** has presolve been called */
203 context::CDO
< bool > d_presolve
;
204 /** presolve cache */
205 NodeSet d_presolve_in
;
206 NodeList d_presolve_cache
;
207 BoolList d_presolve_cache_wq
;
208 BoolList d_presolve_cache_wic
;
211 QuantifiersEngine(context::Context
* c
, context::UserContext
* u
, TheoryEngine
* te
);
212 ~QuantifiersEngine();
213 /** get theory engine */
214 TheoryEngine
* getTheoryEngine() { return d_te
; }
215 /** get equality query */
216 EqualityQuery
* getEqualityQuery();
217 /** get the equality inference */
218 quantifiers::EqualityInference
* getEqualityInference() { return d_eq_inference
; }
219 /** get default sat context for quantifiers engine */
220 context::Context
* getSatContext();
221 /** get default sat context for quantifiers engine */
222 context::UserContext
* getUserContext();
223 /** get default output channel for the quantifiers engine */
224 OutputChannel
& getOutputChannel();
225 /** get default valuation for the quantifiers engine */
226 Valuation
& getValuation();
227 /** get relevant domain */
228 quantifiers::RelevantDomain
* getRelevantDomain() { return d_rel_dom
; }
229 /** get the BV inverter utility */
230 quantifiers::BvInverter
* getBvInverter() { return d_bv_invert
; }
231 /** get quantifier relevance */
232 quantifiers::QuantRelevance
* getQuantifierRelevance() { return d_quant_rel
; }
233 /** get the model builder */
234 quantifiers::QModelBuilder
* getModelBuilder() { return d_builder
; }
235 /** get utility for EPR */
236 quantifiers::QuantEPR
* getQuantEPR() { return d_qepr
; }
238 /** get instantiation engine */
239 quantifiers::InstantiationEngine
* getInstantiationEngine() { return d_inst_engine
; }
240 /** get model engine */
241 quantifiers::ModelEngine
* getModelEngine() { return d_model_engine
; }
242 /** get bounded integers utility */
243 quantifiers::BoundedIntegers
* getBoundedIntegers() { return d_bint
; }
244 /** Conflict find mechanism for quantifiers */
245 quantifiers::QuantConflictFind
* getConflictFind() { return d_qcf
; }
246 /** rewrite rules utility */
247 quantifiers::RewriteEngine
* getRewriteEngine() { return d_rr_engine
; }
248 /** subgoal generator */
249 quantifiers::ConjectureGenerator
* getConjectureGenerator() { return d_sg_gen
; }
250 /** ceg instantiation */
251 quantifiers::CegInstantiation
* getCegInstantiation() { return d_ceg_inst
; }
252 /** local theory ext partial inst */
253 quantifiers::LtePartialInst
* getLtePartialInst() { return d_lte_part_inst
; }
254 /** function definition engine */
255 quantifiers::FunDefEngine
* getFunDefEngine() { return d_fun_def_engine
; }
256 /** quantifiers equality engine */
257 quantifiers::QuantEqualityEngine
* getQuantEqualityEngine() { return d_uee
; }
258 /** get full saturation */
259 quantifiers::InstStrategyEnum
* getInstStrategyEnum() { return d_fs
; }
260 /** get inst strategy cbqi */
261 quantifiers::InstStrategyCbqi
* getInstStrategyCbqi() { return d_i_cbqi
; }
262 /** get quantifiers splitting */
263 quantifiers::QuantDSplit
* getQuantDSplit() { return d_qsplit
; }
264 /** get quantifiers anti-skolemization */
265 quantifiers::QuantAntiSkolem
* getQuantAntiSkolem() { return d_anti_skolem
; }
267 /** owner of quantified formulas */
268 std::map
< Node
, QuantifiersModule
* > d_owner
;
269 std::map
< Node
, int > d_owner_priority
;
272 QuantifiersModule
* getOwner( Node q
);
274 void setOwner( Node q
, QuantifiersModule
* m
, int priority
= 0 );
276 bool hasOwnership( Node q
, QuantifiersModule
* m
= NULL
);
277 /** is finite bound */
278 bool isFiniteBound( Node q
, Node v
);
282 /** notify preprocessed assertion */
283 void ppNotifyAssertions(const std::vector
<Node
>& assertions
);
284 /** check at level */
285 void check( Theory::Effort e
);
286 /** notify that theories were combined */
287 void notifyCombineTheories();
288 /** register quantifier */
289 bool registerQuantifier( Node f
);
290 /** register quantifier */
291 void registerPattern( std::vector
<Node
> & pattern
);
292 /** assert universal quantifier */
293 void assertQuantifier( Node q
, bool pol
);
295 void propagate( Theory::Effort level
);
296 /** get next decision request */
297 Node
getNextDecisionRequest( unsigned& priority
);
299 /** reduceQuantifier, return true if reduced */
300 bool reduceQuantifier( Node q
);
305 bool addLemma( Node lem
, bool doCache
= true, bool doRewrite
= true );
306 /** remove pending lemma */
307 bool removeLemma( Node lem
);
308 /** add require phase */
309 void addRequirePhase( Node lit
, bool req
);
310 /** split on node n */
311 bool addSplit( Node n
, bool reqPhase
= false, bool reqPhasePol
= true );
312 /** add split equality */
313 bool addSplitEquality( Node n1
, Node n2
, bool reqPhase
= false, bool reqPhasePol
= true );
315 bool addEPRAxiom( TypeNode tn
);
316 /** mark relevant quantified formula, this will indicate it should be checked before the others */
317 void markRelevant( Node q
);
318 /** has added lemma */
319 bool hasAddedLemma() { return !d_lemmas_waiting
.empty() || d_hasAddedLemma
; }
320 /** is in conflict */
321 bool inConflict() { return d_conflict
; }
324 /** get current q effort */
325 QuantifiersModule::QEffort
getCurrentQEffort() { return d_curr_effort_level
; }
326 /** get number of waiting lemmas */
327 unsigned getNumLemmasWaiting() { return d_lemmas_waiting
.size(); }
328 /** get needs check */
329 bool getInstWhenNeedsCheck( Theory::Effort e
);
330 /** get user pat mode */
331 quantifiers::UserPatMode
getInstUserPatMode();
334 quantifiers::FirstOrderModel
* getModel() { return d_model
; }
335 /** get term database */
336 quantifiers::TermDb
* getTermDatabase() { return d_term_db
; }
337 /** get term database sygus */
338 quantifiers::TermDbSygus
* getTermDatabaseSygus() { return d_sygus_tdb
; }
339 /** get term utilities */
340 quantifiers::TermUtil
* getTermUtil() { return d_term_util
; }
341 /** get quantifiers attributes */
342 quantifiers::QuantAttributes
* getQuantAttributes() {
343 return d_quant_attr
.get();
345 /** get instantiate utility */
346 quantifiers::Instantiate
* getInstantiate() { return d_instantiate
.get(); }
347 /** get skolemize utility */
348 quantifiers::Skolemize
* getSkolemize() { return d_skolemize
.get(); }
349 /** get term enumeration utility */
350 quantifiers::TermEnumeration
* getTermEnumeration()
352 return d_term_enum
.get();
354 /** get trigger database */
355 inst::TriggerTrie
* getTriggerDatabase() { return d_tr_trie
; }
356 /** add term to database */
357 void addTermToDatabase( Node n
, bool withinQuant
= false, bool withinInstClosure
= false );
358 /** notification when master equality engine is updated */
359 void eqNotifyNewClass(TNode t
);
360 void eqNotifyPreMerge(TNode t1
, TNode t2
);
361 void eqNotifyPostMerge(TNode t1
, TNode t2
);
362 void eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
);
363 /** get the master equality engine */
364 eq::EqualityEngine
* getMasterEqualityEngine();
365 /** get the active equality engine */
366 eq::EqualityEngine
* getActiveEqualityEngine();
367 /** use model equality engine */
368 bool usingModelEqualityEngine() const { return d_useModelEe
; }
369 /** debug print equality engine */
370 void debugPrintEqualityEngine( const char * c
);
371 /** get internal representative */
372 Node
getInternalRepresentative( Node a
, Node q
, int index
);
375 //----------user interface for instantiations (see quantifiers/instantiate.h)
376 /** print instantiations */
377 void printInstantiations(std::ostream
& out
);
378 /** print solution for synthesis conjectures */
379 void printSynthSolution(std::ostream
& out
);
380 /** get list of quantified formulas that were instantiated */
381 void getInstantiatedQuantifiedFormulas(std::vector
<Node
>& qs
);
382 /** get instantiations */
383 void getInstantiations(Node q
, std::vector
<Node
>& insts
);
384 void getInstantiations(std::map
<Node
, std::vector
<Node
> >& insts
);
385 /** get instantiation term vectors */
386 void getInstantiationTermVectors(Node q
,
387 std::vector
<std::vector
<Node
> >& tvecs
);
388 void getInstantiationTermVectors(
389 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
,
395 std::map
<Node
, Node
>& weak_imp
);
396 /** get explanation for instantiation lemmas */
397 void getExplanationForInstLemmas(const std::vector
<Node
>& lems
,
398 std::map
<Node
, Node
>& quant
,
399 std::map
<Node
, std::vector
<Node
> >& tvec
);
401 /** get synth solutions
403 * This function adds entries to sol_map that map functions-to-synthesize with
404 * their solutions, for all active conjectures. This should be called
405 * immediately after the solver answers unsat for sygus input.
407 * For details on what is added to sol_map, see
408 * CegConjecture::getSynthSolutions.
410 void getSynthSolutions(std::map
<Node
, Node
>& sol_map
);
412 //----------end user interface for instantiations
414 /** statistics class */
418 TimerStat d_qcf_time
;
419 TimerStat d_ematching_time
;
421 IntStat d_instantiation_rounds
;
422 IntStat d_instantiation_rounds_lc
;
424 IntStat d_simple_triggers
;
425 IntStat d_multi_triggers
;
426 IntStat d_multi_trigger_instantiations
;
427 IntStat d_red_alpha_equiv
;
428 IntStat d_instantiations_user_patterns
;
429 IntStat d_instantiations_auto_gen
;
430 IntStat d_instantiations_guess
;
431 IntStat d_instantiations_qcf
;
432 IntStat d_instantiations_qcf_prop
;
433 IntStat d_instantiations_fmf_exh
;
434 IntStat d_instantiations_fmf_mbqi
;
435 IntStat d_instantiations_cbqi
;
436 IntStat d_instantiations_rr
;
439 };/* class QuantifiersEngine::Statistics */
440 Statistics d_statistics
;
441 };/* class QuantifiersEngine */
443 }/* CVC4::theory namespace */
444 }/* CVC4 namespace */
446 #endif /* __CVC4__THEORY__QUANTIFIERS_ENGINE_H */