1 /********************* */
2 /*! \file conjecture_generator.h
4 ** Original author: Andrew Reynolds
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 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 conjecture generator class
15 #include "cvc4_private.h"
17 #ifndef CONJECTURE_GENERATOR_H
18 #define CONJECTURE_GENERATOR_H
20 #include "context/cdhashmap.h"
21 #include "context/cdchunk_list.h"
22 #include "theory/quantifiers_engine.h"
23 #include "theory/type_enumerator.h"
27 namespace quantifiers
{
31 //algorithm for computing candidate subgoals
33 class ConjectureGenerator
;
35 // operator independent index of arguments for an EQC
39 std::map
< TNode
, OpArgIndex
> d_child
;
40 std::vector
< TNode
> d_ops
;
41 std::vector
< TNode
> d_op_terms
;
42 void addTerm( ConjectureGenerator
* s
, TNode n
, unsigned index
= 0 );
43 Node
getGroundTerm( ConjectureGenerator
* s
, std::vector
< TNode
>& args
);
44 void getGroundTerms( ConjectureGenerator
* s
, std::vector
< TNode
>& terms
);
50 std::vector
< TNode
> d_terms
;
51 std::map
< TypeNode
, std::map
< unsigned, PatternTypIndex
> > d_children
;
58 class SubstitutionIndex
61 //current variable, or ground EQC if d_children.empty()
63 std::map
< TNode
, SubstitutionIndex
> d_children
;
65 void addSubstitution( TNode eqc
, std::vector
< TNode
>& vars
, std::vector
< TNode
>& terms
, unsigned i
= 0 );
66 //notify substitutions
67 bool notifySubstitutions( ConjectureGenerator
* s
, std::map
< TNode
, TNode
>& subs
, TNode rhs
, unsigned numVars
, unsigned i
= 0 );
75 unsigned calculateGeneralizationDepth( TermGenEnv
* s
, std::map
< TypeNode
, std::vector
< int > >& fvs
);
80 //1 : consider as unique variable
81 //2 : consider equal to another variable
82 //5 : consider a function application
85 //for function applications: the number of children you have built
86 int d_status_child_num
;
87 //children (pointers to TermGenerators)
88 std::vector
< unsigned > d_children
;
92 int d_match_status_child_num
;
94 //0 : different variables must have different matches
95 //1 : variables must map to ground terms
96 //2 : variables must map to non-ground terms
97 unsigned d_match_mode
;
99 std::vector
< std::map
< TNode
, TermArgTrie
>::iterator
> d_match_children
;
100 std::vector
< std::map
< TNode
, TermArgTrie
>::iterator
> d_match_children_end
;
102 void reset( TermGenEnv
* s
, TypeNode tn
);
103 bool getNextTerm( TermGenEnv
* s
, unsigned depth
);
104 void resetMatching( TermGenEnv
* s
, TNode eqc
, unsigned mode
);
105 bool getNextMatch( TermGenEnv
* s
, TNode eqc
, std::map
< TypeNode
, std::map
< unsigned, TNode
> >& subs
, std::map
< TNode
, bool >& rev_subs
);
107 unsigned getDepth( TermGenEnv
* s
);
108 unsigned getGeneralizationDepth( TermGenEnv
* s
);
109 Node
getTerm( TermGenEnv
* s
);
111 void debugPrint( TermGenEnv
* s
, const char * c
, const char * cd
);
118 //collect signature information
119 void collectSignatureInformation();
121 void reset( unsigned gdepth
, bool genRelevant
, TypeNode tgen
);
125 void resetMatching( TNode eqc
, unsigned mode
);
127 bool getNextMatch( TNode eqc
, std::map
< TypeNode
, std::map
< unsigned, TNode
> >& subs
, std::map
< TNode
, bool >& rev_subs
);
131 void debugPrint( const char * c
, const char * cd
);
133 //conjecture generation
134 ConjectureGenerator
* d_cg
;
135 //the current number of enumerated variables per type
136 std::map
< TypeNode
, unsigned > d_var_id
;
137 //the limit of number of variables per type to enumerate
138 std::map
< TypeNode
, unsigned > d_var_limit
;
139 //the functions we can currently generate
140 std::map
< TypeNode
, std::vector
< TNode
> > d_typ_tg_funcs
;
141 //the equivalence classes (if applicable) that match the currently generated term
142 bool d_gen_relevant_terms
;
143 //relevant equivalence classes
144 std::vector
< TNode
> d_relevant_eqc
[2];
145 //candidate equivalence classes
146 std::vector
< std::vector
< TNode
> > d_ccand_eqc
[2];
147 //the term generation objects
149 std::map
< unsigned, TermGenerator
> d_tg_alloc
;
150 unsigned d_tg_gdepth
;
151 int d_tg_gdepth_limit
;
154 std::vector
< TNode
> d_funcs
;
155 //function to kind map
156 std::map
< TNode
, Kind
> d_func_kind
;
157 //type of each argument of the function
158 std::map
< TNode
, std::vector
< TypeNode
> > d_func_args
;
161 unsigned getNumTgVars( TypeNode tn
);
162 bool allowVar( TypeNode tn
);
163 void addVar( TypeNode tn
);
164 void removeVar( TypeNode tn
);
165 unsigned getNumTgFuncs( TypeNode tn
);
166 TNode
getTgFunc( TypeNode tn
, unsigned i
);
167 Node
getFreeVar( TypeNode tn
, unsigned i
);
168 bool considerCurrentTerm();
169 bool considerCurrentTermCanon( unsigned tg_id
);
170 void changeContext( bool add
);
171 bool isRelevantFunc( Node f
);
173 TermDb
* getTermDatabase();
174 Node
getGroundEqc( TNode r
);
175 bool isGroundEqc( TNode r
);
176 bool isGroundTerm( TNode n
);
184 void addTheorem( std::vector
< TNode
>& lhs_v
, std::vector
< unsigned >& lhs_arg
, TNode rhs
);
185 void addTheoremNode( TNode curr
, std::vector
< TNode
>& lhs_v
, std::vector
< unsigned >& lhs_arg
, TNode rhs
);
186 void getEquivalentTerms( std::vector
< TNode
>& n_v
, std::vector
< unsigned >& n_arg
,
187 std::map
< TNode
, TNode
>& smap
, std::vector
< TNode
>& vars
, std::vector
< TNode
>& subs
,
188 std::vector
< Node
>& terms
);
189 void getEquivalentTermsNode( Node curr
, std::vector
< TNode
>& n_v
, std::vector
< unsigned >& n_arg
,
190 std::map
< TNode
, TNode
>& smap
, std::vector
< TNode
>& vars
, std::vector
< TNode
>& subs
,
191 std::vector
< Node
>& terms
);
193 std::map
< TypeNode
, TNode
> d_var
;
194 std::map
< TNode
, TheoremIndex
> d_children
;
195 std::vector
< Node
> d_terms
;
197 void addTheorem( TNode lhs
, TNode rhs
) {
198 std::vector
< TNode
> v
;
199 std::vector
< unsigned > a
;
200 addTheoremNode( lhs
, v
, a
, rhs
);
202 void getEquivalentTerms( TNode n
, std::vector
< Node
>& terms
) {
203 std::vector
< TNode
> nv
;
204 std::vector
< unsigned > na
;
205 std::map
< TNode
, TNode
> smap
;
206 std::vector
< TNode
> vars
;
207 std::vector
< TNode
> subs
;
208 getEquivalentTermsNode( n
, nv
, na
, smap
, vars
, subs
, terms
);
215 void debugPrint( const char * c
, unsigned ind
= 0 );
220 class ConjectureGenerator
: public QuantifiersModule
222 friend class OpArgIndex
;
224 friend class PatternGenEqc
;
225 friend class PatternGen
;
226 friend class SubsEqcIndex
;
227 friend class TermGenerator
;
228 friend class TermGenEnv
;
229 typedef context::CDChunkList
<Node
> NodeList
;
230 typedef context::CDHashMap
< Node
, Node
, NodeHashFunction
> NodeMap
;
231 typedef context::CDHashMap
< Node
, bool, NodeHashFunction
> BoolMap
;
232 //this class maintains a congruence closure for *universal* facts
234 //notification class for equality engine
235 class NotifyClass
: public eq::EqualityEngineNotify
{
236 ConjectureGenerator
& d_sg
;
238 NotifyClass(ConjectureGenerator
& sg
): d_sg(sg
) {}
239 bool eqNotifyTriggerEquality(TNode equality
, bool value
) { return true; }
240 bool eqNotifyTriggerPredicate(TNode predicate
, bool value
) { return true; }
241 bool eqNotifyTriggerTermEquality(TheoryId tag
, TNode t1
, TNode t2
, bool value
) { return true; }
242 void eqNotifyConstantTermMerge(TNode t1
, TNode t2
) { }
243 void eqNotifyNewClass(TNode t
) { d_sg
.eqNotifyNewClass(t
); }
244 void eqNotifyPreMerge(TNode t1
, TNode t2
) { d_sg
.eqNotifyPreMerge(t1
, t2
); }
245 void eqNotifyPostMerge(TNode t1
, TNode t2
) { d_sg
.eqNotifyPostMerge(t1
, t2
); }
246 void eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
) {d_sg
.eqNotifyDisequal(t1
, t2
, reason
); }
247 };/* class ConjectureGenerator::NotifyClass */
248 /** The notify class */
249 NotifyClass d_notify
;
252 EqcInfo( context::Context
* c
);
254 context::CDO
< Node
> d_rep
;
256 /** get or make eqc info */
257 EqcInfo
* getOrMakeEqcInfo( TNode n
, bool doMake
= false );
258 /** (universal) equaltity engine */
259 eq::EqualityEngine d_uequalityEngine
;
261 std::vector
< Node
> d_upendingAdds
;
262 /** relevant terms */
263 std::map
< Node
, bool > d_urelevant_terms
;
264 /** information necessary for equivalence classes */
265 std::map
< Node
, EqcInfo
* > d_eqc_info
;
266 /** called when a new equivalance class is created */
267 void eqNotifyNewClass(TNode t
);
268 /** called when two equivalance classes will merge */
269 void eqNotifyPreMerge(TNode t1
, TNode t2
);
270 /** called when two equivalance classes have merged */
271 void eqNotifyPostMerge(TNode t1
, TNode t2
);
272 /** called when two equivalence classes are made disequal */
273 void eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
);
274 /** are universal equal */
275 bool areUniversalEqual( TNode n1
, TNode n2
);
276 /** are universal disequal */
277 bool areUniversalDisequal( TNode n1
, TNode n2
);
278 /** get universal representative */
279 TNode
getUniversalRepresentative( TNode n
, bool add
= false );
281 void setUniversalRelevant( TNode n
);
282 /** ordering for universal terms */
283 bool isUniversalLessThan( TNode rt1
, TNode rt2
);
285 /** the nodes we have reported as canonical representative */
286 std::vector
< TNode
> d_ue_canon
;
287 /** is reported canon */
288 bool isReportedCanon( TNode n
);
289 /** mark that term has been reported as canonical rep */
290 void markReportedCanon( TNode n
);
292 private: //information regarding the conjectures
293 /** list of all conjectures */
294 std::vector
< Node
> d_conjectures
;
295 /** list of all waiting conjectures */
296 std::vector
< Node
> d_waiting_conjectures_lhs
;
297 std::vector
< Node
> d_waiting_conjectures_rhs
;
298 std::vector
< int > d_waiting_conjectures_score
;
299 /** map of currently considered equality conjectures */
300 std::map
< Node
, std::vector
< Node
> > d_waiting_conjectures
;
301 /** map of equality conjectures */
302 std::map
< Node
, std::vector
< Node
> > d_eq_conjectures
;
303 /** currently existing conjectures in equality engine */
304 BoolMap d_ee_conjectures
;
305 /** conjecture index */
306 TheoremIndex d_thm_index
;
307 private: //free variable list
309 std::map
< TypeNode
, std::vector
< Node
> > d_free_var
;
310 //map from free variable to FV#
311 std::map
< TNode
, unsigned > d_free_var_num
;
312 // get canonical free variable #i of type tn
313 Node
getFreeVar( TypeNode tn
, unsigned i
);
314 // get canonical term, return null if it contains a term apart from handled signature
315 Node
getCanonicalTerm( TNode n
, std::map
< TypeNode
, unsigned >& var_count
, std::map
< TNode
, TNode
>& subs
);
316 private: //information regarding the terms
317 //relevant patterns (the LHS's)
318 std::map
< TypeNode
, std::vector
< Node
> > d_rel_patterns
;
319 //total number of unique variables
320 std::map
< TNode
, unsigned > d_rel_pattern_var_sum
;
322 PatternTypIndex d_rel_pattern_typ_index
;
323 // substitution to ground EQC index
324 std::map
< TNode
, SubstitutionIndex
> d_rel_pattern_subs_index
;
325 //patterns (the RHS's)
326 std::map
< TypeNode
, std::vector
< Node
> > d_patterns
;
327 //patterns to # variables per type
328 std::map
< TNode
, std::map
< TypeNode
, unsigned > > d_pattern_var_id
;
329 // # duplicated variables
330 std::map
< TNode
, unsigned > d_pattern_var_duplicate
;
331 // is normal pattern? (variables allocated in canonical way left to right)
332 std::map
< TNode
, int > d_pattern_is_normal
;
333 std::map
< TNode
, int > d_pattern_is_relevant
;
334 // patterns to a count of # operators (variables and functions)
335 std::map
< TNode
, std::map
< TNode
, unsigned > > d_pattern_fun_id
;
337 std::map
< TNode
, unsigned > d_pattern_fun_sum
;
339 unsigned collectFunctions( TNode opat
, TNode pat
, std::map
< TNode
, unsigned >& funcs
,
340 std::map
< TypeNode
, unsigned >& mnvn
, std::map
< TypeNode
, unsigned >& mxvn
);
342 void registerPattern( Node pat
, TypeNode tpat
);
343 private: //for debugging
344 std::map
< TNode
, unsigned > d_em
;
346 //term generation environment
348 //consider term canon
349 bool considerTermCanon( Node ln
, bool genRelevant
);
350 public: //for generalization
352 bool isGeneralization( TNode patg
, TNode pat
) {
353 std::map
< TNode
, TNode
> subs
;
354 return isGeneralization( patg
, pat
, subs
);
356 bool isGeneralization( TNode patg
, TNode pat
, std::map
< TNode
, TNode
>& subs
);
357 // get generalization depth
358 int calculateGeneralizationDepth( TNode n
, std::vector
< TNode
>& fv
);
360 //ground term enumeration
361 std::map
< TypeNode
, std::vector
< Node
> > d_enum_terms
;
363 std::map
< TypeNode
, unsigned > d_typ_enum_map
;
364 std::vector
< TypeEnumerator
> d_typ_enum
;
365 //get nth term for type
366 Node
getEnumerateTerm( TypeNode tn
, unsigned index
);
368 std::map
< TypeNode
, Node
> d_typ_pred
;
369 //get predicate for type
370 Node
getPredicateForType( TypeNode tn
);
372 void getEnumerateUfTerm( Node n
, unsigned num
, std::vector
< Node
>& terms
);
374 void getEnumeratePredUfTerm( Node n
, unsigned num
, std::vector
< Node
>& terms
);
375 // uf operators enumerated
376 std::map
< Node
, bool > d_uf_enum
;
377 public: //for property enumeration
378 //process this candidate conjecture
379 void processCandidateConjecture( TNode lhs
, TNode rhs
, unsigned lhs_depth
, unsigned rhs_depth
);
380 //whether it should be considered, negative : no, positive returns score
381 int considerCandidateConjecture( TNode lhs
, TNode rhs
);
382 //notified of a substitution
383 bool notifySubstitution( TNode glhs
, std::map
< TNode
, TNode
>& subs
, TNode rhs
);
385 unsigned d_subs_confirmCount
;
386 //individual witnesses (for range)
387 std::vector
< TNode
> d_subs_confirmWitnessRange
;
388 //individual witnesses (for domain)
389 std::map
< TNode
, std::vector
< TNode
> > d_subs_confirmWitnessDomain
;
390 //number of ground substitutions whose equality is unknown
391 unsigned d_subs_unkCount
;
392 public: //for ground equivalence classes
393 eq::EqualityEngine
* getEqualityEngine();
394 bool areDisequal( TNode n1
, TNode n2
);
395 bool areEqual( TNode n1
, TNode n2
);
396 TNode
getRepresentative( TNode n
);
397 TermDb
* getTermDatabase();
398 private: //information about ground equivalence classes
400 std::map
< TNode
, Node
> d_ground_eqc_map
;
401 std::vector
< TNode
> d_ground_terms
;
402 //operator independent term index
403 std::map
< TNode
, OpArgIndex
> d_op_arg_index
;
405 bool isHandledTerm( TNode n
);
406 Node
getGroundEqc( TNode r
);
407 bool isGroundEqc( TNode r
);
408 bool isGroundTerm( TNode n
);
410 bool hasEnumeratedUf( Node n
);
411 // count of full effort checks
412 unsigned d_fullEffortCount
;
414 bool d_hasAddedLemma
;
415 //flush the waiting conjectures
416 unsigned flushWaitingConjectures( unsigned& addedLemmas
, int ldepth
, int rdepth
);
418 ConjectureGenerator( QuantifiersEngine
* qe
, context::Context
* c
);
420 bool needsCheck( Theory::Effort e
);
421 /* reset at a round */
422 void reset_round( Theory::Effort e
);
423 /* Call during quantifier engine's check */
424 void check( Theory::Effort e
, unsigned quant_e
);
425 /* Called for new quantifiers */
426 void registerQuantifier( Node q
);
427 void assertNode( Node n
);
428 /** Identify this module (for debugging, dynamic configuration, etc..) */
429 std::string
identify() const { return "ConjectureGenerator"; }
432 bool optReqDistinctVarPatterns();
433 bool optFilterUnknown();
434 int optFilterScoreThreshold();
435 unsigned optFullCheckFrequency();
436 unsigned optFullCheckConjectures();