GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/conjecture_generator.h Lines: 43 50 86.0 %
Date: 2021-03-22 Branches: 22 36 61.1 %

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