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