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