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