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
;
31 struct sortConjectureScore
{
32 std::vector
< int > d_scores
;
33 bool operator() (unsigned i
, unsigned j
) { return d_scores
[i
]>d_scores
[j
]; }
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
);
45 d_child
[s
->getTermDatabase()->d_arg_reps
[n
][index
]].addTerm( s
, n
, index
+1 );
49 Node
OpArgIndex::getGroundTerm( ConjectureGenerator
* s
, std::vector
< TNode
>& args
) {
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
);
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
);
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
);
82 ConjectureGenerator::ConjectureGenerator( QuantifiersEngine
* qe
, context::Context
* c
) : QuantifiersModule( qe
),
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
);
92 void ConjectureGenerator::eqNotifyNewClass( TNode t
){
93 Trace("thm-ee-debug") << "UEE : new equivalence class " << t
<< std::endl
;
94 d_upendingAdds
.push_back( t
);
97 void ConjectureGenerator::eqNotifyPreMerge(TNode t1
, TNode t2
) {
98 //get maintained representatives
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();
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();
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
;
115 if( isUniversalLessThan( rt2
, rt1
) ){
117 if( it1
==d_eqc_info
.end() ){
118 ei
= getOrMakeEqcInfo( t1
, true );
126 void ConjectureGenerator::eqNotifyPostMerge(TNode t1
, TNode t2
) {
130 void ConjectureGenerator::eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
) {
131 Trace("thm-ee-debug") << "UEE : disequality holds : " << t1
<< " != " << t2
<< std::endl
;
136 ConjectureGenerator::EqcInfo::EqcInfo( context::Context
* c
) : d_rep( c
, Node::null() ){
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
;
146 EqcInfo
* ei
= new EqcInfo( d_quantEngine
->getSatContext() );
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
] );
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() );
172 if( d_pattern_is_relevant
[rt1
] && !d_pattern_is_relevant
[rt2
] ){
173 Trace("thm-ee-debug") << "UEE : LT due to relevant." << std::endl
;
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
;
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
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
);
194 bool ConjectureGenerator::isReportedCanon( TNode n
) {
195 return std::find( d_ue_canon
.begin(), d_ue_canon
.end(), n
)==d_ue_canon
.end();
198 void ConjectureGenerator::markReportedCanon( TNode n
) {
199 if( !isReportedCanon( n
) ){
200 d_ue_canon
.push_back( n
);
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
) );
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 );
212 TNode
ConjectureGenerator::getUniversalRepresentative( TNode n
, bool 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
++ ){
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
);
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() ){
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
] );
257 d_uequalityEngine
.assertEquality( t
.eqNode( eq_terms
[i
] ), true, exp
);
261 Trace("thm-ee-add") << "UEE : No equivalent terms." << std::endl
;
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();
281 eq::EqualityEngine
* ConjectureGenerator::getEqualityEngine() {
282 return d_quantEngine
->getTheoryEngine()->getMasterEqualityEngine();
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
) );
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 );
295 TNode
ConjectureGenerator::getRepresentative( TNode n
) {
296 eq::EqualityEngine
* ee
= getEqualityEngine();
297 if( ee
->hasTerm( n
) ){
298 return ee
->getRepresentative( n
);
304 TermDb
* ConjectureGenerator::getTermDatabase() {
305 return d_quantEngine
->getTermDatabase();
308 Node
ConjectureGenerator::getFreeVar( TypeNode tn
, unsigned i
) {
309 Assert( !tn
.isNull() );
310 while( d_free_var
[tn
].size()<=i
){
311 std::stringstream oss
;
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
);
319 return d_free_var
[tn
][i
];
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();
331 unsigned vn
= var_count
[tn
];
333 subs
[n
] = getFreeVar( tn
, vn
);
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
) ){
346 children
.push_back( op
);
351 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
352 Node cn
= getCanonicalTerm( n
[i
], var_count
, subs
);
356 children
.push_back( cn
);
359 return NodeManager::currentNM()->mkNode( n
.getKind(), children
);
363 bool ConjectureGenerator::isHandledTerm( TNode n
){
364 return !n
.getAttribute(NoMatchAttribute()) && inst::Trigger::isAtomicTrigger( n
) && ( n
.getKind()!=APPLY_UF
|| n
.getOperator().getKind()!=SKOLEM
);
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();
372 bool ConjectureGenerator::isGroundEqc( TNode r
) {
373 return d_ground_eqc_map
.find( r
)!=d_ground_eqc_map
.end();
376 bool ConjectureGenerator::isGroundTerm( TNode n
) {
377 return std::find( d_ground_terms
.begin(), d_ground_terms
.end(), n
)!=d_ground_terms
.end();
380 bool ConjectureGenerator::needsCheck( Theory::Effort e
) {
381 return e
==Theory::EFFORT_FULL
;
384 void ConjectureGenerator::reset_round( Theory::Effort e
) {
388 void ConjectureGenerator::check( Theory::Effort e
, unsigned quant_e
) {
389 if( quant_e
==QuantifiersEngine::QEFFORT_STANDARD
){
391 if( d_fullEffortCount
%optFullCheckFrequency()==0 ){
394 if( Trace
.isOn("sg-engine") ){
395 clSet
= double(clock())/double(CLOCKS_PER_SEC
);
396 Trace("sg-engine") << "---Instantiation Engine Round, effort = " << e
<< "---" << std::endl
;
398 eq::EqualityEngine
* ee
= getEqualityEngine();
400 Trace("sg-proc") << "Get eq classes..." << std::endl
;
401 d_op_arg_index
.clear();
402 d_ground_eqc_map
.clear();
403 d_bool_eqc
[0] = Node::null();
404 d_bool_eqc
[1] = Node::null();
405 std::vector
< TNode
> eqcs
;
407 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( ee
);
408 while( !eqcs_i
.isFinished() ){
411 if( r
.getType().isBoolean() ){
412 if( areEqual( r
, getTermDatabase()->d_true
) ){
413 d_ground_eqc_map
[r
] = getTermDatabase()->d_true
;
415 }else if( areEqual( r
, getTermDatabase()->d_false
) ){
416 d_ground_eqc_map
[r
] = getTermDatabase()->d_false
;
420 d_em
[r
] = eqcs
.size();
421 eq::EqClassIterator ieqc_i
= eq::EqClassIterator( r
, ee
);
422 while( !ieqc_i
.isFinished() ){
424 if( isHandledTerm( n
) ){
425 d_op_arg_index
[r
].addTerm( this, n
);
431 Assert( !d_bool_eqc
[0].isNull() );
432 Assert( !d_bool_eqc
[1].isNull() );
433 d_urelevant_terms
.clear();
434 Trace("sg-proc") << "...done get eq classes" << std::endl
;
436 Trace("sg-proc") << "Determine ground EQC..." << std::endl
;
440 for( unsigned i
=0; i
<eqcs
.size(); i
++ ){
442 if( d_ground_eqc_map
.find( r
)==d_ground_eqc_map
.end() ){
443 std::vector
< TNode
> args
;
444 Trace("sg-pat-debug") << "******* Get ground term for " << r
<< std::endl
;
446 if( getTermDatabase()->isInductionTerm( r
) ){
447 n
= d_op_arg_index
[r
].getGroundTerm( this, args
);
452 Trace("sg-pat") << "Ground term for eqc " << r
<< " : " << std::endl
;
453 Trace("sg-pat") << " " << n
<< std::endl
;
454 d_ground_eqc_map
[r
] = n
;
457 Trace("sg-pat-debug") << "...could not find ground term." << std::endl
;
462 //also get ground terms
463 d_ground_terms
.clear();
464 for( unsigned i
=0; i
<eqcs
.size(); i
++ ){
466 d_op_arg_index
[r
].getGroundTerms( this, d_ground_terms
);
468 Trace("sg-proc") << "...done determine ground EQC" << std::endl
;
471 if( Trace
.isOn("sg-gen-eqc") ){
472 for( unsigned i
=0; i
<eqcs
.size(); i
++ ){
475 bool firstTime
= true;
476 bool isFalse
= areEqual( r
, getTermDatabase()->d_false
);
477 eq::EqClassIterator eqc_i
= eq::EqClassIterator( r
, ee
);
478 while( !eqc_i
.isFinished() ){
480 if( !n
.getAttribute(NoMatchAttribute()) && ( n
.getKind()!=EQUAL
|| isFalse
) ){
482 Trace("sg-gen-eqc") << "e" << d_em
[r
] << " : { " << std::endl
;
485 if( n
.hasOperator() ){
486 Trace("sg-gen-eqc") << " (" << n
.getOperator();
487 getTermDatabase()->computeArgReps( n
);
488 for( unsigned i
=0; i
<getTermDatabase()->d_arg_reps
[n
].size(); i
++ ){
489 Trace("sg-gen-eqc") << " e" << d_em
[getTermDatabase()->d_arg_reps
[n
][i
]];
491 Trace("sg-gen-eqc") << ") :: " << n
<< std::endl
;
493 Trace("sg-gen-eqc") << " " << n
<< std::endl
;
499 Trace("sg-gen-eqc") << "}" << std::endl
;
500 //print out ground term
501 std::map
< TNode
, Node
>::iterator it
= d_ground_eqc_map
.find( r
);
502 if( it
!=d_ground_eqc_map
.end() ){
503 Trace("sg-gen-eqc") << "- Ground term : " << it
->second
<< std::endl
;
509 Trace("sg-proc") << "Compute relevant eqc..." << std::endl
;
510 d_tge
.d_relevant_eqc
[0].clear();
511 d_tge
.d_relevant_eqc
[1].clear();
512 for( unsigned i
=0; i
<eqcs
.size(); i
++ ){
514 std::map
< TNode
, Node
>::iterator it
= d_ground_eqc_map
.find( r
);
516 if( it
==d_ground_eqc_map
.end() ){
519 //based on unproven conjectures? TODO
520 d_tge
.d_relevant_eqc
[index
].push_back( r
);
522 Trace("sg-gen-tg-debug") << "Initial relevant eqc : ";
523 for( unsigned i
=0; i
<d_tge
.d_relevant_eqc
[0].size(); i
++ ){
524 Trace("sg-gen-tg-debug") << "e" << d_em
[d_tge
.d_relevant_eqc
[0][i
]] << " ";
526 Trace("sg-gen-tg-debug") << std::endl
;
527 Trace("sg-proc") << "...done compute relevant eqc" << std::endl
;
530 Trace("sg-proc") << "Collect signature information..." << std::endl
;
531 d_tge
.collectSignatureInformation();
532 Trace("sg-proc") << "...done collect signature information" << std::endl
;
536 Trace("sg-proc") << "Build theorem index..." << std::endl
;
539 std::vector
< Node
> provenConj
;
540 quantifiers::FirstOrderModel
* m
= d_quantEngine
->getModel();
541 for( int i
=0; i
<m
->getNumAssertedQuantifiers(); i
++ ){
542 Node q
= m
->getAssertedQuantifier( i
);
543 Trace("thm-db-debug") << "Is " << q
<< " a relevant theorem?" << std::endl
;
545 if( q
[1].getKind()==EQUAL
){
546 bool isSubsume
= false;
548 for( unsigned r
=0; r
<2; r
++ ){
549 TNode nl
= q
[1][r
==0 ? 0 : 1];
550 TNode nr
= q
[1][r
==0 ? 1 : 0];
551 Node eq
= nl
.eqNode( nr
);
552 if( r
==1 || std::find( d_conjectures
.begin(), d_conjectures
.end(), q
)==d_conjectures
.end() ){
553 //must make it canonical
554 std::map
< TypeNode
, unsigned > var_count
;
555 std::map
< TNode
, TNode
> subs
;
556 Trace("sg-proc-debug") << "get canonical " << eq
<< std::endl
;
557 eq
= getCanonicalTerm( eq
, var_count
, subs
);
561 inEe
= d_ee_conjectures
.find( q
[1] )!=d_ee_conjectures
.end();
563 //add to universal equality engine
564 Node nl
= getUniversalRepresentative( eq
[0], true );
565 Node nr
= getUniversalRepresentative( eq
[1], true );
566 if( areUniversalEqual( nl
, nr
) ){
568 //set inactive (will be ignored by other modules)
569 d_quantEngine
->getModel()->setQuantifierActive( q
, false );
572 d_ee_conjectures
[q
[1]] = true;
573 d_uequalityEngine
.assertEquality( nl
.eqNode( nr
), true, exp
);
576 Trace("sg-conjecture") << "*** CONJECTURE : currently proven" << (isSubsume
? " and subsumed" : "");
577 Trace("sg-conjecture") << " : " << q
[1] << std::endl
;
578 provenConj
.push_back( q
);
581 Trace("thm-db-debug") << "Adding theorem to database " << eq
[0] << " == " << eq
[1] << std::endl
;
582 d_thm_index
.addTheorem( eq
[0], eq
[1] );
592 //examine status of other conjectures
593 for( unsigned i
=0; i
<d_conjectures
.size(); i
++ ){
594 Node q
= d_conjectures
[i
];
595 if( std::find( provenConj
.begin(), provenConj
.end(), q
)==provenConj
.end() ){
596 //check each skolem variable
597 bool disproven
= true;
598 //std::vector< Node > sk;
599 //getTermDatabase()->getSkolemConstants( q, sk, true );
600 Trace("sg-conjecture") << " CONJECTURE : ";
601 std::vector
< Node
> ce
;
602 for( unsigned j
=0; j
<getTermDatabase()->d_skolem_constants
[q
].size(); j
++ ){
603 TNode k
= getTermDatabase()->d_skolem_constants
[q
][j
];
604 TNode rk
= getRepresentative( k
);
605 std::map
< TNode
, Node
>::iterator git
= d_ground_eqc_map
.find( rk
);
606 //check if it is a ground term
607 if( git
==d_ground_eqc_map
.end() ){
608 Trace("sg-conjecture") << "ACTIVE : " << q
;
609 if( Trace
.isOn("sg-gen-eqc") ){
610 Trace("sg-conjecture") << " { ";
611 for( unsigned k
=0; k
<getTermDatabase()->d_skolem_constants
[q
].size(); k
++ ){ Trace("sg-conjecture") << getTermDatabase()->d_skolem_constants
[q
][k
] << ( j
==k
? "*" : "" ) << " "; }
612 Trace("sg-conjecture") << "}";
614 Trace("sg-conjecture") << std::endl
;
618 ce
.push_back( git
->second
);
622 Trace("sg-conjecture") << "disproven : " << q
<< " : ";
623 for( unsigned i
=0; i
<ce
.size(); i
++ ){
624 Trace("sg-conjecture") << q
[0][i
] << " -> " << ce
[i
] << " ";
626 Trace("sg-conjecture") << std::endl
;
630 Trace("thm-db") << "Theorem database is : " << std::endl
;
631 d_thm_index
.debugPrint( "thm-db" );
632 Trace("thm-db") << std::endl
;
633 Trace("sg-proc") << "...done build theorem index" << std::endl
;
638 d_pattern_var_id
.clear();
639 d_pattern_var_duplicate
.clear();
640 d_pattern_is_normal
.clear();
641 d_pattern_is_relevant
.clear();
642 d_pattern_fun_id
.clear();
643 d_pattern_fun_sum
.clear();
644 d_rel_patterns
.clear();
645 d_rel_pattern_var_sum
.clear();
646 d_rel_pattern_typ_index
.clear();
647 d_rel_pattern_subs_index
.clear();
649 unsigned rel_term_count
= 0;
650 std::map
< TypeNode
, unsigned > rt_var_max
;
651 std::vector
< TypeNode
> rt_types
;
652 std::map
< TypeNode
, std::map
< int, std::vector
< Node
> > > conj_lhs
;
653 unsigned addedLemmas
= 0;
654 for( unsigned depth
=1; depth
<=3; depth
++ ){
655 Trace("sg-proc") << "Generate relevant LHS at depth " << depth
<< "..." << std::endl
;
656 Trace("sg-rel-term") << "Relevant terms of depth " << depth
<< " : " << std::endl
;
658 d_tge
.d_var_id
.clear();
659 d_tge
.d_var_limit
.clear();
660 d_tge
.reset( depth
, true, TypeNode::null() );
661 while( d_tge
.getNextTerm() ){
663 Node nn
= d_tge
.getTerm();
664 if( !options::conjectureFilterCanonical() || considerTermCanon( nn
, true ) ){
666 Trace("sg-rel-term") << "*** Relevant term : ";
667 d_tge
.debugPrint( "sg-rel-term", "sg-rel-term-debug2" );
668 Trace("sg-rel-term") << std::endl
;
670 for( unsigned r
=0; r
<2; r
++ ){
671 Trace("sg-rel-term-debug") << "...from equivalence classes (" << r
<< ") : ";
672 int index
= d_tge
.d_ccand_eqc
[r
].size()-1;
673 for( unsigned j
=0; j
<d_tge
.d_ccand_eqc
[r
][index
].size(); j
++ ){
674 Trace("sg-rel-term-debug") << "e" << d_em
[d_tge
.d_ccand_eqc
[r
][index
][j
]] << " ";
676 Trace("sg-rel-term-debug") << std::endl
;
678 TypeNode tnn
= nn
.getType();
679 Trace("sg-gen-tg-debug") << "...term is " << nn
<< std::endl
;
680 conj_lhs
[tnn
][depth
].push_back( nn
);
682 //add information about pattern
683 Trace("sg-gen-tg-debug") << "Collect pattern information..." << std::endl
;
684 Assert( std::find( d_rel_patterns
[tnn
].begin(), d_rel_patterns
[tnn
].end(), nn
)==d_rel_patterns
[tnn
].end() );
685 d_rel_patterns
[tnn
].push_back( nn
);
686 //build information concerning the variables in this pattern
688 std::map
< TypeNode
, unsigned > typ_to_subs_index
;
689 std::vector
< TNode
> gsubs_vars
;
690 for( std::map
< TypeNode
, unsigned >::iterator it
= d_tge
.d_var_id
.begin(); it
!= d_tge
.d_var_id
.end(); ++it
){
692 typ_to_subs_index
[it
->first
] = sum
;
694 for( unsigned i
=0; i
<it
->second
; i
++ ){
695 gsubs_vars
.push_back( getFreeVar( it
->first
, i
) );
699 d_rel_pattern_var_sum
[nn
] = sum
;
700 //register the pattern
701 registerPattern( nn
, tnn
);
702 Assert( d_pattern_is_normal
[nn
] );
703 Trace("sg-gen-tg-debug") << "...done collect pattern information" << std::endl
;
705 //record information about types
706 Trace("sg-gen-tg-debug") << "Collect type information..." << std::endl
;
707 PatternTypIndex
* pti
= &d_rel_pattern_typ_index
;
708 for( std::map
< TypeNode
, unsigned >::iterator it
= d_tge
.d_var_id
.begin(); it
!= d_tge
.d_var_id
.end(); ++it
){
709 pti
= &pti
->d_children
[it
->first
][it
->second
];
711 if( rt_var_max
.find( it
->first
)==rt_var_max
.end() || it
->second
>rt_var_max
[it
->first
] ){
712 rt_var_max
[it
->first
] = it
->second
;
715 if( std::find( rt_types
.begin(), rt_types
.end(), tnn
)==rt_types
.end() ){
716 rt_types
.push_back( tnn
);
718 pti
->d_terms
.push_back( nn
);
719 Trace("sg-gen-tg-debug") << "...done collect type information" << std::endl
;
721 Trace("sg-gen-tg-debug") << "Build substitutions for ground EQC..." << std::endl
;
722 std::vector
< TNode
> gsubs_terms
;
723 gsubs_terms
.resize( gsubs_vars
.size() );
724 int index
= d_tge
.d_ccand_eqc
[1].size()-1;
725 for( unsigned j
=0; j
<d_tge
.d_ccand_eqc
[1][index
].size(); j
++ ){
726 TNode r
= d_tge
.d_ccand_eqc
[1][index
][j
];
727 Trace("sg-rel-term-debug") << " Matches for e" << d_em
[r
] << ", which is ground term " << d_ground_eqc_map
[r
] << ":" << std::endl
;
728 std::map
< TypeNode
, std::map
< unsigned, TNode
> > subs
;
729 std::map
< TNode
, bool > rev_subs
;
730 //only get ground terms
732 d_tge
.resetMatching( r
, mode
);
733 while( d_tge
.getNextMatch( r
, subs
, rev_subs
) ){
734 //we will be building substitutions
735 bool firstTime
= true;
736 for( std::map
< TypeNode
, std::map
< unsigned, TNode
> >::iterator it
= subs
.begin(); it
!= subs
.end(); ++it
){
737 unsigned tindex
= typ_to_subs_index
[it
->first
];
738 for( std::map
< unsigned, TNode
>::iterator it2
= it
->second
.begin(); it2
!= it
->second
.end(); ++it2
){
740 Trace("sg-rel-term-debug") << ", ";
743 Trace("sg-rel-term-debug") << " ";
745 Trace("sg-rel-term-debug") << it
->first
<< ":x" << it2
->first
<< " -> " << it2
->second
;
746 Assert( tindex
+it2
->first
<gsubs_terms
.size() );
747 gsubs_terms
[tindex
+it2
->first
] = it2
->second
;
750 Trace("sg-rel-term-debug") << std::endl
;
751 d_rel_pattern_subs_index
[nn
].addSubstitution( r
, gsubs_vars
, gsubs_terms
);
754 Trace("sg-gen-tg-debug") << "...done build substitutions for ground EQC" << std::endl
;
756 Trace("sg-gen-tg-debug") << "> not canonical : " << nn
<< std::endl
;
759 Trace("sg-proc") << "...done generate terms at depth " << depth
<< std::endl
;
760 Trace("sg-stats") << "--------> Total LHS of depth " << depth
<< " : " << rel_term_count
<< std::endl
;
761 //Trace("conjecture-count") << "Total LHS of depth " << depth << " : " << conj_lhs[depth].size() << std::endl;
764 for( unsigned i=0; i<rt_types.size(); i++ ){
765 Trace("sg-term-enum") << "Term enumeration for " << rt_types[i] << " : " << std::endl;
766 Trace("sg-term-enum") << "Ground term : " << rt_types[i].mkGroundTerm() << std::endl;
767 for( unsigned j=0; j<10; j++ ){
768 Trace("sg-term-enum") << " " << getEnumerateTerm( rt_types[i], j ) << std::endl;
773 //consider types from relevant terms
774 for( unsigned rdepth
=0; rdepth
<=depth
; rdepth
++ ){
776 d_tge
.d_var_id
.clear();
777 d_tge
.d_var_limit
.clear();
778 for( std::map
< TypeNode
, unsigned >::iterator it
= rt_var_max
.begin(); it
!= rt_var_max
.end(); ++it
){
779 d_tge
.d_var_id
[ it
->first
] = it
->second
;
780 d_tge
.d_var_limit
[ it
->first
] = it
->second
;
782 std::random_shuffle( rt_types
.begin(), rt_types
.end() );
783 std::map
< TypeNode
, std::vector
< Node
> > conj_rhs
;
784 for( unsigned i
=0; i
<rt_types
.size(); i
++ ){
786 Trace("sg-proc") << "Generate relevant RHS terms of type " << rt_types
[i
] << " at depth " << rdepth
<< "..." << std::endl
;
787 d_tge
.reset( rdepth
, false, rt_types
[i
] );
789 while( d_tge
.getNextTerm() ){
790 Node rhs
= d_tge
.getTerm();
791 if( considerTermCanon( rhs
, false ) ){
792 Trace("sg-rel-prop") << "Relevant RHS : " << rhs
<< std::endl
;
794 Assert( rhs
.getType()==rt_types
[i
] );
795 registerPattern( rhs
, rt_types
[i
] );
797 //consider against all LHS at depth
798 for( unsigned j
=0; j
<conj_lhs
[rt_types
[i
]][depth
].size(); j
++ ){
799 processCandidateConjecture( conj_lhs
[rt_types
[i
]][depth
][j
], rhs
, depth
, rdepth
);
802 conj_rhs
[rt_types
[i
]].push_back( rhs
);
807 flushWaitingConjectures( addedLemmas
, depth
, rdepth
);
808 //consider against all LHS up to depth
810 for( unsigned lhs_depth
= 1; lhs_depth
<=depth
; lhs_depth
++ ){
811 if( (int)addedLemmas
<options::conjectureGenPerRound() ){
812 Trace("sg-proc") << "Consider conjectures at depth (" << lhs_depth
<< ", " << rdepth
<< ")..." << std::endl
;
813 for( std::map
< TypeNode
, std::vector
< Node
> >::iterator it
= conj_rhs
.begin(); it
!= conj_rhs
.end(); ++it
){
814 for( unsigned j
=0; j
<it
->second
.size(); j
++ ){
815 for( unsigned k
=0; k
<conj_lhs
[it
->first
][lhs_depth
].size(); k
++ ){
816 processCandidateConjecture( conj_lhs
[it
->first
][lhs_depth
][k
], it
->second
[j
], lhs_depth
, rdepth
);
820 flushWaitingConjectures( addedLemmas
, lhs_depth
, depth
);
824 if( (int)addedLemmas
>=options::conjectureGenPerRound() ){
828 if( (int)addedLemmas
>=options::conjectureGenPerRound() ){
833 if( Trace
.isOn("thm-ee") ){
834 Trace("thm-ee") << "Universal equality engine is : " << std::endl
;
835 eq::EqClassesIterator ueqcs_i
= eq::EqClassesIterator( &d_uequalityEngine
);
836 while( !ueqcs_i
.isFinished() ){
837 TNode r
= (*ueqcs_i
);
838 bool firstTime
= true;
839 TNode rr
= getUniversalRepresentative( r
);
840 Trace("thm-ee") << " " << rr
;
841 Trace("thm-ee") << " : { ";
842 eq::EqClassIterator ueqc_i
= eq::EqClassIterator( r
, &d_uequalityEngine
);
843 while( !ueqc_i
.isFinished() ){
847 Trace("thm-ee") << std::endl
;
850 Trace("thm-ee") << " " << n
<< std::endl
;
854 if( !firstTime
){ Trace("thm-ee") << " "; }
855 Trace("thm-ee") << "}" << std::endl
;
858 Trace("thm-ee") << std::endl
;
860 if( Trace
.isOn("sg-engine") ){
861 double clSet2
= double(clock())/double(CLOCKS_PER_SEC
);
862 Trace("sg-engine") << "Finished conjecture generator, time = " << (clSet2
-clSet
) << std::endl
;
868 unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas
, int ldepth
, int rdepth
) {
869 if( !d_waiting_conjectures_lhs
.empty() ){
870 Trace("sg-proc") << "Generated " << d_waiting_conjectures_lhs
.size() << " conjectures at depth " << ldepth
<< "/" << rdepth
<< "." << std::endl
;
871 if( !optStatsOnly() && (int)addedLemmas
<options::conjectureGenPerRound() ){
872 std::vector
< unsigned > indices
;
873 for( unsigned i
=0; i
<d_waiting_conjectures_lhs
.size(); i
++ ){
874 indices
.push_back( i
);
878 //sort them based on score
879 sortConjectureScore scs
;
880 scs
.d_scores
.insert( scs
.d_scores
.begin(), d_waiting_conjectures_score
.begin(), d_waiting_conjectures_score
.end() );
881 std::sort( indices
.begin(), indices
.end(), scs
);
883 if( doSort
&& d_waiting_conjectures_score
[indices
[0]]<optFilterScoreThreshold() ){
884 //do splitting on demand (TODO)
887 for( unsigned i
=0; i
<indices
.size(); i
++ ){
888 //if( d_waiting_conjectures_score[indices[i]]<optFilterScoreThreshold() ){
889 if( d_waiting_conjectures_score
[indices
[i
]]>=optFilterScoreThreshold() ){
890 //we have determined a relevant subgoal
891 Node lhs
= d_waiting_conjectures_lhs
[indices
[i
]];
892 Node rhs
= d_waiting_conjectures_rhs
[indices
[i
]];
893 if( options::conjectureFilterCanonical() && ( getUniversalRepresentative( lhs
)!=lhs
|| getUniversalRepresentative( rhs
)!=rhs
) ){
896 Trace("sg-engine") << "*** Consider conjecture : " << lhs
<< " == " << rhs
<< std::endl
;
897 Trace("sg-engine-debug") << " score : " << d_waiting_conjectures_score
[indices
[i
]] << std::endl
;
898 std::vector
< Node
> bvs
;
899 for( std::map
< TypeNode
, unsigned >::iterator it
= d_pattern_var_id
[lhs
].begin(); it
!= d_pattern_var_id
[lhs
].end(); ++it
){
900 for( unsigned i
=0; i
<=it
->second
; i
++ ){
901 bvs
.push_back( getFreeVar( it
->first
, i
) );
906 Node bvl
= NodeManager::currentNM()->mkNode( BOUND_VAR_LIST
, bvs
);
907 rsg
= NodeManager::currentNM()->mkNode( FORALL
, bvl
, lhs
.eqNode( rhs
) );
909 rsg
= lhs
.eqNode( rhs
);
911 rsg
= Rewriter::rewrite( rsg
);
912 d_conjectures
.push_back( rsg
);
913 d_eq_conjectures
[lhs
].push_back( rhs
);
914 d_eq_conjectures
[rhs
].push_back( lhs
);
916 Node lem
= NodeManager::currentNM()->mkNode( OR
, rsg
.negate(), rsg
);
917 d_quantEngine
->addLemma( lem
, false );
918 d_quantEngine
->addRequirePhase( rsg
, false );
920 if( (int)addedLemmas
>=options::conjectureGenPerRound() ){
931 Trace("sg-proc") << "...have now added " << addedLemmas
<< " conjecture lemmas." << std::endl
;
933 d_waiting_conjectures_lhs
.clear();
934 d_waiting_conjectures_rhs
.clear();
935 d_waiting_conjectures_score
.clear();
936 d_waiting_conjectures
.clear();
941 void ConjectureGenerator::registerQuantifier( Node q
) {
945 void ConjectureGenerator::assertNode( Node n
) {
949 bool ConjectureGenerator::considerTermCanon( Node ln
, bool genRelevant
){
951 //do not consider if it is non-canonical, and either:
952 // (1) we are not generating relevant terms, or
953 // (2) its canonical form is a generalization.
954 TNode lnr
= getUniversalRepresentative( ln
, true );
956 markReportedCanon( ln
);
957 }else if( !genRelevant
|| isGeneralization( lnr
, ln
) ){
958 Trace("sg-gen-consider-term") << "Do not consider term, " << ln
<< " is not canonical representation (which is " << lnr
<< ")." << std::endl
;
962 Trace("sg-gen-tg-debug") << "Will consider term canon " << ln
<< std::endl
;
963 Trace("sg-gen-consider-term-debug") << std::endl
;
967 unsigned ConjectureGenerator::collectFunctions( TNode opat
, TNode pat
, std::map
< TNode
, unsigned >& funcs
,
968 std::map
< TypeNode
, unsigned >& mnvn
, std::map
< TypeNode
, unsigned >& mxvn
){
969 if( pat
.hasOperator() ){
970 funcs
[pat
.getOperator()]++;
971 if( !d_tge
.isRelevantFunc( pat
.getOperator() ) ){
972 d_pattern_is_relevant
[opat
] = false;
975 for( unsigned i
=0; i
<pat
.getNumChildren(); i
++ ){
976 sum
+= collectFunctions( opat
, pat
[i
], funcs
, mnvn
, mxvn
);
980 Assert( pat
.getNumChildren()==0 );
983 if( pat
.getKind()==BOUND_VARIABLE
){
986 d_pattern_var_duplicate
[opat
]++;
989 TypeNode tn
= pat
.getType();
990 unsigned vn
= d_free_var_num
[pat
];
991 std::map
< TypeNode
, unsigned >::iterator it
= mnvn
.find( tn
);
992 if( it
!=mnvn
.end() ){
994 d_pattern_is_normal
[opat
] = false;
996 }else if( vn
>mxvn
[tn
] ){
997 if( vn
!=mxvn
[tn
]+1 ){
998 d_pattern_is_normal
[opat
] = false;
1003 //first variable of this type
1009 d_pattern_is_relevant
[opat
] = false;
1015 void ConjectureGenerator::registerPattern( Node pat
, TypeNode tpat
) {
1016 if( std::find( d_patterns
[tpat
].begin(), d_patterns
[tpat
].end(), pat
)==d_patterns
[tpat
].end() ){
1017 d_patterns
[TypeNode::null()].push_back( pat
);
1018 d_patterns
[tpat
].push_back( pat
);
1020 Assert( d_pattern_fun_id
.find( pat
)==d_pattern_fun_id
.end() );
1021 Assert( d_pattern_var_id
.find( pat
)==d_pattern_var_id
.end() );
1024 std::map
< TypeNode
, unsigned > mnvn
;
1025 d_pattern_fun_sum
[pat
] = collectFunctions( pat
, pat
, d_pattern_fun_id
[pat
], mnvn
, d_pattern_var_id
[pat
] );
1026 if( d_pattern_is_normal
.find( pat
)==d_pattern_is_normal
.end() ){
1027 d_pattern_is_normal
[pat
] = true;
1029 if( d_pattern_is_relevant
.find( pat
)==d_pattern_is_relevant
.end() ){
1030 d_pattern_is_relevant
[pat
] = true;
1035 bool ConjectureGenerator::isGeneralization( TNode patg
, TNode pat
, std::map
< TNode
, TNode
>& subs
) {
1036 if( patg
.getKind()==BOUND_VARIABLE
){
1037 std::map
< TNode
, TNode
>::iterator it
= subs
.find( patg
);
1038 if( it
!=subs
.end() ){
1039 return it
->second
==pat
;
1045 Assert( patg
.hasOperator() );
1046 if( !pat
.hasOperator() || patg
.getOperator()!=pat
.getOperator() ){
1049 Assert( patg
.getNumChildren()==pat
.getNumChildren() );
1050 for( unsigned i
=0; i
<patg
.getNumChildren(); i
++ ){
1051 if( !isGeneralization( patg
[i
], pat
[i
], subs
) ){
1060 int ConjectureGenerator::calculateGeneralizationDepth( TNode n
, std::vector
< TNode
>& fv
) {
1061 if( n
.getKind()==BOUND_VARIABLE
){
1062 if( std::find( fv
.begin(), fv
.end(), n
)==fv
.end() ){
1070 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
1071 depth
+= calculateGeneralizationDepth( n
[i
], fv
);
1077 Node
ConjectureGenerator::getEnumerateTerm( TypeNode tn
, unsigned index
) {
1078 std::map
< TypeNode
, unsigned >::iterator it
= d_typ_enum_map
.find( tn
);
1080 if( it
==d_typ_enum_map
.end() ){
1081 teIndex
= (int)d_typ_enum
.size();
1082 d_typ_enum_map
[tn
] = teIndex
;
1083 d_typ_enum
.push_back( TypeEnumerator(tn
) );
1085 teIndex
= it
->second
;
1087 while( index
>=d_enum_terms
[tn
].size() ){
1088 if( d_typ_enum
[teIndex
].isFinished() ){
1089 return Node::null();
1091 d_enum_terms
[tn
].push_back( *d_typ_enum
[teIndex
] );
1092 ++d_typ_enum
[teIndex
];
1094 return d_enum_terms
[tn
][index
];
1097 void ConjectureGenerator::processCandidateConjecture( TNode lhs
, TNode rhs
, unsigned lhs_depth
, unsigned rhs_depth
) {
1098 int score
= considerCandidateConjecture( lhs
, rhs
);
1100 Trace("sg-conjecture") << "* Candidate conjecture : " << lhs
<< " == " << rhs
<< std::endl
;
1101 Trace("sg-conjecture-debug") << " LHS, RHS generalization depth : " << lhs_depth
<< ", " << rhs_depth
<< std::endl
;
1102 Trace("sg-conjecture-debug") << " confirmed = " << d_subs_confirmCount
<< ", #witnesses range = " << d_subs_confirmWitnessRange
.size() << "." << std::endl
;
1103 Trace("sg-conjecture-debug") << " #witnesses for ";
1104 bool firstTime
= true;
1105 for( std::map
< TNode
, std::vector
< TNode
> >::iterator it
= d_subs_confirmWitnessDomain
.begin(); it
!= d_subs_confirmWitnessDomain
.end(); ++it
){
1107 Trace("sg-conjecture-debug") << ", ";
1109 Trace("sg-conjecture-debug") << it
->first
<< " : " << it
->second
.size();
1110 //if( it->second.size()==1 ){
1111 // Trace("sg-conjecture-debug") << " (" << it->second[0] << ")";
1113 Trace("sg-conjecture-debug2") << " (";
1114 for( unsigned j
=0; j
<it
->second
.size(); j
++ ){
1115 if( j
>0 ){ Trace("sg-conjecture-debug2") << " "; }
1116 Trace("sg-conjecture-debug2") << d_ground_eqc_map
[it
->second
[j
]];
1118 Trace("sg-conjecture-debug2") << ")";
1121 Trace("sg-conjecture-debug") << std::endl
;
1122 Trace("sg-conjecture-debug") << " unknown = " << d_subs_unkCount
<< std::endl
;
1123 //Assert( getUniversalRepresentative( rhs )==rhs );
1124 //Assert( getUniversalRepresentative( lhs )==lhs );
1125 d_waiting_conjectures_lhs
.push_back( lhs
);
1126 d_waiting_conjectures_rhs
.push_back( rhs
);
1127 d_waiting_conjectures_score
.push_back( score
);
1128 d_waiting_conjectures
[lhs
].push_back( rhs
);
1129 d_waiting_conjectures
[rhs
].push_back( lhs
);
1133 int ConjectureGenerator::considerCandidateConjecture( TNode lhs
, TNode rhs
) {
1134 Assert( lhs
.getType()==rhs
.getType() );
1136 Trace("sg-cconj-debug") << "Consider candidate conjecture : " << lhs
<< " == " << rhs
<< "?" << std::endl
;
1138 Trace("sg-cconj-debug") << " -> trivial." << std::endl
;
1141 if( lhs
.getKind()==APPLY_CONSTRUCTOR
&& rhs
.getKind()==APPLY_CONSTRUCTOR
){
1142 Trace("sg-cconj-debug") << " -> irrelevant by syntactic analysis." << std::endl
;
1145 //variables of LHS must subsume variables of RHS
1146 for( std::map
< TypeNode
, unsigned >::iterator it
= d_pattern_var_id
[rhs
].begin(); it
!= d_pattern_var_id
[rhs
].end(); ++it
){
1147 std::map
< TypeNode
, unsigned >::iterator itl
= d_pattern_var_id
[lhs
].find( it
->first
);
1148 if( itl
!=d_pattern_var_id
[lhs
].end() ){
1149 if( itl
->second
<it
->second
){
1150 Trace("sg-cconj-debug") << " -> variables of sort " << it
->first
<< " are not subsumed." << std::endl
;
1153 Trace("sg-cconj-debug2") << " variables of sort " << it
->first
<< " are : " << itl
->second
<< " vs " << it
->second
<< std::endl
;
1156 Trace("sg-cconj-debug") << " -> has no variables of sort " << it
->first
<< "." << std::endl
;
1161 //currently active conjecture?
1162 std::map
< Node
, std::vector
< Node
> >::iterator iteq
= d_eq_conjectures
.find( lhs
);
1163 if( iteq
!=d_eq_conjectures
.end() ){
1164 if( std::find( iteq
->second
.begin(), iteq
->second
.end(), rhs
)!=iteq
->second
.end() ){
1165 Trace("sg-cconj-debug") << " -> this conjecture is already active." << std::endl
;
1169 //current a waiting conjecture?
1170 std::map
< Node
, std::vector
< Node
> >::iterator itw
= d_waiting_conjectures
.find( lhs
);
1171 if( itw
!=d_waiting_conjectures
.end() ){
1172 if( std::find( itw
->second
.begin(), itw
->second
.end(), rhs
)!=itw
->second
.end() ){
1173 Trace("sg-cconj-debug") << " -> already are considering this conjecture." << std::endl
;
1177 //check if canonical representation (should be, but for efficiency this is not guarenteed)
1178 //if( options::conjectureFilterCanonical() && ( getUniversalRepresentative( lhs )!=lhs || getUniversalRepresentative( rhs )!=rhs ) ){
1179 // Trace("sg-cconj") << " -> after processing, not canonical." << std::endl;
1184 bool scoreSet
= false;
1186 Trace("sg-cconj") << "Consider possible candidate conjecture : " << lhs
<< " == " << rhs
<< "?" << std::endl
;
1187 //find witness for counterexample, if possible
1188 if( options::conjectureFilterModel() ){
1189 Assert( d_rel_pattern_var_sum
.find( lhs
)!=d_rel_pattern_var_sum
.end() );
1190 Trace("sg-cconj-debug") << "Notify substitutions over " << d_rel_pattern_var_sum
[lhs
] << " variables." << std::endl
;
1191 std::map
< TNode
, TNode
> subs
;
1192 d_subs_confirmCount
= 0;
1193 d_subs_confirmWitnessRange
.clear();
1194 d_subs_confirmWitnessDomain
.clear();
1195 d_subs_unkCount
= 0;
1196 if( !d_rel_pattern_subs_index
[lhs
].notifySubstitutions( this, subs
, rhs
, d_rel_pattern_var_sum
[lhs
] ) ){
1197 Trace("sg-cconj") << " -> found witness that falsifies the conjecture." << std::endl
;
1200 //score is the minimum number of distinct substitutions for a variable
1201 for( std::map
< TNode
, std::vector
< TNode
> >::iterator it
= d_subs_confirmWitnessDomain
.begin(); it
!= d_subs_confirmWitnessDomain
.end(); ++it
){
1202 int num
= (int)it
->second
.size();
1203 if( !scoreSet
|| num
<score
){
1211 Trace("sg-cconj") << " confirmed = " << d_subs_confirmCount
<< ", #witnesses range = " << d_subs_confirmWitnessRange
.size() << "." << std::endl
;
1212 for( std::map
< TNode
, std::vector
< TNode
> >::iterator it
= d_subs_confirmWitnessDomain
.begin(); it
!= d_subs_confirmWitnessDomain
.end(); ++it
){
1213 Trace("sg-cconj") << " #witnesses for " << it
->first
<< " : " << it
->second
.size() << std::endl
;
1219 Trace("sg-cconj") << " -> SUCCESS." << std::endl
;
1220 Trace("sg-cconj") << " score : " << score
<< std::endl
;
1226 bool ConjectureGenerator::notifySubstitution( TNode glhs
, std::map
< TNode
, TNode
>& subs
, TNode rhs
) {
1227 if( Trace
.isOn("sg-cconj-debug") ){
1228 Trace("sg-cconj-debug") << "Ground eqc for LHS : " << glhs
<< ", based on substituion: " << std::endl
;
1229 for( std::map
< TNode
, TNode
>::iterator it
= subs
.begin(); it
!= subs
.end(); ++it
){
1230 Assert( getRepresentative( it
->second
)==it
->second
);
1231 Trace("sg-cconj-debug") << " " << it
->first
<< " -> " << it
->second
<< std::endl
;
1234 Trace("sg-cconj-debug") << "Evaluate RHS : : " << rhs
<< std::endl
;
1235 //get the representative of rhs with substitution subs
1236 TNode grhs
= getTermDatabase()->evaluateTerm( rhs
, subs
, true );
1237 Trace("sg-cconj-debug") << "...done evaluating term, got : " << grhs
<< std::endl
;
1238 if( !grhs
.isNull() ){
1240 Trace("sg-cconj-debug") << "Ground eqc for RHS : " << grhs
<< std::endl
;
1241 //check based on ground terms
1242 std::map
< TNode
, Node
>::iterator itl
= d_ground_eqc_map
.find( glhs
);
1243 if( itl
!=d_ground_eqc_map
.end() ){
1244 std::map
< TNode
, Node
>::iterator itr
= d_ground_eqc_map
.find( grhs
);
1245 if( itr
!=d_ground_eqc_map
.end() ){
1246 Trace("sg-cconj-debug") << "We have ground terms " << itl
->second
<< " and " << itr
->second
<< "." << std::endl
;
1247 if( itl
->second
.isConst() && itr
->second
.isConst() ){
1248 Trace("sg-cconj-debug") << "...disequal constants." << std::endl
;
1249 Trace("sg-cconj-witness") << " Witness of falsification : " << itl
->second
<< " != " << itr
->second
<< ", substutition is : " << std::endl
;
1250 for( std::map
< TNode
, TNode
>::iterator it
= subs
.begin(); it
!= subs
.end(); ++it
){
1251 Trace("sg-cconj-witness") << " " << it
->first
<< " -> " << it
->second
<< std::endl
;
1258 Trace("sg-cconj-debug") << "RHS is identical." << std::endl
;
1259 bool isGroundSubs
= true;
1260 for( std::map
< TNode
, TNode
>::iterator it
= subs
.begin(); it
!= subs
.end(); ++it
){
1261 std::map
< TNode
, Node
>::iterator git
= d_ground_eqc_map
.find( it
->second
);
1262 if( git
==d_ground_eqc_map
.end() ){
1263 isGroundSubs
= false;
1269 Trace("sg-cconj-witness") << " Witnessed " << glhs
<< " == " << grhs
<< ", substutition is : " << std::endl
;
1270 for( std::map
< TNode
, TNode
>::iterator it
= subs
.begin(); it
!= subs
.end(); ++it
){
1271 Trace("sg-cconj-witness") << " " << it
->first
<< " -> " << it
->second
<< std::endl
;
1272 if( std::find( d_subs_confirmWitnessDomain
[it
->first
].begin(), d_subs_confirmWitnessDomain
[it
->first
].end(), it
->second
)==d_subs_confirmWitnessDomain
[it
->first
].end() ){
1273 d_subs_confirmWitnessDomain
[it
->first
].push_back( it
->second
);
1276 d_subs_confirmCount
++;
1277 if( std::find( d_subs_confirmWitnessRange
.begin(), d_subs_confirmWitnessRange
.end(), glhs
)==d_subs_confirmWitnessRange
.end() ){
1278 d_subs_confirmWitnessRange
.push_back( glhs
);
1281 if( optFilterUnknown() ){
1282 Trace("sg-cconj-debug") << "...ground substitution giving terms that are neither equal nor disequal." << std::endl
;
1288 Trace("sg-cconj-debug") << "(could not ground eqc for RHS)." << std::endl
;
1298 void TermGenerator::reset( TermGenEnv
* s
, TypeNode tn
) {
1299 Assert( d_children
.empty() );
1304 Trace("sg-gen-tg-debug2") << "...add to context " << this << std::endl
;
1306 s
->changeContext( true );
1309 bool TermGenerator::getNextTerm( TermGenEnv
* s
, unsigned depth
) {
1310 if( Trace
.isOn("sg-gen-tg-debug2") ){
1311 Trace("sg-gen-tg-debug2") << this << " getNextTerm depth " << depth
<< " : status = " << d_status
<< ", num = " << d_status_num
;
1313 TNode f
= s
->getTgFunc( d_typ
, d_status_num
);
1314 Trace("sg-gen-tg-debug2") << ", f = " << f
;
1315 Trace("sg-gen-tg-debug2") << ", #args = " << s
->d_func_args
[f
].size();
1316 Trace("sg-gen-tg-debug2") << ", childNum = " << d_status_child_num
;
1317 Trace("sg-gen-tg-debug2") << ", #children = " << d_children
.size();
1319 Trace("sg-gen-tg-debug2") << std::endl
;
1324 if( !d_typ
.isNull() ){
1325 if( s
->allowVar( d_typ
) ){
1327 d_status_num
= s
->d_var_id
[d_typ
];
1329 Trace("sg-gen-tg-debug2") << this << " ...return unique var #" << d_status_num
<< std::endl
;
1330 return s
->considerCurrentTerm() ? true : getNextTerm( s
, depth
);
1332 //check allocating new variable
1335 if( s
->d_gen_relevant_terms
){
1338 return getNextTerm( s
, depth
);
1343 return getNextTerm( s
, depth
);
1345 }else if( d_status
==2 ){
1346 //cleanup previous information
1347 //if( d_status_num>=0 ){
1348 // s->d_var_eq_tg[d_status_num].pop_back();
1350 //check if there is another variable
1351 if( (d_status_num
+1)<(int)s
->getNumTgVars( d_typ
) ){
1353 //we have equated two variables
1354 //s->d_var_eq_tg[d_status_num].push_back( d_id );
1355 Trace("sg-gen-tg-debug2") << this << "...consider other var #" << d_status_num
<< std::endl
;
1356 return s
->considerCurrentTerm() ? true : getNextTerm( s
, depth
);
1358 if( s
->d_gen_relevant_terms
){
1362 return getNextTerm( s
, depth
);
1364 }else if( d_status
==4 ){
1366 if( depth
>0 && (d_status_num
+1)<(int)s
->getNumTgFuncs( d_typ
) ){
1368 d_status_child_num
= 0;
1369 Trace("sg-gen-tg-debug2") << this << "...consider function " << s
->getTgFunc( d_typ
, d_status_num
) << std::endl
;
1371 if( !s
->considerCurrentTerm() ){
1373 //don't consider this function
1376 //we have decided on a function application
1378 return getNextTerm( s
, depth
);
1380 //do not choose function applications at depth 0
1382 return getNextTerm( s
, depth
);
1384 }else if( d_status
==5 ){
1385 //iterating over arguments
1386 TNode f
= s
->getTgFunc( d_typ
, d_status_num
);
1387 if( d_status_child_num
<0 ){
1391 return getNextTerm( s
, depth
);
1392 }else if( d_status_child_num
==(int)s
->d_func_args
[f
].size() ){
1393 d_status_child_num
--;
1394 return s
->considerCurrentTermCanon( d_id
) ? true : getNextTerm( s
, depth
);
1397 Assert( d_status_child_num
<(int)s
->d_func_args
[f
].size() );
1398 if( d_status_child_num
==(int)d_children
.size() ){
1399 d_children
.push_back( s
->d_tg_id
);
1400 Assert( s
->d_tg_alloc
.find( s
->d_tg_id
)==s
->d_tg_alloc
.end() );
1401 s
->d_tg_alloc
[d_children
[d_status_child_num
]].reset( s
, s
->d_func_args
[f
][d_status_child_num
] );
1402 return getNextTerm( s
, depth
);
1404 Assert( d_status_child_num
+1==(int)d_children
.size() );
1405 if( s
->d_tg_alloc
[d_children
[d_status_child_num
]].getNextTerm( s
, depth
-1 ) ){
1406 d_status_child_num
++;
1407 return getNextTerm( s
, depth
);
1409 d_children
.pop_back();
1410 d_status_child_num
--;
1411 return getNextTerm( s
, depth
);
1415 }else if( d_status
==1 || d_status
==3 ){
1417 s
->removeVar( d_typ
);
1418 Assert( d_status_num
==(int)s
->d_var_id
[d_typ
] );
1419 //check if there is only one feasible equivalence class. if so, don't make pattern any more specific.
1420 //unsigned i = s->d_ccand_eqc[0].size()-1;
1421 //if( s->d_ccand_eqc[0][i].size()==1 && s->d_ccand_eqc[1][i].empty() ){
1422 // Trace("ajr-temp") << "Apply this!" << std::endl;
1424 // return getNextTerm( s, depth );
1430 return getNextTerm( s
, depth
);
1433 Assert( d_children
.empty() );
1434 Trace("sg-gen-tg-debug2") << "...remove from context " << this << std::endl
;
1435 s
->changeContext( false );
1436 Assert( d_id
==s
->d_tg_id
);
1441 void TermGenerator::resetMatching( TermGenEnv
* s
, TNode eqc
, unsigned mode
) {
1443 d_match_status_child_num
= 0;
1444 d_match_children
.clear();
1445 d_match_children_end
.clear();
1446 d_match_mode
= mode
;
1447 //if this term generalizes, it must generalize a non-ground term
1448 //if( (d_match_mode & ( 1 << 2 ))!=0 && s->isGroundEqc( eqc ) && d_status==5 ){
1449 // d_match_status = -1;
1453 bool TermGenerator::getNextMatch( TermGenEnv
* s
, TNode eqc
, std::map
< TypeNode
, std::map
< unsigned, TNode
> >& subs
, std::map
< TNode
, bool >& rev_subs
) {
1454 if( d_match_status
<0 ){
1457 if( Trace
.isOn("sg-gen-tg-match") ){
1458 Trace("sg-gen-tg-match") << "Matching ";
1459 debugPrint( s
, "sg-gen-tg-match", "sg-gen-tg-match" );
1460 Trace("sg-gen-tg-match") << " with eqc e" << s
->d_cg
->d_em
[eqc
] << "..." << std::endl
;
1461 Trace("sg-gen-tg-match") << " mstatus = " << d_match_status
;
1463 TNode f
= s
->getTgFunc( d_typ
, d_status_num
);
1464 Trace("sg-gen-tg-debug2") << ", f = " << f
;
1465 Trace("sg-gen-tg-debug2") << ", #args = " << s
->d_func_args
[f
].size();
1466 Trace("sg-gen-tg-debug2") << ", mchildNum = " << d_match_status_child_num
;
1467 Trace("sg-gen-tg-debug2") << ", #mchildren = " << d_match_children
.size();
1469 Trace("sg-gen-tg-debug2") << ", current substitution : {";
1470 for( std::map
< TypeNode
, std::map
< unsigned, TNode
> >::iterator itt
= subs
.begin(); itt
!= subs
.end(); ++itt
){
1471 for( std::map
< unsigned, TNode
>::iterator it
= itt
->second
.begin(); it
!= itt
->second
.end(); ++it
){
1472 Trace("sg-gen-tg-debug2") << " " << it
->first
<< " -> e" << s
->d_cg
->d_em
[it
->second
];
1475 Trace("sg-gen-tg-debug2") << " } " << std::endl
;
1479 if( d_match_status
==0 ){
1481 if( (d_match_mode
& ( 1 << 1 ))!=0 ){
1483 if( !s
->isGroundEqc( eqc
) ){
1486 }else if( (d_match_mode
& ( 1 << 2 ))!=0 ){
1487 //only non-ground terms
1488 //if( s->isGroundEqc( eqc ) ){
1492 //store the match : restricted if match_mode.0 = 1
1493 if( (d_match_mode
& ( 1 << 0 ))!=0 ){
1494 std::map
< TNode
, bool >::iterator it
= rev_subs
.find( eqc
);
1495 if( it
==rev_subs
.end() ){
1496 rev_subs
[eqc
] = true;
1501 Assert( subs
[d_typ
].find( d_status_num
)==subs
[d_typ
].end() );
1502 subs
[d_typ
][d_status_num
] = eqc
;
1506 subs
[d_typ
].erase( d_status_num
);
1507 if( (d_match_mode
& ( 1 << 0 ))!=0 ){
1508 rev_subs
.erase( eqc
);
1512 }else if( d_status
==2 ){
1513 if( d_match_status
==0 ){
1515 Assert( d_status_num
<(int)s
->getNumTgVars( d_typ
) );
1516 std::map
< unsigned, TNode
>::iterator it
= subs
[d_typ
].find( d_status_num
);
1517 Assert( it
!=subs
[d_typ
].end() );
1518 return it
->second
==eqc
;
1522 }else if( d_status
==5 ){
1523 //Assert( d_match_children.size()<=d_children.size() );
1524 //enumerating over f-applications in eqc
1525 if( d_match_status_child_num
<0 ){
1527 }else if( d_match_status
==0 ){
1528 //set up next binding
1529 if( d_match_status_child_num
==(int)d_match_children
.size() ){
1530 if( d_match_status_child_num
==0 ){
1532 TNode f
= s
->getTgFunc( d_typ
, d_status_num
);
1533 std::map
< TNode
, TermArgTrie
>::iterator it
= s
->getTermDatabase()->d_func_map_eqc_trie
[f
].d_data
.find( eqc
);
1534 if( it
!=s
->getTermDatabase()->d_func_map_eqc_trie
[f
].d_data
.end() ){
1535 d_match_children
.push_back( it
->second
.d_data
.begin() );
1536 d_match_children_end
.push_back( it
->second
.d_data
.end() );
1539 d_match_status_child_num
--;
1540 return getNextMatch( s
, eqc
, subs
, rev_subs
);
1543 d_match_children
.push_back( d_match_children
[d_match_status_child_num
-1]->second
.d_data
.begin() );
1544 d_match_children_end
.push_back( d_match_children
[d_match_status_child_num
-1]->second
.d_data
.end() );
1548 Assert( d_match_status_child_num
+1==(int)d_match_children
.size() );
1549 if( d_match_children
[d_match_status_child_num
]==d_match_children_end
[d_match_status_child_num
] ){
1550 //no more arguments to bind
1551 d_match_children
.pop_back();
1552 d_match_children_end
.pop_back();
1553 d_match_status_child_num
--;
1554 return getNextMatch( s
, eqc
, subs
, rev_subs
);
1556 if( d_match_status_child_num
==(int)d_children
.size() ){
1557 //successfully matched all children
1558 d_match_children
.pop_back();
1559 d_match_children_end
.pop_back();
1560 d_match_status_child_num
--;
1561 return true;//return d_match_children[d_match_status]!=d_match_children_end[d_match_status];
1564 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
);
1565 return getNextMatch( s
, eqc
, subs
, rev_subs
);
1569 Assert( d_match_status
==1 );
1570 Assert( d_match_status_child_num
+1==(int)d_match_children
.size() );
1571 Assert( d_match_children
[d_match_status_child_num
]!=d_match_children_end
[d_match_status_child_num
] );
1573 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
) ){
1574 d_match_status_child_num
++;
1575 return getNextMatch( s
, eqc
, subs
, rev_subs
);
1578 d_match_children
[d_match_status_child_num
]++;
1579 return getNextMatch( s
, eqc
, subs
, rev_subs
);
1587 unsigned TermGenerator::getDepth( TermGenEnv
* s
) {
1590 for( unsigned i
=0; i
<d_children
.size(); i
++ ){
1591 unsigned d
= s
->d_tg_alloc
[d_children
[i
]].getDepth( s
);
1602 unsigned TermGenerator::calculateGeneralizationDepth( TermGenEnv
* s
, std::map
< TypeNode
, std::vector
< int > >& fvs
) {
1605 for( unsigned i
=0; i
<d_children
.size(); i
++ ){
1606 sum
+= s
->d_tg_alloc
[d_children
[i
]].calculateGeneralizationDepth( s
, fvs
);
1610 Assert( d_status
==2 || d_status
==1 );
1611 std::map
< TypeNode
, std::vector
< int > >::iterator it
= fvs
.find( d_typ
);
1612 if( it
!=fvs
.end() ){
1613 if( std::find( it
->second
.begin(), it
->second
.end(), d_status_num
)!=it
->second
.end() ){
1617 fvs
[d_typ
].push_back( d_status_num
);
1622 unsigned TermGenerator::getGeneralizationDepth( TermGenEnv
* s
) {
1623 //if( s->d_gen_relevant_terms ){
1624 // return s->d_tg_gdepth;
1626 std::map
< TypeNode
, std::vector
< int > > fvs
;
1627 return calculateGeneralizationDepth( s
, fvs
);
1631 Node
TermGenerator::getTerm( TermGenEnv
* s
) {
1632 if( d_status
==1 || d_status
==2 ){
1633 Assert( !d_typ
.isNull() );
1634 return s
->getFreeVar( d_typ
, d_status_num
);
1635 }else if( d_status
==5 ){
1636 Node f
= s
->getTgFunc( d_typ
, d_status_num
);
1637 if( d_children
.size()==s
->d_func_args
[f
].size() ){
1638 std::vector
< Node
> children
;
1639 children
.push_back( f
);
1640 for( unsigned i
=0; i
<d_children
.size(); i
++ ){
1641 Node nc
= s
->d_tg_alloc
[d_children
[i
]].getTerm( s
);
1643 return Node::null();
1645 //Assert( nc.getType()==s->d_func_args[f][i] );
1646 children
.push_back( nc
);
1649 return NodeManager::currentNM()->mkNode( s
->d_func_kind
[f
], children
);
1654 return Node::null();
1657 void TermGenerator::debugPrint( TermGenEnv
* s
, const char * c
, const char * cd
) {
1658 Trace(cd
) << "[*" << d_id
<< "," << d_status
<< "]:";
1659 if( d_status
==1 || d_status
==2 ){
1660 Trace(c
) << s
->getFreeVar( d_typ
, d_status_num
);
1661 }else if( d_status
==5 ){
1662 TNode f
= s
->getTgFunc( d_typ
, d_status_num
);
1663 Trace(c
) << "(" << f
;
1664 for( unsigned i
=0; i
<d_children
.size(); i
++ ){
1666 s
->d_tg_alloc
[d_children
[i
]].debugPrint( s
, c
, cd
);
1668 if( d_children
.size()<s
->d_func_args
[f
].size() ){
1677 void TermGenEnv::collectSignatureInformation() {
1678 d_typ_tg_funcs
.clear();
1680 d_func_kind
.clear();
1681 d_func_args
.clear();
1683 for( std::map
< Node
, TermArgTrie
>::iterator it
= getTermDatabase()->d_func_map_trie
.begin(); it
!= getTermDatabase()->d_func_map_trie
.end(); ++it
){
1684 if( !getTermDatabase()->d_op_map
[it
->first
].empty() ){
1685 Node nn
= getTermDatabase()->d_op_map
[it
->first
][0];
1686 if( d_cg
->isHandledTerm( nn
) && nn
.getKind()!=APPLY_SELECTOR_TOTAL
&& !nn
.getType().isBoolean() ){
1687 d_funcs
.push_back( it
->first
);
1688 for( unsigned i
=0; i
<nn
.getNumChildren(); i
++ ){
1689 d_func_args
[it
->first
].push_back( nn
[i
].getType() );
1691 d_func_kind
[it
->first
] = nn
.getKind();
1692 d_typ_tg_funcs
[tnull
].push_back( it
->first
);
1693 d_typ_tg_funcs
[nn
.getType()].push_back( it
->first
);
1694 Trace("sg-rel-sig") << "Will enumerate function applications of : " << it
->first
<< ", #args = " << d_func_args
[it
->first
].size() << ", kind = " << nn
.getKind() << std::endl
;
1695 getTermDatabase()->computeUfEqcTerms( it
->first
);
1700 for( std::map
< TypeNode
, std::vector
< TNode
> >::iterator it
= d_typ_tg_funcs
.begin(); it
!= d_typ_tg_funcs
.end(); ++it
){
1701 std::random_shuffle( it
->second
.begin(), it
->second
.end() );
1702 if( it
->first
.isNull() ){
1703 Trace("sg-gen-tg-debug") << "In this order : ";
1704 for( unsigned i
=0; i
<it
->second
.size(); i
++ ){
1705 Trace("sg-gen-tg-debug") << it
->second
[i
] << " ";
1707 Trace("sg-gen-tg-debug") << std::endl
;
1712 void TermGenEnv::reset( unsigned depth
, bool genRelevant
, TypeNode tn
) {
1713 Assert( d_tg_alloc
.empty() );
1717 for( unsigned i
=0; i
<2; i
++ ){
1718 d_ccand_eqc
[i
].clear();
1719 d_ccand_eqc
[i
].push_back( d_relevant_eqc
[i
] );
1725 d_tg_gdepth_limit
= depth
;
1726 d_gen_relevant_terms
= genRelevant
;
1727 d_tg_alloc
[0].reset( this, tn
);
1730 bool TermGenEnv::getNextTerm() {
1731 if( d_tg_alloc
[0].getNextTerm( this, d_tg_gdepth_limit
) ){
1732 Assert( (int)d_tg_alloc
[0].getGeneralizationDepth( this )<=d_tg_gdepth_limit
);
1733 if( (int)d_tg_alloc
[0].getGeneralizationDepth( this )!=d_tg_gdepth_limit
){
1734 return getNextTerm();
1744 void TermGenEnv::resetMatching( TNode eqc
, unsigned mode
) {
1745 d_tg_alloc
[0].resetMatching( this, eqc
, mode
);
1749 bool TermGenEnv::getNextMatch( TNode eqc
, std::map
< TypeNode
, std::map
< unsigned, TNode
> >& subs
, std::map
< TNode
, bool >& rev_subs
) {
1750 return d_tg_alloc
[0].getNextMatch( this, eqc
, subs
, rev_subs
);
1754 Node
TermGenEnv::getTerm() {
1755 return d_tg_alloc
[0].getTerm( this );
1758 void TermGenEnv::debugPrint( const char * c
, const char * cd
) {
1759 d_tg_alloc
[0].debugPrint( this, c
, cd
);
1762 unsigned TermGenEnv::getNumTgVars( TypeNode tn
) {
1763 return d_var_id
[tn
];
1766 bool TermGenEnv::allowVar( TypeNode tn
) {
1767 std::map
< TypeNode
, unsigned >::iterator it
= d_var_limit
.find( tn
);
1768 if( it
==d_var_limit
.end() ){
1771 return d_var_id
[tn
]<it
->second
;
1775 void TermGenEnv::addVar( TypeNode tn
) {
1779 void TermGenEnv::removeVar( TypeNode tn
) {
1781 //d_var_eq_tg.pop_back();
1782 //d_var_tg.pop_back();
1785 unsigned TermGenEnv::getNumTgFuncs( TypeNode tn
) {
1786 return d_typ_tg_funcs
[tn
].size();
1789 TNode
TermGenEnv::getTgFunc( TypeNode tn
, unsigned i
) {
1790 return d_typ_tg_funcs
[tn
][i
];
1793 Node
TermGenEnv::getFreeVar( TypeNode tn
, unsigned i
) {
1794 return d_cg
->getFreeVar( tn
, i
);
1797 bool TermGenEnv::considerCurrentTerm() {
1798 Assert( !d_tg_alloc
.empty() );
1800 //if generalization depth is too large, don't consider it
1801 unsigned i
= d_tg_alloc
.size();
1802 Trace("sg-gen-tg-debug") << "Consider term ";
1803 d_tg_alloc
[0].debugPrint( this, "sg-gen-tg-debug", "sg-gen-tg-debug" );
1804 Trace("sg-gen-tg-debug") << "? curr term size = " << d_tg_alloc
.size() << ", last status = " << d_tg_alloc
[i
-1].d_status
;
1805 Trace("sg-gen-tg-debug") << std::endl
;
1807 if( d_tg_gdepth_limit
>=0 && d_tg_alloc
[0].getGeneralizationDepth( this )>(unsigned)d_tg_gdepth_limit
){
1808 Trace("sg-gen-consider-term") << "-> generalization depth of ";
1809 d_tg_alloc
[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-tg-debug" );
1810 Trace("sg-gen-consider-term") << " is too high " << d_tg_gdepth
<< " " << d_tg_alloc
[0].getGeneralizationDepth( this ) << ", do not consider." << std::endl
;
1816 if( d_tg_alloc[i-1].d_status==1 ){
1817 }else if( d_tg_alloc[i-1].d_status==2 ){
1818 }else if( d_tg_alloc[i-1].d_status==5 ){
1820 Trace("sg-gen-tg-debug") << "Bad tg: " << &d_tg_alloc[i-1] << std::endl;
1824 //if equated two variables, first check if context-independent TODO
1825 //----end optimizations
1828 //check based on which candidate equivalence classes match
1829 if( d_gen_relevant_terms
){
1830 Trace("sg-gen-tg-debug") << "Filter based on relevant ground EQC";
1831 Trace("sg-gen-tg-debug") << ", #eqc to try = " << d_ccand_eqc
[0][i
-1].size() << "/" << d_ccand_eqc
[1][i
-1].size() << std::endl
;
1833 Assert( d_ccand_eqc
[0].size()>=2 );
1834 Assert( d_ccand_eqc
[0].size()==d_ccand_eqc
[1].size() );
1835 Assert( d_ccand_eqc
[0].size()==d_tg_id
+1 );
1836 Assert( d_tg_id
==d_tg_alloc
.size() );
1837 for( unsigned r
=0; r
<2; r
++ ){
1838 d_ccand_eqc
[r
][i
].clear();
1841 //re-check feasibility of EQC
1842 for( unsigned r
=0; r
<2; r
++ ){
1843 for( unsigned j
=0; j
<d_ccand_eqc
[r
][i
-1].size(); j
++ ){
1844 std::map
< TypeNode
, std::map
< unsigned, TNode
> > subs
;
1845 std::map
< TNode
, bool > rev_subs
;
1848 mode
= d_cg
->optReqDistinctVarPatterns() ? ( 1 << 0 ) : 0;
1849 mode
= mode
| (1 << 2 );
1853 d_tg_alloc
[0].resetMatching( this, d_ccand_eqc
[r
][i
-1][j
], mode
);
1854 if( d_tg_alloc
[0].getNextMatch( this, d_ccand_eqc
[r
][i
-1][j
], subs
, rev_subs
) ){
1855 d_ccand_eqc
[r
][i
].push_back( d_ccand_eqc
[r
][i
-1][j
] );
1859 for( unsigned r
=0; r
<2; r
++ ){
1860 Trace("sg-gen-tg-debug") << "Current eqc of type " << r
<< " : ";
1861 for( unsigned j
=0; j
<d_ccand_eqc
[r
][i
].size(); j
++ ){
1862 Trace("sg-gen-tg-debug") << "e" << d_cg
->d_em
[d_ccand_eqc
[r
][i
][j
]] << " ";
1864 Trace("sg-gen-tg-debug") << std::endl
;
1866 if( options::conjectureFilterActiveTerms() && d_ccand_eqc
[0][i
].empty() ){
1867 Trace("sg-gen-consider-term") << "Do not consider term of form ";
1868 d_tg_alloc
[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-consider-term-debug" );
1869 Trace("sg-gen-consider-term") << " since no relevant EQC matches it." << std::endl
;
1872 if( options::conjectureFilterModel() && d_ccand_eqc
[1][i
].empty() ){
1873 Trace("sg-gen-consider-term") << "Do not consider term of form ";
1874 d_tg_alloc
[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-consider-term-debug" );
1875 Trace("sg-gen-consider-term") << " since no ground EQC matches it." << std::endl
;
1879 Trace("sg-gen-tg-debug") << "Will consider term ";
1880 d_tg_alloc
[0].debugPrint( this, "sg-gen-tg-debug", "sg-gen-tg-debug" );
1881 Trace("sg-gen-tg-debug") << std::endl
;
1882 Trace("sg-gen-consider-term-debug") << std::endl
;
1886 void TermGenEnv::changeContext( bool add
) {
1888 for( unsigned r
=0; r
<2; r
++ ){
1889 d_ccand_eqc
[r
].push_back( std::vector
< TNode
>() );
1893 for( unsigned r
=0; r
<2; r
++ ){
1894 d_ccand_eqc
[r
].pop_back();
1897 Assert( d_tg_alloc
.find( d_tg_id
)!=d_tg_alloc
.end() );
1898 d_tg_alloc
.erase( d_tg_id
);
1902 bool TermGenEnv::considerCurrentTermCanon( unsigned tg_id
){
1903 Assert( tg_id
<d_tg_alloc
.size() );
1904 if( options::conjectureFilterCanonical() ){
1905 //check based on a canonicity of the term (if there is one)
1906 Trace("sg-gen-tg-debug") << "Consider term canon ";
1907 d_tg_alloc
[0].debugPrint( this, "sg-gen-tg-debug", "sg-gen-tg-debug" );
1908 Trace("sg-gen-tg-debug") << ", tg is [" << tg_id
<< "]..." << std::endl
;
1910 Node ln
= d_tg_alloc
[tg_id
].getTerm( this );
1911 Trace("sg-gen-tg-debug") << "Term is " << ln
<< std::endl
;
1912 return d_cg
->considerTermCanon( ln
, d_gen_relevant_terms
);
1917 bool TermGenEnv::isRelevantFunc( Node f
) {
1918 return std::find( d_funcs
.begin(), d_funcs
.end(), f
)!=d_funcs
.end();
1920 TermDb
* TermGenEnv::getTermDatabase() {
1921 return d_cg
->getTermDatabase();
1923 Node
TermGenEnv::getGroundEqc( TNode r
) {
1924 return d_cg
->getGroundEqc( r
);
1926 bool TermGenEnv::isGroundEqc( TNode r
){
1927 return d_cg
->isGroundEqc( r
);
1929 bool TermGenEnv::isGroundTerm( TNode n
){
1930 return d_cg
->isGroundTerm( n
);
1935 void SubstitutionIndex::addSubstitution( TNode eqc
, std::vector
< TNode
>& vars
, std::vector
< TNode
>& terms
, unsigned i
) {
1936 if( i
==vars
.size() ){
1939 Assert( d_var
.isNull() || d_var
==vars
[i
] );
1941 d_children
[terms
[i
]].addSubstitution( eqc
, vars
, terms
, i
+1 );
1945 bool SubstitutionIndex::notifySubstitutions( ConjectureGenerator
* s
, std::map
< TNode
, TNode
>& subs
, TNode rhs
, unsigned numVars
, unsigned i
) {
1947 Assert( d_children
.empty() );
1948 return s
->notifySubstitution( d_var
, subs
, rhs
);
1950 Assert( i
==0 || !d_children
.empty() );
1951 for( std::map
< TNode
, SubstitutionIndex
>::iterator it
= d_children
.begin(); it
!= d_children
.end(); ++it
){
1952 Trace("sg-cconj-debug2") << "Try " << d_var
<< " -> " << it
->first
<< " (" << i
<< "/" << numVars
<< ")" << std::endl
;
1953 subs
[d_var
] = it
->first
;
1954 if( !it
->second
.notifySubstitutions( s
, subs
, rhs
, numVars
, i
+1 ) ){
1963 void TheoremIndex::addTheorem( std::vector
< TNode
>& lhs_v
, std::vector
< unsigned >& lhs_arg
, TNode rhs
){
1964 if( lhs_v
.empty() ){
1965 if( std::find( d_terms
.begin(), d_terms
.end(), rhs
)==d_terms
.end() ){
1966 d_terms
.push_back( rhs
);
1969 unsigned index
= lhs_v
.size()-1;
1970 if( lhs_arg
[index
]==lhs_v
[index
].getNumChildren() ){
1973 addTheorem( lhs_v
, lhs_arg
, rhs
);
1976 addTheoremNode( lhs_v
[index
][lhs_arg
[index
]-1], lhs_v
, lhs_arg
, rhs
);
1981 void TheoremIndex::addTheoremNode( TNode curr
, std::vector
< TNode
>& lhs_v
, std::vector
< unsigned >& lhs_arg
, TNode rhs
){
1982 Trace("thm-db-debug") << "Adding conjecture for subterm " << curr
<< "..." << std::endl
;
1983 if( curr
.hasOperator() ){
1984 lhs_v
.push_back( curr
);
1985 lhs_arg
.push_back( 0 );
1986 d_children
[curr
.getOperator()].addTheorem( lhs_v
, lhs_arg
, rhs
);
1988 Assert( curr
.getKind()==kind::BOUND_VARIABLE
);
1989 TypeNode tn
= curr
.getType();
1990 Assert( d_var
[tn
].isNull() || d_var
[tn
]==curr
);
1992 d_children
[curr
].addTheorem( lhs_v
, lhs_arg
, rhs
);
1996 void TheoremIndex::getEquivalentTerms( std::vector
< TNode
>& n_v
, std::vector
< unsigned >& n_arg
,
1997 std::map
< TNode
, TNode
>& smap
, std::vector
< TNode
>& vars
, std::vector
< TNode
>& subs
,
1998 std::vector
< Node
>& terms
) {
1999 Trace("thm-db-debug") << "Get equivalent terms " << n_v
.size() << " " << n_arg
.size() << std::endl
;
2001 Trace("thm-db-debug") << "Number of terms : " << d_terms
.size() << std::endl
;
2002 //apply substutitions to RHS's
2003 for( unsigned i
=0; i
<d_terms
.size(); i
++ ){
2004 Node n
= d_terms
[i
].substitute( vars
.begin(), vars
.end(), subs
.begin(), subs
.end() );
2005 terms
.push_back( n
);
2008 unsigned index
= n_v
.size()-1;
2009 if( n_arg
[index
]==n_v
[index
].getNumChildren() ){
2012 getEquivalentTerms( n_v
, n_arg
, smap
, vars
, subs
, terms
);
2015 getEquivalentTermsNode( n_v
[index
][n_arg
[index
]-1], n_v
, n_arg
, smap
, vars
, subs
, terms
);
2020 void TheoremIndex::getEquivalentTermsNode( Node curr
, std::vector
< TNode
>& n_v
, std::vector
< unsigned >& n_arg
,
2021 std::map
< TNode
, TNode
>& smap
, std::vector
< TNode
>& vars
, std::vector
< TNode
>& subs
,
2022 std::vector
< Node
>& terms
) {
2023 Trace("thm-db-debug") << "Get equivalent based on subterm " << curr
<< "..." << std::endl
;
2024 if( curr
.hasOperator() ){
2025 Trace("thm-db-debug") << "Check based on operator..." << std::endl
;
2026 std::map
< TNode
, TheoremIndex
>::iterator it
= d_children
.find( curr
.getOperator() );
2027 if( it
!=d_children
.end() ){
2028 n_v
.push_back( curr
);
2029 n_arg
.push_back( 0 );
2030 it
->second
.getEquivalentTerms( n_v
, n_arg
, smap
, vars
, subs
, terms
);
2032 Trace("thm-db-debug") << "...done check based on operator" << std::endl
;
2034 TypeNode tn
= curr
.getType();
2035 std::map
< TypeNode
, TNode
>::iterator itt
= d_var
.find( tn
);
2036 if( itt
!=d_var
.end() ){
2037 Trace("thm-db-debug") << "Check for substitution with " << itt
->second
<< "..." << std::endl
;
2038 Assert( curr
.getType()==itt
->second
.getType() );
2039 //add to substitution if possible
2040 bool success
= false;
2041 std::map
< TNode
, TNode
>::iterator it
= smap
.find( itt
->second
);
2042 if( it
==smap
.end() ){
2043 smap
[itt
->second
] = curr
;
2044 vars
.push_back( itt
->second
);
2045 subs
.push_back( curr
);
2047 }else if( it
->second
==curr
){
2050 //also check modulo equality (in universal equality engine)
2052 Trace("thm-db-debug") << "...check for substitution with " << itt
->second
<< ", success = " << success
<< "." << std::endl
;
2054 d_children
[itt
->second
].getEquivalentTerms( n_v
, n_arg
, smap
, vars
, subs
, terms
);
2059 void TheoremIndex::debugPrint( const char * c
, unsigned ind
) {
2060 for( std::map
< TNode
, TheoremIndex
>::iterator it
= d_children
.begin(); it
!= d_children
.end(); ++it
){
2061 for( unsigned i
=0; i
<ind
; i
++ ){ Trace(c
) << " "; }
2062 Trace(c
) << it
->first
<< std::endl
;
2063 it
->second
.debugPrint( c
, ind
+1 );
2065 if( !d_terms
.empty() ){
2066 for( unsigned i
=0; i
<ind
; i
++ ){ Trace(c
) << " "; }
2068 for( unsigned i
=0; i
<d_terms
.size(); i
++ ){
2069 Trace(c
) << " " << d_terms
[i
];
2071 Trace(c
) << " }" << std::endl
;
2073 //if( !d_var.isNull() ){
2074 // for( unsigned i=0; i<ind; i++ ){ Trace(c) << " "; }
2075 // Trace(c) << "var:" << d_var << std::endl;
2079 bool ConjectureGenerator::optReqDistinctVarPatterns() { return false; }
2080 bool ConjectureGenerator::optFilterUnknown() { return true; } //may change
2081 int ConjectureGenerator::optFilterScoreThreshold() { return 1; }
2082 unsigned ConjectureGenerator::optFullCheckFrequency() { return 1; }
2084 bool ConjectureGenerator::optStatsOnly() { return false; }