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