GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/conjecture_generator.cpp Lines: 1246 1407 88.6 %
Date: 2021-03-22 Branches: 2560 6020 42.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file conjecture_generator.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, Aina Niemetz
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
16
#include "theory/quantifiers/conjecture_generator.h"
17
#include "expr/term_canonize.h"
18
#include "options/quantifiers_options.h"
19
#include "theory/quantifiers/ematching/trigger_term_info.h"
20
#include "theory/quantifiers/first_order_model.h"
21
#include "theory/quantifiers/skolemize.h"
22
#include "theory/quantifiers/term_database.h"
23
#include "theory/quantifiers/term_enumeration.h"
24
#include "theory/quantifiers/term_util.h"
25
#include "theory/quantifiers_engine.h"
26
#include "theory/rewriter.h"
27
#include "util/random.h"
28
29
using namespace CVC4;
30
using namespace CVC4::kind;
31
using namespace CVC4::theory;
32
using namespace CVC4::theory::quantifiers;
33
using namespace std;
34
35
namespace CVC4 {
36
37
struct sortConjectureScore {
38
  std::vector< int > d_scores;
39
  bool operator() (unsigned i, unsigned j) { return d_scores[i]>d_scores[j]; }
40
};
41
42
43
21620
void OpArgIndex::addTerm( std::vector< TNode >& terms, TNode n, unsigned index ){
44
21620
  if( index==n.getNumChildren() ){
45
8821
    Assert(n.hasOperator());
46
8821
    if( std::find( d_ops.begin(), d_ops.end(), n.getOperator() )==d_ops.end() ){
47
8809
      d_ops.push_back( n.getOperator() );
48
8809
      d_op_terms.push_back( n );
49
    }
50
  }else{
51
12799
    d_child[terms[index]].addTerm( terms, n, index+1 );
52
  }
53
21620
}
54
55
9878
Node OpArgIndex::getGroundTerm( ConjectureGenerator * s, std::vector< TNode >& args ) {
56
9878
  if( d_ops.empty() ){
57
8446
    for( std::map< TNode, OpArgIndex >::iterator it = d_child.begin(); it != d_child.end(); ++it ){
58
6662
      std::map< TNode, Node >::iterator itf = s->d_ground_eqc_map.find( it->first );
59
6662
      if( itf!=s->d_ground_eqc_map.end() ){
60
4995
        args.push_back( itf->second );
61
5154
        Node n = it->second.getGroundTerm( s, args );
62
4995
        args.pop_back();
63
4995
        if( !n.isNull() ){
64
4836
          return n;
65
        }
66
      }
67
    }
68
1784
    return Node::null();
69
  }
70
6516
  std::vector<TNode> args2;
71
3258
  if (d_op_terms[0].getMetaKind() == kind::metakind::PARAMETERIZED)
72
  {
73
3258
    args2.push_back( d_ops[0] );
74
  }
75
3258
  args2.insert(args2.end(), args.begin(), args.end());
76
3258
  return NodeManager::currentNM()->mkNode(d_op_terms[0].getKind(), args2);
77
}
78
79
13922
void OpArgIndex::getGroundTerms( ConjectureGenerator * s, std::vector< TNode >& terms ) {
80
13922
  terms.insert( terms.end(), d_op_terms.begin(), d_op_terms.end() );
81
23902
  for( std::map< TNode, OpArgIndex >::iterator it = d_child.begin(); it != d_child.end(); ++it ){
82
9980
    if( s->isGroundEqc( it->first ) ){
83
9222
      it->second.getGroundTerms( s, terms );
84
    }
85
  }
86
13922
}
87
88
12
ConjectureGenerator::ConjectureGenerator(QuantifiersEngine* qe,
89
                                         QuantifiersState& qs,
90
                                         QuantifiersInferenceManager& qim,
91
12
                                         QuantifiersRegistry& qr)
92
    : QuantifiersModule(qs, qim, qr, qe),
93
      d_notify(*this),
94
      d_uequalityEngine(
95
          d_notify, qs.getSatContext(), "ConjectureGenerator::ee", false),
96
      d_ee_conjectures(qs.getSatContext()),
97
      d_conj_count(0),
98
      d_subs_confirmCount(0),
99
      d_subs_unkCount(0),
100
      d_fullEffortCount(0),
101
12
      d_hasAddedLemma(false)
102
{
103
12
  d_true = NodeManager::currentNM()->mkConst(true);
104
12
  d_false = NodeManager::currentNM()->mkConst(false);
105
12
  d_uequalityEngine.addFunctionKind( kind::APPLY_UF );
106
12
  d_uequalityEngine.addFunctionKind( kind::APPLY_CONSTRUCTOR );
107
108
12
}
109
110
36
ConjectureGenerator::~ConjectureGenerator()
111
{
112
33
  for (std::map<Node, EqcInfo*>::iterator i = d_eqc_info.begin(),
113
12
                                          iend = d_eqc_info.end();
114
33
       i != iend;
115
       ++i)
116
  {
117
21
    EqcInfo* current = (*i).second;
118
21
    Assert(current != nullptr);
119
21
    delete current;
120
  }
121
24
}
122
123
1618
void ConjectureGenerator::eqNotifyNewClass( TNode t ){
124
1618
  Trace("thm-ee-debug") << "UEE : new equivalence class " << t << std::endl;
125
1618
  d_upendingAdds.push_back( t );
126
1618
}
127
128
196
void ConjectureGenerator::eqNotifyMerge(TNode t1, TNode t2)
129
{
130
  //get maintained representatives
131
392
  TNode rt1 = t1;
132
392
  TNode rt2 = t2;
133
196
  std::map< Node, EqcInfo* >::iterator it1 = d_eqc_info.find( t1 );
134
196
  if( it1!=d_eqc_info.end() && !it1->second->d_rep.get().isNull() ){
135
24
    rt1 = it1->second->d_rep.get();
136
  }
137
196
  std::map< Node, EqcInfo* >::iterator it2 = d_eqc_info.find( t2 );
138
196
  if( it2!=d_eqc_info.end() && !it2->second->d_rep.get().isNull() ){
139
    rt2 = it2->second->d_rep.get();
140
  }
141
196
  Trace("thm-ee-debug") << "UEE : equality holds : " << t1 << " == " << t2 << std::endl;
142
196
  Trace("thm-ee-debug") << "      ureps : " << rt1 << " == " << rt2 << std::endl;
143
196
  Trace("thm-ee-debug") << "      relevant : " << d_pattern_is_relevant[rt1] << " " << d_pattern_is_relevant[rt2] << std::endl;
144
196
  Trace("thm-ee-debug") << "      normal : " << d_pattern_is_normal[rt1] << " " << d_pattern_is_normal[rt2] << std::endl;
145
196
  Trace("thm-ee-debug") << "      size :   " << d_pattern_fun_sum[rt1] << " " << d_pattern_fun_sum[rt2] << std::endl;
146
147
196
  if( isUniversalLessThan( rt2, rt1 ) ){
148
    EqcInfo * ei;
149
43
    if( it1==d_eqc_info.end() ){
150
21
      ei = getOrMakeEqcInfo( t1, true );
151
    }else{
152
22
      ei = it1->second;
153
    }
154
43
    ei->d_rep = t2;
155
  }
156
196
}
157
158
159
21
ConjectureGenerator::EqcInfo::EqcInfo( context::Context* c ) : d_rep( c, Node::null() ){
160
161
21
}
162
163
7719
ConjectureGenerator::EqcInfo* ConjectureGenerator::getOrMakeEqcInfo( TNode n, bool doMake ) {
164
  //Assert( getUniversalRepresentative( n )==n );
165
7719
  std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n );
166
7719
  if( eqc_i!=d_eqc_info.end() ){
167
366
    return eqc_i->second;
168
7353
  }else if( doMake ){
169
21
    EqcInfo* ei = new EqcInfo(d_qstate.getSatContext());
170
21
    d_eqc_info[n] = ei;
171
21
    return ei;
172
  }else{
173
7332
    return NULL;
174
  }
175
}
176
177
5020
void ConjectureGenerator::setUniversalRelevant( TNode n ) {
178
  //add pattern information
179
5020
  registerPattern( n, n.getType() );
180
5020
  d_urelevant_terms[n] = true;
181
8641
  for( unsigned i=0; i<n.getNumChildren(); i++ ){
182
3621
    setUniversalRelevant( n[i] );
183
  }
184
5020
}
185
186
305
bool ConjectureGenerator::isUniversalLessThan( TNode rt1, TNode rt2 ) {
187
  //prefer the one that is (normal, smaller) lexographically
188
305
  Assert(d_pattern_is_relevant.find(rt1) != d_pattern_is_relevant.end());
189
305
  Assert(d_pattern_is_relevant.find(rt2) != d_pattern_is_relevant.end());
190
305
  Assert(d_pattern_is_normal.find(rt1) != d_pattern_is_normal.end());
191
305
  Assert(d_pattern_is_normal.find(rt2) != d_pattern_is_normal.end());
192
305
  Assert(d_pattern_fun_sum.find(rt1) != d_pattern_fun_sum.end());
193
305
  Assert(d_pattern_fun_sum.find(rt2) != d_pattern_fun_sum.end());
194
195
305
  if( d_pattern_is_relevant[rt1] && !d_pattern_is_relevant[rt2] ){
196
    Trace("thm-ee-debug") << "UEE : LT due to relevant." << std::endl;
197
    return true;
198
305
  }else if( d_pattern_is_relevant[rt1]==d_pattern_is_relevant[rt2] ){
199
288
    if( d_pattern_is_normal[rt1] && !d_pattern_is_normal[rt2] ){
200
      Trace("thm-ee-debug") << "UEE : LT due to normal." << std::endl;
201
      return true;
202
288
    }else if( d_pattern_is_normal[rt1]==d_pattern_is_normal[rt2] ){
203
288
      if( d_pattern_fun_sum[rt1]<d_pattern_fun_sum[rt2] ){
204
55
        Trace("thm-ee-debug") << "UEE : LT due to size." << std::endl;
205
        //decide which representative to use : based on size of the term
206
55
        return true;
207
233
      }else if( d_pattern_fun_sum[rt1]==d_pattern_fun_sum[rt2] ){
208
        //same size : tie goes to term that has already been reported
209
145
        return isReportedCanon( rt1 ) && !isReportedCanon( rt2 );
210
      }
211
    }
212
  }
213
105
  return false;
214
}
215
216
217
7487
bool ConjectureGenerator::isReportedCanon( TNode n ) {
218
7487
  return std::find( d_ue_canon.begin(), d_ue_canon.end(), n )==d_ue_canon.end();
219
}
220
221
7197
void ConjectureGenerator::markReportedCanon( TNode n ) {
222
7197
  if( !isReportedCanon( n ) ){
223
    d_ue_canon.push_back( n );
224
  }
225
7197
}
226
227
46
bool ConjectureGenerator::areUniversalEqual( TNode n1, TNode n2 ) {
228
46
  return n1==n2 || ( d_uequalityEngine.hasTerm( n1 ) && d_uequalityEngine.hasTerm( n2 ) && d_uequalityEngine.areEqual( n1, n2 ) );
229
}
230
231
bool ConjectureGenerator::areUniversalDisequal( TNode n1, TNode n2 ) {
232
  return n1!=n2 && d_uequalityEngine.hasTerm( n1 ) && d_uequalityEngine.hasTerm( n2 ) && d_uequalityEngine.areDisequal( n1, n2, false );
233
}
234
235
7698
Node ConjectureGenerator::getUniversalRepresentative(TNode n, bool add)
236
{
237
7698
  if( add ){
238
7645
    if( d_urelevant_terms.find( n )==d_urelevant_terms.end() ){
239
1387
      setUniversalRelevant( n );
240
      //add term to universal equality engine
241
1387
      d_uequalityEngine.addTerm( n );
242
      // addding this term to equality engine will lead to a set of new terms (the new subterms of n)
243
      // now, do instantiation-based merging for each of these terms
244
1387
      Trace("thm-ee-debug") << "Merge equivalence classes based on instantiations of terms..." << std::endl;
245
      //merge all pending equalities
246
4185
      while( !d_upendingAdds.empty() ){
247
1399
        Trace("sg-pending") << "Add " << d_upendingAdds.size() << " pending terms..." << std::endl;
248
2798
        std::vector< Node > pending;
249
1399
        pending.insert( pending.end(), d_upendingAdds.begin(), d_upendingAdds.end() );
250
1399
        d_upendingAdds.clear();
251
3017
        for( unsigned i=0; i<pending.size(); i++ ){
252
3236
          Node t = pending[i];
253
3236
          TypeNode tn = t.getType();
254
1618
          Trace("thm-ee-add") << "UEE : Add universal term " << t << std::endl;
255
3236
          std::vector< Node > eq_terms;
256
          //if occurs modulo equality at ground level, it is equivalent to representative of ground equality engine
257
3236
          Node gt = getTermDatabase()->evaluateTerm(t);
258
1618
          if( !gt.isNull() && gt!=t ){
259
56
            eq_terms.push_back( gt );
260
          }
261
          //get all equivalent terms based on theorem database
262
1618
          d_thm_index.getEquivalentTerms( t, eq_terms );
263
1618
          if( !eq_terms.empty() ){
264
216
            Trace("thm-ee-add") << "UEE : Based on ground EE/theorem DB, it is equivalent to " << eq_terms.size() << " terms : " << std::endl;
265
            //add equivalent terms as equalities to universal engine
266
436
            for (const Node& eqt : eq_terms)
267
            {
268
220
              Trace("thm-ee-add") << "  " << eqt << std::endl;
269
220
              bool assertEq = false;
270
220
              if (d_urelevant_terms.find(eqt) != d_urelevant_terms.end())
271
              {
272
111
                assertEq = true;
273
              }
274
              else
275
              {
276
109
                Assert(eqt.getType() == tn);
277
109
                registerPattern(eqt, tn);
278
436
                if (isUniversalLessThan(eqt, t)
279
545
                    || (options::conjectureUeeIntro()
280
109
                        && d_pattern_fun_sum[t] >= d_pattern_fun_sum[eqt]))
281
                {
282
12
                  setUniversalRelevant(eqt);
283
12
                  assertEq = true;
284
                }
285
              }
286
220
              if( assertEq ){
287
246
                Node exp;
288
123
                d_uequalityEngine.assertEquality(t.eqNode(eqt), true, exp);
289
              }else{
290
194
                Trace("thm-ee-no-add")
291
97
                    << "Do not add : " << t << " == " << eqt << std::endl;
292
              }
293
            }
294
          }else{
295
1402
            Trace("thm-ee-add") << "UEE : No equivalent terms." << std::endl;
296
          }
297
        }
298
      }
299
    }
300
  }
301
302
7698
  if( d_uequalityEngine.hasTerm( n ) ){
303
15396
    Node r = d_uequalityEngine.getRepresentative( n );
304
7698
    EqcInfo * ei = getOrMakeEqcInfo( r );
305
7698
    if( ei && !ei->d_rep.get().isNull() ){
306
352
      return ei->d_rep.get();
307
    }else{
308
7346
      return r;
309
    }
310
  }else{
311
    return n;
312
  }
313
}
314
315
40936
Node ConjectureGenerator::getFreeVar( TypeNode tn, unsigned i ) {
316
40936
  return d_termCanon.getCanonicalFreeVar(tn, i);
317
}
318
319
23763
bool ConjectureGenerator::isHandledTerm( TNode n ){
320
71289
  return d_quantEngine->getTermDatabase()->isTermActive(n)
321
44528
         && inst::TriggerTermInfo::isAtomicTrigger(n)
322
107708
         && (n.getKind() != APPLY_UF || n.getOperator().getKind() != SKOLEM);
323
}
324
325
Node ConjectureGenerator::getGroundEqc( TNode r ) {
326
  std::map< TNode, Node >::iterator it = d_ground_eqc_map.find( r );
327
  return it!=d_ground_eqc_map.end() ? it->second : Node::null();
328
}
329
330
348118
bool ConjectureGenerator::isGroundEqc( TNode r ) {
331
348118
  return d_ground_eqc_map.find( r )!=d_ground_eqc_map.end();
332
}
333
334
bool ConjectureGenerator::isGroundTerm( TNode n ) {
335
  return std::find( d_ground_terms.begin(), d_ground_terms.end(), n )!=d_ground_terms.end();
336
}
337
338
457
bool ConjectureGenerator::needsCheck( Theory::Effort e ) {
339
  // synchonized with instantiation engine
340
457
  return d_qstate.getInstWhenNeedsCheck(e);
341
}
342
343
77
bool ConjectureGenerator::hasEnumeratedUf( Node n ) {
344
169
  if( options::conjectureGenGtEnum()>0 ){
345
77
    std::map< Node, bool >::iterator it = d_uf_enum.find( n.getOperator() );
346
77
    if( it==d_uf_enum.end() ){
347
15
      d_uf_enum[n.getOperator()] = true;
348
15
      std::vector< Node > lem;
349
15
      getEnumeratePredUfTerm( n, options::conjectureGenGtEnum(), lem );
350
15
      if( !lem.empty() ){
351
765
        for (const Node& l : lem)
352
        {
353
750
          d_qim.addPendingLemma(l, InferenceId::UNKNOWN);
354
        }
355
15
        d_hasAddedLemma = true;
356
15
        return false;
357
      }
358
    }
359
  }
360
62
  return true;
361
}
362
363
158
void ConjectureGenerator::reset_round( Theory::Effort e ) {
364
365
158
}
366
174
void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e)
367
{
368
174
  if (quant_e == QEFFORT_STANDARD)
369
  {
370
48
    d_fullEffortCount++;
371
48
    if( d_fullEffortCount%optFullCheckFrequency()==0 ){
372
48
      d_hasAddedLemma = false;
373
48
      d_tge.d_cg = this;
374
48
      double clSet = 0;
375
48
      if( Trace.isOn("sg-engine") ){
376
        clSet = double(clock())/double(CLOCKS_PER_SEC);
377
        Trace("sg-engine") << "---Conjecture Engine Round, effort = " << e << "---" << std::endl;
378
      }
379
48
      eq::EqualityEngine * ee = getEqualityEngine();
380
48
      d_conj_count = 0;
381
382
48
      Trace("sg-proc") << "Get eq classes..." << std::endl;
383
48
      d_op_arg_index.clear();
384
48
      d_ground_eqc_map.clear();
385
48
      d_bool_eqc[0] = Node::null();
386
48
      d_bool_eqc[1] = Node::null();
387
96
      std::vector< TNode > eqcs;
388
48
      d_em.clear();
389
48
      eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
390
9448
      while( !eqcs_i.isFinished() ){
391
9400
        TNode r = (*eqcs_i);
392
4700
        Trace("sg-proc-debug") << "...eqc : " << r << std::endl;
393
4700
        eqcs.push_back( r );
394
4700
        if( r.getType().isBoolean() ){
395
816
          if (areEqual(r, d_true))
396
          {
397
48
            d_ground_eqc_map[r] = d_true;
398
48
            d_bool_eqc[0] = r;
399
          }
400
768
          else if (areEqual(r, d_false))
401
          {
402
48
            d_ground_eqc_map[r] = d_false;
403
48
            d_bool_eqc[1] = r;
404
          }
405
        }
406
4700
        d_em[r] = eqcs.size();
407
4700
        eq::EqClassIterator ieqc_i = eq::EqClassIterator( r, ee );
408
50768
        while( !ieqc_i.isFinished() ){
409
46068
          TNode n = (*ieqc_i);
410
23034
          Trace("sg-proc-debug") << "......term : " << n << std::endl;
411
23034
          if( getTermDatabase()->hasTermCurrent( n ) ){
412
23034
            if( isHandledTerm( n ) ){
413
17642
              std::vector<TNode> areps;
414
21620
              for (const Node& nc : n)
415
              {
416
12799
                areps.push_back(d_qstate.getRepresentative(nc));
417
              }
418
8821
              d_op_arg_index[r].addTerm(areps, n);
419
            }
420
          }
421
23034
          ++ieqc_i;
422
        }
423
4700
        ++eqcs_i;
424
      }
425
48
      Assert(!d_bool_eqc[0].isNull());
426
48
      Assert(!d_bool_eqc[1].isNull());
427
48
      d_urelevant_terms.clear();
428
48
      Trace("sg-proc") << "...done get eq classes" << std::endl;
429
430
48
      Trace("sg-proc") << "Determine ground EQC..." << std::endl;
431
      bool success;
432
119
      do{
433
119
        success = false;
434
12823
        for( unsigned i=0; i<eqcs.size(); i++ ){
435
25408
          TNode r = eqcs[i];
436
12704
          if( d_ground_eqc_map.find( r )==d_ground_eqc_map.end() ){
437
11254
            std::vector< TNode > args;
438
5627
            Trace("sg-pat-debug") << "******* Get ground term for " << r << std::endl;
439
11254
            Node n;
440
5627
            if (Skolemize::isInductionTerm(r))
441
            {
442
4883
              n = d_op_arg_index[r].getGroundTerm( this, args );
443
            }else{
444
744
              n = r;
445
            }
446
5627
            if( !n.isNull() ){
447
4002
              Trace("sg-pat") << "Ground term for eqc " << r << " : " << std::endl;
448
4002
              Trace("sg-pat") << "   " << n << std::endl;
449
4002
              d_ground_eqc_map[r] = n;
450
4002
              success = true;
451
            }else{
452
1625
              Trace("sg-pat-debug") << "...could not find ground term." << std::endl;
453
            }
454
          }
455
        }
456
      }while( success );
457
      //also get ground terms
458
48
      d_ground_terms.clear();
459
4748
      for( unsigned i=0; i<eqcs.size(); i++ ){
460
9400
        TNode r = eqcs[i];
461
4700
        d_op_arg_index[r].getGroundTerms( this, d_ground_terms );
462
      }
463
48
      Trace("sg-proc") << "...done determine ground EQC" << std::endl;
464
465
      //debug printing
466
48
      if( Trace.isOn("sg-gen-eqc") ){
467
        for( unsigned i=0; i<eqcs.size(); i++ ){
468
          TNode r = eqcs[i];
469
          //print out members
470
          bool firstTime = true;
471
          bool isFalse = areEqual(r, d_false);
472
          eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
473
          while( !eqc_i.isFinished() ){
474
            TNode n = (*eqc_i);
475
            if( getTermDatabase()->hasTermCurrent( n ) && getTermDatabase()->isTermActive( n ) && ( n.getKind()!=EQUAL || isFalse ) ){
476
              if( firstTime ){
477
                Trace("sg-gen-eqc") << "e" << d_em[r] << " : { " << std::endl;
478
                firstTime = false;
479
              }
480
              if( n.hasOperator() ){
481
                Trace("sg-gen-eqc") << "   (" << n.getOperator();
482
                for (const Node& nc : n)
483
                {
484
                  TNode ar = d_qstate.getRepresentative(nc);
485
                  Trace("sg-gen-eqc") << " e" << d_em[ar];
486
                }
487
                Trace("sg-gen-eqc") << ") :: " << n << std::endl;
488
              }else{
489
                Trace("sg-gen-eqc") << "   " << n << std::endl;
490
              }
491
            }
492
            ++eqc_i;
493
          }
494
          if( !firstTime ){
495
            Trace("sg-gen-eqc") << "}" << std::endl;
496
            //print out ground term
497
            std::map< TNode, Node >::iterator it = d_ground_eqc_map.find( r );
498
            if( it!=d_ground_eqc_map.end() ){
499
              Trace("sg-gen-eqc") << "- Ground term : " << it->second << std::endl;
500
            }
501
          }
502
        }
503
      }
504
505
48
      Trace("sg-proc") << "Compute relevant eqc..." << std::endl;
506
48
      d_tge.d_relevant_eqc[0].clear();
507
48
      d_tge.d_relevant_eqc[1].clear();
508
4748
      for( unsigned i=0; i<eqcs.size(); i++ ){
509
9400
        TNode r = eqcs[i];
510
4700
        std::map< TNode, Node >::iterator it = d_ground_eqc_map.find( r );
511
4700
        unsigned index = 1;
512
4700
        if( it==d_ground_eqc_map.end() ){
513
602
          index = 0;
514
        }
515
        //based on unproven conjectures? TODO
516
4700
        d_tge.d_relevant_eqc[index].push_back( r );
517
      }
518
48
      Trace("sg-gen-tg-debug") << "Initial relevant eqc : ";
519
650
      for( unsigned i=0; i<d_tge.d_relevant_eqc[0].size(); i++ ){
520
602
        Trace("sg-gen-tg-debug") << "e" << d_em[d_tge.d_relevant_eqc[0][i]] << " ";
521
      }
522
48
      Trace("sg-gen-tg-debug") << std::endl;
523
48
      Trace("sg-proc") << "...done compute relevant eqc" << std::endl;
524
525
526
48
      Trace("sg-proc") << "Collect signature information..." << std::endl;
527
48
      d_tge.collectSignatureInformation();
528
48
      if( d_hasAddedLemma ){
529
8
        Trace("sg-proc") << "...added enumeration lemmas." << std::endl;
530
      }
531
48
      Trace("sg-proc") << "...done collect signature information" << std::endl;
532
533
534
535
48
      Trace("sg-proc") << "Build theorem index..." << std::endl;
536
48
      d_ue_canon.clear();
537
48
      d_thm_index.clear();
538
96
      std::vector< Node > provenConj;
539
48
      quantifiers::FirstOrderModel* m = d_quantEngine->getModel();
540
271
      for( unsigned i=0; i<m->getNumAssertedQuantifiers(); i++ ){
541
446
        Node q = m->getAssertedQuantifier( i );
542
223
        Trace("thm-db-debug") << "Is " << q << " a relevant theorem?" << std::endl;
543
446
        Node conjEq;
544
223
        if( q[1].getKind()==EQUAL ){
545
123
          bool isSubsume = false;
546
123
          bool inEe = false;
547
215
          for( unsigned r=0; r<2; r++ ){
548
261
            TNode nl = q[1][r==0 ? 0 : 1];
549
261
            TNode nr = q[1][r==0 ? 1 : 0];
550
261
            Node eq = nl.eqNode( nr );
551
169
            if( r==1 || std::find( d_conjectures.begin(), d_conjectures.end(), q )==d_conjectures.end() ){
552
              //check if it contains only relevant functions
553
169
              if( d_tge.isRelevantTerm( eq ) ){
554
                //make it canonical
555
92
                Trace("sg-proc-debug") << "get canonical " << eq << std::endl;
556
92
                eq = d_termCanon.getCanonicalTerm(eq);
557
              }else{
558
77
                eq = Node::null();
559
              }
560
            }
561
169
            if( !eq.isNull() ){
562
92
              if( r==0 ){
563
46
                inEe = d_ee_conjectures.find( q[1] )!=d_ee_conjectures.end();
564
46
                if( !inEe ){
565
                  //add to universal equality engine
566
92
                  Node nlu = getUniversalRepresentative(eq[0], true);
567
92
                  Node nru = getUniversalRepresentative(eq[1], true);
568
46
                  if (areUniversalEqual(nlu, nru))
569
                  {
570
                    isSubsume = true;
571
                    //set inactive (will be ignored by other modules)
572
                    d_quantEngine->getModel()->setQuantifierActive( q, false );
573
                  }
574
                  else
575
                  {
576
92
                    Node exp;
577
46
                    d_ee_conjectures[q[1]] = true;
578
138
                    d_uequalityEngine.assertEquality(
579
92
                        nlu.eqNode(nru), true, exp);
580
                  }
581
                }
582
46
                Trace("sg-conjecture") << "*** CONJECTURE : currently proven" << (isSubsume ? " and subsumed" : "");
583
46
                Trace("sg-conjecture") << " : " << q[1] << std::endl;
584
46
                provenConj.push_back( q );
585
              }
586
92
              if( !isSubsume ){
587
92
                Trace("thm-db-debug") << "Adding theorem to database " << eq[0] << " == " << eq[1] << std::endl;
588
92
                d_thm_index.addTheorem( eq[0], eq[1] );
589
              }else{
590
                break;
591
              }
592
            }else{
593
77
              break;
594
            }
595
          }
596
        }
597
      }
598
      //examine status of other conjectures
599
81
      for( unsigned i=0; i<d_conjectures.size(); i++ ){
600
66
        Node q = d_conjectures[i];
601
33
        if( std::find( provenConj.begin(), provenConj.end(), q )==provenConj.end() ){
602
          //check each skolem variable
603
33
          bool disproven = true;
604
66
          std::vector<Node> skolems;
605
33
          d_quantEngine->getSkolemize()->getSkolemConstants(q, skolems);
606
33
          Trace("sg-conjecture") << "    CONJECTURE : ";
607
66
          std::vector< Node > ce;
608
37
          for (unsigned j = 0; j < skolems.size(); j++)
609
          {
610
41
            TNode rk = getRepresentative(skolems[j]);
611
37
            std::map< TNode, Node >::iterator git = d_ground_eqc_map.find( rk );
612
            //check if it is a ground term
613
37
            if( git==d_ground_eqc_map.end() ){
614
33
              Trace("sg-conjecture") << "ACTIVE : " << q;
615
33
              if( Trace.isOn("sg-gen-eqc") ){
616
                Trace("sg-conjecture") << " { ";
617
                for (unsigned k = 0; k < skolems.size(); k++)
618
                {
619
                  Trace("sg-conjecture") << skolems[k] << (j == k ? "*" : "")
620
                                         << " ";
621
                }
622
                Trace("sg-conjecture") << "}";
623
              }
624
33
              Trace("sg-conjecture") << std::endl;
625
33
              disproven = false;
626
33
              break;
627
            }else{
628
4
              ce.push_back( git->second );
629
            }
630
          }
631
33
          if( disproven ){
632
            Trace("sg-conjecture") << "disproven : " << q << " : ";
633
            for (unsigned j = 0, ceSize = ce.size(); j < ceSize; j++)
634
            {
635
              Trace("sg-conjecture") << q[0][j] << " -> " << ce[j] << " ";
636
            }
637
            Trace("sg-conjecture") << std::endl;
638
          }
639
        }
640
      }
641
48
      Trace("thm-db") << "Theorem database is : " << std::endl;
642
48
      d_thm_index.debugPrint( "thm-db" );
643
48
      Trace("thm-db") << std::endl;
644
48
      Trace("sg-proc") << "...done build theorem index" << std::endl;
645
646
647
      //clear patterns
648
48
      d_patterns.clear();
649
48
      d_pattern_var_id.clear();
650
48
      d_pattern_var_duplicate.clear();
651
48
      d_pattern_is_normal.clear();
652
48
      d_pattern_is_relevant.clear();
653
48
      d_pattern_fun_id.clear();
654
48
      d_pattern_fun_sum.clear();
655
48
      d_rel_patterns.clear();
656
48
      d_rel_pattern_var_sum.clear();
657
48
      d_rel_pattern_typ_index.clear();
658
48
      d_rel_pattern_subs_index.clear();
659
660
48
      unsigned rel_term_count = 0;
661
96
      std::map< TypeNode, unsigned > rt_var_max;
662
96
      std::vector< TypeNode > rt_types;
663
96
      std::map< TypeNode, std::map< int, std::vector< Node > > > conj_lhs;
664
48
      unsigned addedLemmas = 0;
665
96
      unsigned maxDepth = options::conjectureGenMaxDepth();
666
163
      for( unsigned depth=1; depth<=maxDepth; depth++ ){
667
133
        Trace("sg-proc") << "Generate relevant LHS at depth " << depth << "..." << std::endl;
668
133
        Trace("sg-rel-term") << "Relevant terms of depth " << depth << " : " << std::endl;
669
        //set up environment
670
133
        d_tge.d_var_id.clear();
671
133
        d_tge.d_var_limit.clear();
672
133
        d_tge.reset( depth, true, TypeNode::null() );
673
1473
        while( d_tge.getNextTerm() ){
674
          //construct term
675
1340
          Node nn = d_tge.getTerm();
676
670
          if( !options::conjectureFilterCanonical() || considerTermCanon( nn, true ) ){
677
670
            rel_term_count++;
678
670
            Trace("sg-rel-term") << "*** Relevant term : ";
679
670
            d_tge.debugPrint( "sg-rel-term", "sg-rel-term-debug2" );
680
670
            Trace("sg-rel-term") << std::endl;
681
682
2010
            for( unsigned r=0; r<2; r++ ){
683
1340
              Trace("sg-rel-term-debug") << "...from equivalence classes (" << r << ") : ";
684
1340
              int index = d_tge.d_ccand_eqc[r].size()-1;
685
24922
              for( unsigned j=0; j<d_tge.d_ccand_eqc[r][index].size(); j++ ){
686
23582
                Trace("sg-rel-term-debug") << "e" << d_em[d_tge.d_ccand_eqc[r][index][j]] << " ";
687
              }
688
1340
              Trace("sg-rel-term-debug") << std::endl;
689
            }
690
1340
            TypeNode tnn = nn.getType();
691
670
            Trace("sg-gen-tg-debug") << "...term is " << nn << std::endl;
692
670
            conj_lhs[tnn][depth].push_back( nn );
693
694
            //add information about pattern
695
670
            Trace("sg-gen-tg-debug") << "Collect pattern information..." << std::endl;
696
670
            Assert(std::find(d_rel_patterns[tnn].begin(),
697
                             d_rel_patterns[tnn].end(),
698
                             nn)
699
                   == d_rel_patterns[tnn].end());
700
670
            d_rel_patterns[tnn].push_back( nn );
701
            //build information concerning the variables in this pattern
702
670
            unsigned sum = 0;
703
1340
            std::map< TypeNode, unsigned > typ_to_subs_index;
704
1340
            std::vector< TNode > gsubs_vars;
705
1867
            for( std::map< TypeNode, unsigned >::iterator it = d_tge.d_var_id.begin(); it != d_tge.d_var_id.end(); ++it ){
706
1197
              if( it->second>0 ){
707
922
                typ_to_subs_index[it->first] = sum;
708
922
                sum += it->second;
709
2014
                for( unsigned i=0; i<it->second; i++ ){
710
1092
                  gsubs_vars.push_back(
711
2184
                      d_termCanon.getCanonicalFreeVar(it->first, i));
712
                }
713
              }
714
            }
715
670
            d_rel_pattern_var_sum[nn] = sum;
716
            //register the pattern
717
670
            registerPattern( nn, tnn );
718
670
            Assert(d_pattern_is_normal[nn]);
719
670
            Trace("sg-gen-tg-debug") << "...done collect pattern information" << std::endl;
720
721
            //record information about types
722
670
            Trace("sg-gen-tg-debug") << "Collect type information..." << std::endl;
723
670
            PatternTypIndex * pti = &d_rel_pattern_typ_index;
724
1867
            for( std::map< TypeNode, unsigned >::iterator it = d_tge.d_var_id.begin(); it != d_tge.d_var_id.end(); ++it ){
725
1197
              pti = &pti->d_children[it->first][it->second];
726
              //record maximum
727
1197
              if( rt_var_max.find( it->first )==rt_var_max.end() || it->second>rt_var_max[it->first] ){
728
60
                rt_var_max[it->first] = it->second;
729
              }
730
            }
731
670
            if( std::find( rt_types.begin(), rt_types.end(), tnn )==rt_types.end() ){
732
95
              rt_types.push_back( tnn );
733
            }
734
670
            pti->d_terms.push_back( nn );
735
670
            Trace("sg-gen-tg-debug") << "...done collect type information" << std::endl;
736
737
670
            Trace("sg-gen-tg-debug") << "Build substitutions for ground EQC..." << std::endl;
738
1340
            std::vector< TNode > gsubs_terms;
739
670
            gsubs_terms.resize( gsubs_vars.size() );
740
670
            int index = d_tge.d_ccand_eqc[1].size()-1;
741
22959
            for( unsigned j=0; j<d_tge.d_ccand_eqc[1][index].size(); j++ ){
742
44578
              TNode r = d_tge.d_ccand_eqc[1][index][j];
743
22289
              Trace("sg-rel-term-debug") << "  Matches for e" << d_em[r] << ", which is ground term " << d_ground_eqc_map[r] << ":" << std::endl;
744
44578
              std::map< TypeNode, std::map< unsigned, TNode > > subs;
745
44578
              std::map< TNode, bool > rev_subs;
746
              //only get ground terms
747
22289
              unsigned mode = 2;
748
22289
              d_tge.resetMatching( r, mode );
749
192191
              while( d_tge.getNextMatch( r, subs, rev_subs ) ){
750
                //we will be building substitutions
751
84951
                bool firstTime = true;
752
214256
                for( std::map< TypeNode, std::map< unsigned, TNode > >::iterator it = subs.begin(); it != subs.end(); ++it ){
753
129305
                  unsigned tindex = typ_to_subs_index[it->first];
754
317353
                  for( std::map< unsigned, TNode >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
755
188048
                    if( !firstTime ){
756
103161
                      Trace("sg-rel-term-debug") << ", ";
757
                    }else{
758
84887
                      firstTime = false;
759
84887
                      Trace("sg-rel-term-debug") << "    ";
760
                    }
761
188048
                    Trace("sg-rel-term-debug") << it->first << ":x" << it2->first << " -> " << it2->second;
762
188048
                    Assert(tindex + it2->first < gsubs_terms.size());
763
188048
                    gsubs_terms[tindex+it2->first] = it2->second;
764
                  }
765
                }
766
84951
                Trace("sg-rel-term-debug") << std::endl;
767
84951
                d_rel_pattern_subs_index[nn].addSubstitution( r, gsubs_vars, gsubs_terms );
768
              }
769
            }
770
670
            Trace("sg-gen-tg-debug") << "...done build substitutions for ground EQC" << std::endl;
771
          }else{
772
            Trace("sg-gen-tg-debug") << "> not canonical : " << nn << std::endl;
773
          }
774
        }
775
133
        Trace("sg-proc") << "...done generate terms at depth " << depth << std::endl;
776
133
        Trace("sg-stats") << "--------> Total LHS of depth " << depth << " : " << rel_term_count << std::endl;
777
        //Trace("conjecture-count") << "Total LHS of depth " << depth << " : " << conj_lhs[depth].size() << std::endl;
778
779
        /* test...
780
        for( unsigned i=0; i<rt_types.size(); i++ ){
781
          Trace("sg-term-enum") << "Term enumeration for " << rt_types[i] << " : " << std::endl;
782
          Trace("sg-term-enum") << "Ground term : " << rt_types[i].mkGroundTerm() << std::endl;
783
          for( unsigned j=0; j<150; j++ ){
784
            Trace("sg-term-enum") << "  " << getEnumerateTerm( rt_types[i], j ) << std::endl;
785
          }
786
        }
787
        */
788
789
        //consider types from relevant terms
790
487
        for( unsigned rdepth=0; rdepth<=depth; rdepth++ ){
791
          //set up environment
792
372
          d_tge.d_var_id.clear();
793
372
          d_tge.d_var_limit.clear();
794
648
          for( std::map< TypeNode, unsigned >::iterator it = rt_var_max.begin(); it != rt_var_max.end(); ++it ){
795
276
            d_tge.d_var_id[ it->first ] = it->second;
796
276
            d_tge.d_var_limit[ it->first ] = it->second;
797
          }
798
372
          std::shuffle(rt_types.begin(), rt_types.end(), Random::getRandom());
799
726
          std::map< TypeNode, std::vector< Node > > conj_rhs;
800
1089
          for( unsigned i=0; i<rt_types.size(); i++ ){
801
802
717
            Trace("sg-proc") << "Generate relevant RHS terms of type " << rt_types[i] << " at depth " << rdepth << "..." << std::endl;
803
717
            d_tge.reset( rdepth, false, rt_types[i] );
804
805
5091
            while( d_tge.getNextTerm() ){
806
4374
              Node rhs = d_tge.getTerm();
807
2187
              if( considerTermCanon( rhs, false ) ){
808
2187
                Trace("sg-rel-prop") << "Relevant RHS : " << rhs << std::endl;
809
                //register pattern
810
2187
                Assert(rhs.getType() == rt_types[i]);
811
2187
                registerPattern( rhs, rt_types[i] );
812
2187
                if( rdepth<depth ){
813
                  //consider against all LHS at depth
814
15207
                  for( unsigned j=0; j<conj_lhs[rt_types[i]][depth].size(); j++ ){
815
13913
                    processCandidateConjecture( conj_lhs[rt_types[i]][depth][j], rhs, depth, rdepth );
816
                  }
817
                }else{
818
893
                  conj_rhs[rt_types[i]].push_back( rhs );
819
                }
820
              }
821
            }
822
          }
823
372
          flushWaitingConjectures( addedLemmas, depth, rdepth );
824
          //consider against all LHS up to depth
825
372
          if( rdepth==depth ){
826
340
            for( unsigned lhs_depth = 1; lhs_depth<=depth; lhs_depth++ ){
827
221
              if( (int)addedLemmas<options::conjectureGenPerRound() ){
828
221
                Trace("sg-proc") << "Consider conjectures at depth (" << lhs_depth << ", " << rdepth << ")..." << std::endl;
829
420
                for( std::map< TypeNode, std::vector< Node > >::iterator it = conj_rhs.begin(); it != conj_rhs.end(); ++it ){
830
1815
                  for( unsigned j=0; j<it->second.size(); j++ ){
831
8843
                    for( unsigned k=0; k<conj_lhs[it->first][lhs_depth].size(); k++ ){
832
7227
                      processCandidateConjecture( conj_lhs[it->first][lhs_depth][k], it->second[j], lhs_depth, rdepth );
833
                    }
834
                  }
835
                }
836
221
                flushWaitingConjectures( addedLemmas, lhs_depth, depth );
837
              }
838
            }
839
          }
840
372
          if( (int)addedLemmas>=options::conjectureGenPerRound() ){
841
18
            break;
842
          }
843
        }
844
133
        if( (int)addedLemmas>=options::conjectureGenPerRound() ){
845
18
          break;
846
        }
847
      }
848
48
      Trace("sg-stats") << "Total conjectures considered : " << d_conj_count << std::endl;
849
48
      if( Trace.isOn("thm-ee") ){
850
        Trace("thm-ee") << "Universal equality engine is : " << std::endl;
851
        eq::EqClassesIterator ueqcs_i = eq::EqClassesIterator( &d_uequalityEngine );
852
        while( !ueqcs_i.isFinished() ){
853
          TNode r = (*ueqcs_i);
854
          bool firstTime = true;
855
          Node rr = getUniversalRepresentative(r);
856
          Trace("thm-ee") << "  " << rr;
857
          Trace("thm-ee") << " : { ";
858
          eq::EqClassIterator ueqc_i = eq::EqClassIterator( r, &d_uequalityEngine );
859
          while( !ueqc_i.isFinished() ){
860
            TNode n = (*ueqc_i);
861
            if( rr!=n ){
862
              if( firstTime ){
863
                Trace("thm-ee") << std::endl;
864
                firstTime = false;
865
              }
866
              Trace("thm-ee") << "    " << n << std::endl;
867
            }
868
            ++ueqc_i;
869
          }
870
          if( !firstTime ){ Trace("thm-ee") << "  "; }
871
          Trace("thm-ee") << "}" << std::endl;
872
          ++ueqcs_i;
873
        }
874
        Trace("thm-ee") << std::endl;
875
      }
876
48
      if( Trace.isOn("sg-engine") ){
877
        double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
878
        Trace("sg-engine") << "Finished conjecture generator, time = " << (clSet2-clSet) << std::endl;
879
      }
880
    }
881
  }
882
174
}
883
884
593
unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth ) {
885
593
  if( !d_waiting_conjectures_lhs.empty() ){
886
26
    Trace("sg-proc") << "Generated " << d_waiting_conjectures_lhs.size() << " conjectures at depth " << ldepth << "/" << rdepth << "." << std::endl;
887
26
    if( (int)addedLemmas<options::conjectureGenPerRound() ){
888
      /*
889
      std::vector< unsigned > indices;
890
      for( unsigned i=0; i<d_waiting_conjectures_lhs.size(); i++ ){
891
        indices.push_back( i );
892
      }
893
      bool doSort = false;
894
      if( doSort ){
895
        //sort them based on score
896
        sortConjectureScore scs;
897
        scs.d_scores.insert( scs.d_scores.begin(), d_waiting_conjectures_score.begin(), d_waiting_conjectures_score.end() );
898
        std::sort( indices.begin(), indices.end(), scs );
899
      }
900
      //if( doSort && d_waiting_conjectures_score[indices[0]]<optFilterScoreThreshold() ){
901
      */
902
26
      unsigned prevCount = d_conj_count;
903
43
      for( unsigned i=0; i<d_waiting_conjectures_lhs.size(); i++ ){
904
35
        if( d_waiting_conjectures_score[i]>=optFilterScoreThreshold() ){
905
          //we have determined a relevant subgoal
906
52
          Node lhs = d_waiting_conjectures_lhs[i];
907
52
          Node rhs = d_waiting_conjectures_rhs[i];
908
35
          if( options::conjectureFilterCanonical() && ( getUniversalRepresentative( lhs )!=lhs || getUniversalRepresentative( rhs )!=rhs ) ){
909
            //skip
910
          }else{
911
18
            Trace("sg-engine") << "*** Consider conjecture : " << lhs << " == " << rhs << std::endl;
912
18
            Trace("sg-engine-debug") << "      score : " << d_waiting_conjectures_score[i] << std::endl;
913
18
            if( optStatsOnly() ){
914
              d_conj_count++;
915
            }else{
916
18
              std::vector< Node > bvs;
917
25
              for (const std::pair<const TypeNode, unsigned>& lhs_pattern :
918
18
                   d_pattern_var_id[lhs])
919
              {
920
50
                for (unsigned j = 0; j <= lhs_pattern.second; j++)
921
                {
922
25
                  bvs.push_back(getFreeVar(lhs_pattern.first, j));
923
                }
924
              }
925
18
              Node rsg;
926
18
              if( !bvs.empty() ){
927
36
                Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs );
928
18
                rsg = NodeManager::currentNM()->mkNode( FORALL, bvl, lhs.eqNode( rhs ) );
929
              }else{
930
                rsg = lhs.eqNode( rhs );
931
              }
932
18
              rsg = Rewriter::rewrite( rsg );
933
18
              d_conjectures.push_back( rsg );
934
18
              d_eq_conjectures[lhs].push_back( rhs );
935
18
              d_eq_conjectures[rhs].push_back( lhs );
936
937
18
              Node lem = NodeManager::currentNM()->mkNode( OR, rsg.negate(), rsg );
938
18
              d_qim.addPendingLemma(lem, InferenceId::UNKNOWN);
939
18
              d_qim.addPendingPhaseRequirement(rsg, false);
940
18
              addedLemmas++;
941
18
              if( (int)addedLemmas>=options::conjectureGenPerRound() ){
942
18
                break;
943
              }
944
            }
945
          }
946
        }
947
      }
948
26
      Trace("sg-proc") << "...have now added " << addedLemmas << " conjecture lemmas." << std::endl;
949
26
      if( optStatsOnly() ){
950
        Trace("sg-stats") << "Generated " << (d_conj_count-prevCount) << " conjectures at depth " << ldepth << "/" << rdepth << "." << std::endl;
951
      }
952
    }
953
26
    d_waiting_conjectures_lhs.clear();
954
26
    d_waiting_conjectures_rhs.clear();
955
26
    d_waiting_conjectures_score.clear();
956
26
    d_waiting_conjectures.clear();
957
  }
958
593
  return addedLemmas;
959
}
960
961
7553
bool ConjectureGenerator::considerTermCanon( Node ln, bool genRelevant ){
962
7553
  if( !ln.isNull() ){
963
    //do not consider if it is non-canonical, and either:
964
    //  (1) we are not generating relevant terms, or
965
    //  (2) its canonical form is a generalization.
966
14938
    Node lnr = getUniversalRepresentative(ln, true);
967
7553
    if( lnr==ln ){
968
7197
      markReportedCanon( ln );
969
356
    }else if( !genRelevant || isGeneralization( lnr, ln ) ){
970
168
      Trace("sg-gen-consider-term") << "Do not consider term, " << ln << " is not canonical representation (which is " << lnr << ")." << std::endl;
971
168
      return false;
972
    }
973
  }
974
7385
  Trace("sg-gen-tg-debug") << "Will consider term canon " << ln << std::endl;
975
7385
  Trace("sg-gen-consider-term-debug") << std::endl;
976
7385
  return true;
977
}
978
979
5540
unsigned ConjectureGenerator::collectFunctions( TNode opat, TNode pat, std::map< TNode, unsigned >& funcs,
980
                                             std::map< TypeNode, unsigned >& mnvn, std::map< TypeNode, unsigned >& mxvn ){
981
5540
  if( pat.hasOperator() ){
982
2997
    funcs[pat.getOperator()]++;
983
2997
    if( !d_tge.isRelevantFunc( pat.getOperator() ) ){
984
      d_pattern_is_relevant[opat] = false;
985
    }
986
2997
    unsigned sum = 1;
987
6929
    for( unsigned i=0; i<pat.getNumChildren(); i++ ){
988
3932
      sum += collectFunctions( opat, pat[i], funcs, mnvn, mxvn );
989
    }
990
2997
    return sum;
991
  }else{
992
2543
    Assert(pat.getNumChildren() == 0);
993
2543
    funcs[pat]++;
994
    //for variables
995
2543
    if( pat.getKind()==BOUND_VARIABLE ){
996
2526
      if( funcs[pat]>1 ){
997
        //duplicate variable
998
31
        d_pattern_var_duplicate[opat]++;
999
      }else{
1000
        //check for max/min
1001
4990
        TypeNode tn = pat.getType();
1002
2495
        unsigned vn = pat.getAttribute(InstVarNumAttribute());
1003
2495
        std::map< TypeNode, unsigned >::iterator it = mnvn.find( tn );
1004
2495
        if( it!=mnvn.end() ){
1005
315
          if( vn<it->second ){
1006
            d_pattern_is_normal[opat] = false;
1007
            mnvn[tn] = vn;
1008
315
          }else if( vn>mxvn[tn] ){
1009
            if( vn!=mxvn[tn]+1 ){
1010
              d_pattern_is_normal[opat] = false;
1011
            }
1012
            mxvn[tn] = vn;
1013
          }
1014
        }else{
1015
          //first variable of this type
1016
2180
          mnvn[tn] = vn;
1017
2180
          mxvn[tn] = vn;
1018
        }
1019
      }
1020
    }else{
1021
17
      d_pattern_is_relevant[opat] = false;
1022
    }
1023
2543
    return 1;
1024
  }
1025
}
1026
1027
7986
void ConjectureGenerator::registerPattern( Node pat, TypeNode tpat ) {
1028
7986
  if( std::find( d_patterns[tpat].begin(), d_patterns[tpat].end(), pat )==d_patterns[tpat].end() ){
1029
1608
    d_patterns[TypeNode::null()].push_back( pat );
1030
1608
    d_patterns[tpat].push_back( pat );
1031
1032
1608
    Assert(d_pattern_fun_id.find(pat) == d_pattern_fun_id.end());
1033
1608
    Assert(d_pattern_var_id.find(pat) == d_pattern_var_id.end());
1034
1035
    //collect functions
1036
3216
    std::map< TypeNode, unsigned > mnvn;
1037
1608
    d_pattern_fun_sum[pat] = collectFunctions( pat, pat, d_pattern_fun_id[pat], mnvn, d_pattern_var_id[pat] );
1038
1608
    if( d_pattern_is_normal.find( pat )==d_pattern_is_normal.end() ){
1039
1608
      d_pattern_is_normal[pat] = true;
1040
    }
1041
1608
    if( d_pattern_is_relevant.find( pat )==d_pattern_is_relevant.end() ){
1042
1591
      d_pattern_is_relevant[pat] = true;
1043
    }
1044
  }
1045
7986
}
1046
1047
226
bool ConjectureGenerator::isGeneralization( TNode patg, TNode pat, std::map< TNode, TNode >& subs ) {
1048
226
  if( patg.getKind()==BOUND_VARIABLE ){
1049
8
    std::map< TNode, TNode >::iterator it = subs.find( patg );
1050
8
    if( it!=subs.end() ){
1051
      return it->second==pat;
1052
    }else{
1053
8
      subs[patg] = pat;
1054
8
      return true;
1055
    }
1056
  }else{
1057
218
    Assert(patg.hasOperator());
1058
218
    if( !pat.hasOperator() || patg.getOperator()!=pat.getOperator() ){
1059
188
      return false;
1060
    }else{
1061
30
      Assert(patg.getNumChildren() == pat.getNumChildren());
1062
38
      for( unsigned i=0; i<patg.getNumChildren(); i++ ){
1063
38
        if( !isGeneralization( patg[i], pat[i], subs ) ){
1064
30
          return false;
1065
        }
1066
      }
1067
      return true;
1068
    }
1069
  }
1070
}
1071
1072
int ConjectureGenerator::calculateGeneralizationDepth( TNode n, std::vector< TNode >& fv ) {
1073
  if( n.getKind()==BOUND_VARIABLE ){
1074
    if( std::find( fv.begin(), fv.end(), n )==fv.end() ){
1075
      fv.push_back( n );
1076
      return 0;
1077
    }else{
1078
      return 1;
1079
    }
1080
  }else{
1081
    int depth = 1;
1082
    for( unsigned i=0; i<n.getNumChildren(); i++ ){
1083
      depth += calculateGeneralizationDepth( n[i], fv );
1084
    }
1085
    return depth;
1086
  }
1087
}
1088
1089
15
Node ConjectureGenerator::getPredicateForType( TypeNode tn ) {
1090
15
  std::map< TypeNode, Node >::iterator it = d_typ_pred.find( tn );
1091
15
  if( it==d_typ_pred.end() ){
1092
22
    TypeNode op_tn = NodeManager::currentNM()->mkFunctionType( tn, NodeManager::currentNM()->booleanType() );
1093
22
    Node op = NodeManager::currentNM()->mkSkolem( "PE", op_tn, "was created by conjecture ground term enumerator." );
1094
11
    d_typ_pred[tn] = op;
1095
11
    return op;
1096
  }else{
1097
4
    return it->second;
1098
  }
1099
}
1100
1101
15
void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< Node >& terms ) {
1102
15
  if( n.getNumChildren()>0 ){
1103
30
    Trace("sg-gt-enum-debug") << "Get enumerate uf terms " << n << " (" << num
1104
15
                              << ")" << std::endl;
1105
15
    TermEnumeration* te = d_quantEngine->getTermEnumeration();
1106
    // below, we do a fair enumeration of vectors vec of indices whose sum is
1107
    // 1,2,3, ...
1108
30
    std::vector< int > vec;
1109
30
    std::vector< TypeNode > types;
1110
34
    for( unsigned i=0; i<n.getNumChildren(); i++ ){
1111
19
      vec.push_back( 0 );
1112
38
      TypeNode tn = n[i].getType();
1113
19
      if (tn.isClosedEnumerable())
1114
      {
1115
19
        types.push_back( tn );
1116
      }else{
1117
        return;
1118
      }
1119
    }
1120
    // the index of the last child is determined by the limit of the sum
1121
    // of indices of children (size_limit) and the sum of the indices of the
1122
    // other children (vec_sum). Hence, we pop here and add this value at each
1123
    // iteration of the loop.
1124
15
    vec.pop_back();
1125
15
    int size_limit = 0;
1126
15
    int vec_sum = -1;
1127
15
    unsigned index = 0;
1128
15
    unsigned last_size = terms.size();
1129
2665
    while( terms.size()<num ){
1130
1325
      if( vec_sum==-1 ){
1131
590
        vec_sum = 0;
1132
        // we will construct a new child below
1133
        // since sum is 0, the index of last child is limit
1134
590
        vec.push_back( size_limit );
1135
      }
1136
735
      else if (index < vec.size())
1137
      {
1138
196
        Assert(index < types.size());
1139
        //see if we can iterate current
1140
392
        if (vec_sum < size_limit
1141
392
            && !te->getEnumerateTerm(types[index], vec[index] + 1).isNull())
1142
        {
1143
160
          vec[index]++;
1144
160
          vec_sum++;
1145
          // we will construct a new child below
1146
          // add the index of the last child, its index is (limit-sum)
1147
160
          vec.push_back( size_limit - vec_sum );
1148
        }else{
1149
          // reset the index
1150
36
          vec_sum -= vec[index];
1151
36
          vec[index] = 0;
1152
36
          index++;
1153
        }
1154
      }
1155
1325
      if (index < vec.size())
1156
      {
1157
        // if we are ready to construct the term
1158
750
        if( vec.size()==n.getNumChildren() ){
1159
          Node lc =
1160
1500
              te->getEnumerateTerm(types[vec.size() - 1], vec[vec.size() - 1]);
1161
750
          if( !lc.isNull() ){
1162
1700
            for( unsigned i=0; i<vec.size(); i++ ){
1163
950
              Trace("sg-gt-enum-debug") << vec[i] << " ";
1164
            }
1165
750
            Trace("sg-gt-enum-debug") << " / " << size_limit << std::endl;
1166
1700
            for( unsigned i=0; i<n.getNumChildren(); i++ ){
1167
950
              Trace("sg-gt-enum-debug") << n[i].getType() << " ";
1168
            }
1169
750
            Trace("sg-gt-enum-debug") << std::endl;
1170
1500
            std::vector< Node > children;
1171
750
            children.push_back( n.getOperator() );
1172
950
            for( unsigned i=0; i<(vec.size()-1); i++ ){
1173
400
              Node nn = te->getEnumerateTerm(types[i], vec[i]);
1174
200
              Assert(!nn.isNull());
1175
200
              Assert(nn.getType() == n[i].getType());
1176
200
              children.push_back( nn );
1177
            }
1178
750
            children.push_back( lc );
1179
1500
            Node nenum = NodeManager::currentNM()->mkNode(APPLY_UF, children);
1180
1500
            Trace("sg-gt-enum")
1181
750
                << "Ground term enumerate : " << nenum << std::endl;
1182
750
            terms.push_back(nenum);
1183
          }
1184
          // pop the index for the last child
1185
750
          vec.pop_back();
1186
750
          index = 0;
1187
        }
1188
      }else{
1189
        // no more indices to increment, we reset and increment size_limit
1190
575
        if( terms.size()>last_size ){
1191
575
          last_size = terms.size();
1192
575
          size_limit++;
1193
611
          for( unsigned i=0; i<vec.size(); i++ ){
1194
36
            vec[i] = 0;
1195
          }
1196
575
          vec_sum = -1;
1197
        }else{
1198
          // No terms were generated at the previous size.
1199
          // Thus, we've saturated, no more terms can be enumerated.
1200
          return;
1201
        }
1202
      }
1203
    }
1204
  }else{
1205
    terms.push_back( n );
1206
  }
1207
}
1208
1209
15
void ConjectureGenerator::getEnumeratePredUfTerm( Node n, unsigned num, std::vector< Node >& terms ) {
1210
30
  std::vector< Node > uf_terms;
1211
15
  getEnumerateUfTerm( n, num, uf_terms );
1212
30
  Node p = getPredicateForType( n.getType() );
1213
765
  for( unsigned i=0; i<uf_terms.size(); i++ ){
1214
750
    terms.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, p, uf_terms[i] ) );
1215
  }
1216
15
}
1217
1218
21140
void ConjectureGenerator::processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth ) {
1219
21140
  int score = considerCandidateConjecture( lhs, rhs );
1220
21140
  if( score>0 ){
1221
63
    Trace("sg-conjecture") << "* Candidate conjecture : " << lhs << " == " << rhs << std::endl;
1222
63
    Trace("sg-conjecture-debug") << "     LHS, RHS generalization depth : " << lhs_depth << ", " << rhs_depth << std::endl;
1223
63
    Trace("sg-conjecture-debug") << "     confirmed = " << d_subs_confirmCount << ", #witnesses range = " << d_subs_confirmWitnessRange.size() << "." << std::endl;
1224
63
    Trace("sg-conjecture-debug") << "     #witnesses for ";
1225
63
    bool firstTime = true;
1226
171
    for( std::map< TNode, std::vector< TNode > >::iterator it = d_subs_confirmWitnessDomain.begin(); it != d_subs_confirmWitnessDomain.end(); ++it ){
1227
108
      if( !firstTime ){
1228
45
        Trace("sg-conjecture-debug") << ", ";
1229
      }
1230
108
      Trace("sg-conjecture-debug") << it->first << " : " << it->second.size();
1231
      //if( it->second.size()==1 ){
1232
      //  Trace("sg-conjecture-debug") << " (" << it->second[0] << ")";
1233
      //}
1234
108
      Trace("sg-conjecture-debug2") << " (";
1235
2932
      for( unsigned j=0; j<it->second.size(); j++ ){
1236
2824
        if( j>0 ){ Trace("sg-conjecture-debug2") << " "; }
1237
2824
        Trace("sg-conjecture-debug2") << d_ground_eqc_map[it->second[j]];
1238
      }
1239
108
      Trace("sg-conjecture-debug2") << ")";
1240
108
      firstTime = false;
1241
    }
1242
63
    Trace("sg-conjecture-debug") << std::endl;
1243
63
    Trace("sg-conjecture-debug") << "     unknown = " << d_subs_unkCount << std::endl;
1244
    //Assert( getUniversalRepresentative( rhs )==rhs );
1245
    //Assert( getUniversalRepresentative( lhs )==lhs );
1246
63
    d_waiting_conjectures_lhs.push_back( lhs );
1247
63
    d_waiting_conjectures_rhs.push_back( rhs );
1248
63
    d_waiting_conjectures_score.push_back( score );
1249
63
    d_waiting_conjectures[lhs].push_back( rhs );
1250
63
    d_waiting_conjectures[rhs].push_back( lhs );
1251
  }else{
1252
21077
    Trace("sg-conjecture-debug2") << "...do not consider " << lhs << " == " << rhs << ", score = " << score << std::endl;
1253
  }
1254
21140
}
1255
1256
21140
int ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) {
1257
21140
  Assert(lhs.getType() == rhs.getType());
1258
1259
21140
  Trace("sg-cconj-debug") << "Consider candidate conjecture : " << lhs << " == " << rhs << "?" << std::endl;
1260
21140
  if( lhs==rhs ){
1261
318
    Trace("sg-cconj-debug") << "  -> trivial." << std::endl;
1262
318
    return -1;
1263
  }else{
1264
20822
    if( lhs.getKind()==APPLY_CONSTRUCTOR && rhs.getKind()==APPLY_CONSTRUCTOR ){
1265
3813
      Trace("sg-cconj-debug") << "  -> irrelevant by syntactic analysis." << std::endl;
1266
3813
      return -1;
1267
    }
1268
    //variables of LHS must subsume variables of RHS
1269
37131
    for( std::map< TypeNode, unsigned >::iterator it = d_pattern_var_id[rhs].begin(); it != d_pattern_var_id[rhs].end(); ++it ){
1270
24819
      std::map< TypeNode, unsigned >::iterator itl = d_pattern_var_id[lhs].find( it->first );
1271
24819
      if( itl!=d_pattern_var_id[lhs].end() ){
1272
20122
        if( itl->second<it->second ){
1273
          Trace("sg-cconj-debug") << "  -> variables of sort " << it->first << " are not subsumed." << std::endl;
1274
4697
          return -1;
1275
        }else{
1276
20122
          Trace("sg-cconj-debug2") << "  variables of sort " << it->first << " are : " << itl->second << " vs " << it->second << std::endl;
1277
        }
1278
      }else{
1279
4697
        Trace("sg-cconj-debug") << "  -> has no variables of sort " << it->first << "." << std::endl;
1280
4697
        return -1;
1281
      }
1282
    }
1283
1284
    //currently active conjecture?
1285
12312
    std::map< Node, std::vector< Node > >::iterator iteq = d_eq_conjectures.find( lhs );
1286
12312
    if( iteq!=d_eq_conjectures.end() ){
1287
343
      if( std::find( iteq->second.begin(), iteq->second.end(), rhs )!=iteq->second.end() ){
1288
31
        Trace("sg-cconj-debug") << "  -> this conjecture is already active." << std::endl;
1289
31
        return -1;
1290
      }
1291
    }
1292
    //current a waiting conjecture?
1293
12281
    std::map< Node, std::vector< Node > >::iterator itw = d_waiting_conjectures.find( lhs );
1294
12281
    if( itw!=d_waiting_conjectures.end() ){
1295
152
      if( std::find( itw->second.begin(), itw->second.end(), rhs )!=itw->second.end() ){
1296
        Trace("sg-cconj-debug") << "  -> already are considering this conjecture." << std::endl;
1297
        return -1;
1298
      }
1299
    }
1300
    //check if canonical representation (should be, but for efficiency this is not guarenteed)
1301
    //if( options::conjectureFilterCanonical() && ( getUniversalRepresentative( lhs )!=lhs || getUniversalRepresentative( rhs )!=rhs ) ){
1302
    //  Trace("sg-cconj") << "  -> after processing, not canonical." << std::endl;
1303
    //  return -1;
1304
    //}
1305
1306
    int score;
1307
12281
    bool scoreSet = false;
1308
1309
12281
    Trace("sg-cconj") << "Consider possible candidate conjecture : " << lhs << " == " << rhs << "?" << std::endl;
1310
    //find witness for counterexample, if possible
1311
12281
    if( options::conjectureFilterModel() ){
1312
12281
      Assert(d_rel_pattern_var_sum.find(lhs) != d_rel_pattern_var_sum.end());
1313
12281
      Trace("sg-cconj-debug") << "Notify substitutions over " << d_rel_pattern_var_sum[lhs] << " variables." << std::endl;
1314
19351
      std::map< TNode, TNode > subs;
1315
12281
      d_subs_confirmCount = 0;
1316
12281
      d_subs_confirmWitnessRange.clear();
1317
12281
      d_subs_confirmWitnessDomain.clear();
1318
12281
      d_subs_unkCount = 0;
1319
12281
      if( !d_rel_pattern_subs_index[lhs].notifySubstitutions( this, subs, rhs, d_rel_pattern_var_sum[lhs] ) ){
1320
5211
        Trace("sg-cconj") << "  -> found witness that falsifies the conjecture." << std::endl;
1321
5211
        return -1;
1322
      }
1323
      //score is the minimum number of distinct substitutions for a variable
1324
7178
      for( std::map< TNode, std::vector< TNode > >::iterator it = d_subs_confirmWitnessDomain.begin(); it != d_subs_confirmWitnessDomain.end(); ++it ){
1325
108
        int num = (int)it->second.size();
1326
108
        if( !scoreSet || num<score ){
1327
73
          score = num;
1328
73
          scoreSet = true;
1329
        }
1330
      }
1331
7070
      if( !scoreSet ){
1332
7007
        score = 0;
1333
      }
1334
7070
      Trace("sg-cconj") << "     confirmed = " << d_subs_confirmCount << ", #witnesses range = " << d_subs_confirmWitnessRange.size() << "." << std::endl;
1335
7178
      for( std::map< TNode, std::vector< TNode > >::iterator it = d_subs_confirmWitnessDomain.begin(); it != d_subs_confirmWitnessDomain.end(); ++it ){
1336
108
        Trace("sg-cconj") << "     #witnesses for " << it->first << " : " << it->second.size() << std::endl;
1337
      }
1338
    }else{
1339
      score = 1;
1340
    }
1341
1342
7070
    Trace("sg-cconj") << "  -> SUCCESS." << std::endl;
1343
7070
    Trace("sg-cconj") << "     score : " << score << std::endl;
1344
1345
7070
    return score;
1346
  }
1347
}
1348
1349
882686
bool ConjectureGenerator::notifySubstitution( TNode glhs, std::map< TNode, TNode >& subs, TNode rhs ) {
1350
882686
  if( Trace.isOn("sg-cconj-debug") ){
1351
    Trace("sg-cconj-debug") << "Ground eqc for LHS : " << glhs << ", based on substituion: " << std::endl;
1352
    for( std::map< TNode, TNode >::iterator it = subs.begin(); it != subs.end(); ++it ){
1353
      Assert(getRepresentative(it->second) == it->second);
1354
      Trace("sg-cconj-debug") << "  " << it->first << " -> " << it->second << std::endl;
1355
    }
1356
  }
1357
882686
  Trace("sg-cconj-debug") << "Evaluate RHS : : " << rhs << std::endl;
1358
  //get the representative of rhs with substitution subs
1359
1765372
  TNode grhs = getTermDatabase()->getEntailedTerm( rhs, subs, true );
1360
882686
  Trace("sg-cconj-debug") << "...done evaluating term, got : " << grhs << std::endl;
1361
882686
  if( !grhs.isNull() ){
1362
17673
    if( glhs!=grhs ){
1363
5211
      Trace("sg-cconj-debug") << "Ground eqc for RHS : " << grhs << std::endl;
1364
      //check based on ground terms
1365
5211
      std::map< TNode, Node >::iterator itl = d_ground_eqc_map.find( glhs );
1366
5211
      if( itl!=d_ground_eqc_map.end() ){
1367
5211
        std::map< TNode, Node >::iterator itr = d_ground_eqc_map.find( grhs );
1368
5211
        if( itr!=d_ground_eqc_map.end() ){
1369
1802
          Trace("sg-cconj-debug") << "We have ground terms " << itl->second << " and " << itr->second << "." << std::endl;
1370
1802
          if( itl->second.isConst() && itr->second.isConst() ){
1371
1734
            Trace("sg-cconj-debug") << "...disequal constants." << std::endl;
1372
1734
            Trace("sg-cconj-witness") << "  Witness of falsification : " << itl->second << " != " << itr->second << ", substutition is : " << std::endl;
1373
5744
            for( std::map< TNode, TNode >::iterator it = subs.begin(); it != subs.end(); ++it ){
1374
4010
              Trace("sg-cconj-witness") << "    " << it->first << " -> " << it->second << std::endl;
1375
            }
1376
1734
            return false;
1377
          }
1378
        }
1379
      }
1380
    }
1381
15939
    Trace("sg-cconj-debug") << "RHS is identical." << std::endl;
1382
15939
    bool isGroundSubs = true;
1383
49155
    for( std::map< TNode, TNode >::iterator it = subs.begin(); it != subs.end(); ++it ){
1384
33216
      std::map< TNode, Node >::iterator git = d_ground_eqc_map.find( it->second );
1385
33216
      if( git==d_ground_eqc_map.end() ){
1386
        isGroundSubs = false;
1387
        break;
1388
      }
1389
    }
1390
15939
    if( isGroundSubs ){
1391
15939
      if( glhs==grhs ){
1392
12462
        Trace("sg-cconj-witness") << "  Witnessed " << glhs << " == " << grhs << ", substutition is : " << std::endl;
1393
37248
        for( std::map< TNode, TNode >::iterator it = subs.begin(); it != subs.end(); ++it ){
1394
24786
          Trace("sg-cconj-witness") << "    " << it->first << " -> " << it->second << std::endl;
1395
24786
          if( std::find( d_subs_confirmWitnessDomain[it->first].begin(), d_subs_confirmWitnessDomain[it->first].end(), it->second )==d_subs_confirmWitnessDomain[it->first].end() ){
1396
5633
            d_subs_confirmWitnessDomain[it->first].push_back( it->second );
1397
          }
1398
        }
1399
12462
        d_subs_confirmCount++;
1400
12462
        if( std::find( d_subs_confirmWitnessRange.begin(), d_subs_confirmWitnessRange.end(), glhs )==d_subs_confirmWitnessRange.end() ){
1401
2643
          d_subs_confirmWitnessRange.push_back( glhs );
1402
        }
1403
      }else{
1404
3477
        if( optFilterUnknown() ){
1405
3477
          Trace("sg-cconj-debug") << "...ground substitution giving terms that are neither equal nor disequal." << std::endl;
1406
3477
          return false;
1407
        }
1408
      }
1409
    }
1410
  }else{
1411
865013
    Trace("sg-cconj-debug") << "(could not ground eqc for RHS)." << std::endl;
1412
  }
1413
877475
  return true;
1414
}
1415
1416
1417
1418
1419
1420
1421
3674
void TermGenerator::reset( TermGenEnv * s, TypeNode tn ) {
1422
3674
  Assert(d_children.empty());
1423
3674
  d_typ = tn;
1424
3674
  d_status = 0;
1425
3674
  d_status_num = 0;
1426
3674
  d_children.clear();
1427
3674
  Trace("sg-gen-tg-debug2") << "...add to context " << this << std::endl;
1428
3674
  d_id = s->d_tg_id;
1429
3674
  s->changeContext( true );
1430
3674
}
1431
1432
48580
bool TermGenerator::getNextTerm( TermGenEnv * s, unsigned depth ) {
1433
48580
  if( Trace.isOn("sg-gen-tg-debug2") ){
1434
    Trace("sg-gen-tg-debug2") << this << " getNextTerm depth " << depth << " : status = " << d_status << ", num = " << d_status_num;
1435
    if( d_status==5 ){
1436
      TNode f = s->getTgFunc( d_typ, d_status_num );
1437
      Trace("sg-gen-tg-debug2") << ", f = " << f;
1438
      Trace("sg-gen-tg-debug2") << ", #args = " << s->d_func_args[f].size();
1439
      Trace("sg-gen-tg-debug2") << ", childNum = " << d_status_child_num;
1440
      Trace("sg-gen-tg-debug2") << ", #children = " << d_children.size();
1441
    }
1442
    Trace("sg-gen-tg-debug2") << std::endl;
1443
  }
1444
1445
48580
  if( d_status==0 ){
1446
3674
    d_status++;
1447
3674
    if( !d_typ.isNull() ){
1448
3541
      if( s->allowVar( d_typ ) ){
1449
        //allocate variable
1450
1691
        d_status_num = s->d_var_id[d_typ];
1451
1691
        s->addVar( d_typ );
1452
1691
        Trace("sg-gen-tg-debug2") << this << " ...return unique var #" << d_status_num << std::endl;
1453
1691
        return s->considerCurrentTerm() ? true : getNextTerm( s, depth );
1454
      }else{
1455
        //check allocating new variable
1456
1850
        d_status++;
1457
1850
        d_status_num = -1;
1458
1850
        if( s->d_gen_relevant_terms ){
1459
          s->d_tg_gdepth++;
1460
        }
1461
1850
        return getNextTerm( s, depth );
1462
      }
1463
    }else{
1464
133
      d_status = 4;
1465
133
      d_status_num = -1;
1466
133
      return getNextTerm( s, depth );
1467
    }
1468
44906
  }else if( d_status==2 ){
1469
    //cleanup previous information
1470
    //if( d_status_num>=0 ){
1471
    //  s->d_var_eq_tg[d_status_num].pop_back();
1472
    //}
1473
    //check if there is another variable
1474
6994
    if( (d_status_num+1)<(int)s->getNumTgVars( d_typ ) ){
1475
3453
      d_status_num++;
1476
      //we have equated two variables
1477
      //s->d_var_eq_tg[d_status_num].push_back( d_id );
1478
3453
      Trace("sg-gen-tg-debug2") << this << "...consider other var #" << d_status_num << std::endl;
1479
3453
      return s->considerCurrentTerm() ? true : getNextTerm( s, depth );
1480
    }else{
1481
3541
      if( s->d_gen_relevant_terms ){
1482
1250
        s->d_tg_gdepth--;
1483
      }
1484
3541
      d_status++;
1485
3541
      return getNextTerm( s, depth );
1486
    }
1487
37912
  }else if( d_status==4 ){
1488
8758
    d_status++;
1489
8758
    if( depth>0 && (d_status_num+1)<(int)s->getNumTgFuncs( d_typ ) ){
1490
5084
      d_status_num++;
1491
5084
      d_status_child_num = 0;
1492
5084
      Trace("sg-gen-tg-debug2") << this << "...consider function " << s->getTgFunc( d_typ, d_status_num ) << std::endl;
1493
5084
      s->d_tg_gdepth++;
1494
5084
      if( !s->considerCurrentTerm() ){
1495
2386
        s->d_tg_gdepth--;
1496
        //don't consider this function
1497
2386
        d_status--;
1498
      }else{
1499
        //we have decided on a function application
1500
      }
1501
5084
      return getNextTerm( s, depth );
1502
    }else{
1503
      //do not choose function applications at depth 0
1504
3674
      d_status++;
1505
3674
      return getNextTerm( s, depth );
1506
    }
1507
29154
  }else if( d_status==5 ){
1508
    //iterating over arguments
1509
40496
    TNode f = s->getTgFunc( d_typ, d_status_num );
1510
20248
    if( d_status_child_num<0 ){
1511
      //no more arguments
1512
2698
      s->d_tg_gdepth--;
1513
2698
      d_status--;
1514
2698
      return getNextTerm( s, depth );
1515
17550
    }else if( d_status_child_num==(int)s->d_func_args[f].size() ){
1516
5888
      d_status_child_num--;
1517
5888
      return s->considerCurrentTermCanon( d_id ) ? true : getNextTerm( s, depth );
1518
      //return true;
1519
    }else{
1520
11662
      Assert(d_status_child_num < (int)s->d_func_args[f].size());
1521
11662
      if( d_status_child_num==(int)d_children.size() ){
1522
2824
        d_children.push_back( s->d_tg_id );
1523
2824
        Assert(s->d_tg_alloc.find(s->d_tg_id) == s->d_tg_alloc.end());
1524
2824
        s->d_tg_alloc[d_children[d_status_child_num]].reset( s, s->d_func_args[f][d_status_child_num] );
1525
2824
        return getNextTerm( s, depth );
1526
      }else{
1527
8838
        Assert(d_status_child_num + 1 == (int)d_children.size());
1528
8838
        if( s->d_tg_alloc[d_children[d_status_child_num]].getNextTerm( s, depth-1 ) ){
1529
6014
          d_status_child_num++;
1530
6014
          return getNextTerm( s, depth );
1531
        }else{
1532
5648
          Trace("sg-gen-tg-debug2")
1533
2824
              << "...remove child from context " << std::endl;
1534
2824
          s->changeContext(false);
1535
2824
          d_children.pop_back();
1536
2824
          d_status_child_num--;
1537
2824
          return getNextTerm( s, depth );
1538
        }
1539
      }
1540
    }
1541
8906
  }else if( d_status==1 || d_status==3 ){
1542
5232
    if( d_status==1 ){
1543
1691
      s->removeVar( d_typ );
1544
1691
      Assert(d_status_num == (int)s->d_var_id[d_typ]);
1545
      //check if there is only one feasible equivalence class.  if so, don't make pattern any more specific.
1546
      //unsigned i = s->d_ccand_eqc[0].size()-1;
1547
      //if( s->d_ccand_eqc[0][i].size()==1 && s->d_ccand_eqc[1][i].empty() ){
1548
      //  d_status = 6;
1549
      //  return getNextTerm( s, depth );
1550
      //}
1551
1691
      s->d_tg_gdepth++;
1552
    }
1553
5232
    d_status++;
1554
5232
    d_status_num = -1;
1555
5232
    return getNextTerm( s, depth );
1556
  }else{
1557
3674
    Assert(d_children.empty());
1558
3674
    return false;
1559
  }
1560
}
1561
1562
862532
void TermGenerator::resetMatching( TermGenEnv * s, TNode eqc, unsigned mode ) {
1563
862532
  d_match_status = 0;
1564
862532
  d_match_status_child_num = 0;
1565
862532
  d_match_children.clear();
1566
862532
  d_match_children_end.clear();
1567
862532
  d_match_mode = mode;
1568
  //if this term generalizes, it must generalize a non-ground term
1569
  //if( (d_match_mode & ( 1 << 2 ))!=0 && s->isGroundEqc( eqc ) && d_status==5 ){
1570
  //  d_match_status = -1;
1571
  //}
1572
862532
}
1573
1574
3340628
bool TermGenerator::getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode, std::map< unsigned, TNode > >& subs, std::map< TNode, bool >& rev_subs ) {
1575
3340628
  if( d_match_status<0 ){
1576
    return false;
1577
  }
1578
3340628
  if( Trace.isOn("sg-gen-tg-match") ){
1579
    Trace("sg-gen-tg-match") << "Matching ";
1580
    debugPrint( s, "sg-gen-tg-match", "sg-gen-tg-match" );
1581
    Trace("sg-gen-tg-match") << " with eqc e" << s->d_cg->d_em[eqc] << "..." << std::endl;
1582
    Trace("sg-gen-tg-match") << "   mstatus = " << d_match_status;
1583
    if( d_status==5 ){
1584
      TNode f = s->getTgFunc( d_typ, d_status_num );
1585
      Trace("sg-gen-tg-debug2") << ", f = " << f;
1586
      Trace("sg-gen-tg-debug2") << ", #args = " << s->d_func_args[f].size();
1587
      Trace("sg-gen-tg-debug2") << ", mchildNum = " << d_match_status_child_num;
1588
      Trace("sg-gen-tg-debug2") << ", #mchildren = " << d_match_children.size();
1589
    }
1590
    Trace("sg-gen-tg-debug2") << ", current substitution : {";
1591
    for( std::map< TypeNode, std::map< unsigned, TNode > >::iterator itt = subs.begin(); itt != subs.end(); ++itt ){
1592
      for( std::map< unsigned, TNode >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
1593
        Trace("sg-gen-tg-debug2")  << " " << it->first << " -> e" << s->d_cg->d_em[it->second];
1594
      }
1595
    }
1596
    Trace("sg-gen-tg-debug2") << " } " << std::endl;
1597
  }
1598
3340628
  if( d_status==1 ){
1599
    //a variable
1600
559160
    if( d_match_status==0 ){
1601
344293
      d_match_status++;
1602
344293
      if( (d_match_mode & ( 1 << 1 ))!=0 ){
1603
        //only ground terms
1604
338138
        if( !s->isGroundEqc( eqc ) ){
1605
3929
          return false;
1606
        }
1607
6155
      }else if( (d_match_mode & ( 1 << 2 ))!=0 ){
1608
        //only non-ground terms
1609
        //if( s->isGroundEqc( eqc ) ){
1610
        //  return false;
1611
        //}
1612
      }
1613
      //store the match : restricted if match_mode.0 = 1
1614
340364
      if( (d_match_mode & ( 1 << 0 ))!=0 ){
1615
        std::map< TNode, bool >::iterator it = rev_subs.find( eqc );
1616
        if( it==rev_subs.end() ){
1617
          rev_subs[eqc] = true;
1618
        }else{
1619
          return false;
1620
        }
1621
      }
1622
340364
      Assert(subs[d_typ].find(d_status_num) == subs[d_typ].end());
1623
340364
      subs[d_typ][d_status_num] = eqc;
1624
340364
      return true;
1625
    }else{
1626
      //clean up
1627
214867
      subs[d_typ].erase( d_status_num );
1628
214867
      if( (d_match_mode & ( 1 << 0 ))!=0 ){
1629
        rev_subs.erase( eqc );
1630
      }
1631
214867
      return false;
1632
    }
1633
2781468
  }else if( d_status==2 ){
1634
9700
    if( d_match_status==0 ){
1635
9698
      d_match_status++;
1636
9698
      Assert(d_status_num < (int)s->getNumTgVars(d_typ));
1637
9698
      std::map< unsigned, TNode >::iterator it = subs[d_typ].find( d_status_num );
1638
9698
      Assert(it != subs[d_typ].end());
1639
9698
      return it->second==eqc;
1640
    }else{
1641
2
      return false;
1642
    }
1643
2771768
  }else if( d_status==5 ){
1644
    //Assert( d_match_children.size()<=d_children.size() );
1645
    //enumerating over f-applications in eqc
1646
2771768
    if( d_match_status_child_num<0 ){
1647
273769
      return false;
1648
2497999
    }else if( d_match_status==0 ){
1649
      //set up next binding
1650
1503270
      if( d_match_status_child_num==(int)d_match_children.size() ){
1651
1126695
        if( d_match_status_child_num==0 ){
1652
          //initial binding
1653
871708
          TNode f = s->getTgFunc( d_typ, d_status_num );
1654
508541
          Assert(!eqc.isNull());
1655
508541
          TNodeTrie* tat = s->getTermDatabase()->getTermArgTrie(eqc, f);
1656
508541
          if( tat ){
1657
363167
            d_match_children.push_back( tat->d_data.begin() );
1658
363167
            d_match_children_end.push_back( tat->d_data.end() );
1659
          }else{
1660
145374
            d_match_status++;
1661
145374
            d_match_status_child_num--;
1662
145374
            return getNextMatch( s, eqc, subs, rev_subs );
1663
          }
1664
        }else{
1665
618154
          d_match_children.push_back( d_match_children[d_match_status_child_num-1]->second.d_data.begin() );
1666
618154
          d_match_children_end.push_back( d_match_children[d_match_status_child_num-1]->second.d_data.end() );
1667
        }
1668
      }
1669
1357896
      d_match_status++;
1670
1357896
      Assert(d_match_status_child_num + 1 == (int)d_match_children.size());
1671
1357896
      if( d_match_children[d_match_status_child_num]==d_match_children_end[d_match_status_child_num] ){
1672
        //no more arguments to bind
1673
258313
        d_match_children.pop_back();
1674
258313
        d_match_children_end.pop_back();
1675
258313
        d_match_status_child_num--;
1676
258313
        return getNextMatch( s, eqc, subs, rev_subs );
1677
      }else{
1678
1099583
        if( d_match_status_child_num==(int)d_children.size() ){
1679
          //successfully matched all children
1680
477026
          d_match_children.pop_back();
1681
477026
          d_match_children_end.pop_back();
1682
477026
          d_match_status_child_num--;
1683
477026
          return true;//return d_match_children[d_match_status]!=d_match_children_end[d_match_status];
1684
        }else{
1685
          //do next binding
1686
622557
          s->d_tg_alloc[d_children[d_match_status_child_num]].resetMatching( s, d_match_children[d_match_status_child_num]->first, d_match_mode );
1687
622557
          return getNextMatch( s, eqc, subs, rev_subs );
1688
        }
1689
      }
1690
    }else{
1691
994729
      Assert(d_match_status == 1);
1692
994729
      Assert(d_match_status_child_num + 1 == (int)d_match_children.size());
1693
994729
      Assert(d_match_children[d_match_status_child_num]
1694
             != d_match_children_end[d_match_status_child_num]);
1695
994729
      d_match_status--;
1696
994729
      if( s->d_tg_alloc[d_children[d_match_status_child_num]].getNextMatch( s, d_match_children[d_match_status_child_num]->first, subs, rev_subs ) ){
1697
618154
        d_match_status_child_num++;
1698
618154
        return getNextMatch( s, eqc, subs, rev_subs );
1699
      }else{
1700
        //iterate
1701
376575
        d_match_children[d_match_status_child_num]++;
1702
376575
        return getNextMatch( s, eqc, subs, rev_subs );
1703
      }
1704
    }
1705
  }
1706
  Assert(false);
1707
  return false;
1708
}
1709
1710
unsigned TermGenerator::getDepth( TermGenEnv * s ) {
1711
  if( d_status==5 ){
1712
    unsigned maxd = 0;
1713
    for( unsigned i=0; i<d_children.size(); i++ ){
1714
      unsigned d = s->d_tg_alloc[d_children[i]].getDepth( s );
1715
      if( d>maxd ){
1716
        maxd = d;
1717
      }
1718
    }
1719
    return 1+maxd;
1720
  }else{
1721
    return 0;
1722
  }
1723
}
1724
1725
60727
unsigned TermGenerator::calculateGeneralizationDepth( TermGenEnv * s, std::map< TypeNode, std::vector< int > >& fvs ) {
1726
60727
  if( d_status==5 ){
1727
36783
    unsigned sum = 1;
1728
76542
    for( unsigned i=0; i<d_children.size(); i++ ){
1729
39759
      sum += s->d_tg_alloc[d_children[i]].calculateGeneralizationDepth( s, fvs );
1730
    }
1731
36783
    return sum;
1732
  }else{
1733
23944
    Assert(d_status == 2 || d_status == 1);
1734
23944
    std::map< TypeNode, std::vector< int > >::iterator it = fvs.find( d_typ );
1735
23944
    if( it!=fvs.end() ){
1736
3252
      if( std::find( it->second.begin(), it->second.end(), d_status_num )!=it->second.end() ){
1737
979
        return 1;
1738
      }
1739
    }
1740
22965
    fvs[d_typ].push_back( d_status_num );
1741
22965
    return 0;
1742
  }
1743
}
1744
1745
20968
unsigned TermGenerator::getGeneralizationDepth( TermGenEnv * s ) {
1746
  //if( s->d_gen_relevant_terms ){
1747
  //  return s->d_tg_gdepth;
1748
  //}else{
1749
41936
    std::map< TypeNode, std::vector< int > > fvs;
1750
41936
    return calculateGeneralizationDepth( s, fvs );
1751
  //}
1752
}
1753
1754
23006
Node TermGenerator::getTerm( TermGenEnv * s ) {
1755
23006
  if( d_status==1 || d_status==2 ){
1756
11284
    Assert(!d_typ.isNull());
1757
11284
    return s->getFreeVar( d_typ, d_status_num );
1758
11722
  }else if( d_status==5 ){
1759
11722
    Node f = s->getTgFunc( d_typ, d_status_num );
1760
11722
    if( d_children.size()==s->d_func_args[f].size() ){
1761
23444
      std::vector< Node > children;
1762
11722
      if( s->d_tg_func_param[f] ){
1763
11722
        children.push_back( f );
1764
      }
1765
27085
      for( unsigned i=0; i<d_children.size(); i++ ){
1766
30726
        Node nc = s->d_tg_alloc[d_children[i]].getTerm( s );
1767
15363
        if( nc.isNull() ){
1768
          return Node::null();
1769
        }else{
1770
          //Assert( nc.getType()==s->d_func_args[f][i] );
1771
15363
          children.push_back( nc );
1772
        }
1773
      }
1774
11722
      return NodeManager::currentNM()->mkNode( s->d_func_kind[f], children );
1775
    }
1776
  }else{
1777
    Assert(false);
1778
  }
1779
  return Node::null();
1780
}
1781
1782
79079
void TermGenerator::debugPrint( TermGenEnv * s, const char * c, const char * cd ) {
1783
79079
  Trace(cd) << "[*" << d_id << "," << d_status << "]:";
1784
79079
  if( d_status==1 || d_status==2 ){
1785
29627
    Trace(c) << s->getFreeVar( d_typ, d_status_num );
1786
49452
  }else if( d_status==5 ){
1787
98904
    TNode f = s->getTgFunc( d_typ, d_status_num );
1788
49452
    Trace(c) << "(" << f;
1789
102619
    for( unsigned i=0; i<d_children.size(); i++ ){
1790
53167
      Trace(c) << " ";
1791
53167
       s->d_tg_alloc[d_children[i]].debugPrint( s, c, cd );
1792
    }
1793
49452
    if( d_children.size()<s->d_func_args[f].size() ){
1794
10474
      Trace(c) << " ...";
1795
    }
1796
49452
    Trace(c) << ")";
1797
  }else{
1798
    Trace(c) << "???";
1799
  }
1800
79079
}
1801
1802
48
void TermGenEnv::collectSignatureInformation() {
1803
48
  d_typ_tg_funcs.clear();
1804
48
  d_funcs.clear();
1805
48
  d_func_kind.clear();
1806
48
  d_func_args.clear();
1807
96
  TypeNode tnull;
1808
48
  TermDb* tdb = getTermDatabase();
1809
789
  for (size_t i = 0, nops = tdb->getNumOperators(); i < nops; i++)
1810
  {
1811
1482
    Node op = tdb->getOperator(i);
1812
741
    DbList* dbl = tdb->getOrMkDbListForOp(op);
1813
741
    if (!dbl->d_list.empty())
1814
    {
1815
1458
      Node nn = dbl->d_list[0];
1816
729
      Trace("sg-rel-sig-debug") << "Check in signature : " << nn << std::endl;
1817
729
      if( d_cg->isHandledTerm( nn ) && nn.getKind()!=APPLY_SELECTOR_TOTAL && !nn.getType().isBoolean() ){
1818
225
        bool do_enum = true;
1819
        //check if we have enumerated ground terms
1820
225
        if( nn.getKind()==APPLY_UF ){
1821
77
          Trace("sg-rel-sig-debug") << "Check enumeration..." << std::endl;
1822
77
          if( !d_cg->hasEnumeratedUf( nn ) ){
1823
15
            do_enum = false;
1824
          }
1825
        }
1826
225
        if( do_enum ){
1827
210
          Trace("sg-rel-sig-debug") << "Set enumeration..." << std::endl;
1828
210
          d_funcs.push_back(op);
1829
364
          for (const Node& nnc : nn)
1830
          {
1831
154
            d_func_args[op].push_back(nnc.getType());
1832
          }
1833
210
          d_func_kind[op] = nn.getKind();
1834
210
          d_typ_tg_funcs[tnull].push_back(op);
1835
210
          d_typ_tg_funcs[nn.getType()].push_back(op);
1836
210
          d_tg_func_param[op] =
1837
210
              (nn.getMetaKind() == kind::metakind::PARAMETERIZED);
1838
420
          Trace("sg-rel-sig")
1839
210
              << "Will enumerate function applications of : " << op
1840
420
              << ", #args = " << d_func_args[op].size()
1841
210
              << ", kind = " << nn.getKind() << std::endl;
1842
        }
1843
      }
1844
729
      Trace("sg-rel-sig-debug") << "Done check in signature : " << nn << std::endl;
1845
    }
1846
  }
1847
  //shuffle functions
1848
144
  for (std::map<TypeNode, std::vector<TNode> >::iterator it =
1849
48
           d_typ_tg_funcs.begin();
1850
192
       it != d_typ_tg_funcs.end();
1851
       ++it)
1852
  {
1853
144
    std::shuffle(it->second.begin(), it->second.end(), Random::getRandom());
1854
144
    if (it->first.isNull())
1855
    {
1856
38
      Trace("sg-gen-tg-debug") << "In this order : ";
1857
248
      for (unsigned i = 0; i < it->second.size(); i++)
1858
      {
1859
210
        Trace("sg-gen-tg-debug") << it->second[i] << " ";
1860
      }
1861
38
      Trace("sg-gen-tg-debug") << std::endl;
1862
    }
1863
  }
1864
48
}
1865
1866
850
void TermGenEnv::reset( unsigned depth, bool genRelevant, TypeNode tn ) {
1867
850
  Assert(d_tg_alloc.empty());
1868
850
  d_tg_alloc.clear();
1869
1870
850
  if( genRelevant ){
1871
399
    for( unsigned i=0; i<2; i++ ){
1872
266
      d_ccand_eqc[i].clear();
1873
266
      d_ccand_eqc[i].push_back( d_relevant_eqc[i] );
1874
    }
1875
  }
1876
1877
850
  d_tg_id = 0;
1878
850
  d_tg_gdepth = 0;
1879
850
  d_tg_gdepth_limit = depth;
1880
850
  d_gen_relevant_terms = genRelevant;
1881
850
  d_tg_alloc[0].reset( this, tn );
1882
850
}
1883
1884
5267
bool TermGenEnv::getNextTerm() {
1885
5267
  if( d_tg_alloc[0].getNextTerm( this, d_tg_gdepth_limit ) ){
1886
4417
    Assert((int)d_tg_alloc[0].getGeneralizationDepth(this)
1887
           <= d_tg_gdepth_limit);
1888
4417
    if( (int)d_tg_alloc[0].getGeneralizationDepth( this )!=d_tg_gdepth_limit ){
1889
1560
      return getNextTerm();
1890
    }else{
1891
2857
      return true;
1892
    }
1893
  }
1894
850
  Trace("sg-gen-tg-debug2") << "...remove from context " << std::endl;
1895
850
  changeContext(false);
1896
850
  return false;
1897
}
1898
1899
//reset matching
1900
22289
void TermGenEnv::resetMatching( TNode eqc, unsigned mode ) {
1901
22289
  d_tg_alloc[0].resetMatching( this, eqc, mode );
1902
22289
}
1903
1904
//get next match
1905
107240
bool TermGenEnv::getNextMatch( TNode eqc, std::map< TypeNode, std::map< unsigned, TNode > >& subs, std::map< TNode, bool >& rev_subs ) {
1906
107240
  return d_tg_alloc[0].getNextMatch( this, eqc, subs, rev_subs );
1907
}
1908
1909
//get term
1910
2857
Node TermGenEnv::getTerm() {
1911
2857
  return d_tg_alloc[0].getTerm( this );
1912
}
1913
1914
670
void TermGenEnv::debugPrint( const char * c, const char * cd ) {
1915
670
  d_tg_alloc[0].debugPrint( this, c, cd );
1916
670
}
1917
1918
16692
unsigned TermGenEnv::getNumTgVars( TypeNode tn ) {
1919
16692
  return d_var_id[tn];
1920
}
1921
1922
3541
bool TermGenEnv::allowVar( TypeNode tn ) {
1923
3541
  std::map< TypeNode, unsigned >::iterator it = d_var_limit.find( tn );
1924
3541
  if( it==d_var_limit.end() ){
1925
1691
    return true;
1926
  }else{
1927
1850
    return d_var_id[tn]<it->second;
1928
  }
1929
}
1930
1931
1691
void TermGenEnv::addVar( TypeNode tn ) {
1932
1691
  d_var_id[tn]++;
1933
1691
}
1934
1935
1691
void TermGenEnv::removeVar( TypeNode tn ) {
1936
1691
  d_var_id[tn]--;
1937
  //d_var_eq_tg.pop_back();
1938
  //d_var_tg.pop_back();
1939
1691
}
1940
1941
6759
unsigned TermGenEnv::getNumTgFuncs( TypeNode tn ) {
1942
6759
  return d_typ_tg_funcs[tn].size();
1943
}
1944
1945
595047
TNode TermGenEnv::getTgFunc( TypeNode tn, unsigned i ) {
1946
595047
  return d_typ_tg_funcs[tn][i];
1947
}
1948
1949
40911
Node TermGenEnv::getFreeVar( TypeNode tn, unsigned i ) {
1950
40911
  return d_cg->getFreeVar( tn, i );
1951
}
1952
1953
10228
bool TermGenEnv::considerCurrentTerm() {
1954
10228
  Assert(!d_tg_alloc.empty());
1955
1956
  //if generalization depth is too large, don't consider it
1957
10228
  unsigned i = d_tg_alloc.size();
1958
10228
  Trace("sg-gen-tg-debug") << "Consider term ";
1959
10228
  d_tg_alloc[0].debugPrint( this, "sg-gen-tg-debug", "sg-gen-tg-debug" );
1960
10228
  Trace("sg-gen-tg-debug") << "?  curr term size = " << d_tg_alloc.size() << ", last status = " << d_tg_alloc[i-1].d_status;
1961
10228
  Trace("sg-gen-tg-debug") << std::endl;
1962
1963
10228
  if( d_tg_gdepth_limit>=0 && d_tg_alloc[0].getGeneralizationDepth( this )>(unsigned)d_tg_gdepth_limit ){
1964
1906
    Trace("sg-gen-consider-term") << "-> generalization depth of ";
1965
1906
    d_tg_alloc[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-tg-debug" );
1966
1906
    Trace("sg-gen-consider-term") << " is too high " << d_tg_gdepth << " " << d_tg_alloc[0].getGeneralizationDepth( this ) << ", do not consider." << std::endl;
1967
1906
    return false;
1968
  }
1969
1970
  //----optimizations
1971
  /*
1972
  if( d_tg_alloc[i-1].d_status==1 ){
1973
  }else if( d_tg_alloc[i-1].d_status==2 ){
1974
  }else if( d_tg_alloc[i-1].d_status==5 ){
1975
  }else{
1976
    Trace("sg-gen-tg-debug") << "Bad tg: " << &d_tg_alloc[i-1] << std::endl;
1977
    Assert( false );
1978
  }
1979
  */
1980
  //if equated two variables, first check if context-independent TODO
1981
  //----end optimizations
1982
1983
1984
  //check based on which candidate equivalence classes match
1985
8322
  if( d_gen_relevant_terms ){
1986
3245
    Trace("sg-gen-tg-debug") << "Filter based on relevant ground EQC";
1987
3245
    Trace("sg-gen-tg-debug") << ", #eqc to try = " << d_ccand_eqc[0][i-1].size() << "/" << d_ccand_eqc[1][i-1].size() << std::endl;
1988
1989
3245
    Assert(d_ccand_eqc[0].size() >= 2);
1990
3245
    Assert(d_ccand_eqc[0].size() == d_ccand_eqc[1].size());
1991
3245
    Assert(d_ccand_eqc[0].size() == d_tg_id + 1);
1992
3245
    Assert(d_tg_id == d_tg_alloc.size());
1993
9735
    for( unsigned r=0; r<2; r++ ){
1994
6490
      d_ccand_eqc[r][i].clear();
1995
    }
1996
1997
    //re-check feasibility of EQC
1998
9735
    for( unsigned r=0; r<2; r++ ){
1999
224176
      for( unsigned j=0; j<d_ccand_eqc[r][i-1].size(); j++ ){
2000
435372
        std::map< TypeNode, std::map< unsigned, TNode > > subs;
2001
435372
        std::map< TNode, bool > rev_subs;
2002
        unsigned mode;
2003
217686
        if( r==0 ){
2004
18985
          mode = d_cg->optReqDistinctVarPatterns() ? ( 1 << 0 ) : 0;
2005
18985
          mode = mode | (1 << 2 );
2006
        }else{
2007
198701
          mode =  1 << 1;
2008
        }
2009
217686
        d_tg_alloc[0].resetMatching( this, d_ccand_eqc[r][i-1][j], mode );
2010
217686
        if( d_tg_alloc[0].getNextMatch( this, d_ccand_eqc[r][i-1][j], subs, rev_subs ) ){
2011
114775
          d_ccand_eqc[r][i].push_back( d_ccand_eqc[r][i-1][j] );
2012
        }
2013
      }
2014
    }
2015
9735
    for( unsigned r=0; r<2; r++ ){
2016
6490
      Trace("sg-gen-tg-debug") << "Current eqc of type " << r << " : ";
2017
121265
      for( unsigned j=0; j<d_ccand_eqc[r][i].size(); j++ ){
2018
114775
        Trace("sg-gen-tg-debug") << "e" << d_cg->d_em[d_ccand_eqc[r][i][j]] << " ";
2019
      }
2020
6490
      Trace("sg-gen-tg-debug") << std::endl;
2021
    }
2022
3245
    if( options::conjectureFilterActiveTerms() && d_ccand_eqc[0][i].empty() ){
2023
859
      Trace("sg-gen-consider-term") << "Do not consider term of form ";
2024
859
      d_tg_alloc[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-consider-term-debug" );
2025
859
      Trace("sg-gen-consider-term") << " since no relevant EQC matches it." << std::endl;
2026
859
      return false;
2027
    }
2028
2386
    if( options::conjectureFilterModel() && d_ccand_eqc[1][i].empty() ){
2029
54
      Trace("sg-gen-consider-term") << "Do not consider term of form ";
2030
54
      d_tg_alloc[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-consider-term-debug" );
2031
54
      Trace("sg-gen-consider-term") << " since no ground EQC matches it." << std::endl;
2032
54
      return false;
2033
    }
2034
  }
2035
7409
  Trace("sg-gen-tg-debug") << "Will consider term ";
2036
7409
  d_tg_alloc[0].debugPrint( this, "sg-gen-tg-debug", "sg-gen-tg-debug" );
2037
7409
  Trace("sg-gen-tg-debug") << std::endl;
2038
7409
  Trace("sg-gen-consider-term-debug") << std::endl;
2039
7409
  return true;
2040
}
2041
2042
7348
void TermGenEnv::changeContext( bool add ) {
2043
7348
  if( add ){
2044
11022
    for( unsigned r=0; r<2; r++ ){
2045
7348
      d_ccand_eqc[r].push_back( std::vector< TNode >() );
2046
    }
2047
3674
    d_tg_id++;
2048
  }else{
2049
11022
    for( unsigned r=0; r<2; r++ ){
2050
7348
      d_ccand_eqc[r].pop_back();
2051
    }
2052
3674
    d_tg_id--;
2053
3674
    Assert(d_tg_alloc.find(d_tg_id) != d_tg_alloc.end());
2054
3674
    d_tg_alloc.erase( d_tg_id );
2055
  }
2056
7348
}
2057
2058
5888
bool TermGenEnv::considerCurrentTermCanon( unsigned tg_id ){
2059
5888
  Assert(tg_id < d_tg_alloc.size());
2060
5888
  if( options::conjectureFilterCanonical() ){
2061
    //check based on a canonicity of the term (if there is one)
2062
4786
    Trace("sg-gen-tg-debug") << "Consider term canon ";
2063
4786
    d_tg_alloc[0].debugPrint( this, "sg-gen-tg-debug", "sg-gen-tg-debug" );
2064
4786
    Trace("sg-gen-tg-debug") << ", tg is [" << tg_id << "]..." << std::endl;
2065
2066
9572
    Node ln = d_tg_alloc[tg_id].getTerm( this );
2067
4786
    Trace("sg-gen-tg-debug") << "Term is " << ln << std::endl;
2068
4786
    return d_cg->considerTermCanon( ln, d_gen_relevant_terms );
2069
  }
2070
1102
  return true;
2071
}
2072
2073
3482
bool TermGenEnv::isRelevantFunc( Node f ) {
2074
3482
  return std::find( d_funcs.begin(), d_funcs.end(), f )!=d_funcs.end();
2075
}
2076
2077
978
bool TermGenEnv::isRelevantTerm( Node t ) {
2078
978
  if( t.getKind()!=BOUND_VARIABLE ){
2079
670
    if( t.getKind()!=EQUAL ){
2080
493
      if( t.hasOperator() ){
2081
901
        TNode op = t.getOperator();
2082
485
        if( !isRelevantFunc( op ) ){
2083
69
          return false;
2084
        }
2085
      }else{
2086
8
        return false;
2087
      }
2088
    }
2089
1309
    for( unsigned i=0; i<t.getNumChildren(); i++ ){
2090
809
      if( !isRelevantTerm( t[i] ) ){
2091
93
        return false;
2092
      }
2093
    }
2094
  }
2095
808
  return true;
2096
}
2097
2098
508589
TermDb * TermGenEnv::getTermDatabase() {
2099
508589
  return d_cg->getTermDatabase();
2100
}
2101
Node TermGenEnv::getGroundEqc( TNode r ) {
2102
  return d_cg->getGroundEqc( r );
2103
}
2104
338138
bool TermGenEnv::isGroundEqc( TNode r ){
2105
338138
  return d_cg->isGroundEqc( r );
2106
}
2107
bool TermGenEnv::isGroundTerm( TNode n ){
2108
  return d_cg->isGroundTerm( n );
2109
}
2110
2111
2112
272999
void SubstitutionIndex::addSubstitution( TNode eqc, std::vector< TNode >& vars, std::vector< TNode >& terms, unsigned i ) {
2113
272999
  if( i==vars.size() ){
2114
84951
    d_var = eqc;
2115
  }else{
2116
188048
    Assert(d_var.isNull() || d_var == vars[i]);
2117
188048
    d_var = vars[i];
2118
188048
    d_children[terms[i]].addSubstitution( eqc, vars, terms, i+1 );
2119
  }
2120
272999
}
2121
2122
1188998
bool SubstitutionIndex::notifySubstitutions( ConjectureGenerator * s, std::map< TNode, TNode >& subs, TNode rhs, unsigned numVars, unsigned i ) {
2123
1188998
  if( i==numVars ){
2124
882686
    Assert(d_children.empty());
2125
882686
    return s->notifySubstitution( d_var, subs, rhs );
2126
  }else{
2127
306312
    Assert(i == 0 || !d_children.empty());
2128
1470589
    for( std::map< TNode, SubstitutionIndex >::iterator it = d_children.begin(); it != d_children.end(); ++it ){
2129
1176717
      Trace("sg-cconj-debug2") << "Try " << d_var << " -> " << it->first << " (" << i << "/" << numVars << ")" << std::endl;
2130
1176717
      subs[d_var] = it->first;
2131
1176717
      if( !it->second.notifySubstitutions( s, subs, rhs, numVars, i+1 ) ){
2132
12440
        return false;
2133
      }
2134
    }
2135
293872
    return true;
2136
  }
2137
}
2138
2139
2140
506
void TheoremIndex::addTheorem( std::vector< TNode >& lhs_v, std::vector< unsigned >& lhs_arg, TNode rhs ){
2141
506
  if( lhs_v.empty() ){
2142
92
    if( std::find( d_terms.begin(), d_terms.end(), rhs )==d_terms.end() ){
2143
92
      d_terms.push_back( rhs );
2144
    }
2145
  }else{
2146
414
    unsigned index = lhs_v.size()-1;
2147
414
    if( lhs_arg[index]==lhs_v[index].getNumChildren() ){
2148
184
      lhs_v.pop_back();
2149
184
      lhs_arg.pop_back();
2150
184
      addTheorem( lhs_v, lhs_arg, rhs );
2151
    }else{
2152
230
      lhs_arg[index]++;
2153
230
      addTheoremNode( lhs_v[index][lhs_arg[index]-1], lhs_v, lhs_arg, rhs );
2154
    }
2155
  }
2156
506
}
2157
2158
322
void TheoremIndex::addTheoremNode( TNode curr, std::vector< TNode >& lhs_v, std::vector< unsigned >& lhs_arg, TNode rhs ){
2159
322
  Trace("thm-db-debug") << "Adding conjecture for subterm " << curr << "..." << std::endl;
2160
322
  if( curr.hasOperator() ){
2161
184
    lhs_v.push_back( curr );
2162
184
    lhs_arg.push_back( 0 );
2163
184
    d_children[curr.getOperator()].addTheorem( lhs_v, lhs_arg, rhs );
2164
  }else{
2165
138
    Assert(curr.getKind() == kind::BOUND_VARIABLE);
2166
276
    TypeNode tn = curr.getType();
2167
138
    Assert(d_var[tn].isNull() || d_var[tn] == curr);
2168
138
    d_var[tn] = curr;
2169
138
    d_children[curr].addTheorem( lhs_v, lhs_arg, rhs );
2170
  }
2171
322
}
2172
2173
2272
void TheoremIndex::getEquivalentTerms( std::vector< TNode >& n_v, std::vector< unsigned >& n_arg,
2174
                                       std::map< TNode, TNode >& smap, std::vector< TNode >& vars, std::vector< TNode >& subs,
2175
                                       std::vector< Node >& terms ) {
2176
2272
  Trace("thm-db-debug") << "Get equivalent terms " << n_v.size() << " " << n_arg.size() << std::endl;
2177
2272
  if( n_v.empty() ){
2178
164
    Trace("thm-db-debug") << "Number of terms : " << d_terms.size() << std::endl;
2179
    //apply substutitions to RHS's
2180
328
    for( unsigned i=0; i<d_terms.size(); i++ ){
2181
328
      Node n = d_terms[i].substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
2182
164
      terms.push_back( n );
2183
    }
2184
  }else{
2185
2108
    unsigned index = n_v.size()-1;
2186
2108
    if( n_arg[index]==n_v[index].getNumChildren() ){
2187
328
      n_v.pop_back();
2188
328
      n_arg.pop_back();
2189
328
      getEquivalentTerms( n_v, n_arg, smap, vars, subs, terms );
2190
    }else{
2191
1780
      n_arg[index]++;
2192
1780
      getEquivalentTermsNode( n_v[index][n_arg[index]-1], n_v, n_arg, smap, vars, subs, terms );
2193
    }
2194
  }
2195
2272
}
2196
2197
3398
void TheoremIndex::getEquivalentTermsNode( Node curr, std::vector< TNode >& n_v, std::vector< unsigned >& n_arg,
2198
                                           std::map< TNode, TNode >& smap, std::vector< TNode >& vars, std::vector< TNode >& subs,
2199
                                           std::vector< Node >& terms ) {
2200
3398
  Trace("thm-db-debug") << "Get equivalent based on subterm " << curr << "..." << std::endl;
2201
3398
  if( curr.hasOperator() ){
2202
2379
    Trace("thm-db-debug") << "Check based on operator..." << std::endl;
2203
2379
    std::map< TNode, TheoremIndex >::iterator it = d_children.find( curr.getOperator() );
2204
2379
    if( it!=d_children.end() ){
2205
1141
      n_v.push_back( curr );
2206
1141
      n_arg.push_back( 0 );
2207
1141
      it->second.getEquivalentTerms( n_v, n_arg, smap, vars, subs, terms );
2208
    }
2209
2379
    Trace("thm-db-debug") << "...done check based on operator" << std::endl;
2210
  }
2211
6796
  TypeNode tn = curr.getType();
2212
3398
  std::map< TypeNode, TNode >::iterator itt = d_var.find( tn );
2213
3398
  if( itt!=d_var.end() ){
2214
803
    Trace("thm-db-debug") << "Check for substitution with " << itt->second << "..." << std::endl;
2215
803
    Assert(curr.getType() == itt->second.getType());
2216
    //add to substitution if possible
2217
803
    bool success = false;
2218
803
    std::map< TNode, TNode >::iterator it = smap.find( itt->second );
2219
803
    if( it==smap.end() ){
2220
803
      smap[itt->second] = curr;
2221
803
      vars.push_back( itt->second );
2222
803
      subs.push_back( curr );
2223
803
      success = true;
2224
    }else if( it->second==curr ){
2225
      success = true;
2226
    }else{
2227
      //also check modulo equality (in universal equality engine)
2228
    }
2229
803
    Trace("thm-db-debug") << "...check for substitution with " << itt->second << ", success = " << success << "." << std::endl;
2230
803
    if( success ){
2231
803
      d_children[itt->second].getEquivalentTerms( n_v, n_arg, smap, vars, subs, terms );
2232
    }
2233
  }
2234
3398
}
2235
2236
342
void TheoremIndex::debugPrint( const char * c, unsigned ind ) {
2237
636
  for( std::map< TNode, TheoremIndex >::iterator it = d_children.begin(); it != d_children.end(); ++it ){
2238
294
    for( unsigned i=0; i<ind; i++ ){ Trace(c) << "  "; }
2239
294
    Trace(c) << it->first << std::endl;
2240
294
    it->second.debugPrint( c, ind+1 );
2241
  }
2242
342
  if( !d_terms.empty() ){
2243
92
    for( unsigned i=0; i<ind; i++ ){ Trace(c) << "  "; }
2244
92
    Trace(c) << "{";
2245
184
    for( unsigned i=0; i<d_terms.size(); i++ ){
2246
92
      Trace(c) << " " << d_terms[i];
2247
    }
2248
92
    Trace(c) << " }" << std::endl;
2249
  }
2250
  //if( !d_var.isNull() ){
2251
  //  for( unsigned i=0; i<ind; i++ ){ Trace(c) << "  "; }
2252
  //  Trace(c) << "var:" << d_var << std::endl;
2253
  //}
2254
342
}
2255
2256
18985
bool ConjectureGenerator::optReqDistinctVarPatterns() { return false; }
2257
3477
bool ConjectureGenerator::optFilterUnknown() { return true; }  //may change
2258
35
int ConjectureGenerator::optFilterScoreThreshold() { return 1; }
2259
48
unsigned ConjectureGenerator::optFullCheckFrequency() { return 1; }
2260
2261
44
bool ConjectureGenerator::optStatsOnly() { return false; }
2262
2263
26913
}