Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * conjecture generator class
11 : : */
12 : :
13 : : #include "cvc5_private.h"
14 : :
15 : : #ifndef CONJECTURE_GENERATOR_H
16 : : #define CONJECTURE_GENERATOR_H
17 : :
18 : : #include "context/cdhashmap.h"
19 : : #include "expr/node_trie.h"
20 : : #include "expr/term_canonize.h"
21 : : #include "smt/env_obj.h"
22 : : #include "theory/quantifiers/quant_module.h"
23 : : #include "theory/type_enumerator.h"
24 : :
25 : : namespace cvc5::internal {
26 : : namespace theory {
27 : : namespace quantifiers {
28 : :
29 : : // algorithm for computing candidate subgoals
30 : :
31 : : class ConjectureGenerator;
32 : :
33 : : /** operator independent index of arguments for an EQC
34 : : *
35 : : * The (almost) inductive definition of the set of irrelevant terms suggests
36 : : * the following algorithm to compute I, the set of irrelevant equivalence
37 : : * classes. It is a standard algorithm that starts from the empty set and
38 : : * iterates up to a fixed point.
39 : : *
40 : : * declare I and set its value to the empty set
41 : : *
42 : : * for each equivalence class e:
43 : : * if the sort of e is not an inductive datatype sort:
44 : : * add e to I
45 : : *
46 : : * declare I_old
47 : : *
48 : : * do:
49 : : * set I_old to the current value of I
50 : : * for each equivalence class e:
51 : : * if e is not in I:
52 : : * for each term t in e:
53 : : * if t has the form f(t_1, ..., t_n) where f is an atomic
54 : : * trigger that is not a skolem function and the equivalence class
55 : : * of each t_i is in I:
56 : : * add e to I
57 : : * continue to the next equivalence class
58 : : * else
59 : : * continue to the next term in e
60 : : * while I_old is different from I
61 : : *
62 : : * Note the three nested loops in the second phase of the algorithm above.
63 : : * We can avoid inspecting each element of each equivalence class that is not
64 : : * already in I by preparing a family of indices, which can be described
65 : : * abstractly as follows.
66 : : *
67 : : * _Definitions_
68 : : *
69 : : * - 'E' is the set of representatives of equivalence classes.
70 : : * - 'F' is the set of function symbols.
71 : : * - 'T' is the set of terms.
72 : : * - For a set 'X', X* denotes the set of all strings over X.
73 : : * - For a set 'X', X+ denotes the set of non-empty strings over X.
74 : : * - For sets 'X' and 'Y', X x Y denotes their cartesian product.
75 : : * - 't = u' means the terms t and u are syntactically equal.
76 : : * - 't ~ u' means the terms t and u are in the same equivalence class according
77 : : * to the current model
78 : : *
79 : : * _Declarations_
80 : : *
81 : : * - 'OpArgIndex' is a subset of E+, we intend that OpArgIndex(e e_1 ... e_n) is
82 : : * true iff the string e e_1 ... e_n denotes an instance of the C++ class named
83 : : * OpArgIndex
84 : : *
85 : : * - '[[e e_1 ... e_n]]' is the instance of the OpArgIndex class denoted by the
86 : : * string e e_1 ... e_n when OpArgIndex(e e_1 ... e_n) is true, and it is
87 : : * equal to d_op_arg_index[e].d_child[e_1].(...).d_child[e_n]
88 : : *
89 : : * - 'child' is a subset of E+ x E, we intend that child(e e_1 ... e_n, e^) is
90 : : * true iff the map [[e e_1 ... e_n]].d_child contains e^ as a key.
91 : : *
92 : : * - 'ops' : OpArgIndex -> F* is a function where we intend ops(e e_1 ... e_n)
93 : : * to be the same sequence of function symbols as the vector
94 : : * [[e e_1 ... e_n]].d_ops
95 : : *
96 : : * - 'op_terms' : OpArgIndex -> T* is a function where we intend
97 : : * op_terms(e e_1 ... e_n) to be the same sequence of terms as the vector
98 : : * [[e e_1 ... e_n]].d_op_terms
99 : : *
100 : : * - 'added' is a subset of E x T where we intend added(e, t) to be true iff
101 : : * d_op_arg_index[e].addTerm(t) executes successfully.
102 : : *
103 : : * _Invariants_
104 : : *
105 : : * (i) child(e e_1 ... e_n, e^)
106 : : * <==> OpArgIndex(e e_1 ... e_n e^)
107 : : *
108 : : * (ii) OpArgIndex(e e_1 ... e_n)
109 : : * ==> for all 0 <= i < n. OpArgIndex(e e_1 ... e_i)
110 : : *
111 : : * (iii) added(e, f(t_1, ..., t_n))
112 : : * <==> OpArgIndex(e e_1 ... e_n)
113 : : * /\ there exists j. ops(e e_1 ... e_n)(j) = f
114 : : * /\ op_terms(e e_1 ... e_n)(j) = f(t_1, ..., t_n)
115 : : *
116 : : * (iv) d_ops(e e_1 ... e_n) has the same length as |d_op_terms(e e_1 ... e_n)|
117 : : *
118 : : * _Additional guarantees_
119 : : *
120 : : * In the implementation of getEquivalenceClasses, note that we add
121 : : * f(t_1, ..., t_n) to d_op_terms[e] when, among satisfying certain other
122 : : * properties, it is in e's equivalence class. This guarantees that
123 : : * added(e, f(t_1, ..., t_n)) ==> f(t_1, ..., t_n) ~ e.
124 : : *
125 : : * Furthermore the implementation of addTerm ensures that for any equivalence
126 : : * class representative e and for any two terms t = f(t_1, ..., t_n) and
127 : : * u = f(u_1, ..., u_n) such that t != u, t ~ e, u ~ e,
128 : : * and t_i ~ u_i for each i, we that at most one of added(e, t) and
129 : : * added(e, u) is true.
130 : : *
131 : : * _Take-away_
132 : : *
133 : : * The problem of deciding whether the equivalence class represented by e is
134 : : * irrelevant (see comment for computeIrrelevantEqcs) falls to searching for
135 : : * a string e e_1 ... e_n such that
136 : : *
137 : : * - OpArgIndex(e e_1 ... e_n), and
138 : : * - for all 1 <= i < n. e_i is irrelevant, and
139 : : * - ops(e e_1 ... e_n) is non-empty.
140 : : *
141 : : * as implemented in 'getGroundTerms'.
142 : : *
143 : : * We hope is that searching for such a string is more efficient than the
144 : : * naive approach of iterating over all terms in e's equivalence class and
145 : : * checking if any one of these terms is irrelevant.
146 : : *
147 : : * _Example_
148 : : *
149 : : * Let e, e_1, e_2 and e_3 be representatives of equivalence classes.
150 : : * Suppose we're given that
151 : : *
152 : : * - f(t_1,t_2) ~ g(t_3) ~ f(t_4,t_5) ~ f(t_6,t_7) ~ e, and
153 : : * - t_1 ~ t_3 ~ t_4 ~ t_6 ~ e_1, and
154 : : * - t_2 ~ t_5 ~ e_2, and
155 : : * - t_7 ~ e_3
156 : : *
157 : : * Suppose also that we add f(t_1,t_2), g(t_3), f(t_4,t_5), and f(t_6,t_7)
158 : : * to d_op_arg_index[e] in sequence. The resulting data structure looks like
159 : : *
160 : : * [[e]], d_ops = [], d_op_terms = []
161 : : * |
162 : : * e_1 '-- [[e e_1]], d_ops = [ g ], d_op_terms = [ g(t_3) ]
163 : : * |
164 : : * e_2 |-- [[e e_1 e_2]], d_ops = [ f ], d_op_terms = [ f(t_4,t_5) ]
165 : : * |
166 : : * e_3 '-- [[e e_1 e_3]], d_ops = [ f ], d_op_terms = [ f(t_6,t_7) ]
167 : : */
168 : : class OpArgIndex
169 : : {
170 : : public:
171 : : std::map<TNode, OpArgIndex> d_child;
172 : : std::vector<TNode> d_ops;
173 : : std::vector<TNode> d_op_terms;
174 : : void addTerm(std::vector<TNode>& terms, TNode n, unsigned index = 0);
175 : : Node getGroundTerm(ConjectureGenerator* s, std::vector<TNode>& args);
176 : : void getGroundTerms(ConjectureGenerator* s, std::vector<TNode>& terms);
177 : : };
178 : :
179 : : class PatternTypIndex
180 : : {
181 : : public:
182 : : std::vector<TNode> d_terms;
183 : : std::map<TypeNode, std::map<unsigned, PatternTypIndex> > d_children;
184 : 240 : void clear()
185 : : {
186 : 240 : d_terms.clear();
187 : 240 : d_children.clear();
188 : 240 : }
189 : : };
190 : :
191 : : class SubstitutionIndex
192 : : {
193 : : public:
194 : : // current variable, or ground EQC if d_children.empty()
195 : : TNode d_var;
196 : : std::map<TNode, SubstitutionIndex> d_children;
197 : : // add substitution
198 : : void addSubstitution(TNode eqc,
199 : : std::vector<TNode>& vars,
200 : : std::vector<TNode>& terms,
201 : : unsigned i = 0);
202 : : // notify substitutions
203 : : bool notifySubstitutions(ConjectureGenerator* s,
204 : : std::map<TNode, TNode>& subs,
205 : : TNode rhs,
206 : : unsigned numVars,
207 : : unsigned i = 0);
208 : : };
209 : :
210 : : class TermGenEnv;
211 : :
212 : : class TermGenerator
213 : : {
214 : : private:
215 : : unsigned calculateGeneralizationDepth(
216 : : TermGenEnv* s, std::map<TypeNode, std::vector<int> >& fvs);
217 : :
218 : : public:
219 : 25147 : TermGenerator()
220 : 50294 : : d_id(0),
221 : 25147 : d_status(0),
222 : 25147 : d_status_num(0),
223 : 25147 : d_status_child_num(0),
224 : 25147 : d_match_status(0),
225 : 25147 : d_match_status_child_num(0),
226 : 25147 : d_match_mode(0)
227 : : {
228 : 25147 : }
229 : : TypeNode d_typ;
230 : : unsigned d_id;
231 : : // 1 : consider as unique variable
232 : : // 2 : consider equal to another variable
233 : : // 5 : consider a function application
234 : : unsigned d_status;
235 : : int d_status_num;
236 : : // for function applications: the number of children you have built
237 : : int d_status_child_num;
238 : : // children (pointers to TermGenerators)
239 : : std::vector<unsigned> d_children;
240 : :
241 : : // match status
242 : : int d_match_status;
243 : : int d_match_status_child_num;
244 : : // match mode bits
245 : : // 0 : different variables must have different matches
246 : : // 1 : variables must map to ground terms
247 : : // 2 : variables must map to non-ground terms
248 : : unsigned d_match_mode;
249 : : // children
250 : : std::vector<std::map<TNode, TNodeTrie>::iterator> d_match_children;
251 : : std::vector<std::map<TNode, TNodeTrie>::iterator> d_match_children_end;
252 : :
253 : : void reset(TermGenEnv* s, TypeNode tn);
254 : : bool getNextTerm(TermGenEnv* s, unsigned depth);
255 : : void resetMatching(unsigned mode);
256 : : bool getNextMatch(TermGenEnv* s,
257 : : TNode eqc,
258 : : std::map<TypeNode, std::map<unsigned, TNode> >& subs,
259 : : std::map<TNode, bool>& rev_subs);
260 : :
261 : : unsigned getDepth(TermGenEnv* s);
262 : : unsigned getGeneralizationDepth(TermGenEnv* s);
263 : : Node getTerm(TermGenEnv* s);
264 : :
265 : : void debugPrint(TermGenEnv* s, const char* c, const char* cd);
266 : : };
267 : :
268 : : class TermGenEnv
269 : : {
270 : : public:
271 : : // collect signature information
272 : : void collectSignatureInformation();
273 : : // reset function
274 : : void reset(unsigned gdepth, bool genRelevant, TypeNode tgen);
275 : : // get next term
276 : : bool getNextTerm();
277 : : // reset matching
278 : : void resetMatching(unsigned mode);
279 : : // get next match
280 : : bool getNextMatch(TNode eqc,
281 : : std::map<TypeNode, std::map<unsigned, TNode> >& subs,
282 : : std::map<TNode, bool>& rev_subs);
283 : : // get term
284 : : Node getTerm();
285 : : // debug print
286 : : void debugPrint(const char* c, const char* cd);
287 : :
288 : : // conjecture generation
289 : : ConjectureGenerator* d_cg;
290 : : // the current number of enumerated variables per type
291 : : std::map<TypeNode, unsigned> d_var_id;
292 : : // the limit of number of variables per type to enumerate
293 : : std::map<TypeNode, unsigned> d_var_limit;
294 : : // the functions we can currently generate
295 : : std::map<TypeNode, std::vector<TNode> > d_typ_tg_funcs;
296 : : // whether functions must add operators
297 : : std::map<TNode, bool> d_tg_func_param;
298 : : // the equivalence classes (if applicable) that match the currently generated
299 : : // term
300 : : bool d_gen_relevant_terms;
301 : : // relevant equivalence classes
302 : : std::vector<TNode> d_relevant_eqc[2];
303 : : // candidate equivalence classes
304 : : std::vector<std::vector<TNode> > d_ccand_eqc[2];
305 : : // the term generation objects
306 : : unsigned d_tg_id;
307 : : std::map<unsigned, TermGenerator> d_tg_alloc;
308 : : unsigned d_tg_gdepth;
309 : : int d_tg_gdepth_limit;
310 : :
311 : : // all functions
312 : : std::vector<TNode> d_funcs;
313 : : // function to kind map
314 : : std::map<TNode, Kind> d_func_kind;
315 : : // type of each argument of the function
316 : : std::map<TNode, std::vector<TypeNode> > d_func_args;
317 : :
318 : : // access functions
319 : : unsigned getNumTgVars(TypeNode tn);
320 : : bool allowVar(TypeNode tn);
321 : : void addVar(TypeNode tn);
322 : : void removeVar(TypeNode tn);
323 : : unsigned getNumTgFuncs(TypeNode tn);
324 : : TNode getTgFunc(TypeNode tn, unsigned i);
325 : : Node getFreeVar(TypeNode tn, unsigned i);
326 : : bool considerCurrentTerm();
327 : : bool considerCurrentTermCanon(unsigned tg_id);
328 : : void changeContext(bool add);
329 : : bool isRelevantFunc(Node f);
330 : : bool isRelevantTerm(Node t);
331 : : // carry
332 : : TermDb* getTermDatabase();
333 : : Node getGroundEqc(TNode r);
334 : : bool isGroundEqc(TNode r);
335 : : bool isGroundTerm(TNode n);
336 : : };
337 : :
338 : : class TheoremIndex
339 : : {
340 : : private:
341 : : void addTheorem(std::vector<TNode>& lhs_v,
342 : : std::vector<unsigned>& lhs_arg,
343 : : TNode rhs);
344 : : void addTheoremNode(TNode curr,
345 : : std::vector<TNode>& lhs_v,
346 : : std::vector<unsigned>& lhs_arg,
347 : : TNode rhs);
348 : : void getEquivalentTerms(std::vector<TNode>& n_v,
349 : : std::vector<unsigned>& n_arg,
350 : : std::map<TNode, TNode>& smap,
351 : : std::vector<TNode>& vars,
352 : : std::vector<TNode>& subs,
353 : : std::vector<Node>& terms);
354 : : void getEquivalentTermsNode(Node curr,
355 : : std::vector<TNode>& n_v,
356 : : std::vector<unsigned>& n_arg,
357 : : std::map<TNode, TNode>& smap,
358 : : std::vector<TNode>& vars,
359 : : std::vector<TNode>& subs,
360 : : std::vector<Node>& terms);
361 : :
362 : : public:
363 : : std::map<TypeNode, TNode> d_var;
364 : : std::map<TNode, TheoremIndex> d_children;
365 : : std::vector<Node> d_terms;
366 : :
367 : 282 : void addTheorem(TNode lhs, TNode rhs)
368 : : {
369 : 282 : std::vector<TNode> v;
370 : 282 : std::vector<unsigned> a;
371 : 282 : addTheoremNode(lhs, v, a, rhs);
372 : 282 : }
373 : 13531 : void getEquivalentTerms(TNode n, std::vector<Node>& terms)
374 : : {
375 : 13531 : std::vector<TNode> nv;
376 : 13531 : std::vector<unsigned> na;
377 : 13531 : std::map<TNode, TNode> smap;
378 : 13531 : std::vector<TNode> vars;
379 : 13531 : std::vector<TNode> subs;
380 : 13531 : getEquivalentTermsNode(n, nv, na, smap, vars, subs, terms);
381 : 13531 : }
382 : 240 : void clear()
383 : : {
384 : 240 : d_var.clear();
385 : 240 : d_children.clear();
386 : 240 : d_terms.clear();
387 : 240 : }
388 : : void debugPrint(const char* c, unsigned ind = 0);
389 : : };
390 : :
391 : : class ConjectureGenerator : public QuantifiersModule
392 : : {
393 : : friend class OpArgIndex;
394 : : friend class PatGen;
395 : : friend class PatternGenEqc;
396 : : friend class PatternGen;
397 : : friend class SubsEqcIndex;
398 : : friend class TermGenerator;
399 : : friend class TermGenEnv;
400 : : typedef context::CDHashMap<Node, Node> NodeMap;
401 : : typedef context::CDHashMap<Node, bool> BoolMap;
402 : : // this class maintains a congruence closure for *universal* facts
403 : : private:
404 : : // notification class for equality engine
405 : : class NotifyClass : public eq::EqualityEngineNotify
406 : : {
407 : : ConjectureGenerator& d_sg;
408 : :
409 : : public:
410 : 64 : NotifyClass(ConjectureGenerator& sg) : d_sg(sg) {}
411 : 0 : bool eqNotifyTriggerPredicate(CVC5_UNUSED TNode predicate,
412 : : CVC5_UNUSED bool value) override
413 : : {
414 : 0 : return true;
415 : : }
416 : 0 : bool eqNotifyTriggerTermEquality(CVC5_UNUSED TheoryId tag,
417 : : CVC5_UNUSED TNode t1,
418 : : CVC5_UNUSED TNode t2,
419 : : CVC5_UNUSED bool value) override
420 : : {
421 : 0 : return true;
422 : : }
423 : 0 : void eqNotifyConstantTermMerge(CVC5_UNUSED TNode t1,
424 : : CVC5_UNUSED TNode t2) override
425 : : {
426 : 0 : }
427 : 13531 : void eqNotifyNewClass(TNode t) override { d_sg.eqNotifyNewClass(t); }
428 : 588 : void eqNotifyMerge(TNode t1, TNode t2) override
429 : : {
430 : 588 : d_sg.eqNotifyMerge(t1, t2);
431 : 588 : }
432 : 0 : void eqNotifyDisequal(CVC5_UNUSED TNode t1,
433 : : CVC5_UNUSED TNode t2,
434 : : CVC5_UNUSED TNode reason) override
435 : : {
436 : 0 : }
437 : : }; /* class ConjectureGenerator::NotifyClass */
438 : : /** The notify class */
439 : : NotifyClass d_notify;
440 : : class EqcInfo
441 : : {
442 : : public:
443 : : EqcInfo(context::Context* c);
444 : : // representative
445 : : context::CDO<Node> d_rep;
446 : : };
447 : : /** get or make eqc info */
448 : : EqcInfo* getOrMakeEqcInfo(TNode n, bool doMake = false);
449 : : /** boolean terms */
450 : : Node d_true;
451 : : Node d_false;
452 : : /** (universal) equaltity engine */
453 : : eq::EqualityEngine d_uequalityEngine;
454 : : /** pending adds */
455 : : std::vector<Node> d_upendingAdds;
456 : : /** relevant terms */
457 : : std::map<Node, bool> d_urelevant_terms;
458 : : /** information necessary for equivalence classes */
459 : : std::map<Node, EqcInfo*> d_eqc_info;
460 : : /** called when a new equivalance class is created */
461 : : void eqNotifyNewClass(TNode t);
462 : : /** called when two equivalance classes have merged */
463 : : void eqNotifyMerge(TNode t1, TNode t2);
464 : : /** are universal equal */
465 : : bool areUniversalEqual(TNode n1, TNode n2);
466 : : /** are universal disequal */
467 : : bool areUniversalDisequal(TNode n1, TNode n2);
468 : : /** get universal representative */
469 : : Node getUniversalRepresentative(TNode n, bool add = false);
470 : : /** set relevant */
471 : : void setUniversalRelevant(TNode n);
472 : : /** ordering for universal terms */
473 : : bool isUniversalLessThan(TNode rt1, TNode rt2);
474 : :
475 : : /** the nodes we have reported as canonical representative */
476 : : std::vector<TNode> d_ue_canon;
477 : : /** is reported canon */
478 : : bool isReportedCanon(TNode n);
479 : : /** mark that term has been reported as canonical rep */
480 : : void markReportedCanon(TNode n);
481 : :
482 : : private: // information regarding the conjectures
483 : : /** list of all conjectures */
484 : : std::vector<Node> d_conjectures;
485 : : /** list of all waiting conjectures */
486 : : std::vector<Node> d_waiting_conjectures_lhs;
487 : : std::vector<Node> d_waiting_conjectures_rhs;
488 : : std::vector<int> d_waiting_conjectures_score;
489 : : /** map of currently considered equality conjectures */
490 : : std::map<Node, std::vector<Node> > d_waiting_conjectures;
491 : : /** map of equality conjectures */
492 : : std::map<Node, std::vector<Node> > d_eq_conjectures;
493 : : /** currently existing conjectures in equality engine */
494 : : BoolMap d_ee_conjectures;
495 : : /** conjecture index */
496 : : TheoremIndex d_thm_index;
497 : :
498 : : private: // free variable list
499 : : // get canonical free variable #i of type tn
500 : : Node getFreeVar(TypeNode tn, unsigned i);
501 : :
502 : : private: // information regarding the terms
503 : : // relevant patterns (the LHS's)
504 : : std::map<TypeNode, std::vector<Node> > d_rel_patterns;
505 : : // total number of unique variables
506 : : std::map<TNode, unsigned> d_rel_pattern_var_sum;
507 : : // by types
508 : : PatternTypIndex d_rel_pattern_typ_index;
509 : : // substitution to ground EQC index
510 : : std::map<TNode, SubstitutionIndex> d_rel_pattern_subs_index;
511 : : // patterns (the RHS's)
512 : : std::map<TypeNode, std::vector<Node> > d_patterns;
513 : : // patterns to # variables per type
514 : : std::map<TNode, std::map<TypeNode, unsigned> > d_pattern_var_id;
515 : : // # duplicated variables
516 : : std::map<TNode, unsigned> d_pattern_var_duplicate;
517 : : // is normal pattern? (variables allocated in canonical way left to right)
518 : : std::map<TNode, int> d_pattern_is_normal;
519 : : std::map<TNode, int> d_pattern_is_relevant;
520 : : // patterns to a count of # operators (variables and functions)
521 : : std::map<TNode, std::map<TNode, unsigned> > d_pattern_fun_id;
522 : : // term size
523 : : std::map<TNode, unsigned> d_pattern_fun_sum;
524 : : // collect functions
525 : : unsigned collectFunctions(TNode opat,
526 : : TNode pat,
527 : : std::map<TNode, unsigned>& funcs,
528 : : std::map<TypeNode, unsigned>& mnvn,
529 : : std::map<TypeNode, unsigned>& mxvn);
530 : : // add pattern
531 : : void registerPattern(Node pat, TypeNode tpat);
532 : :
533 : : private: // for debugging
534 : : std::map<TNode, unsigned> d_em;
535 : : unsigned d_conj_count;
536 : :
537 : : public:
538 : : // term generation environment
539 : : TermGenEnv d_tge;
540 : : // consider term canon
541 : : bool considerTermCanon(Node ln, bool genRelevant);
542 : : /** collect equivalence classes
543 : : *
544 : : * This function iterates over the representative 'r'
545 : : * of each equivalence class and
546 : : *
547 : : * - adds 'r' to 'eqcs',
548 : : * - assigns to 'r' a 1-indexed serial number 'd_em[r]',
549 : : * - and adds every term 't' in the equivalence class represented by 'r'
550 : : * to the operator-argument index, which will be used to identify
551 : : * equivalence classes that do not contain concrete terms and so are
552 : : * relevant for conjecture generation.
553 : : */
554 : : void getEquivalenceClasses(std::vector<TNode>& eqcs);
555 : : /** compute irrelevant equivalence classes
556 : : *
557 : : * This function populates 'd_ground_eqc_map' with irrelevant equivalence
558 : : * classes. In other words, it populates this map with key-value pairs
559 : : * where each key is an irrelevant term that is also the representative of
560 : : * some equivalence class. The values are not important.
561 : : *
562 : : * In principle a term is *irrelevant* if and only if
563 : : *
564 : : * 1. it is not of inductive datatype sort,
565 : : * 2. OR it is of inductive datatype sort,
566 : : * - AND it has an operator which is an *atomic trigger* but not a skolem
567 : : * function,
568 : : * - AND all of its immediate children -- the operator's arguments -- are
569 : : * themselves irrelevant terms,
570 : : * 3. OR it is equivalent to an irrelevant term in the current model.
571 : : *
572 : : * The objective behind defining irrelevance this way is to narrow the set
573 : : * of *relevant* terms to datatype-sorted terms that are impossible to express
574 : : * using only non-datatype terms, constructors, selectors,
575 : : * uninterpreted functions, or other function-like symbols (atomic triggers).
576 : : *
577 : : * Consequently the set of relevant terms contains (among other terms)
578 : : * datatype-sorted skolem constants that represent "arbitrary" values of that
579 : : * sort rather than "concrete" values. These are precisely the skolem
580 : : * constants we may want to translate into universally quantified variables
581 : : * when synthesizing conjectures.
582 : : */
583 : : void computeIrrelevantEqcs(const std::vector<TNode>& eqcs);
584 : : /** print information related to the computation of irrelevant equivalence
585 : : * classes
586 : : *
587 : : * This function requires that the contents of the input vector 'eqcs' are
588 : : * exactly the representatives of each equivalence class in the current model.
589 : : *
590 : : * For each element e of eqcs other than nodeManager()->mkConst(false), this
591 : : * function prints all terms t ~ e such that t is active (according to the
592 : : * term database) and t is not an equality. If e is computed irrelevant (see
593 : : * computeIrrelevantEqcs) this function also prints a term that explains why e
594 : : * is irrelevant.
595 : : */
596 : : void debugPrintIrrelevantEqcs(const std::vector<TNode>& eqcs);
597 : : /** compute relevant equivalence classes
598 : : *
599 : : * This function requires that the contents of the input vector eqcs are
600 : : * exactly the representatives of each equivalence class in the current model.
601 : : *
602 : : * This function guarantees that
603 : : *
604 : : * - the contents of d_tge.d_relevant_eqc[0] are exactly the relevant
605 : : * equivalence class representatives in eqcs,
606 : : * - the contents of d_tge.d_relevant_eqc[1] are exactly the irrelevant
607 : : * equivalence class representatives in eqcs, and
608 : : * - eqcs is unchanged.
609 : : */
610 : : void computeRelevantEqcs(const std::vector<TNode>& eqcs);
611 : : /** build theorem index from universally quantified formulas
612 : : *
613 : : * We look at all asserted formulas q of the below form and try to add their
614 : : * data to both the theorem index (d_thm_index) and the universal equality
615 : : * engine (d_uequalityEngine).
616 : : *
617 : : * q := (forall x_1,...,x_n. l = r)
618 : : *
619 : : * However the theorem index expects equalities (t = u) that are in canonical
620 : : * form, contain only *relevant* function symbols, and are not *subsumed*
621 : : * (entailed in the universal equality engine). Therefore if q's body (l = r)
622 : : * contains an irrelevant function symbol, we skip over q. Otherwise we
623 : : * canonize (l = r) to (l' = r') and check if it is subsumed. If it is, we
624 : : * skip over q. At this point we know that (l' = r') is relevant, canonical
625 : : * and not subsumed, so we (1) ensure that the equivalence classes of l' and
626 : : * r' are merged in the universal equality engine, and (2) add both (l' = r')
627 : : * and the canonical form of (r = l) to the theorem index.
628 : : *
629 : : * We also return all *proven conjectures* in a vector. These are conjectures
630 : : * that had been proposed in prior rounds (elements of d_conjectures) and are
631 : : * asserted true in the current model.
632 : : *
633 : : * *Note.* There appear to be some unstated assumptions in the code.
634 : : * - if q is in d_conjectures it is assumed that its body (l = r) contains
635 : : * only relevant function symbols and is already in canonical form, and
636 : : * - if (l = r) is in the equality engine it is assumed that its canonical
637 : : * form (l' = r') is not subsumed and also that the equivalence classes of l'
638 : : * and r' do not have to be merged in the universal equality engine. (I'm not
639 : : * sure that this is right.)
640 : : */
641 : : std::vector<Node> buildTheoremIndex();
642 : : /* examine status of conjectures
643 : : *
644 : : * This is a debug printing function that does not modify the state of the
645 : : * conjecture generator. We iterate over all unproven conjectures q. If all
646 : : * of q's bound variables are irrelevant, we claim that q has been *disproven*
647 : : * and print the values of these bound variables as a counterexample to q. If
648 : : * at least one of q's bound variables is still relevant we print all of q's
649 : : * relevant bound variables and claim that q remains *active*.
650 : : *
651 : : * *Note.* From the documentation for buildTheoremIndex(), any element of
652 : : * d_conjectures that is not in provenConj is considered an unproven
653 : : * conjecture.
654 : : */
655 : : void debugPrintUnprovenConjectures(const std::vector<Node>& provenConj);
656 : : /* print theorem index
657 : : *
658 : : * This function just calls d_thm_index.debugPrint().
659 : : */
660 : : void debugPrintTheoremIndex();
661 : : /* print pattern-type index
662 : : */
663 : : void debugPrintPatternTypIndex();
664 : : /* generate conjectures
665 : : *
666 : : * This function synthesizes candidate equality conjectures, removes "bad"
667 : : * candidates, and submits the remainder to the inference manager. For each
668 : : * value d of generalization depth from 1 up to maxDepth (determined by a
669 : : * command line option with default value 3), we synthesize a canonical[1]
670 : : * left-hand term of (generalization) depth exactly d subject to a filter[2].
671 : : * We then use the synthesized term as a pattern and employ e-matching to
672 : : * compute a number of substitutions from the free variables in the pattern to
673 : : * irrelevant terms. We repeat the process till all possible left-hand terms
674 : : * with depth d are exhausted. Next, for each value d' of generalization
675 : : * depth between 1 and d (inclusive) we synthesize a canonical right-hand term
676 : : * of depth d' using the same free variables as the left-hand terms. The
677 : : * right-hand term is also run through a filter[2]. If d' < d, we process
678 : : * conjectures l = r where l is any synthesized left-hand term of depth
679 : : * exactly d and r is the just-synthesized right-hand term. On the other hand
680 : : * if d' = d, we store r for later. We repeat till all possible right-hand
681 : : * terms of depth d' are exhausted. We then process conjectures l = r where l
682 : : * is any synthesized term of depth up to and including d and r is any term of
683 : : * depth exactly d. Each processed conjecture is put through more checks. It
684 : : * is rejected if
685 : : * - it has already been sent to the inference manager[3], or
686 : : * - it is already waiting to be sent to the inference manager[3], or
687 : : * - it is falsified by one of the aforementioned substitutions that maps free
688 : : * variables to irrelevant terms[3], or
689 : : * - it is non-canonical[4], or
690 : : * - its "score" is below a threshold[4].
691 : : *
692 : : * [1]: See ConjectureGenerator::considerTermCanon()
693 : : * [2]: See TermGenEnv::considerCurrentTerm()
694 : : * [3]: See ConjectureGenerator::considerCandidateConjecture()
695 : : * [4]: See ConjectureGenerator::flushWaitingConjectures()
696 : : *
697 : : * ---------------------------------------------------------------------------
698 : : *
699 : : * This function uses a number of variables. Here's a short description for
700 : : * each.
701 : : *
702 : : * rel_term_count. For a particular value of *depth*, the "relevant term
703 : : * count" is the number of canonical left-hand terms generated at that depth.
704 : : *
705 : : * rt_var_max. "Right variable maximum" is a map from types to natural
706 : : * numbers. Given a type t, rt_var_max[t] is the largest index among all
707 : : * canonical variables of type t that appear free in any left-hand term
708 : : * synthesized so far. For example, if rt_var_max[t] is 3 then the only free
709 : : * variables of type t in the left-hand terms synthesized so far must be {t0,
710 : : * t1, t2, t3}. When we generate right-hand terms of less or same depth, we
711 : : * run the lines
712 : : *
713 : : * d_tge.d_var_id[t] = rt_var_max[t];
714 : : * d_tge.d_var_limit[t] = rt_var_max[t];
715 : : *
716 : : * for each type t to ensure that the right-hand terms draw from the same pool
717 : : * of free variables.
718 : : *
719 : : * rt_types. "Right types" stores the types of all the left-hand terms
720 : : * synthesizesd so far by the term generator. Since we want to build equality
721 : : * conjectures, we only synthesize right-hand of types from rt_types.
722 : : *
723 : : * nn. The most recently synthesized left-hand term.
724 : : *
725 : : * tnn. The type of nn.
726 : : *
727 : : * conj_lhs. conj_lhs[t][n] is the list of left-hand terms synthesized so far
728 : : * with type t and generalization depth n.
729 : : *
730 : : * addedLemmas. The number of lemmas sent to the instantiation manager.
731 : : *
732 : : * maxDepth. Gets it value from options().quantifiers.conjectureGenMaxDepth.
733 : : * We do not synthesize left-hand terms with generalization depth maxDepth.
734 : : *
735 : : * gsubs_vars. Our description of generateConjectures() mentions that for
736 : : * each synthesized left-hand term we compute substitutions from the free
737 : : * variables in the term to irrelevant terms. gsubs_vars lists the free
738 : : * variables in the most recently synthesized left-hand term and is the domain
739 : : * of such a substitution. Suppose d_tge.d_var_id has the form [(t_0, n_0),
740 : : * (t_1, n_1), ..., (t_k, n_k)]. Then the first n_0 elements of gsubs_vars
741 : : * are the first n_0 canonical variables of type t_0, the next n_1 elements of
742 : : * gsubs_vars are the first n_1 canonical variables of type t_1, and more
743 : : * generally the n_i elements of gsubs_vars from indices n_0 + ... + n_(i-1)
744 : : * to n_0 + ... + n_i - 1 are the first n_i canonical variables of type t_i,
745 : : * assuming 0 <= i <= k.
746 : : *
747 : : * d_rel_pattern_var_sum. For any synthesized left-hand term t,
748 : : * d_rel_pattern_var_sum[t] equals the length of t's gsubs_vars.
749 : : *
750 : : * typ_to_subs_index. Let d_tge.d_var_id have the form [(t_1, n_1), ...,
751 : : * (t_k, n_k)] where all t_i's are distinct and all n_i's are non-negative.
752 : : * Let lhs denote the most recently generated canonical term.
753 : : * d_rel_pattern_var_sum[lhs] is set to n_1 + ... + n_k.
754 : : * typ_to_subs_index[t_i] is set to n_1 + ... + n_(i-1) for 1 <= i <= k. For
755 : : * i < k, the elements of gsubs_vars from index typ_to_subs_index[t_i] up to
756 : : * but not including typ_to_subs_index[t_(i+1)] are the first n_i canonical
757 : : * variables of type t_i. The elements of gsubs_vars from index
758 : : * typ_to_subs_index[t_k] up to but not including d_rel_pattern_var_sum[lhs]
759 : : * are the first n_k canonical variables of type t_k.
760 : : *
761 : : * gsubs_terms. Where gsubs_vars is the domain of a substitution from free
762 : : * variables to irrelevant terms, gsubs_terms is the substitution's range.
763 : : * For each i from 0 up to but not including d_rel_pattern_var_sum[nn], the
764 : : * variable gsubs_vars[i] maps to the irrelevant term gsubs_terms[i].
765 : : *
766 : : * d_rel_pattern_typ_index. This index stores synthesized left-hand terms
767 : : * based on the type and count of its free variables. All terms with exactly
768 : : * 1 free variable of type t_1 and 2 free variables of type t_2 are stored in
769 : : * the same node in this index. Since all the terms we add to this index are
770 : : * canonical, we are guaranteed that if a term uses n variables of type t_i
771 : : * then these variables are exactly the first n canonical variables of t_i.
772 : : * An example is:
773 : : *
774 : : * null, 0 -> []
775 : : * Nat, 0 -> []
776 : : * Lst, 1 -> [(last L0), (append L0 nil)]
777 : : * Lst, 2 -> [(append L0 L1),
778 : : * (cons (last L0) L1),
779 : : * (last (append L0 L1))]
780 : : * Lst, 3 -> [(append L0 (append L1 L2)),
781 : : * (append (append L0 L1) L2)]
782 : : * Nat, 1 -> []
783 : : * Lst, 0 -> [(cons N0 nil)]
784 : : * Lst, 1 -> [(cons N0 L0), (last (cons N0 L0))]
785 : : * Lst, 2 -> [(cons N0 (append L0 L1)), (append (cons N0 L0) L1)]
786 : : *
787 : : * *Note.* d_rel_pattern_typ_index is never actually used.
788 : : *
789 : : * conj_rhs. Suppose we have just synthesized left-hand terms of
790 : : * generalization depth d and are synthesizing right-hand terms of depth d' <=
791 : : * d. Synthesized right-hand terms of type t and depth exactly d (i.e. when
792 : : * d' = d) are stored in conj_rhs[t].
793 : : */
794 : : void generateConjectures();
795 : :
796 : : public: // for generalization
797 : : // generalizations
798 : 516 : bool isGeneralization(TNode patg, TNode pat)
799 : : {
800 : 516 : std::map<TNode, TNode> subs;
801 : 1032 : return isGeneralization(patg, pat, subs);
802 : 516 : }
803 : : bool isGeneralization(TNode patg, TNode pat, std::map<TNode, TNode>& subs);
804 : : // get generalization depth
805 : : int calculateGeneralizationDepth(TNode n, std::vector<TNode>& fv);
806 : :
807 : : private:
808 : : // predicate for type
809 : : std::map<TypeNode, Node> d_typ_pred;
810 : : // get predicate for type
811 : : Node getPredicateForType(TypeNode tn);
812 : : /** get enumerate uf term
813 : : *
814 : : * This function adds up to #num f-applications to terms, where f is
815 : : * n.getOperator(). These applications are enumerated in a fair manner based
816 : : * on an iterative deepening of the sum of indices of the arguments. For
817 : : * example, if f : U x U -> U, an the term enumerator for U gives t1, t2, t3
818 : : * ..., then we add f-applications to terms in this order:
819 : : * f( t1, t1 )
820 : : * f( t2, t1 )
821 : : * f( t1, t2 )
822 : : * f( t1, t3 )
823 : : * f( t2, t2 )
824 : : * f( t3, t1 )
825 : : * ...
826 : : * This function may add fewer than #num terms to terms if the enumeration is
827 : : * exhausted, or if an internal error occurs.
828 : : */
829 : : void getEnumerateUfTerm(Node n, unsigned num, std::vector<Node>& terms);
830 : : //
831 : : void getEnumeratePredUfTerm(Node n, unsigned num, std::vector<Node>& terms);
832 : : // uf operators enumerated
833 : : std::map<Node, bool> d_uf_enum;
834 : :
835 : : public: // for property enumeration
836 : : // process this candidate conjecture
837 : : void processCandidateConjecture(TNode lhs,
838 : : TNode rhs,
839 : : unsigned lhs_depth,
840 : : unsigned rhs_depth);
841 : : // whether it should be considered, negative : no, positive returns score
842 : : int considerCandidateConjecture(TNode lhs, TNode rhs);
843 : : // notified of a substitution
844 : : bool notifySubstitution(TNode glhs, std::map<TNode, TNode>& subs, TNode rhs);
845 : : // confirmation count
846 : : unsigned d_subs_confirmCount;
847 : : // individual witnesses (for range)
848 : : std::vector<TNode> d_subs_confirmWitnessRange;
849 : : // individual witnesses (for domain)
850 : : std::map<TNode, std::vector<TNode> > d_subs_confirmWitnessDomain;
851 : : // number of ground substitutions whose equality is unknown
852 : : unsigned d_subs_unkCount;
853 : :
854 : : private: // information about ground equivalence classes
855 : : TNode d_bool_eqc[2];
856 : : std::map<TNode, Node> d_ground_eqc_map;
857 : : std::vector<TNode> d_ground_terms;
858 : : // operator independent term index
859 : : std::map<TNode, OpArgIndex> d_op_arg_index;
860 : : // is handled term
861 : : bool isHandledTerm(TNode n);
862 : : Node getGroundEqc(TNode r);
863 : : bool isGroundEqc(TNode r);
864 : : bool isGroundTerm(TNode n);
865 : : // has enumerated UF
866 : : bool hasEnumeratedUf(Node n);
867 : : // count of full effort checks
868 : : unsigned d_fullEffortCount;
869 : : // has added lemma
870 : : bool d_hasAddedLemma;
871 : : // flush the waiting conjectures
872 : : unsigned flushWaitingConjectures(unsigned& addedLemmas,
873 : : int ldepth,
874 : : int rdepth);
875 : :
876 : : public:
877 : : ConjectureGenerator(Env& env,
878 : : QuantifiersState& qs,
879 : : QuantifiersInferenceManager& qim,
880 : : QuantifiersRegistry& qr,
881 : : TermRegistry& tr);
882 : : ~ConjectureGenerator();
883 : :
884 : : /* needs check */
885 : : bool needsCheck(Theory::Effort e) override;
886 : : /* reset at a round */
887 : : void reset_round(Theory::Effort e) override;
888 : : /* Call during quantifier engine's check */
889 : : void check(Theory::Effort e, QEffort quant_e) override;
890 : : /** Identify this module (for debugging, dynamic configuration, etc..) */
891 : : std::string identify() const override;
892 : : // options
893 : : private:
894 : : bool optReqDistinctVarPatterns();
895 : : bool optFilterUnknown();
896 : : int optFilterScoreThreshold();
897 : : unsigned optFullCheckFrequency();
898 : : unsigned optFullCheckConjectures();
899 : :
900 : : bool optStatsOnly();
901 : : /** term canonizer */
902 : : expr::TermCanonize d_termCanon;
903 : : };
904 : :
905 : : } // namespace quantifiers
906 : : } // namespace theory
907 : : } // namespace cvc5::internal
908 : :
909 : : #endif
|
