1 /********************* */
2 /*! \file conjecture_generator.cpp
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
12 ** \brief conjecture generator class
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"
24 using namespace CVC4::kind
;
25 using namespace CVC4::theory
;
26 using namespace CVC4::theory::quantifiers
;
32 void OpArgIndex::addTerm( ConjectureGenerator
* s
, TNode n
, unsigned index
){
33 if( index
==n
.getNumChildren() ){
34 Assert( n
.hasOperator() );
35 if( std::find( d_ops
.begin(), d_ops
.end(), n
.getOperator() )==d_ops
.end() ){
36 d_ops
.push_back( n
.getOperator() );
37 d_op_terms
.push_back( n
);
40 d_child
[s
->getTermDatabase()->d_arg_reps
[n
][index
]].addTerm( s
, n
, index
+1 );
44 Node
OpArgIndex::getGroundTerm( ConjectureGenerator
* s
, std::vector
< TNode
>& args
) {
46 for( std::map
< TNode
, OpArgIndex
>::iterator it
= d_child
.begin(); it
!= d_child
.end(); ++it
){
47 std::map
< TNode
, Node
>::iterator itf
= s
->d_ground_eqc_map
.find( it
->first
);
48 if( itf
!=s
->d_ground_eqc_map
.end() ){
49 args
.push_back( itf
->second
);
50 Node n
= it
->second
.getGroundTerm( s
, args
);
59 std::vector
< TNode
> args2
;
60 args2
.push_back( d_ops
[0] );
61 args2
.insert( args2
.end(), args
.begin(), args
.end() );
62 return NodeManager::currentNM()->mkNode( d_op_terms
[0].getKind(), args2
);
66 void OpArgIndex::getGroundTerms( ConjectureGenerator
* s
, std::vector
< TNode
>& terms
) {
67 terms
.insert( terms
.end(), d_op_terms
.begin(), d_op_terms
.end() );
68 for( std::map
< TNode
, OpArgIndex
>::iterator it
= d_child
.begin(); it
!= d_child
.end(); ++it
){
69 if( s
->isGroundEqc( it
->first
) ){
70 it
->second
.getGroundTerms( s
, terms
);
77 ConjectureGenerator::ConjectureGenerator( QuantifiersEngine
* qe
, context::Context
* c
) : QuantifiersModule( qe
),
79 d_uequalityEngine(d_notify
, c
, "ConjectureGenerator::ee"),
80 d_ee_conjectures( c
){
81 d_fullEffortCount
= 0;
82 d_uequalityEngine
.addFunctionKind( kind::APPLY_UF
);
83 d_uequalityEngine
.addFunctionKind( kind::APPLY_CONSTRUCTOR
);
87 void ConjectureGenerator::eqNotifyNewClass( TNode t
){
88 Trace("thm-ee-debug") << "UEE : new equivalence class " << t
<< std::endl
;
89 d_upendingAdds
.push_back( t
);
92 void ConjectureGenerator::eqNotifyPreMerge(TNode t1
, TNode t2
) {
93 //get maintained representatives
96 std::map
< Node
, EqcInfo
* >::iterator it1
= d_eqc_info
.find( t1
);
97 if( it1
!=d_eqc_info
.end() && !it1
->second
->d_rep
.get().isNull() ){
98 rt1
= it1
->second
->d_rep
.get();
100 std::map
< Node
, EqcInfo
* >::iterator it2
= d_eqc_info
.find( t2
);
101 if( it2
!=d_eqc_info
.end() && !it2
->second
->d_rep
.get().isNull() ){
102 rt2
= it2
->second
->d_rep
.get();
104 Trace("thm-ee-debug") << "UEE : equality holds : " << t1
<< " == " << t2
<< std::endl
;
105 Trace("thm-ee-debug") << " ureps : " << rt1
<< " == " << rt2
<< std::endl
;
106 Trace("thm-ee-debug") << " normal : " << d_pattern_is_normal
[rt1
] << " " << d_pattern_is_normal
[rt2
] << std::endl
;
107 Trace("thm-ee-debug") << " size : " << d_pattern_fun_sum
[rt1
] << " " << d_pattern_fun_sum
[rt2
] << std::endl
;
109 if( isUniversalLessThan( rt2
, rt1
) ){
111 if( it1
==d_eqc_info
.end() ){
112 ei
= getOrMakeEqcInfo( t1
, true );
120 void ConjectureGenerator::eqNotifyPostMerge(TNode t1
, TNode t2
) {
124 void ConjectureGenerator::eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
) {
125 Trace("thm-ee-debug") << "UEE : disequality holds : " << t1
<< " != " << t2
<< std::endl
;
130 ConjectureGenerator::EqcInfo::EqcInfo( context::Context
* c
) : d_rep( c
, Node::null() ){
134 ConjectureGenerator::EqcInfo
* ConjectureGenerator::getOrMakeEqcInfo( TNode n
, bool doMake
) {
135 //Assert( getUniversalRepresentative( n )==n );
136 std::map
< Node
, EqcInfo
* >::iterator eqc_i
= d_eqc_info
.find( n
);
137 if( eqc_i
!=d_eqc_info
.end() ){
138 return eqc_i
->second
;
140 EqcInfo
* ei
= new EqcInfo( d_quantEngine
->getSatContext() );
148 void ConjectureGenerator::doPendingAddUniversalTerms() {
149 //merge all pending equalities
150 while( !d_upendingAdds
.empty() ){
151 Trace("sg-pending") << "Add " << d_upendingAdds
.size() << " pending terms..." << std::endl
;
152 std::vector
< Node
> pending
;
153 pending
.insert( pending
.end(), d_upendingAdds
.begin(), d_upendingAdds
.end() );
154 d_upendingAdds
.clear();
155 for( unsigned i
=0; i
<pending
.size(); i
++ ){
157 TypeNode tn
= t
.getType();
158 Trace("thm-ee-add") << "UEE : Add universal term " << t
<< std::endl
;
159 //get all equivalent terms based on theorem database
160 std::vector
< Node
> eq_terms
;
161 d_thm_index
.getEquivalentTerms( t
, eq_terms
);
162 if( !eq_terms
.empty() ){
163 Trace("thm-ee-add") << "UEE : Based on theorem database, it is equivalent to " << eq_terms
.size() << " terms : " << std::endl
;
164 //add equivalent terms as equalities to universal engine
165 for( unsigned i
=0; i
<eq_terms
.size(); i
++ ){
166 Trace("thm-ee-add") << " " << eq_terms
[i
] << std::endl
;
167 //if( d_urelevant_terms.find( eq_terms[i] )!=d_urelevant_terms.end() ){
168 bool assertEq
= false;
169 if( d_urelevant_terms
.find( eq_terms
[i
] )!=d_urelevant_terms
.end() ){
172 Assert( eq_terms
[i
].getType()==tn
);
173 registerPattern( eq_terms
[i
], tn
);
174 if( isUniversalLessThan( eq_terms
[i
], t
) ){
175 setUniversalRelevant( eq_terms
[i
] );
181 d_uequalityEngine
.assertEquality( t
.eqNode( eq_terms
[i
] ), true, exp
);
185 Trace("thm-ee-add") << "UEE : No equivalent terms." << std::endl
;
187 //if occurs at ground level, merge with representative of ground equality engine
189 eq::EqualityEngine * ee = getEqualityEngine();
190 if( ee->hasTerm( t ) ){
191 TNode grt = ee->getRepresentative( t );
194 d_uequalityEngine.assertEquality( t.eqNode( grt ), true, exp );
202 void ConjectureGenerator::setUniversalRelevant( TNode n
) {
203 //add pattern information
204 registerPattern( n
, n
.getType() );
205 d_urelevant_terms
[n
] = true;
206 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
207 setUniversalRelevant( n
[i
] );
211 bool ConjectureGenerator::isUniversalLessThan( TNode rt1
, TNode rt2
) {
212 //prefer the one that is (normal, smaller) lexographically
213 Assert( d_pattern_is_normal
.find( rt1
)!=d_pattern_is_normal
.end() );
214 Assert( d_pattern_is_normal
.find( rt2
)!=d_pattern_is_normal
.end() );
215 Assert( d_pattern_fun_sum
.find( rt1
)!=d_pattern_fun_sum
.end() );
216 Assert( d_pattern_fun_sum
.find( rt2
)!=d_pattern_fun_sum
.end() );
218 if( d_pattern_is_normal
[rt1
] && !d_pattern_is_normal
[rt2
] ){
219 Trace("thm-ee-debug") << "UEE : LT due to normal." << std::endl
;
221 }else if( d_pattern_is_normal
[rt1
]==d_pattern_is_normal
[rt2
] ){
222 if( d_pattern_fun_sum
[rt1
]<d_pattern_fun_sum
[rt2
] ){
223 Trace("thm-ee-debug") << "UEE : LT due to size." << std::endl
;
224 //decide which representative to use : based on size of the term
226 }else if( d_pattern_fun_sum
[rt1
]==d_pattern_fun_sum
[rt2
] ){
227 //same size : tie goes to term that has already been reported
228 return isReportedCanon( rt1
) && !isReportedCanon( rt2
);
235 bool ConjectureGenerator::isReportedCanon( TNode n
) {
236 return std::find( d_ue_canon
.begin(), d_ue_canon
.end(), n
)==d_ue_canon
.end();
239 void ConjectureGenerator::markReportedCanon( TNode n
) {
240 if( !isReportedCanon( n
) ){
241 d_ue_canon
.push_back( n
);
245 bool ConjectureGenerator::areUniversalEqual( TNode n1
, TNode n2
) {
246 return n1
==n2
|| ( d_uequalityEngine
.hasTerm( n1
) && d_uequalityEngine
.hasTerm( n2
) && d_uequalityEngine
.areEqual( n1
, n2
) );
249 bool ConjectureGenerator::areUniversalDisequal( TNode n1
, TNode n2
) {
250 return n1
!=n2
&& d_uequalityEngine
.hasTerm( n1
) && d_uequalityEngine
.hasTerm( n2
) && d_uequalityEngine
.areDisequal( n1
, n2
, false );
253 TNode
ConjectureGenerator::getUniversalRepresentative( TNode n
, bool add
) {
255 if( d_urelevant_terms
.find( n
)==d_urelevant_terms
.end() ){
256 setUniversalRelevant( n
);
257 //add term to universal equality engine
258 d_uequalityEngine
.addTerm( n
);
259 Trace("thm-ee-debug") << "Merge equivalence classes based on terms..." << std::endl
;
260 doPendingAddUniversalTerms();
263 if( d_uequalityEngine
.hasTerm( n
) ){
264 Node r
= d_uequalityEngine
.getRepresentative( n
);
265 EqcInfo
* ei
= getOrMakeEqcInfo( r
);
266 if( ei
&& !ei
->d_rep
.get().isNull() ){
267 return ei
->d_rep
.get();
276 eq::EqualityEngine
* ConjectureGenerator::getEqualityEngine() {
277 return d_quantEngine
->getTheoryEngine()->getMasterEqualityEngine();
280 bool ConjectureGenerator::areEqual( TNode n1
, TNode n2
) {
281 eq::EqualityEngine
* ee
= getEqualityEngine();
282 return n1
==n2
|| ( ee
->hasTerm( n1
) && ee
->hasTerm( n2
) && ee
->areEqual( n1
, n2
) );
285 bool ConjectureGenerator::areDisequal( TNode n1
, TNode n2
) {
286 eq::EqualityEngine
* ee
= getEqualityEngine();
287 return n1
!=n2
&& ee
->hasTerm( n1
) && ee
->hasTerm( n2
) && ee
->areDisequal( n1
, n2
, false );
290 TNode
ConjectureGenerator::getRepresentative( TNode n
) {
291 eq::EqualityEngine
* ee
= getEqualityEngine();
292 if( ee
->hasTerm( n
) ){
293 return ee
->getRepresentative( n
);
299 TermDb
* ConjectureGenerator::getTermDatabase() {
300 return d_quantEngine
->getTermDatabase();
303 Node
ConjectureGenerator::getFreeVar( TypeNode tn
, unsigned i
) {
304 Assert( !tn
.isNull() );
305 while( d_free_var
[tn
].size()<=i
){
306 std::stringstream oss
;
308 std::stringstream os
;
309 os
<< oss
.str()[0] << i
;
310 Node x
= NodeManager::currentNM()->mkBoundVar( os
.str().c_str(), tn
);
311 d_free_var_num
[x
] = d_free_var
[tn
].size();
312 d_free_var
[tn
].push_back( x
);
314 return d_free_var
[tn
][i
];
319 Node
ConjectureGenerator::getCanonicalTerm( TNode n
, std::map
< TypeNode
, unsigned >& var_count
, std::map
< TNode
, TNode
>& subs
) {
320 Trace("ajr-temp") << "get canonical term " << n
<< " " << n
.getKind() << " " << n
.hasOperator() << std::endl
;
321 if( n
.getKind()==BOUND_VARIABLE
){
322 std::map
< TNode
, TNode
>::iterator it
= subs
.find( n
);
323 if( it
==subs
.end() ){
324 TypeNode tn
= n
.getType();
326 unsigned vn
= var_count
[tn
];
328 subs
[n
] = getFreeVar( tn
, vn
);
334 std::vector
< Node
> children
;
335 if( n
.getKind()!=EQUAL
){
336 if( n
.hasOperator() ){
337 TNode op
= n
.getOperator();
338 if( std::find( d_funcs
.begin(), d_funcs
.end(), op
)==d_funcs
.end() ){
341 children
.push_back( op
);
346 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
347 Node cn
= getCanonicalTerm( n
[i
], var_count
, subs
);
351 children
.push_back( cn
);
354 return NodeManager::currentNM()->mkNode( n
.getKind(), children
);
358 bool ConjectureGenerator::isHandledTerm( TNode n
){
359 return !n
.getAttribute(NoMatchAttribute()) && inst::Trigger::isAtomicTrigger( n
) && ( n
.getKind()!=APPLY_UF
|| n
.getOperator().getKind()!=SKOLEM
);
362 Node
ConjectureGenerator::getGroundEqc( TNode r
) {
363 std::map
< TNode
, Node
>::iterator it
= d_ground_eqc_map
.find( r
);
364 return it
!=d_ground_eqc_map
.end() ? it
->second
: Node::null();
367 bool ConjectureGenerator::isGroundEqc( TNode r
) {
368 return d_ground_eqc_map
.find( r
)!=d_ground_eqc_map
.end();
371 bool ConjectureGenerator::isGroundTerm( TNode n
) {
372 return std::find( d_ground_terms
.begin(), d_ground_terms
.end(), n
)!=d_ground_terms
.end();
375 bool ConjectureGenerator::needsCheck( Theory::Effort e
) {
376 return e
==Theory::EFFORT_FULL
;
379 void ConjectureGenerator::reset_round( Theory::Effort e
) {
383 void ConjectureGenerator::check( Theory::Effort e
, unsigned quant_e
) {
384 if( quant_e
==QuantifiersEngine::QEFFORT_STANDARD
){
386 if( d_fullEffortCount
%optFullCheckFrequency()==0 ){
387 Trace("sg-engine") << "---Conjecture generator, effort = " << e
<< "--- " << std::endl
;
388 eq::EqualityEngine
* ee
= getEqualityEngine();
390 Trace("sg-proc") << "Get eq classes..." << std::endl
;
391 d_op_arg_index
.clear();
392 d_ground_eqc_map
.clear();
393 d_bool_eqc
[0] = Node::null();
394 d_bool_eqc
[1] = Node::null();
395 std::vector
< TNode
> eqcs
;
397 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( ee
);
398 while( !eqcs_i
.isFinished() ){
401 if( r
.getType().isBoolean() ){
402 if( areEqual( r
, getTermDatabase()->d_true
) ){
403 d_ground_eqc_map
[r
] = getTermDatabase()->d_true
;
405 }else if( areEqual( r
, getTermDatabase()->d_false
) ){
406 d_ground_eqc_map
[r
] = getTermDatabase()->d_false
;
410 d_em
[r
] = eqcs
.size();
411 eq::EqClassIterator ieqc_i
= eq::EqClassIterator( r
, ee
);
412 while( !ieqc_i
.isFinished() ){
414 if( isHandledTerm( n
) ){
415 d_op_arg_index
[r
].addTerm( this, n
);
421 Assert( !d_bool_eqc
[0].isNull() );
422 Assert( !d_bool_eqc
[1].isNull() );
423 d_urelevant_terms
.clear();
424 Trace("sg-proc") << "...done get eq classes" << std::endl
;
426 Trace("sg-proc") << "Determine ground EQC..." << std::endl
;
430 for( unsigned i
=0; i
<eqcs
.size(); i
++ ){
432 if( d_ground_eqc_map
.find( r
)==d_ground_eqc_map
.end() ){
433 std::vector
< TNode
> args
;
434 Trace("sg-pat-debug") << "******* Get ground term for " << r
<< std::endl
;
436 if( getTermDatabase()->isInductionTerm( r
) ){
437 n
= d_op_arg_index
[r
].getGroundTerm( this, args
);
442 Trace("sg-pat") << "Ground term for eqc " << r
<< " : " << std::endl
;
443 Trace("sg-pat") << " " << n
<< std::endl
;
444 d_ground_eqc_map
[r
] = n
;
447 Trace("sg-pat-debug") << "...could not find ground term." << std::endl
;
452 //also get ground terms
453 d_ground_terms
.clear();
454 for( unsigned i
=0; i
<eqcs
.size(); i
++ ){
456 d_op_arg_index
[r
].getGroundTerms( this, d_ground_terms
);
458 Trace("sg-proc") << "...done determine ground EQC" << std::endl
;
461 if( Trace
.isOn("sg-gen-eqc") ){
462 for( unsigned i
=0; i
<eqcs
.size(); i
++ ){
465 bool firstTime
= true;
466 bool isFalse
= areEqual( r
, getTermDatabase()->d_false
);
467 eq::EqClassIterator eqc_i
= eq::EqClassIterator( r
, ee
);
468 while( !eqc_i
.isFinished() ){
470 if( !n
.getAttribute(NoMatchAttribute()) && ( n
.getKind()!=EQUAL
|| isFalse
) ){
472 Trace("sg-gen-eqc") << "e" << d_em
[r
] << " : { " << std::endl
;
475 if( n
.hasOperator() ){
476 Trace("sg-gen-eqc") << " (" << n
.getOperator();
477 getTermDatabase()->computeArgReps( n
);
478 for( unsigned i
=0; i
<getTermDatabase()->d_arg_reps
[n
].size(); i
++ ){
479 Trace("sg-gen-eqc") << " e" << d_em
[getTermDatabase()->d_arg_reps
[n
][i
]];
481 Trace("sg-gen-eqc") << ") :: " << n
<< std::endl
;
483 Trace("sg-gen-eqc") << " " << n
<< std::endl
;
489 Trace("sg-gen-eqc") << "}" << std::endl
;
490 //print out ground term
491 std::map
< TNode
, Node
>::iterator it
= d_ground_eqc_map
.find( r
);
492 if( it
!=d_ground_eqc_map
.end() ){
493 Trace("sg-gen-eqc") << "- Ground term : " << it
->second
<< std::endl
;
499 Trace("sg-proc") << "Compute relevant eqc..." << std::endl
;
500 d_relevant_eqc
[0].clear();
501 d_relevant_eqc
[1].clear();
502 for( unsigned i
=0; i
<eqcs
.size(); i
++ ){
504 std::map
< TNode
, Node
>::iterator it
= d_ground_eqc_map
.find( r
);
506 if( it
==d_ground_eqc_map
.end() ){
509 //based on unproven conjectures? TODO
510 d_relevant_eqc
[index
].push_back( r
);
512 Trace("sg-gen-tg-debug") << "Initial relevant eqc : ";
513 for( unsigned i
=0; i
<d_relevant_eqc
[0].size(); i
++ ){
514 Trace("sg-gen-tg-debug") << "e" << d_em
[d_relevant_eqc
[0][i
]] << " ";
516 Trace("sg-gen-tg-debug") << std::endl
;
517 Trace("sg-proc") << "...done compute relevant eqc" << std::endl
;
520 Trace("sg-proc") << "Collect signature information..." << std::endl
;
526 for( std::map
< Node
, TermArgTrie
>::iterator it
= getTermDatabase()->d_func_map_trie
.begin(); it
!= getTermDatabase()->d_func_map_trie
.end(); ++it
){
527 if( !getTermDatabase()->d_op_map
[it
->first
].empty() ){
528 Node nn
= getTermDatabase()->d_op_map
[it
->first
][0];
529 if( isHandledTerm( nn
) && nn
.getKind()!=APPLY_SELECTOR_TOTAL
&& !nn
.getType().isBoolean() ){
530 d_funcs
.push_back( it
->first
);
531 d_typ_funcs
[tnull
].push_back( it
->first
);
532 d_typ_funcs
[nn
.getType()].push_back( it
->first
);
533 for( unsigned i
=0; i
<nn
.getNumChildren(); i
++ ){
534 d_func_args
[it
->first
].push_back( nn
[i
].getType() );
536 d_func_kind
[it
->first
] = nn
.getKind();
537 Trace("sg-rel-sig") << "Will enumerate function applications of : " << it
->first
<< ", #args = " << d_func_args
[it
->first
].size() << ", kind = " << nn
.getKind() << std::endl
;
538 getTermDatabase()->computeUfEqcTerms( it
->first
);
543 for( std::map
< TypeNode
, std::vector
< TNode
> >::iterator it
= d_typ_funcs
.begin(); it
!=d_typ_funcs
.end(); ++it
){
544 std::random_shuffle( it
->second
.begin(), it
->second
.end() );
545 if( it
->first
.isNull() ){
546 Trace("sg-gen-tg-debug") << "In this order : ";
547 for( unsigned i
=0; i
<it
->second
.size(); i
++ ){
548 Trace("sg-gen-tg-debug") << it
->second
[i
] << " ";
550 Trace("sg-gen-tg-debug") << std::endl
;
553 Trace("sg-proc") << "...done collect signature information" << std::endl
;
556 Trace("sg-proc") << "Build theorem index..." << std::endl
;
559 std::vector
< Node
> provenConj
;
560 quantifiers::FirstOrderModel
* m
= d_quantEngine
->getModel();
561 for( int i
=0; i
<m
->getNumAssertedQuantifiers(); i
++ ){
562 Node q
= m
->getAssertedQuantifier( i
);
563 Trace("thm-db-debug") << "Is " << q
<< " a relevant theorem?" << std::endl
;
565 if( q
[1].getKind()==EQUAL
){
566 bool isSubsume
= false;
568 for( unsigned r
=0; r
<2; r
++ ){
569 TNode nl
= q
[1][r
==0 ? 0 : 1];
570 TNode nr
= q
[1][r
==0 ? 1 : 0];
571 Node eq
= nl
.eqNode( nr
);
572 if( r
==1 || std::find( d_conjectures
.begin(), d_conjectures
.end(), q
)==d_conjectures
.end() ){
573 //must make it canonical
574 std::map
< TypeNode
, unsigned > var_count
;
575 std::map
< TNode
, TNode
> subs
;
576 Trace("sg-proc-debug") << "get canonical " << eq
<< std::endl
;
577 eq
= getCanonicalTerm( eq
, var_count
, subs
);
581 inEe
= d_ee_conjectures
.find( q
[1] )!=d_ee_conjectures
.end();
583 //add to universal equality engine
584 Node nl
= getUniversalRepresentative( eq
[0], true );
585 Node nr
= getUniversalRepresentative( eq
[1], true );
586 if( areUniversalEqual( nl
, nr
) ){
588 //set inactive (will be ignored by other modules)
589 d_quantEngine
->getModel()->setQuantifierActive( q
, false );
592 d_ee_conjectures
[q
[1]] = true;
593 d_uequalityEngine
.assertEquality( nl
.eqNode( nr
), true, exp
);
596 Trace("sg-conjecture") << "*** CONJECTURE : currently proven" << (isSubsume
? " and subsumed" : "");
597 Trace("sg-conjecture") << " : " << q
[1] << std::endl
;
598 provenConj
.push_back( q
);
601 Trace("thm-db-debug") << "Adding theorem to database " << eq
[0] << " == " << eq
[1] << std::endl
;
602 d_thm_index
.addTheorem( eq
[0], eq
[1] );
612 //examine status of other conjectures
613 for( unsigned i
=0; i
<d_conjectures
.size(); i
++ ){
614 Node q
= d_conjectures
[i
];
615 if( std::find( provenConj
.begin(), provenConj
.end(), q
)==provenConj
.end() ){
616 //check each skolem variable
617 bool disproven
= true;
618 //std::vector< Node > sk;
619 //getTermDatabase()->getSkolemConstants( q, sk, true );
620 Trace("sg-conjecture") << " CONJECTURE : ";
621 std::vector
< Node
> ce
;
622 for( unsigned j
=0; j
<getTermDatabase()->d_skolem_constants
[q
].size(); j
++ ){
623 TNode k
= getTermDatabase()->d_skolem_constants
[q
][j
];
624 TNode rk
= getRepresentative( k
);
625 std::map
< TNode
, Node
>::iterator git
= d_ground_eqc_map
.find( rk
);
626 //check if it is a ground term
627 if( git
==d_ground_eqc_map
.end() ){
628 Trace("sg-conjecture") << "ACTIVE : " << q
;
629 if( Trace
.isOn("sg-gen-eqc") ){
630 Trace("sg-conjecture") << " { ";
631 for( unsigned k
=0; k
<getTermDatabase()->d_skolem_constants
[q
].size(); k
++ ){ Trace("sg-conjecture") << getTermDatabase()->d_skolem_constants
[q
][k
] << ( j
==k
? "*" : "" ) << " "; }
632 Trace("sg-conjecture") << "}";
634 Trace("sg-conjecture") << std::endl
;
638 ce
.push_back( git
->second
);
642 Trace("sg-conjecture") << "disproven : " << q
<< " : ";
643 for( unsigned i
=0; i
<ce
.size(); i
++ ){
644 Trace("sg-conjecture") << q
[0][i
] << " -> " << ce
[i
] << " ";
646 Trace("sg-conjecture") << std::endl
;
650 Trace("thm-db") << "Theorem database is : " << std::endl
;
651 d_thm_index
.debugPrint( "thm-db" );
652 Trace("thm-db") << std::endl
;
653 Trace("sg-proc") << "...done build theorem index" << std::endl
;
657 d_pattern_var_id
.clear();
658 d_pattern_var_duplicate
.clear();
659 d_pattern_is_normal
.clear();
660 d_pattern_fun_id
.clear();
661 d_pattern_fun_sum
.clear();
662 d_rel_patterns
.clear();
663 d_rel_pattern_var_sum
.clear();
664 d_rel_pattern_typ_index
.clear();
665 d_rel_pattern_subs_index
.clear();
666 d_gen_lat_maximal
.clear();
667 d_gen_lat_child
.clear();
668 d_gen_lat_parent
.clear();
671 //the following generates a set of relevant terms
672 d_use_ccand_eqc
= true;
673 for( unsigned i
=0; i
<2; i
++ ){
674 d_ccand_eqc
[i
].clear();
675 d_ccand_eqc
[i
].push_back( d_relevant_eqc
[i
] );
677 d_rel_term_count
= 0;
678 //consider all functions
679 d_typ_tg_funcs
.clear();
680 for( std::map
< TypeNode
, std::vector
< TNode
> >::iterator it
= d_typ_funcs
.begin(); it
!= d_typ_funcs
.end(); ++it
){
681 d_typ_tg_funcs
[it
->first
].insert( d_typ_tg_funcs
[it
->first
].end(), it
->second
.begin(), it
->second
.end() );
683 std::map
< TypeNode
, unsigned > rt_var_max
;
684 std::vector
< TypeNode
> rt_types
;
685 //map from generalization depth to maximum depth
686 //std::map< unsigned, unsigned > gdepth_to_tdepth;
687 for( unsigned depth
=1; depth
<3; depth
++ ){
688 Assert( d_tg_alloc
.empty() );
689 Trace("sg-proc") << "Generate terms at depth " << depth
<< "..." << std::endl
;
690 Trace("sg-rel-term") << "Relevant terms of depth " << depth
<< " : " << std::endl
;
696 d_tg_gdepth_limit
= -1;
698 d_tg_alloc
[0].reset( this, TypeNode::null() );
699 while( d_tg_alloc
[0].getNextTerm( this, depth
) ){
700 Assert( d_tg_alloc
[0].getGeneralizationDepth( this )==d_tg_gdepth
);
701 if( d_tg_alloc
[0].getDepth( this )==depth
){
703 Node nn
= d_tg_alloc
[0].getTerm( this );
704 if( getUniversalRepresentative( nn
)==nn
){
706 Trace("sg-rel-term") << "*** Relevant term : ";
707 d_tg_alloc
[0].debugPrint( this, "sg-rel-term", "sg-rel-term-debug2" );
708 Trace("sg-rel-term") << std::endl
;
710 for( unsigned r
=0; r
<2; r
++ ){
711 Trace("sg-gen-tg-eqc") << "...from equivalence classes (" << r
<< ") : ";
712 int index
= d_ccand_eqc
[r
].size()-1;
713 for( unsigned j
=0; j
<d_ccand_eqc
[r
][index
].size(); j
++ ){
714 Trace("sg-gen-tg-eqc") << "e" << d_em
[d_ccand_eqc
[r
][index
][j
]] << " ";
716 Trace("sg-gen-tg-eqc") << std::endl
;
718 TypeNode tnn
= nn
.getType();
719 Trace("sg-gen-tg-debug") << "...term is " << nn
<< std::endl
;
720 Assert( getUniversalRepresentative( nn
)==nn
);
722 //add information about pattern
723 Trace("sg-gen-tg-debug") << "Collect pattern information..." << std::endl
;
724 Assert( std::find( d_rel_patterns
[tnn
].begin(), d_rel_patterns
[tnn
].end(), nn
)==d_rel_patterns
[tnn
].end() );
725 d_rel_patterns
[tnn
].push_back( nn
);
726 //build information concerning the variables in this pattern
728 std::map
< TypeNode
, unsigned > typ_to_subs_index
;
729 std::vector
< TNode
> gsubs_vars
;
730 for( std::map
< TypeNode
, unsigned >::iterator it
= d_var_id
.begin(); it
!= d_var_id
.end(); ++it
){
732 typ_to_subs_index
[it
->first
] = sum
;
734 for( unsigned i
=0; i
<it
->second
; i
++ ){
735 gsubs_vars
.push_back( getFreeVar( it
->first
, i
) );
739 d_rel_pattern_var_sum
[nn
] = sum
;
740 //register the pattern
741 registerPattern( nn
, tnn
);
742 Assert( d_pattern_is_normal
[nn
] );
743 Trace("sg-gen-tg-debug") << "...done collect pattern information" << std::endl
;
745 //compute generalization relation
746 Trace("sg-gen-tg-debug") << "Build generalization information..." << std::endl
;
747 std::map
< TNode
, bool > patProc
;
748 int maxGenDepth
= -1;
749 unsigned i
= d_rel_patterns
[tnn
].size()-1;
750 for( int j
=(int)(i
-1); j
>=0; j
-- ){
751 TNode np
= d_rel_patterns
[tnn
][j
];
752 if( patProc
.find( np
)==patProc
.end() ){
753 Trace("sg-gen-tg-debug2") << "Check if generalized by " << np
<< "..." << std::endl
;
754 if( isGeneralization( np
, nn
) ){
755 Trace("sg-rel-terms-debug") << " is generalized by : " << np
<< std::endl
;
756 d_gen_lat_child
[np
].push_back( nn
);
757 d_gen_lat_parent
[nn
].push_back( np
);
758 if( d_gen_depth
[np
]>maxGenDepth
){
759 maxGenDepth
= d_gen_depth
[np
];
761 //don't consider the transitive closure of generalizes
762 Trace("sg-gen-tg-debug2") << "Add generalizations" << std::endl
;
763 addGeneralizationsOf( np
, patProc
);
764 Trace("sg-gen-tg-debug2") << "Done add generalizations" << std::endl
;
766 Trace("sg-gen-tg-debug2") << " is not generalized by : " << np
<< std::endl
;
770 if( d_gen_lat_parent
[nn
].empty() ){
771 d_gen_lat_maximal
[tnn
].push_back( nn
);
773 d_gen_depth
[nn
] = maxGenDepth
+1;
774 Trace("sg-rel-term-debug") << " -> generalization depth is " << d_gen_depth
[nn
] << " <> " << depth
<< std::endl
;
775 Trace("sg-gen-tg-debug") << "...done build generalization information" << std::endl
;
777 //record information about types
778 Trace("sg-gen-tg-debug") << "Collect type information..." << std::endl
;
779 PatternTypIndex
* pti
= &d_rel_pattern_typ_index
;
780 for( std::map
< TypeNode
, unsigned >::iterator it
= d_var_id
.begin(); it
!= d_var_id
.end(); ++it
){
781 pti
= &pti
->d_children
[it
->first
][it
->second
];
783 if( rt_var_max
.find( it
->first
)==rt_var_max
.end() || it
->second
>rt_var_max
[it
->first
] ){
784 rt_var_max
[it
->first
] = it
->second
;
787 if( std::find( rt_types
.begin(), rt_types
.end(), tnn
)==rt_types
.end() ){
788 rt_types
.push_back( tnn
);
790 pti
->d_terms
.push_back( nn
);
791 Trace("sg-gen-tg-debug") << "...done collect type information" << std::endl
;
793 Trace("sg-gen-tg-debug") << "Build substitutions for ground EQC..." << std::endl
;
794 std::vector
< TNode
> gsubs_terms
;
795 gsubs_terms
.resize( gsubs_vars
.size() );
796 int index
= d_ccand_eqc
[1].size()-1;
797 for( unsigned j
=0; j
<d_ccand_eqc
[1][index
].size(); j
++ ){
798 TNode r
= d_ccand_eqc
[1][index
][j
];
799 Trace("sg-gen-tg-eqc") << " Matches for e" << d_em
[r
] << ", which is ground term " << d_ground_eqc_map
[r
] << ":" << std::endl
;
800 std::map
< TypeNode
, std::map
< unsigned, TNode
> > subs
;
801 std::map
< TNode
, bool > rev_subs
;
802 //only get ground terms
803 unsigned mode
= optFilterConfirmationOnlyGround() ? 2 : 0;
804 d_tg_alloc
[0].resetMatching( this, r
, mode
);
805 while( d_tg_alloc
[0].getNextMatch( this, r
, subs
, rev_subs
) ){
806 //we will be building substitutions
807 bool firstTime
= true;
808 for( std::map
< TypeNode
, std::map
< unsigned, TNode
> >::iterator it
= subs
.begin(); it
!= subs
.end(); ++it
){
809 unsigned tindex
= typ_to_subs_index
[it
->first
];
810 for( std::map
< unsigned, TNode
>::iterator it2
= it
->second
.begin(); it2
!= it
->second
.end(); ++it2
){
812 Trace("sg-gen-tg-eqc") << ", ";
815 Trace("sg-gen-tg-eqc") << " ";
817 Trace("sg-gen-tg-eqc") << it
->first
<< ":x" << it2
->first
<< " -> " << it2
->second
;
818 Assert( tindex
+it2
->first
<gsubs_terms
.size() );
819 gsubs_terms
[tindex
+it2
->first
] = it2
->second
;
822 Trace("sg-gen-tg-eqc") << std::endl
;
823 d_rel_pattern_subs_index
[nn
].addSubstitution( r
, gsubs_vars
, gsubs_terms
);
826 Trace("sg-gen-tg-debug") << "...done build substitutions for ground EQC" << std::endl
;
828 Trace("sg-gen-tg-debug") << "> not canonical : " << nn
<< std::endl
;
831 Trace("sg-gen-tg-debug") << "> produced term at previous depth : ";
832 d_tg_alloc
[0].debugPrint( this, "sg-gen-tg-debug", "sg-gen-tg-debug" );
833 Trace("sg-gen-tg-debug") << std::endl
;
836 Trace("sg-proc") << "...done generate terms at depth " << depth
<< std::endl
;
839 //now generate right hand sides
843 Trace("sg-stats") << "--------> Total relevant patterns : " << d_rel_term_count
<< std::endl
;
845 Trace("sg-proc") << "Generate properties..." << std::endl
;
847 d_use_ccand_eqc
= false;
850 for( std::map
< TypeNode
, unsigned >::iterator it
= rt_var_max
.begin(); it
!= rt_var_max
.end(); ++it
){
851 d_var_id
[ it
->first
] = it
->second
;
852 d_var_limit
[ it
->first
] = it
->second
;
854 //set up environment for candidate conjectures
855 d_cconj_at_depth
.clear();
856 for( unsigned i
=0; i
<2; i
++ ){
859 d_cconj_rhs_paired
.clear();
860 unsigned totalCount
= 0;
861 for( unsigned depth
=0; depth
<5; depth
++ ){
862 //consider types from relevant terms
863 std::random_shuffle( rt_types
.begin(), rt_types
.end() );
864 for( unsigned i
=0; i
<rt_types
.size(); i
++ ){
865 Assert( d_tg_alloc
.empty() );
866 Trace("sg-proc") << "Generate relevant RHS terms of type " << rt_types
[i
] << " at depth " << depth
<< "..." << std::endl
;
868 d_tg_alloc
[0].reset( this, rt_types
[i
] );
869 while( d_tg_alloc
[0].getNextTerm( this, depth
) && totalCount
<100 ){
870 if( d_tg_alloc
[0].getDepth( this )==depth
){
871 Node rhs
= d_tg_alloc
[0].getTerm( this );
872 Trace("sg-rel-prop") << "Relevant RHS : " << rhs
<< std::endl
;
874 Assert( rhs
.getType()==rt_types
[i
] );
875 registerPattern( rhs
, rt_types
[i
] );
876 //for each maximal node of type rt_types[i] in generalization lattice
877 for( unsigned j
=0; j
<d_gen_lat_maximal
[rt_types
[i
]].size(); j
++ ){
878 //add candidate conjecture
879 addCandidateConjecture( d_gen_lat_maximal
[rt_types
[i
]][j
], rhs
, 0 );
884 //could have been partial, we must clear
887 Trace("sg-proc") << "Process candidate conjectures up to RHS term depth " << depth
<< "..." << std::endl
;
888 for( unsigned conj_depth
=0; conj_depth
<depth
; conj_depth
++ ){
889 //process all conjectures waiting at depth
890 unsigned sz
= d_cconj_at_depth
[conj_depth
].size();
891 for( int i
=(int)(sz
-1); i
>=0; i
-- ){
892 processCandidateConjecture( d_cconj_at_depth
[conj_depth
][i
], conj_depth
);
894 Assert( d_cconj_at_depth
[conj_depth
].size()==sz
);
895 d_cconj_at_depth
[conj_depth
].clear();
897 Trace("sg-proc") << "...done process candidate conjectures at RHS term depth " << depth
<< std::endl
;
899 Trace("sg-proc") << "...done generate properties" << std::endl
;
901 if( !d_waiting_conjectures
.empty() ){
902 Trace("sg-proc") << "Generated " << d_waiting_conjectures
.size() << " conjectures." << std::endl
;
903 d_conjectures
.insert( d_conjectures
.end(), d_waiting_conjectures
.begin(), d_waiting_conjectures
.end() );
904 for( unsigned i
=0; i
<d_waiting_conjectures
.size(); i
++ ){
905 Assert( d_waiting_conjectures
[i
].getKind()==FORALL
);
906 Node lem
= NodeManager::currentNM()->mkNode( OR
, d_waiting_conjectures
[i
].negate(), d_waiting_conjectures
[i
] );
907 d_quantEngine
->addLemma( lem
, false );
908 d_quantEngine
->addRequirePhase( d_waiting_conjectures
[i
], false );
910 d_waiting_conjectures
.clear();
913 Trace("thm-ee") << "Universal equality engine is : " << std::endl
;
914 eq::EqClassesIterator ueqcs_i
= eq::EqClassesIterator( &d_uequalityEngine
);
915 while( !ueqcs_i
.isFinished() ){
916 TNode r
= (*ueqcs_i
);
917 bool firstTime
= true;
918 TNode rr
= getUniversalRepresentative( r
);
919 Trace("thm-ee") << " " << r
;
920 if( rr
!=r
){ Trace("thm-ee") << " [" << rr
<< "]"; }
921 Trace("thm-ee") << " : { ";
922 eq::EqClassIterator ueqc_i
= eq::EqClassIterator( r
, &d_uequalityEngine
);
923 while( !ueqc_i
.isFinished() ){
927 Trace("thm-ee") << std::endl
;
930 Trace("thm-ee") << " " << n
<< std::endl
;
934 if( !firstTime
){ Trace("thm-ee") << " "; }
935 Trace("thm-ee") << "}" << std::endl
;
938 Trace("thm-ee") << std::endl
;
943 void ConjectureGenerator::registerQuantifier( Node q
) {
947 void ConjectureGenerator::assertNode( Node n
) {
952 unsigned ConjectureGenerator::getNumTgVars( TypeNode tn
) {
953 //return d_var_tg.size();
957 bool ConjectureGenerator::allowVar( TypeNode tn
) {
958 std::map
< TypeNode
, unsigned >::iterator it
= d_var_limit
.find( tn
);
959 if( it
==d_var_limit
.end() ){
962 return d_var_id
[tn
]<it
->second
;
966 void ConjectureGenerator::addVar( TypeNode tn
) {
967 //d_var_tg.push_back( v );
969 //d_var_eq_tg.push_back( std::vector< unsigned >() );
972 void ConjectureGenerator::removeVar( TypeNode tn
) {
974 //d_var_eq_tg.pop_back();
975 //d_var_tg.pop_back();
978 unsigned ConjectureGenerator::getNumTgFuncs( TypeNode tn
) {
979 return d_typ_tg_funcs
[tn
].size();
982 TNode
ConjectureGenerator::getTgFunc( TypeNode tn
, unsigned i
) {
983 return d_typ_tg_funcs
[tn
][i
];
986 bool ConjectureGenerator::considerCurrentTerm() {
987 Assert( !d_tg_alloc
.empty() );
989 //if generalization depth is too large, don't consider it
990 unsigned i
= d_tg_alloc
.size();
991 Trace("sg-gen-tg-debug") << "Consider term ";
992 d_tg_alloc
[0].debugPrint( this, "sg-gen-tg-debug", "sg-gen-tg-debug" );
993 Trace("sg-gen-tg-debug") << "? curr term size = " << d_tg_alloc
.size() << ", last status = " << d_tg_alloc
[i
-1].d_status
;
994 Trace("sg-gen-tg-debug") << std::endl
;
996 Assert( d_tg_alloc
[0].getGeneralizationDepth( this )==d_tg_gdepth
);
998 if( d_tg_gdepth_limit
>=0 && d_tg_gdepth
>(unsigned)d_tg_gdepth_limit
){
999 Trace("sg-gen-consider-term") << "-> generalization depth of ";
1000 d_tg_alloc
[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-tg-debug" );
1001 Trace("sg-gen-consider-term") << " is too high " << d_tg_gdepth
<< " " << d_tg_alloc
[0].getGeneralizationDepth( this ) << ", do not consider." << std::endl
;
1006 if( d_tg_alloc
[i
-1].d_status
==1 ){
1007 }else if( d_tg_alloc
[i
-1].d_status
==2 ){
1008 }else if( d_tg_alloc
[i
-1].d_status
==5 ){
1010 Trace("sg-gen-tg-debug") << "Bad tg: " << &d_tg_alloc
[i
-1] << std::endl
;
1013 //if equated two variables, first check if context-independent TODO
1014 //----end optimizations
1017 //check based on which candidate equivalence classes match
1018 if( d_use_ccand_eqc
){
1019 Trace("sg-gen-tg-debug") << "Filter based on relevant ground EQC";
1020 Trace("sg-gen-tg-debug") << ", #eqc to try = " << d_ccand_eqc
[0][i
-1].size() << "/" << d_ccand_eqc
[1][i
-1].size() << std::endl
;
1022 Assert( d_ccand_eqc
[0].size()>=2 );
1023 Assert( d_ccand_eqc
[0].size()==d_ccand_eqc
[1].size() );
1024 Assert( d_ccand_eqc
[0].size()==d_tg_id
+1 );
1025 Assert( d_tg_id
==d_tg_alloc
.size() );
1026 for( unsigned r
=0; r
<2; r
++ ){
1027 d_ccand_eqc
[r
][i
].clear();
1030 //re-check feasibility of EQC
1031 for( unsigned r
=0; r
<2; r
++ ){
1032 for( unsigned j
=0; j
<d_ccand_eqc
[r
][i
-1].size(); j
++ ){
1033 std::map
< TypeNode
, std::map
< unsigned, TNode
> > subs
;
1034 std::map
< TNode
, bool > rev_subs
;
1037 mode
= optReqDistinctVarPatterns() ? 1 : 0;
1039 mode
= (optFilterConfirmation() && optFilterConfirmationOnlyGround() ) ? 2 : 0;
1041 d_tg_alloc
[0].resetMatching( this, d_ccand_eqc
[r
][i
-1][j
], mode
);
1042 if( d_tg_alloc
[0].getNextMatch( this, d_ccand_eqc
[r
][i
-1][j
], subs
, rev_subs
) ){
1043 d_ccand_eqc
[r
][i
].push_back( d_ccand_eqc
[r
][i
-1][j
] );
1047 for( unsigned r
=0; r
<2; r
++ ){
1048 Trace("sg-gen-tg-debug") << "Current eqc of type " << r
<< " : ";
1049 for( unsigned j
=0; j
<d_ccand_eqc
[r
][i
].size(); j
++ ){
1050 Trace("sg-gen-tg-debug") << "e" << d_em
[d_ccand_eqc
[r
][i
][j
]] << " ";
1052 Trace("sg-gen-tg-debug") << std::endl
;
1054 if( d_ccand_eqc
[0][i
].empty() ){
1055 Trace("sg-gen-consider-term") << "Do not consider term of form ";
1056 d_tg_alloc
[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-consider-term-debug" );
1057 Trace("sg-gen-consider-term") << " since no relevant EQC matches it." << std::endl
;
1060 if( d_ccand_eqc
[1][i
].empty() && optFilterConfirmation() ){
1061 Trace("sg-gen-consider-term") << "Do not consider term of form ";
1062 d_tg_alloc
[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-consider-term-debug" );
1063 Trace("sg-gen-consider-term") << " since no ground EQC matches it." << std::endl
;
1067 Trace("sg-gen-tg-debug") << "Will consider term ";
1068 d_tg_alloc
[0].debugPrint( this, "sg-gen-tg-debug", "sg-gen-tg-debug" );
1069 Trace("sg-gen-tg-debug") << std::endl
;
1070 Trace("sg-gen-consider-term-debug") << std::endl
;
1074 bool ConjectureGenerator::considerTermCanon( unsigned tg_id
){
1075 Assert( tg_id
<d_tg_alloc
.size() );
1076 //check based on a canonicity of the term (if there is one)
1077 Trace("sg-gen-tg-debug") << "Consider term canon ";
1078 d_tg_alloc
[0].debugPrint( this, "sg-gen-tg-debug", "sg-gen-tg-debug" );
1079 Trace("sg-gen-tg-debug") << ", tg is [" << tg_id
<< "]..." << std::endl
;
1081 Node ln
= d_tg_alloc
[tg_id
].getTerm( this );
1082 Trace("sg-gen-tg-debug") << "Term is " << ln
<< std::endl
;
1084 //do not consider if it is non-canonical, and either:
1085 // (1) we are not filtering based on matching candidate eqc, or
1086 // (2) its canonical form is a generalization.
1087 TNode lnr
= getUniversalRepresentative( ln
, true );
1089 markReportedCanon( ln
);
1090 }else if( !d_use_ccand_eqc
|| isGeneralization( lnr
, ln
) ){
1091 Trace("sg-gen-consider-term") << "Do not consider term of form ";
1092 d_tg_alloc
[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-consider-term-debug" );
1093 Trace("sg-gen-consider-term") << " since sub-term " << ln
<< " is not canonical representation (which is " << lnr
<< ")." << std::endl
;
1097 Trace("sg-gen-tg-debug") << "Will consider term canon ";
1098 d_tg_alloc
[0].debugPrint( this, "sg-gen-tg-debug", "sg-gen-tg-debug" );
1099 Trace("sg-gen-tg-debug") << std::endl
;
1100 Trace("sg-gen-consider-term-debug") << std::endl
;
1104 void ConjectureGenerator::changeContext( bool add
) {
1106 for( unsigned r
=0; r
<2; r
++ ){
1107 d_ccand_eqc
[r
].push_back( std::vector
< TNode
>() );
1111 for( unsigned r
=0; r
<2; r
++ ){
1112 d_ccand_eqc
[r
].pop_back();
1115 Assert( d_tg_alloc
.find( d_tg_id
)!=d_tg_alloc
.end() );
1116 d_tg_alloc
.erase( d_tg_id
);
1120 unsigned ConjectureGenerator::collectFunctions( TNode opat
, TNode pat
, std::map
< TNode
, unsigned >& funcs
,
1121 std::map
< TypeNode
, unsigned >& mnvn
, std::map
< TypeNode
, unsigned >& mxvn
){
1122 if( pat
.hasOperator() ){
1123 funcs
[pat
.getOperator()]++;
1125 for( unsigned i
=0; i
<pat
.getNumChildren(); i
++ ){
1126 sum
+= collectFunctions( opat
, pat
[i
], funcs
, mnvn
, mxvn
);
1130 Assert( pat
.getNumChildren()==0 );
1133 if( pat
.getKind()==BOUND_VARIABLE
){
1135 //duplicate variable
1136 d_pattern_var_duplicate
[opat
]++;
1139 TypeNode tn
= pat
.getType();
1140 unsigned vn
= d_free_var_num
[pat
];
1141 std::map
< TypeNode
, unsigned >::iterator it
= mnvn
.find( tn
);
1142 if( it
!=mnvn
.end() ){
1143 if( vn
<it
->second
){
1144 d_pattern_is_normal
[opat
] = false;
1146 }else if( vn
>mxvn
[tn
] ){
1147 if( vn
!=mxvn
[tn
]+1 ){
1148 d_pattern_is_normal
[opat
] = false;
1153 //first variable of this type
1163 void ConjectureGenerator::registerPattern( Node pat
, TypeNode tpat
) {
1164 if( std::find( d_patterns
[tpat
].begin(), d_patterns
[tpat
].end(), pat
)==d_patterns
[tpat
].end() ){
1165 d_patterns
[TypeNode::null()].push_back( pat
);
1166 d_patterns
[tpat
].push_back( pat
);
1168 Assert( d_pattern_fun_id
.find( pat
)==d_pattern_fun_id
.end() );
1169 Assert( d_pattern_var_id
.find( pat
)==d_pattern_var_id
.end() );
1172 std::map
< TypeNode
, unsigned > mnvn
;
1173 d_pattern_fun_sum
[pat
] = collectFunctions( pat
, pat
, d_pattern_fun_id
[pat
], mnvn
, d_pattern_var_id
[pat
] );
1174 if( d_pattern_is_normal
.find( pat
)==d_pattern_is_normal
.end() ){
1175 d_pattern_is_normal
[pat
] = true;
1180 bool ConjectureGenerator::isGeneralization( TNode patg
, TNode pat
, std::map
< TNode
, TNode
>& subs
) {
1181 if( patg
.getKind()==BOUND_VARIABLE
){
1182 std::map
< TNode
, TNode
>::iterator it
= subs
.find( patg
);
1183 if( it
!=subs
.end() ){
1184 return it
->second
==pat
;
1190 Assert( patg
.hasOperator() );
1191 if( !pat
.hasOperator() || patg
.getOperator()!=pat
.getOperator() ){
1194 Assert( patg
.getNumChildren()==pat
.getNumChildren() );
1195 for( unsigned i
=0; i
<patg
.getNumChildren(); i
++ ){
1196 if( !isGeneralization( patg
[i
], pat
[i
], subs
) ){
1205 void ConjectureGenerator::addGeneralizationsOf( TNode pat
, std::map
< TNode
, bool >& patProc
) {
1206 patProc
[pat
] = true;
1207 for( unsigned k
=0; k
<d_gen_lat_parent
[pat
].size(); k
++ ){
1208 addGeneralizationsOf( d_gen_lat_parent
[pat
][k
], patProc
);
1212 void ConjectureGenerator::addCandidateConjecture( TNode lhs
, TNode rhs
, unsigned depth
) {
1213 if( std::find( d_cconj_rhs_paired
[rhs
].begin(), d_cconj_rhs_paired
[rhs
].end(), lhs
)==d_cconj_rhs_paired
[rhs
].end() ){
1214 //add conjecture to list to process
1215 d_cconj_at_depth
[depth
].push_back( d_cconj
[0].size() );
1217 d_cconj
[0].push_back( lhs
);
1218 d_cconj
[1].push_back( rhs
);
1219 d_cconj_rhs_paired
[rhs
].push_back( lhs
);
1223 void ConjectureGenerator::processCandidateConjecture( unsigned cid
, unsigned depth
) {
1224 if( d_waiting_conjectures
.size()>=optFullCheckConjectures() ){
1227 TNode lhs
= d_cconj
[0][cid
];
1228 TNode rhs
= d_cconj
[1][cid
];
1229 if( !considerCandidateConjecture( lhs
, rhs
) ){
1230 //push to children of generalization lattice
1231 for( unsigned i
=0; i
<d_gen_lat_child
[lhs
].size(); i
++ ){
1232 if( d_gen_depth
[lhs
]+1==d_gen_depth
[d_gen_lat_child
[lhs
][i
]] ){
1233 addCandidateConjecture( d_gen_lat_child
[lhs
][i
], rhs
, depth
+1 );
1237 Trace("sg-conjecture") << "* Candidate conjecture : " << lhs
<< " == " << rhs
<< std::endl
;
1238 Trace("sg-conjecture-debug") << " LHS generalization depth : " << d_gen_depth
[lhs
] << std::endl
;
1239 if( optFilterConfirmation() || optFilterFalsification() ){
1240 Trace("sg-conjecture-debug") << " confirmed = " << d_subs_confirmCount
<< ", #witnesses range = " << d_subs_confirmWitnessRange
.size() << "." << std::endl
;
1241 Trace("sg-conjecture-debug") << " #witnesses for ";
1242 bool firstTime
= true;
1243 for( std::map
< TNode
, std::vector
< TNode
> >::iterator it
= d_subs_confirmWitnessDomain
.begin(); it
!= d_subs_confirmWitnessDomain
.end(); ++it
){
1245 Trace("sg-conjecture-debug") << ", ";
1247 Trace("sg-conjecture-debug") << it
->first
<< " : " << it
->second
.size() << "/" << d_pattern_fun_id
[lhs
][it
->first
];
1248 if( it
->second
.size()==1 ){
1249 Trace("sg-conjecture-debug") << " (" << it
->second
[0] << ")";
1253 Trace("sg-conjecture-debug") << std::endl
;
1255 Assert( getUniversalRepresentative( rhs
)==rhs
);
1256 Assert( getUniversalRepresentative( lhs
)==lhs
);
1257 //make universal quantified formula
1258 Assert( std::find( d_eq_conjectures
[lhs
].begin(), d_eq_conjectures
[lhs
].end(), rhs
)==d_eq_conjectures
[lhs
].end() );
1259 d_eq_conjectures
[lhs
].push_back( rhs
);
1260 d_eq_conjectures
[rhs
].push_back( lhs
);
1261 std::vector
< Node
> bvs
;
1262 for( std::map
< TypeNode
, unsigned >::iterator it
= d_pattern_var_id
[lhs
].begin(); it
!= d_pattern_var_id
[lhs
].end(); ++it
){
1263 for( unsigned i
=0; i
<=it
->second
; i
++ ){
1264 bvs
.push_back( getFreeVar( it
->first
, i
) );
1267 Node bvl
= NodeManager::currentNM()->mkNode( BOUND_VAR_LIST
, bvs
);
1268 Node conj
= NodeManager::currentNM()->mkNode( FORALL
, bvl
, lhs
.eqNode( rhs
) );
1269 conj
= Rewriter::rewrite( conj
);
1270 d_waiting_conjectures
.push_back( conj
);
1274 bool ConjectureGenerator::considerCandidateConjecture( TNode lhs
, TNode rhs
) {
1275 Trace("sg-cconj-debug") << "Consider candidate conjecture : " << lhs
<< " == " << rhs
<< "?" << std::endl
;
1277 Trace("sg-cconj-debug") << " -> trivial." << std::endl
;
1280 if( lhs
.getKind()==APPLY_CONSTRUCTOR
&& rhs
.getKind()==APPLY_CONSTRUCTOR
){
1281 Trace("sg-cconj-debug") << " -> irrelevant by syntactic analysis." << std::endl
;
1284 //variables of LHS must subsume variables of RHS
1285 for( std::map
< TypeNode
, unsigned >::iterator it
= d_pattern_var_id
[rhs
].begin(); it
!= d_pattern_var_id
[rhs
].end(); ++it
){
1286 std::map
< TypeNode
, unsigned >::iterator itl
= d_pattern_var_id
[lhs
].find( it
->first
);
1287 if( itl
!=d_pattern_var_id
[lhs
].end() ){
1288 if( itl
->second
<it
->second
){
1289 Trace("sg-cconj-debug") << " -> variables of sort " << it
->first
<< " are not subsumed." << std::endl
;
1292 Trace("sg-cconj-debug2") << " variables of sort " << it
->first
<< " are : " << itl
->second
<< " vs " << it
->second
<< std::endl
;
1295 Trace("sg-cconj-debug") << " -> has no variables of sort " << it
->first
<< "." << std::endl
;
1299 //currently active conjecture?
1300 std::map
< Node
, std::vector
< Node
> >::iterator iteq
= d_eq_conjectures
.find( lhs
);
1301 if( iteq
!=d_eq_conjectures
.end() ){
1302 if( std::find( iteq
->second
.begin(), iteq
->second
.end(), rhs
)!=iteq
->second
.end() ){
1303 Trace("sg-cconj-debug") << " -> already are considering this conjecture." << std::endl
;
1307 Trace("sg-cconj") << "Consider possible candidate conjecture : " << lhs
<< " == " << rhs
<< "?" << std::endl
;
1308 //find witness for counterexample, if possible
1309 if( optFilterConfirmation() || optFilterFalsification() ){
1310 Assert( d_rel_pattern_var_sum
.find( lhs
)!=d_rel_pattern_var_sum
.end() );
1311 Trace("sg-cconj-debug") << "Notify substitutions over " << d_rel_pattern_var_sum
[lhs
] << " variables." << std::endl
;
1312 std::map
< TNode
, TNode
> subs
;
1313 d_subs_confirmCount
= 0;
1314 d_subs_confirmWitnessRange
.clear();
1315 d_subs_confirmWitnessDomain
.clear();
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
;
1320 if( optFilterConfirmation() ){
1321 if( d_subs_confirmCount
==0 ){
1322 Trace("sg-cconj") << " -> not confirmed by a ground substitutions." << std::endl
;
1326 if( optFilterConfirmationDomain() ){
1327 std::vector
< TNode
> vars
;
1328 std::vector
< TNode
> subs
;
1329 for( std::map
< TNode
, std::vector
< TNode
> >::iterator it
= d_subs_confirmWitnessDomain
.begin(); it
!= d_subs_confirmWitnessDomain
.end(); ++it
){
1330 Assert( d_pattern_fun_id
[lhs
].find( it
->first
)!=d_pattern_fun_id
[lhs
].end() );
1331 unsigned req
= d_pattern_fun_id
[lhs
][it
->first
];
1332 std::map
< TNode
, unsigned >::iterator itrf
= d_pattern_fun_id
[rhs
].find( it
->first
);
1333 if( itrf
!=d_pattern_fun_id
[rhs
].end() ){
1334 req
= itrf
->second
>req
? itrf
->second
: req
;
1336 if( it
->second
.size()<req
){
1337 Trace("sg-cconj") << " -> did not find at least " << d_pattern_fun_id
[lhs
][it
->first
] << " different values in ground substitutions for variable " << it
->first
<< "." << std::endl
;
1340 if( it
->second
.size()==1 ){
1341 vars
.push_back( it
->first
);
1342 subs
.push_back( it
->second
[0] );
1345 if( optFilterConfirmationNonCanonical() && !vars
.empty() ){
1346 Node slhs
= lhs
.substitute( vars
.begin(), vars
.end(), subs
.begin(), subs
.end() );
1347 Node srhs
= rhs
.substitute( vars
.begin(), vars
.end(), subs
.begin(), subs
.end() );
1348 TNode slhsr
= getUniversalRepresentative( slhs
, true );
1349 TNode srhsr
= getUniversalRepresentative( srhs
, true );
1350 if( areUniversalEqual( slhsr
, srhsr
) ){
1351 Trace("sg-cconj") << " -> all ground witnesses can be proven by other theorems." << std::endl
;
1354 Trace("sg-cconj-debug") << "Checked if " << slhsr
<< " and " << srhsr
<< " were equal." << std::endl
;
1360 Trace("sg-cconj") << " -> SUCCESS." << std::endl
;
1361 if( optFilterConfirmation() || optFilterFalsification() ){
1362 Trace("sg-cconj") << " confirmed = " << d_subs_confirmCount
<< ", #witnesses range = " << d_subs_confirmWitnessRange
.size() << "." << std::endl
;
1363 for( std::map
< TNode
, std::vector
< TNode
> >::iterator it
= d_subs_confirmWitnessDomain
.begin(); it
!= d_subs_confirmWitnessDomain
.end(); ++it
){
1364 Trace("sg-cconj") << " #witnesses for " << it
->first
<< " : " << it
->second
.size() << std::endl
;
1369 if( getUniversalRepresentative( lhs )!=lhs ){
1370 std::cout << "bad universal representative LHS : " << lhs << " " << getUniversalRepresentative( lhs ) << std::endl;
1373 if( getUniversalRepresentative( rhs )!=rhs ){
1374 std::cout << "bad universal representative RHS : " << rhs << " " << getUniversalRepresentative( rhs ) << std::endl;
1379 //check if still canonical representation (should be, but for efficiency this is not guarenteed)
1380 if( getUniversalRepresentative( lhs
)!=lhs
|| getUniversalRepresentative( rhs
)!=rhs
){
1381 Trace("sg-cconj") << " -> after processing, not canonical." << std::endl
;
1388 bool ConjectureGenerator::notifySubstitution( TNode glhs
, std::map
< TNode
, TNode
>& subs
, TNode rhs
) {
1389 if( Trace
.isOn("sg-cconj-debug") ){
1390 Trace("sg-cconj-debug") << "Ground eqc for LHS : " << glhs
<< ", based on substituion: " << std::endl
;
1391 for( std::map
< TNode
, TNode
>::iterator it
= subs
.begin(); it
!= subs
.end(); ++it
){
1392 Assert( getRepresentative( it
->second
)==it
->second
);
1393 Trace("sg-cconj-debug") << " " << it
->first
<< " -> " << it
->second
<< std::endl
;
1396 Trace("sg-cconj-debug") << "Evaluate RHS : : " << rhs
<< std::endl
;
1397 //get the representative of rhs with substitution subs
1398 TNode grhs
= getTermDatabase()->evaluateTerm( rhs
, subs
, true );
1399 Trace("sg-cconj-debug") << "...done evaluating term, got : " << grhs
<< std::endl
;
1400 if( !grhs
.isNull() ){
1402 if( optFilterFalsification() ){
1403 Trace("sg-cconj-debug") << "Ground eqc for RHS : " << grhs
<< std::endl
;
1404 //check based on ground terms
1405 std::map
< TNode
, Node
>::iterator itl
= d_ground_eqc_map
.find( glhs
);
1406 if( itl
!=d_ground_eqc_map
.end() ){
1407 std::map
< TNode
, Node
>::iterator itr
= d_ground_eqc_map
.find( grhs
);
1408 if( itr
!=d_ground_eqc_map
.end() ){
1409 Trace("sg-cconj-debug") << "We have ground terms " << itl
->second
<< " and " << itr
->second
<< "." << std::endl
;
1410 if( itl
->second
.isConst() && itr
->second
.isConst() ){
1411 Trace("sg-cconj-debug") << "...disequal constants." << std::endl
;
1412 Trace("sg-cconj-witness") << " Witness of falsification : " << itl
->second
<< " != " << itr
->second
<< ", substutition is : " << std::endl
;
1413 for( std::map
< TNode
, TNode
>::iterator it
= subs
.begin(); it
!= subs
.end(); ++it
){
1414 Trace("sg-cconj-witness") << " " << it
->first
<< " -> " << it
->second
<< std::endl
;
1422 if( getEqualityEngine()->areDisequal( glhs, grhs, false ) ){
1423 Trace("sg-cconj-debug") << "..." << glhs << " and " << grhs << " are disequal." << std::endl;
1426 Trace("sg-cconj-debug") << "..." << glhs << " and " << grhs << " are not disequal." << std::endl;
1430 Trace("sg-cconj-witness") << " Witnessed " << glhs
<< " == " << grhs
<< ", substutition is : " << std::endl
;
1431 for( std::map
< TNode
, TNode
>::iterator it
= subs
.begin(); it
!= subs
.end(); ++it
){
1432 Trace("sg-cconj-witness") << " " << it
->first
<< " -> " << it
->second
<< std::endl
;
1433 if( std::find( d_subs_confirmWitnessDomain
[it
->first
].begin(), d_subs_confirmWitnessDomain
[it
->first
].end(), it
->second
)==d_subs_confirmWitnessDomain
[it
->first
].end() ){
1434 d_subs_confirmWitnessDomain
[it
->first
].push_back( it
->second
);
1437 d_subs_confirmCount
++;
1438 if( std::find( d_subs_confirmWitnessRange
.begin(), d_subs_confirmWitnessRange
.end(), glhs
)==d_subs_confirmWitnessRange
.end() ){
1439 d_subs_confirmWitnessRange
.push_back( glhs
);
1441 Trace("sg-cconj-debug") << "RHS is identical." << std::endl
;
1444 Trace("sg-cconj-debug") << "(could not ground eqc for RHS)." << std::endl
;
1450 void TermGenerator::reset( ConjectureGenerator
* s
, TypeNode tn
) {
1451 Assert( d_children
.empty() );
1456 Trace("sg-gen-tg-debug2") << "...add to context " << this << std::endl
;
1458 s
->changeContext( true );
1461 bool TermGenerator::getNextTerm( ConjectureGenerator
* s
, unsigned depth
) {
1462 if( Trace
.isOn("sg-gen-tg-debug2") ){
1463 Trace("sg-gen-tg-debug2") << this << " getNextTerm depth " << depth
<< " : status = " << d_status
<< ", num = " << d_status_num
;
1465 TNode f
= s
->getTgFunc( d_typ
, d_status_num
);
1466 Trace("sg-gen-tg-debug2") << ", f = " << f
;
1467 Trace("sg-gen-tg-debug2") << ", #args = " << s
->d_func_args
[f
].size();
1468 Trace("sg-gen-tg-debug2") << ", childNum = " << d_status_child_num
;
1469 Trace("sg-gen-tg-debug2") << ", #children = " << d_children
.size();
1471 Trace("sg-gen-tg-debug2") << std::endl
;
1476 if( !d_typ
.isNull() ){
1477 if( s
->allowVar( d_typ
) ){
1479 d_status_num
= s
->d_var_id
[d_typ
];
1481 Trace("sg-gen-tg-debug2") << this << " ...return unique var #" << d_status_num
<< std::endl
;
1482 return s
->considerCurrentTerm() ? true : getNextTerm( s
, depth
);
1484 //check allocating new variable
1488 return getNextTerm( s
, depth
);
1493 return getNextTerm( s
, depth
);
1495 }else if( d_status
==2 ){
1496 //cleanup previous information
1497 //if( d_status_num>=0 ){
1498 // s->d_var_eq_tg[d_status_num].pop_back();
1500 //check if there is another variable
1501 if( (d_status_num
+1)<(int)s
->getNumTgVars( d_typ
) ){
1503 //we have equated two variables
1504 //s->d_var_eq_tg[d_status_num].push_back( d_id );
1505 Trace("sg-gen-tg-debug2") << this << "...consider other var #" << d_status_num
<< std::endl
;
1506 return s
->considerCurrentTerm() ? true : getNextTerm( s
, depth
);
1510 return getNextTerm( s
, depth
);
1512 }else if( d_status
==4 ){
1514 if( depth
>0 && (d_status_num
+1)<(int)s
->getNumTgFuncs( d_typ
) ){
1516 d_status_child_num
= 0;
1517 Trace("sg-gen-tg-debug2") << this << "...consider function " << s
->getTgFunc( d_typ
, d_status_num
) << std::endl
;
1519 if( !s
->considerCurrentTerm() ){
1521 //don't consider this function
1524 //we have decided on a function application
1526 return getNextTerm( s
, depth
);
1528 //do not choose function applications at depth 0
1530 return getNextTerm( s
, depth
);
1532 }else if( d_status
==5 ){
1533 //iterating over arguments
1534 TNode f
= s
->getTgFunc( d_typ
, d_status_num
);
1535 if( d_status_child_num
<0 ){
1539 return getNextTerm( s
, depth
);
1540 }else if( d_status_child_num
==(int)s
->d_func_args
[f
].size() ){
1541 d_status_child_num
--;
1542 return s
->considerTermCanon( d_id
) ? true : getNextTerm( s
, depth
);
1545 Assert( d_status_child_num
<(int)s
->d_func_args
[f
].size() );
1546 if( d_status_child_num
==(int)d_children
.size() ){
1547 d_children
.push_back( s
->d_tg_id
);
1548 Assert( s
->d_tg_alloc
.find( s
->d_tg_id
)==s
->d_tg_alloc
.end() );
1549 s
->d_tg_alloc
[d_children
[d_status_child_num
]].reset( s
, s
->d_func_args
[f
][d_status_child_num
] );
1550 return getNextTerm( s
, depth
);
1552 Assert( d_status_child_num
+1==(int)d_children
.size() );
1553 if( s
->d_tg_alloc
[d_children
[d_status_child_num
]].getNextTerm( s
, depth
-1 ) ){
1554 d_status_child_num
++;
1555 return getNextTerm( s
, depth
);
1557 d_children
.pop_back();
1558 d_status_child_num
--;
1559 return getNextTerm( s
, depth
);
1563 }else if( d_status
==1 || d_status
==3 ){
1565 s
->removeVar( d_typ
);
1566 Assert( d_status_num
==(int)s
->d_var_id
[d_typ
] );
1567 //check if there is only one feasible equivalence class. if so, don't make pattern any more specific.
1568 //unsigned i = s->d_ccand_eqc[0].size()-1;
1569 //if( s->d_ccand_eqc[0][i].size()==1 && s->d_ccand_eqc[1][i].empty() ){
1570 // Trace("ajr-temp") << "Apply this!" << std::endl;
1572 // return getNextTerm( s, depth );
1578 return getNextTerm( s
, depth
);
1581 Assert( d_children
.empty() );
1582 Trace("sg-gen-tg-debug2") << "...remove from context " << this << std::endl
;
1583 s
->changeContext( false );
1584 Assert( d_id
==s
->d_tg_id
);
1589 void TermGenerator::resetMatching( ConjectureGenerator
* s
, TNode eqc
, unsigned mode
) {
1591 d_match_status_child_num
= 0;
1592 d_match_children
.clear();
1593 d_match_children_end
.clear();
1594 d_match_mode
= mode
;
1597 bool TermGenerator::getNextMatch( ConjectureGenerator
* s
, TNode eqc
, std::map
< TypeNode
, std::map
< unsigned, TNode
> >& subs
, std::map
< TNode
, bool >& rev_subs
) {
1598 if( Trace
.isOn("sg-gen-tg-match") ){
1599 Trace("sg-gen-tg-match") << "Matching ";
1600 debugPrint( s
, "sg-gen-tg-match", "sg-gen-tg-match" );
1601 Trace("sg-gen-tg-match") << " with eqc e" << s
->d_em
[eqc
] << "..." << std::endl
;
1602 Trace("sg-gen-tg-match") << " mstatus = " << d_match_status
;
1604 TNode f
= s
->getTgFunc( d_typ
, d_status_num
);
1605 Trace("sg-gen-tg-debug2") << ", f = " << f
;
1606 Trace("sg-gen-tg-debug2") << ", #args = " << s
->d_func_args
[f
].size();
1607 Trace("sg-gen-tg-debug2") << ", mchildNum = " << d_match_status_child_num
;
1608 Trace("sg-gen-tg-debug2") << ", #mchildren = " << d_match_children
.size();
1610 Trace("sg-gen-tg-debug2") << ", current substitution : {";
1611 for( std::map
< TypeNode
, std::map
< unsigned, TNode
> >::iterator itt
= subs
.begin(); itt
!= subs
.end(); ++itt
){
1612 for( std::map
< unsigned, TNode
>::iterator it
= itt
->second
.begin(); it
!= itt
->second
.end(); ++it
){
1613 Trace("sg-gen-tg-debug2") << " " << it
->first
<< " -> e" << s
->d_em
[it
->second
];
1616 Trace("sg-gen-tg-debug2") << " } " << std::endl
;
1620 if( d_match_status
==0 ){
1622 if( d_match_mode
>=2 ){
1624 if( !s
->isGroundEqc( eqc
) ){
1628 if( d_match_mode
%2==1 ){
1629 std::map
< TNode
, bool >::iterator it
= rev_subs
.find( eqc
);
1630 if( it
==rev_subs
.end() ){
1631 rev_subs
[eqc
] = true;
1636 Assert( subs
[d_typ
].find( d_status_num
)==subs
[d_typ
].end() );
1637 subs
[d_typ
][d_status_num
] = eqc
;
1641 subs
[d_typ
].erase( d_status_num
);
1642 if( d_match_mode
%2==1 ){
1643 rev_subs
.erase( eqc
);
1647 }else if( d_status
==2 ){
1648 if( d_match_status
==0 ){
1650 Assert( d_status_num
<(int)s
->getNumTgVars( d_typ
) );
1651 std::map
< unsigned, TNode
>::iterator it
= subs
[d_typ
].find( d_status_num
);
1652 Assert( it
!=subs
[d_typ
].end() );
1653 return it
->second
==eqc
;
1657 }else if( d_status
==5 ){
1658 //Assert( d_match_children.size()<=d_children.size() );
1659 //enumerating over f-applications in eqc
1660 if( d_match_status_child_num
<0 ){
1662 }else if( d_match_status
==0 ){
1663 //set up next binding
1664 if( d_match_status_child_num
==(int)d_match_children
.size() ){
1665 if( d_match_status_child_num
==0 ){
1667 TNode f
= s
->getTgFunc( d_typ
, d_status_num
);
1668 std::map
< TNode
, TermArgTrie
>::iterator it
= s
->getTermDatabase()->d_func_map_eqc_trie
[f
].d_data
.find( eqc
);
1669 if( it
!=s
->getTermDatabase()->d_func_map_eqc_trie
[f
].d_data
.end() ){
1670 d_match_children
.push_back( it
->second
.d_data
.begin() );
1671 d_match_children_end
.push_back( it
->second
.d_data
.end() );
1674 d_match_status_child_num
--;
1675 return getNextMatch( s
, eqc
, subs
, rev_subs
);
1678 d_match_children
.push_back( d_match_children
[d_match_status_child_num
-1]->second
.d_data
.begin() );
1679 d_match_children_end
.push_back( d_match_children
[d_match_status_child_num
-1]->second
.d_data
.end() );
1683 Assert( d_match_status_child_num
+1==(int)d_match_children
.size() );
1684 if( d_match_children
[d_match_status_child_num
]==d_match_children_end
[d_match_status_child_num
] ){
1685 //no more arguments to bind
1686 d_match_children
.pop_back();
1687 d_match_children_end
.pop_back();
1688 d_match_status_child_num
--;
1689 return getNextMatch( s
, eqc
, subs
, rev_subs
);
1691 if( d_match_status_child_num
==(int)d_children
.size() ){
1692 //successfully matched all children
1693 d_match_children
.pop_back();
1694 d_match_children_end
.pop_back();
1695 d_match_status_child_num
--;
1696 return true;//return d_match_children[d_match_status]!=d_match_children_end[d_match_status];
1699 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
);
1700 return getNextMatch( s
, eqc
, subs
, rev_subs
);
1704 Assert( d_match_status
==1 );
1705 Assert( d_match_status_child_num
+1==(int)d_match_children
.size() );
1706 Assert( d_match_children
[d_match_status_child_num
]!=d_match_children_end
[d_match_status_child_num
] );
1708 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
) ){
1709 d_match_status_child_num
++;
1710 return getNextMatch( s
, eqc
, subs
, rev_subs
);
1713 d_match_children
[d_match_status_child_num
]++;
1714 return getNextMatch( s
, eqc
, subs
, rev_subs
);
1722 unsigned TermGenerator::getDepth( ConjectureGenerator
* s
) {
1725 for( unsigned i
=0; i
<d_children
.size(); i
++ ){
1726 unsigned d
= s
->d_tg_alloc
[d_children
[i
]].getDepth( s
);
1737 unsigned TermGenerator::getGeneralizationDepth( ConjectureGenerator
* s
) {
1740 for( unsigned i
=0; i
<d_children
.size(); i
++ ){
1741 sum
+= s
->d_tg_alloc
[d_children
[i
]].getGeneralizationDepth( s
);
1744 }else if( d_status
==2 ){
1747 Assert( d_status
==1 );
1752 Node
TermGenerator::getTerm( ConjectureGenerator
* s
) {
1753 if( d_status
==1 || d_status
==2 ){
1754 Assert( !d_typ
.isNull() );
1755 return s
->getFreeVar( d_typ
, d_status_num
);
1756 }else if( d_status
==5 ){
1757 Node f
= s
->getTgFunc( d_typ
, d_status_num
);
1758 if( d_children
.size()==s
->d_func_args
[f
].size() ){
1759 std::vector
< Node
> children
;
1760 children
.push_back( f
);
1761 for( unsigned i
=0; i
<d_children
.size(); i
++ ){
1762 Node nc
= s
->d_tg_alloc
[d_children
[i
]].getTerm( s
);
1764 return Node::null();
1766 //Assert( nc.getType()==s->d_func_args[f][i] );
1767 children
.push_back( nc
);
1770 return NodeManager::currentNM()->mkNode( s
->d_func_kind
[f
], children
);
1775 return Node::null();
1778 void TermGenerator::debugPrint( ConjectureGenerator
* s
, const char * c
, const char * cd
) {
1779 Trace(cd
) << "[*" << d_id
<< "," << d_status
<< "]:";
1780 if( d_status
==1 || d_status
==2 ){
1781 Trace(c
) << s
->getFreeVar( d_typ
, d_status_num
);
1782 }else if( d_status
==5 ){
1783 TNode f
= s
->getTgFunc( d_typ
, d_status_num
);
1784 Trace(c
) << "(" << f
;
1785 for( unsigned i
=0; i
<d_children
.size(); i
++ ){
1787 s
->d_tg_alloc
[d_children
[i
]].debugPrint( s
, c
, cd
);
1789 if( d_children
.size()<s
->d_func_args
[f
].size() ){
1799 void SubstitutionIndex::addSubstitution( TNode eqc
, std::vector
< TNode
>& vars
, std::vector
< TNode
>& terms
, unsigned i
) {
1800 if( i
==vars
.size() ){
1803 Assert( d_var
.isNull() || d_var
==vars
[i
] );
1805 d_children
[terms
[i
]].addSubstitution( eqc
, vars
, terms
, i
+1 );
1809 bool SubstitutionIndex::notifySubstitutions( ConjectureGenerator
* s
, std::map
< TNode
, TNode
>& subs
, TNode rhs
, unsigned numVars
, unsigned i
) {
1811 Assert( d_children
.empty() );
1812 return s
->notifySubstitution( d_var
, subs
, rhs
);
1814 Assert( i
==0 || !d_children
.empty() );
1815 for( std::map
< TNode
, SubstitutionIndex
>::iterator it
= d_children
.begin(); it
!= d_children
.end(); ++it
){
1816 Trace("sg-cconj-debug2") << "Try " << d_var
<< " -> " << it
->first
<< " (" << i
<< "/" << numVars
<< ")" << std::endl
;
1817 subs
[d_var
] = it
->first
;
1818 if( !it
->second
.notifySubstitutions( s
, subs
, rhs
, numVars
, i
+1 ) ){
1827 void TheoremIndex::addTheorem( std::vector
< TNode
>& lhs_v
, std::vector
< unsigned >& lhs_arg
, TNode rhs
){
1828 if( lhs_v
.empty() ){
1829 if( std::find( d_terms
.begin(), d_terms
.end(), rhs
)==d_terms
.end() ){
1830 d_terms
.push_back( rhs
);
1833 unsigned index
= lhs_v
.size()-1;
1834 if( lhs_arg
[index
]==lhs_v
[index
].getNumChildren() ){
1837 addTheorem( lhs_v
, lhs_arg
, rhs
);
1840 addTheoremNode( lhs_v
[index
][lhs_arg
[index
]-1], lhs_v
, lhs_arg
, rhs
);
1845 void TheoremIndex::addTheoremNode( TNode curr
, std::vector
< TNode
>& lhs_v
, std::vector
< unsigned >& lhs_arg
, TNode rhs
){
1846 Trace("thm-db-debug") << "Adding conjecture for subterm " << curr
<< "..." << std::endl
;
1847 if( curr
.hasOperator() ){
1848 lhs_v
.push_back( curr
);
1849 lhs_arg
.push_back( 0 );
1850 d_children
[curr
.getOperator()].addTheorem( lhs_v
, lhs_arg
, rhs
);
1852 Assert( curr
.getKind()==kind::BOUND_VARIABLE
);
1853 Assert( d_var
.isNull() || d_var
==curr
);
1855 d_children
[curr
].addTheorem( lhs_v
, lhs_arg
, rhs
);
1859 void TheoremIndex::getEquivalentTerms( std::vector
< TNode
>& n_v
, std::vector
< unsigned >& n_arg
,
1860 std::map
< TNode
, TNode
>& smap
, std::vector
< TNode
>& vars
, std::vector
< TNode
>& subs
,
1861 std::vector
< Node
>& terms
) {
1862 Trace("thm-db-debug") << "Get equivalent terms " << n_v
.size() << " " << n_arg
.size() << std::endl
;
1864 Trace("thm-db-debug") << "Number of terms : " << d_terms
.size() << std::endl
;
1865 //apply substutitions to RHS's
1866 for( unsigned i
=0; i
<d_terms
.size(); i
++ ){
1867 Node n
= d_terms
[i
].substitute( vars
.begin(), vars
.end(), subs
.begin(), subs
.end() );
1868 terms
.push_back( n
);
1871 unsigned index
= n_v
.size()-1;
1872 if( n_arg
[index
]==n_v
[index
].getNumChildren() ){
1875 getEquivalentTerms( n_v
, n_arg
, smap
, vars
, subs
, terms
);
1878 getEquivalentTermsNode( n_v
[index
][n_arg
[index
]-1], n_v
, n_arg
, smap
, vars
, subs
, terms
);
1883 void TheoremIndex::getEquivalentTermsNode( Node curr
, std::vector
< TNode
>& n_v
, std::vector
< unsigned >& n_arg
,
1884 std::map
< TNode
, TNode
>& smap
, std::vector
< TNode
>& vars
, std::vector
< TNode
>& subs
,
1885 std::vector
< Node
>& terms
) {
1886 Trace("thm-db-debug") << "Get equivalent based on subterm " << curr
<< "..." << std::endl
;
1887 if( curr
.hasOperator() ){
1888 Trace("thm-db-debug") << "Check based on operator..." << std::endl
;
1889 std::map
< TNode
, TheoremIndex
>::iterator it
= d_children
.find( curr
.getOperator() );
1890 if( it
!=d_children
.end() ){
1891 n_v
.push_back( curr
);
1892 n_arg
.push_back( 0 );
1893 it
->second
.getEquivalentTerms( n_v
, n_arg
, smap
, vars
, subs
, terms
);
1895 Trace("thm-db-debug") << "...done check based on operator" << std::endl
;
1897 if( !d_var
.isNull() ){
1898 Trace("thm-db-debug") << "Check for substitution with " << d_var
<< "..." << std::endl
;
1899 if( curr
.getType()==d_var
.getType() ){
1900 //add to substitution if possible
1901 bool success
= false;
1902 std::map
< TNode
, TNode
>::iterator it
= smap
.find( d_var
);
1903 if( it
==smap
.end() ){
1905 vars
.push_back( d_var
);
1906 subs
.push_back( curr
);
1908 }else if( it
->second
==curr
){
1911 //also check modulo equality (in universal equality engine)
1913 Trace("thm-db-debug") << "...check for substitution with " << d_var
<< ", success = " << success
<< "." << std::endl
;
1915 d_children
[d_var
].getEquivalentTerms( n_v
, n_arg
, smap
, vars
, subs
, terms
);
1921 void TheoremIndex::debugPrint( const char * c
, unsigned ind
) {
1922 for( std::map
< TNode
, TheoremIndex
>::iterator it
= d_children
.begin(); it
!= d_children
.end(); ++it
){
1923 for( unsigned i
=0; i
<ind
; i
++ ){ Trace(c
) << " "; }
1924 Trace(c
) << it
->first
<< std::endl
;
1925 it
->second
.debugPrint( c
, ind
+1 );
1927 if( !d_terms
.empty() ){
1928 for( unsigned i
=0; i
<ind
; i
++ ){ Trace(c
) << " "; }
1930 for( unsigned i
=0; i
<d_terms
.size(); i
++ ){
1931 Trace(c
) << " " << d_terms
[i
];
1933 Trace(c
) << " }" << std::endl
;
1935 //if( !d_var.isNull() ){
1936 // for( unsigned i=0; i<ind; i++ ){ Trace(c) << " "; }
1937 // Trace(c) << "var:" << d_var << std::endl;
1941 bool ConjectureGenerator::optReqDistinctVarPatterns() { return false; }
1942 bool ConjectureGenerator::optFilterFalsification() { return true; }
1943 bool ConjectureGenerator::optFilterConfirmation() { return true; }
1944 bool ConjectureGenerator::optFilterConfirmationDomain() { return true; }
1945 bool ConjectureGenerator::optFilterConfirmationOnlyGround() { return true; }//false; }
1946 bool ConjectureGenerator::optFilterConfirmationNonCanonical() { return false; }//true; }
1947 unsigned ConjectureGenerator::optFullCheckFrequency() { return 1; }
1948 unsigned ConjectureGenerator::optFullCheckConjectures() { return 1; }