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