Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Mathias Preiner, Tim King
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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.
11 : : * ****************************************************************************
12 : : *
13 : : * conjecture generator class
14 : : */
15 : :
16 : : #include "cvc5_private.h"
17 : :
18 : : #ifndef CONJECTURE_GENERATOR_H
19 : : #define CONJECTURE_GENERATOR_H
20 : :
21 : : #include "context/cdhashmap.h"
22 : : #include "expr/node_trie.h"
23 : : #include "expr/term_canonize.h"
24 : : #include "smt/env_obj.h"
25 : : #include "theory/quantifiers/quant_module.h"
26 : : #include "theory/type_enumerator.h"
27 : :
28 : : namespace cvc5::internal {
29 : : namespace theory {
30 : : namespace quantifiers {
31 : :
32 : : //algorithm for computing candidate subgoals
33 : :
34 : : class ConjectureGenerator;
35 : :
36 : : // operator independent index of arguments for an EQC
37 : : class OpArgIndex
38 : : {
39 : : public:
40 : : std::map< TNode, OpArgIndex > d_child;
41 : : std::vector< TNode > d_ops;
42 : : std::vector< TNode > d_op_terms;
43 : : void addTerm( std::vector< TNode >& terms, TNode n, unsigned index = 0 );
44 : : Node getGroundTerm( ConjectureGenerator * s, std::vector< TNode >& args );
45 : : void getGroundTerms( ConjectureGenerator * s, std::vector< TNode >& terms );
46 : : };
47 : :
48 : : class PatternTypIndex
49 : : {
50 : : public:
51 : : std::vector< TNode > d_terms;
52 : : std::map< TypeNode, std::map< unsigned, PatternTypIndex > > d_children;
53 : 68 : void clear() {
54 : 68 : d_terms.clear();
55 : 68 : d_children.clear();
56 : 68 : }
57 : : };
58 : :
59 : : class SubstitutionIndex
60 : : {
61 : : public:
62 : : //current variable, or ground EQC if d_children.empty()
63 : : TNode d_var;
64 : : std::map< TNode, SubstitutionIndex > d_children;
65 : : //add substitution
66 : : void addSubstitution( TNode eqc, std::vector< TNode >& vars, std::vector< TNode >& terms, unsigned i = 0 );
67 : : //notify substitutions
68 : : bool notifySubstitutions( ConjectureGenerator * s, std::map< TNode, TNode >& subs, TNode rhs, unsigned numVars, unsigned i = 0 );
69 : : };
70 : :
71 : : class TermGenEnv;
72 : :
73 : : class TermGenerator
74 : : {
75 : : private:
76 : : unsigned calculateGeneralizationDepth( TermGenEnv * s, std::map< TypeNode, std::vector< int > >& fvs );
77 : :
78 : : public:
79 : 6150 : TermGenerator()
80 : 6150 : : d_id(0),
81 : : d_status(0),
82 : : d_status_num(0),
83 : : d_status_child_num(0),
84 : : d_match_status(0),
85 : : d_match_status_child_num(0),
86 : 6150 : d_match_mode(0)
87 : : {
88 : 6150 : }
89 : : TypeNode d_typ;
90 : : unsigned d_id;
91 : : //1 : consider as unique variable
92 : : //2 : consider equal to another variable
93 : : //5 : consider a function application
94 : : unsigned d_status;
95 : : int d_status_num;
96 : : //for function applications: the number of children you have built
97 : : int d_status_child_num;
98 : : //children (pointers to TermGenerators)
99 : : std::vector< unsigned > d_children;
100 : :
101 : : //match status
102 : : int d_match_status;
103 : : int d_match_status_child_num;
104 : : //match mode bits
105 : : //0 : different variables must have different matches
106 : : //1 : variables must map to ground terms
107 : : //2 : variables must map to non-ground terms
108 : : unsigned d_match_mode;
109 : : //children
110 : : std::vector<std::map<TNode, TNodeTrie>::iterator> d_match_children;
111 : : std::vector<std::map<TNode, TNodeTrie>::iterator> d_match_children_end;
112 : :
113 : : void reset( TermGenEnv * s, TypeNode tn );
114 : : bool getNextTerm( TermGenEnv * s, unsigned depth );
115 : : void resetMatching( TermGenEnv * s, TNode eqc, unsigned mode );
116 : : bool getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode, std::map< unsigned, TNode > >& subs, std::map< TNode, bool >& rev_subs );
117 : :
118 : : unsigned getDepth( TermGenEnv * s );
119 : : unsigned getGeneralizationDepth( TermGenEnv * s );
120 : : Node getTerm( TermGenEnv * s );
121 : :
122 : : void debugPrint( TermGenEnv * s, const char * c, const char * cd );
123 : : };
124 : :
125 : :
126 : : class TermGenEnv
127 : : {
128 : : public:
129 : : //collect signature information
130 : : void collectSignatureInformation();
131 : : //reset function
132 : : void reset( unsigned gdepth, bool genRelevant, TypeNode tgen );
133 : : //get next term
134 : : bool getNextTerm();
135 : : //reset matching
136 : : void resetMatching( TNode eqc, unsigned mode );
137 : : //get next match
138 : : bool getNextMatch( TNode eqc, std::map< TypeNode, std::map< unsigned, TNode > >& subs, std::map< TNode, bool >& rev_subs );
139 : : //get term
140 : : Node getTerm();
141 : : //debug print
142 : : void debugPrint( const char * c, const char * cd );
143 : :
144 : : //conjecture generation
145 : : ConjectureGenerator * d_cg;
146 : : //the current number of enumerated variables per type
147 : : std::map< TypeNode, unsigned > d_var_id;
148 : : //the limit of number of variables per type to enumerate
149 : : std::map< TypeNode, unsigned > d_var_limit;
150 : : //the functions we can currently generate
151 : : std::map< TypeNode, std::vector< TNode > > d_typ_tg_funcs;
152 : : // whether functions must add operators
153 : : std::map< TNode, bool > d_tg_func_param;
154 : : //the equivalence classes (if applicable) that match the currently generated term
155 : : bool d_gen_relevant_terms;
156 : : //relevant equivalence classes
157 : : std::vector< TNode > d_relevant_eqc[2];
158 : : //candidate equivalence classes
159 : : std::vector< std::vector< TNode > > d_ccand_eqc[2];
160 : : //the term generation objects
161 : : unsigned d_tg_id;
162 : : std::map< unsigned, TermGenerator > d_tg_alloc;
163 : : unsigned d_tg_gdepth;
164 : : int d_tg_gdepth_limit;
165 : :
166 : : //all functions
167 : : std::vector< TNode > d_funcs;
168 : : //function to kind map
169 : : std::map< TNode, Kind > d_func_kind;
170 : : //type of each argument of the function
171 : : std::map< TNode, std::vector< TypeNode > > d_func_args;
172 : :
173 : : //access functions
174 : : unsigned getNumTgVars( TypeNode tn );
175 : : bool allowVar( TypeNode tn );
176 : : void addVar( TypeNode tn );
177 : : void removeVar( TypeNode tn );
178 : : unsigned getNumTgFuncs( TypeNode tn );
179 : : TNode getTgFunc( TypeNode tn, unsigned i );
180 : : Node getFreeVar( TypeNode tn, unsigned i );
181 : : bool considerCurrentTerm();
182 : : bool considerCurrentTermCanon( unsigned tg_id );
183 : : void changeContext( bool add );
184 : : bool isRelevantFunc( Node f );
185 : : bool isRelevantTerm( Node t );
186 : : //carry
187 : : TermDb * getTermDatabase();
188 : : Node getGroundEqc( TNode r );
189 : : bool isGroundEqc( TNode r );
190 : : bool isGroundTerm( TNode n );
191 : : };
192 : :
193 : :
194 : :
195 : : class TheoremIndex
196 : : {
197 : : private:
198 : : void addTheorem( std::vector< TNode >& lhs_v, std::vector< unsigned >& lhs_arg, TNode rhs );
199 : : void addTheoremNode( TNode curr, std::vector< TNode >& lhs_v, std::vector< unsigned >& lhs_arg, TNode rhs );
200 : : void getEquivalentTerms( std::vector< TNode >& n_v, std::vector< unsigned >& n_arg,
201 : : std::map< TNode, TNode >& smap, std::vector< TNode >& vars, std::vector< TNode >& subs,
202 : : std::vector< Node >& terms );
203 : : void getEquivalentTermsNode( Node curr, std::vector< TNode >& n_v, std::vector< unsigned >& n_arg,
204 : : std::map< TNode, TNode >& smap, std::vector< TNode >& vars, std::vector< TNode >& subs,
205 : : std::vector< Node >& terms );
206 : : public:
207 : : std::map< TypeNode, TNode > d_var;
208 : : std::map< TNode, TheoremIndex > d_children;
209 : : std::vector< Node > d_terms;
210 : :
211 : 172 : void addTheorem( TNode lhs, TNode rhs ) {
212 : 344 : std::vector< TNode > v;
213 : 172 : std::vector< unsigned > a;
214 : 172 : addTheoremNode( lhs, v, a, rhs );
215 : 172 : }
216 : 3088 : void getEquivalentTerms( TNode n, std::vector< Node >& terms ) {
217 : 6176 : std::vector< TNode > nv;
218 : 6176 : std::vector< unsigned > na;
219 : 6176 : std::map< TNode, TNode > smap;
220 : 6176 : std::vector< TNode > vars;
221 : 3088 : std::vector< TNode > subs;
222 : 3088 : getEquivalentTermsNode( n, nv, na, smap, vars, subs, terms );
223 : 3088 : }
224 : 68 : void clear(){
225 : 68 : d_var.clear();
226 : 68 : d_children.clear();
227 : 68 : d_terms.clear();
228 : 68 : }
229 : : void debugPrint( const char * c, unsigned ind = 0 );
230 : : };
231 : :
232 : :
233 : :
234 : : class ConjectureGenerator : public QuantifiersModule
235 : : {
236 : : friend class OpArgIndex;
237 : : friend class PatGen;
238 : : friend class PatternGenEqc;
239 : : friend class PatternGen;
240 : : friend class SubsEqcIndex;
241 : : friend class TermGenerator;
242 : : friend class TermGenEnv;
243 : : typedef context::CDHashMap<Node, Node> NodeMap;
244 : : typedef context::CDHashMap<Node, bool> BoolMap;
245 : : // this class maintains a congruence closure for *universal* facts
246 : : private:
247 : : //notification class for equality engine
248 : : class NotifyClass : public eq::EqualityEngineNotify {
249 : : ConjectureGenerator& d_sg;
250 : : public:
251 : 15 : NotifyClass(ConjectureGenerator& sg): d_sg(sg) {}
252 : 0 : bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
253 : : {
254 : 0 : return true;
255 : : }
256 : 0 : bool eqNotifyTriggerTermEquality(TheoryId tag,
257 : : TNode t1,
258 : : TNode t2,
259 : : bool value) override
260 : : {
261 : 0 : return true;
262 : : }
263 : 0 : void eqNotifyConstantTermMerge(TNode t1, TNode t2) override {}
264 : 3088 : void eqNotifyNewClass(TNode t) override { d_sg.eqNotifyNewClass(t); }
265 : 387 : void eqNotifyMerge(TNode t1, TNode t2) override
266 : : {
267 : 387 : d_sg.eqNotifyMerge(t1, t2);
268 : 387 : }
269 : 0 : void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
270 : : {
271 : 0 : }
272 : : };/* class ConjectureGenerator::NotifyClass */
273 : : /** The notify class */
274 : : NotifyClass d_notify;
275 : : class EqcInfo{
276 : : public:
277 : : EqcInfo(context::Context* c);
278 : : // representative
279 : : context::CDO<Node> d_rep;
280 : : };
281 : : /** get or make eqc info */
282 : : EqcInfo* getOrMakeEqcInfo( TNode n, bool doMake = false );
283 : : /** boolean terms */
284 : : Node d_true;
285 : : Node d_false;
286 : : /** (universal) equaltity engine */
287 : : eq::EqualityEngine d_uequalityEngine;
288 : : /** pending adds */
289 : : std::vector< Node > d_upendingAdds;
290 : : /** relevant terms */
291 : : std::map< Node, bool > d_urelevant_terms;
292 : : /** information necessary for equivalence classes */
293 : : std::map< Node, EqcInfo* > d_eqc_info;
294 : : /** called when a new equivalance class is created */
295 : : void eqNotifyNewClass(TNode t);
296 : : /** called when two equivalance classes have merged */
297 : : void eqNotifyMerge(TNode t1, TNode t2);
298 : : /** are universal equal */
299 : : bool areUniversalEqual( TNode n1, TNode n2 );
300 : : /** are universal disequal */
301 : : bool areUniversalDisequal( TNode n1, TNode n2 );
302 : : /** get universal representative */
303 : : Node getUniversalRepresentative(TNode n, bool add = false);
304 : : /** set relevant */
305 : : void setUniversalRelevant( TNode n );
306 : : /** ordering for universal terms */
307 : : bool isUniversalLessThan( TNode rt1, TNode rt2 );
308 : :
309 : : /** the nodes we have reported as canonical representative */
310 : : std::vector< TNode > d_ue_canon;
311 : : /** is reported canon */
312 : : bool isReportedCanon( TNode n );
313 : : /** mark that term has been reported as canonical rep */
314 : : void markReportedCanon( TNode n );
315 : :
316 : : private: //information regarding the conjectures
317 : : /** list of all conjectures */
318 : : std::vector< Node > d_conjectures;
319 : : /** list of all waiting conjectures */
320 : : std::vector< Node > d_waiting_conjectures_lhs;
321 : : std::vector< Node > d_waiting_conjectures_rhs;
322 : : std::vector< int > d_waiting_conjectures_score;
323 : : /** map of currently considered equality conjectures */
324 : : std::map< Node, std::vector< Node > > d_waiting_conjectures;
325 : : /** map of equality conjectures */
326 : : std::map< Node, std::vector< Node > > d_eq_conjectures;
327 : : /** currently existing conjectures in equality engine */
328 : : BoolMap d_ee_conjectures;
329 : : /** conjecture index */
330 : : TheoremIndex d_thm_index;
331 : : private: //free variable list
332 : : // get canonical free variable #i of type tn
333 : : Node getFreeVar( TypeNode tn, unsigned i );
334 : : private: //information regarding the terms
335 : : //relevant patterns (the LHS's)
336 : : std::map< TypeNode, std::vector< Node > > d_rel_patterns;
337 : : //total number of unique variables
338 : : std::map< TNode, unsigned > d_rel_pattern_var_sum;
339 : : //by types
340 : : PatternTypIndex d_rel_pattern_typ_index;
341 : : // substitution to ground EQC index
342 : : std::map< TNode, SubstitutionIndex > d_rel_pattern_subs_index;
343 : : //patterns (the RHS's)
344 : : std::map< TypeNode, std::vector< Node > > d_patterns;
345 : : //patterns to # variables per type
346 : : std::map< TNode, std::map< TypeNode, unsigned > > d_pattern_var_id;
347 : : // # duplicated variables
348 : : std::map< TNode, unsigned > d_pattern_var_duplicate;
349 : : // is normal pattern? (variables allocated in canonical way left to right)
350 : : std::map< TNode, int > d_pattern_is_normal;
351 : : std::map< TNode, int > d_pattern_is_relevant;
352 : : // patterns to a count of # operators (variables and functions)
353 : : std::map< TNode, std::map< TNode, unsigned > > d_pattern_fun_id;
354 : : // term size
355 : : std::map< TNode, unsigned > d_pattern_fun_sum;
356 : : // collect functions
357 : : unsigned collectFunctions( TNode opat, TNode pat, std::map< TNode, unsigned >& funcs,
358 : : std::map< TypeNode, unsigned >& mnvn, std::map< TypeNode, unsigned >& mxvn );
359 : : // add pattern
360 : : void registerPattern( Node pat, TypeNode tpat );
361 : : private: //for debugging
362 : : std::map< TNode, unsigned > d_em;
363 : : unsigned d_conj_count;
364 : : public:
365 : : //term generation environment
366 : : TermGenEnv d_tge;
367 : : //consider term canon
368 : : bool considerTermCanon( Node ln, bool genRelevant );
369 : : public: //for generalization
370 : : //generalizations
371 : 318 : bool isGeneralization( TNode patg, TNode pat ) {
372 : 318 : std::map< TNode, TNode > subs;
373 : 636 : return isGeneralization( patg, pat, subs );
374 : : }
375 : : bool isGeneralization( TNode patg, TNode pat, std::map< TNode, TNode >& subs );
376 : : // get generalization depth
377 : : int calculateGeneralizationDepth( TNode n, std::vector< TNode >& fv );
378 : : private:
379 : : //predicate for type
380 : : std::map< TypeNode, Node > d_typ_pred;
381 : : //get predicate for type
382 : : Node getPredicateForType( TypeNode tn );
383 : : /** get enumerate uf term
384 : : *
385 : : * This function adds up to #num f-applications to terms, where f is
386 : : * n.getOperator(). These applications are enumerated in a fair manner based
387 : : * on an iterative deepening of the sum of indices of the arguments. For
388 : : * example, if f : U x U -> U, an the term enumerator for U gives t1, t2, t3
389 : : * ..., then we add f-applications to terms in this order:
390 : : * f( t1, t1 )
391 : : * f( t2, t1 )
392 : : * f( t1, t2 )
393 : : * f( t1, t3 )
394 : : * f( t2, t2 )
395 : : * f( t3, t1 )
396 : : * ...
397 : : * This function may add fewer than #num terms to terms if the enumeration is
398 : : * exhausted, or if an internal error occurs.
399 : : */
400 : : void getEnumerateUfTerm( Node n, unsigned num, std::vector< Node >& terms );
401 : : //
402 : : void getEnumeratePredUfTerm( Node n, unsigned num, std::vector< Node >& terms );
403 : : // uf operators enumerated
404 : : std::map< Node, bool > d_uf_enum;
405 : : public: //for property enumeration
406 : : //process this candidate conjecture
407 : : void processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth );
408 : : //whether it should be considered, negative : no, positive returns score
409 : : int considerCandidateConjecture( TNode lhs, TNode rhs );
410 : : //notified of a substitution
411 : : bool notifySubstitution( TNode glhs, std::map< TNode, TNode >& subs, TNode rhs );
412 : : //confirmation count
413 : : unsigned d_subs_confirmCount;
414 : : //individual witnesses (for range)
415 : : std::vector< TNode > d_subs_confirmWitnessRange;
416 : : //individual witnesses (for domain)
417 : : std::map< TNode, std::vector< TNode > > d_subs_confirmWitnessDomain;
418 : : //number of ground substitutions whose equality is unknown
419 : : unsigned d_subs_unkCount;
420 : : private: //information about ground equivalence classes
421 : : TNode d_bool_eqc[2];
422 : : std::map< TNode, Node > d_ground_eqc_map;
423 : : std::vector< TNode > d_ground_terms;
424 : : //operator independent term index
425 : : std::map< TNode, OpArgIndex > d_op_arg_index;
426 : : //is handled term
427 : : bool isHandledTerm( TNode n );
428 : : Node getGroundEqc( TNode r );
429 : : bool isGroundEqc( TNode r );
430 : : bool isGroundTerm( TNode n );
431 : : //has enumerated UF
432 : : bool hasEnumeratedUf( Node n );
433 : : // count of full effort checks
434 : : unsigned d_fullEffortCount;
435 : : // has added lemma
436 : : bool d_hasAddedLemma;
437 : : //flush the waiting conjectures
438 : : unsigned flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth );
439 : :
440 : : public:
441 : : ConjectureGenerator(Env& env,
442 : : QuantifiersState& qs,
443 : : QuantifiersInferenceManager& qim,
444 : : QuantifiersRegistry& qr,
445 : : TermRegistry& tr);
446 : : ~ConjectureGenerator();
447 : :
448 : : /* needs check */
449 : : bool needsCheck(Theory::Effort e) override;
450 : : /* reset at a round */
451 : : void reset_round(Theory::Effort e) override;
452 : : /* Call during quantifier engine's check */
453 : : void check(Theory::Effort e, QEffort quant_e) override;
454 : : /** Identify this module (for debugging, dynamic configuration, etc..) */
455 : : std::string identify() const override;
456 : : // options
457 : : private:
458 : : bool optReqDistinctVarPatterns();
459 : : bool optFilterUnknown();
460 : : int optFilterScoreThreshold();
461 : : unsigned optFullCheckFrequency();
462 : : unsigned optFullCheckConjectures();
463 : :
464 : : bool optStatsOnly();
465 : : /** term canonizer */
466 : : expr::TermCanonize d_termCanon;
467 : : };
468 : :
469 : :
470 : : }
471 : : }
472 : : } // namespace cvc5::internal
473 : :
474 : : #endif
|
