1 /********************* */
2 /*! \file conjecture_generator.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Mathias Preiner, Aina Niemetz
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
8 ** in the top-level source directory and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief conjecture generator class
16 #include "theory/quantifiers/conjecture_generator.h"
17 #include "expr/term_canonize.h"
18 #include "options/quantifiers_options.h"
19 #include "theory/quantifiers/ematching/trigger_term_info.h"
20 #include "theory/quantifiers/first_order_model.h"
21 #include "theory/quantifiers/skolemize.h"
22 #include "theory/quantifiers/term_database.h"
23 #include "theory/quantifiers/term_enumeration.h"
24 #include "theory/quantifiers/term_util.h"
25 #include "theory/quantifiers_engine.h"
26 #include "util/random.h"
29 using namespace CVC4::kind
;
30 using namespace CVC4::theory
;
31 using namespace CVC4::theory::quantifiers
;
36 struct sortConjectureScore
{
37 std::vector
< int > d_scores
;
38 bool operator() (unsigned i
, unsigned j
) { return d_scores
[i
]>d_scores
[j
]; }
42 void OpArgIndex::addTerm( std::vector
< TNode
>& terms
, TNode n
, unsigned index
){
43 if( index
==n
.getNumChildren() ){
44 Assert(n
.hasOperator());
45 if( std::find( d_ops
.begin(), d_ops
.end(), n
.getOperator() )==d_ops
.end() ){
46 d_ops
.push_back( n
.getOperator() );
47 d_op_terms
.push_back( n
);
50 d_child
[terms
[index
]].addTerm( terms
, n
, index
+1 );
54 Node
OpArgIndex::getGroundTerm( ConjectureGenerator
* s
, std::vector
< TNode
>& args
) {
56 for( std::map
< TNode
, OpArgIndex
>::iterator it
= d_child
.begin(); it
!= d_child
.end(); ++it
){
57 std::map
< TNode
, Node
>::iterator itf
= s
->d_ground_eqc_map
.find( it
->first
);
58 if( itf
!=s
->d_ground_eqc_map
.end() ){
59 args
.push_back( itf
->second
);
60 Node n
= it
->second
.getGroundTerm( s
, args
);
69 std::vector
<TNode
> args2
;
70 if (d_op_terms
[0].getMetaKind() == kind::metakind::PARAMETERIZED
)
72 args2
.push_back( d_ops
[0] );
74 args2
.insert(args2
.end(), args
.begin(), args
.end());
75 return NodeManager::currentNM()->mkNode(d_op_terms
[0].getKind(), args2
);
78 void OpArgIndex::getGroundTerms( ConjectureGenerator
* s
, std::vector
< TNode
>& terms
) {
79 terms
.insert( terms
.end(), d_op_terms
.begin(), d_op_terms
.end() );
80 for( std::map
< TNode
, OpArgIndex
>::iterator it
= d_child
.begin(); it
!= d_child
.end(); ++it
){
81 if( s
->isGroundEqc( it
->first
) ){
82 it
->second
.getGroundTerms( s
, terms
);
87 ConjectureGenerator::ConjectureGenerator(QuantifiersEngine
* qe
,
89 QuantifiersInferenceManager
& qim
,
90 QuantifiersRegistry
& qr
)
91 : QuantifiersModule(qs
, qim
, qr
, qe
),
94 d_notify
, qs
.getSatContext(), "ConjectureGenerator::ee", false),
95 d_ee_conjectures(qs
.getSatContext()),
97 d_subs_confirmCount(0),
100 d_hasAddedLemma(false)
102 d_true
= NodeManager::currentNM()->mkConst(true);
103 d_false
= NodeManager::currentNM()->mkConst(false);
104 d_uequalityEngine
.addFunctionKind( kind::APPLY_UF
);
105 d_uequalityEngine
.addFunctionKind( kind::APPLY_CONSTRUCTOR
);
109 ConjectureGenerator::~ConjectureGenerator()
111 for (std::map
<Node
, EqcInfo
*>::iterator i
= d_eqc_info
.begin(),
112 iend
= d_eqc_info
.end();
116 EqcInfo
* current
= (*i
).second
;
117 Assert(current
!= nullptr);
122 void ConjectureGenerator::eqNotifyNewClass( TNode t
){
123 Trace("thm-ee-debug") << "UEE : new equivalence class " << t
<< std::endl
;
124 d_upendingAdds
.push_back( t
);
127 void ConjectureGenerator::eqNotifyMerge(TNode t1
, TNode t2
)
129 //get maintained representatives
132 std::map
< Node
, EqcInfo
* >::iterator it1
= d_eqc_info
.find( t1
);
133 if( it1
!=d_eqc_info
.end() && !it1
->second
->d_rep
.get().isNull() ){
134 rt1
= it1
->second
->d_rep
.get();
136 std::map
< Node
, EqcInfo
* >::iterator it2
= d_eqc_info
.find( t2
);
137 if( it2
!=d_eqc_info
.end() && !it2
->second
->d_rep
.get().isNull() ){
138 rt2
= it2
->second
->d_rep
.get();
140 Trace("thm-ee-debug") << "UEE : equality holds : " << t1
<< " == " << t2
<< std::endl
;
141 Trace("thm-ee-debug") << " ureps : " << rt1
<< " == " << rt2
<< std::endl
;
142 Trace("thm-ee-debug") << " relevant : " << d_pattern_is_relevant
[rt1
] << " " << d_pattern_is_relevant
[rt2
] << std::endl
;
143 Trace("thm-ee-debug") << " normal : " << d_pattern_is_normal
[rt1
] << " " << d_pattern_is_normal
[rt2
] << std::endl
;
144 Trace("thm-ee-debug") << " size : " << d_pattern_fun_sum
[rt1
] << " " << d_pattern_fun_sum
[rt2
] << std::endl
;
146 if( isUniversalLessThan( rt2
, rt1
) ){
148 if( it1
==d_eqc_info
.end() ){
149 ei
= getOrMakeEqcInfo( t1
, true );
158 ConjectureGenerator::EqcInfo::EqcInfo( context::Context
* c
) : d_rep( c
, Node::null() ){
162 ConjectureGenerator::EqcInfo
* ConjectureGenerator::getOrMakeEqcInfo( TNode n
, bool doMake
) {
163 //Assert( getUniversalRepresentative( n )==n );
164 std::map
< Node
, EqcInfo
* >::iterator eqc_i
= d_eqc_info
.find( n
);
165 if( eqc_i
!=d_eqc_info
.end() ){
166 return eqc_i
->second
;
168 EqcInfo
* ei
= new EqcInfo(d_qstate
.getSatContext());
176 void ConjectureGenerator::setUniversalRelevant( TNode n
) {
177 //add pattern information
178 registerPattern( n
, n
.getType() );
179 d_urelevant_terms
[n
] = true;
180 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
181 setUniversalRelevant( n
[i
] );
185 bool ConjectureGenerator::isUniversalLessThan( TNode rt1
, TNode rt2
) {
186 //prefer the one that is (normal, smaller) lexographically
187 Assert(d_pattern_is_relevant
.find(rt1
) != d_pattern_is_relevant
.end());
188 Assert(d_pattern_is_relevant
.find(rt2
) != d_pattern_is_relevant
.end());
189 Assert(d_pattern_is_normal
.find(rt1
) != d_pattern_is_normal
.end());
190 Assert(d_pattern_is_normal
.find(rt2
) != d_pattern_is_normal
.end());
191 Assert(d_pattern_fun_sum
.find(rt1
) != d_pattern_fun_sum
.end());
192 Assert(d_pattern_fun_sum
.find(rt2
) != d_pattern_fun_sum
.end());
194 if( d_pattern_is_relevant
[rt1
] && !d_pattern_is_relevant
[rt2
] ){
195 Trace("thm-ee-debug") << "UEE : LT due to relevant." << std::endl
;
197 }else if( d_pattern_is_relevant
[rt1
]==d_pattern_is_relevant
[rt2
] ){
198 if( d_pattern_is_normal
[rt1
] && !d_pattern_is_normal
[rt2
] ){
199 Trace("thm-ee-debug") << "UEE : LT due to normal." << std::endl
;
201 }else if( d_pattern_is_normal
[rt1
]==d_pattern_is_normal
[rt2
] ){
202 if( d_pattern_fun_sum
[rt1
]<d_pattern_fun_sum
[rt2
] ){
203 Trace("thm-ee-debug") << "UEE : LT due to size." << std::endl
;
204 //decide which representative to use : based on size of the term
206 }else if( d_pattern_fun_sum
[rt1
]==d_pattern_fun_sum
[rt2
] ){
207 //same size : tie goes to term that has already been reported
208 return isReportedCanon( rt1
) && !isReportedCanon( rt2
);
216 bool ConjectureGenerator::isReportedCanon( TNode n
) {
217 return std::find( d_ue_canon
.begin(), d_ue_canon
.end(), n
)==d_ue_canon
.end();
220 void ConjectureGenerator::markReportedCanon( TNode n
) {
221 if( !isReportedCanon( n
) ){
222 d_ue_canon
.push_back( n
);
226 bool ConjectureGenerator::areUniversalEqual( TNode n1
, TNode n2
) {
227 return n1
==n2
|| ( d_uequalityEngine
.hasTerm( n1
) && d_uequalityEngine
.hasTerm( n2
) && d_uequalityEngine
.areEqual( n1
, n2
) );
230 bool ConjectureGenerator::areUniversalDisequal( TNode n1
, TNode n2
) {
231 return n1
!=n2
&& d_uequalityEngine
.hasTerm( n1
) && d_uequalityEngine
.hasTerm( n2
) && d_uequalityEngine
.areDisequal( n1
, n2
, false );
234 Node
ConjectureGenerator::getUniversalRepresentative(TNode n
, bool add
)
237 if( d_urelevant_terms
.find( n
)==d_urelevant_terms
.end() ){
238 setUniversalRelevant( n
);
239 //add term to universal equality engine
240 d_uequalityEngine
.addTerm( n
);
241 // addding this term to equality engine will lead to a set of new terms (the new subterms of n)
242 // now, do instantiation-based merging for each of these terms
243 Trace("thm-ee-debug") << "Merge equivalence classes based on instantiations of terms..." << std::endl
;
244 //merge all pending equalities
245 while( !d_upendingAdds
.empty() ){
246 Trace("sg-pending") << "Add " << d_upendingAdds
.size() << " pending terms..." << std::endl
;
247 std::vector
< Node
> pending
;
248 pending
.insert( pending
.end(), d_upendingAdds
.begin(), d_upendingAdds
.end() );
249 d_upendingAdds
.clear();
250 for( unsigned i
=0; i
<pending
.size(); i
++ ){
252 TypeNode tn
= t
.getType();
253 Trace("thm-ee-add") << "UEE : Add universal term " << t
<< std::endl
;
254 std::vector
< Node
> eq_terms
;
255 //if occurs modulo equality at ground level, it is equivalent to representative of ground equality engine
256 Node gt
= getTermDatabase()->evaluateTerm(t
);
257 if( !gt
.isNull() && gt
!=t
){
258 eq_terms
.push_back( gt
);
260 //get all equivalent terms based on theorem database
261 d_thm_index
.getEquivalentTerms( t
, eq_terms
);
262 if( !eq_terms
.empty() ){
263 Trace("thm-ee-add") << "UEE : Based on ground EE/theorem DB, it is equivalent to " << eq_terms
.size() << " terms : " << std::endl
;
264 //add equivalent terms as equalities to universal engine
265 for (const Node
& eqt
: eq_terms
)
267 Trace("thm-ee-add") << " " << eqt
<< std::endl
;
268 bool assertEq
= false;
269 if (d_urelevant_terms
.find(eqt
) != d_urelevant_terms
.end())
275 Assert(eqt
.getType() == tn
);
276 registerPattern(eqt
, tn
);
277 if (isUniversalLessThan(eqt
, t
)
278 || (options::conjectureUeeIntro()
279 && d_pattern_fun_sum
[t
] >= d_pattern_fun_sum
[eqt
]))
281 setUniversalRelevant(eqt
);
287 d_uequalityEngine
.assertEquality(t
.eqNode(eqt
), true, exp
);
289 Trace("thm-ee-no-add")
290 << "Do not add : " << t
<< " == " << eqt
<< std::endl
;
294 Trace("thm-ee-add") << "UEE : No equivalent terms." << std::endl
;
301 if( d_uequalityEngine
.hasTerm( n
) ){
302 Node r
= d_uequalityEngine
.getRepresentative( n
);
303 EqcInfo
* ei
= getOrMakeEqcInfo( r
);
304 if( ei
&& !ei
->d_rep
.get().isNull() ){
305 return ei
->d_rep
.get();
314 Node
ConjectureGenerator::getFreeVar( TypeNode tn
, unsigned i
) {
315 return d_termCanon
.getCanonicalFreeVar(tn
, i
);
318 bool ConjectureGenerator::isHandledTerm( TNode n
){
319 return d_quantEngine
->getTermDatabase()->isTermActive(n
)
320 && inst::TriggerTermInfo::isAtomicTrigger(n
)
321 && (n
.getKind() != APPLY_UF
|| n
.getOperator().getKind() != SKOLEM
);
324 Node
ConjectureGenerator::getGroundEqc( TNode r
) {
325 std::map
< TNode
, Node
>::iterator it
= d_ground_eqc_map
.find( r
);
326 return it
!=d_ground_eqc_map
.end() ? it
->second
: Node::null();
329 bool ConjectureGenerator::isGroundEqc( TNode r
) {
330 return d_ground_eqc_map
.find( r
)!=d_ground_eqc_map
.end();
333 bool ConjectureGenerator::isGroundTerm( TNode n
) {
334 return std::find( d_ground_terms
.begin(), d_ground_terms
.end(), n
)!=d_ground_terms
.end();
337 bool ConjectureGenerator::needsCheck( Theory::Effort e
) {
338 // synchonized with instantiation engine
339 return d_quantEngine
->getInstWhenNeedsCheck( e
);
342 bool ConjectureGenerator::hasEnumeratedUf( Node n
) {
343 if( options::conjectureGenGtEnum()>0 ){
344 std::map
< Node
, bool >::iterator it
= d_uf_enum
.find( n
.getOperator() );
345 if( it
==d_uf_enum
.end() ){
346 d_uf_enum
[n
.getOperator()] = true;
347 std::vector
< Node
> lem
;
348 getEnumeratePredUfTerm( n
, options::conjectureGenGtEnum(), lem
);
350 for (const Node
& l
: lem
)
352 d_qim
.addPendingLemma(l
);
354 d_hasAddedLemma
= true;
362 void ConjectureGenerator::reset_round( Theory::Effort e
) {
365 void ConjectureGenerator::check(Theory::Effort e
, QEffort quant_e
)
367 if (quant_e
== QEFFORT_STANDARD
)
370 if( d_fullEffortCount
%optFullCheckFrequency()==0 ){
371 d_hasAddedLemma
= false;
374 if( Trace
.isOn("sg-engine") ){
375 clSet
= double(clock())/double(CLOCKS_PER_SEC
);
376 Trace("sg-engine") << "---Conjecture Engine Round, effort = " << e
<< "---" << std::endl
;
378 eq::EqualityEngine
* ee
= getEqualityEngine();
381 Trace("sg-proc") << "Get eq classes..." << std::endl
;
382 d_op_arg_index
.clear();
383 d_ground_eqc_map
.clear();
384 d_bool_eqc
[0] = Node::null();
385 d_bool_eqc
[1] = Node::null();
386 std::vector
< TNode
> eqcs
;
388 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( ee
);
389 while( !eqcs_i
.isFinished() ){
391 Trace("sg-proc-debug") << "...eqc : " << r
<< std::endl
;
393 if( r
.getType().isBoolean() ){
394 if (areEqual(r
, d_true
))
396 d_ground_eqc_map
[r
] = d_true
;
399 else if (areEqual(r
, d_false
))
401 d_ground_eqc_map
[r
] = d_false
;
405 d_em
[r
] = eqcs
.size();
406 eq::EqClassIterator ieqc_i
= eq::EqClassIterator( r
, ee
);
407 while( !ieqc_i
.isFinished() ){
409 Trace("sg-proc-debug") << "......term : " << n
<< std::endl
;
410 if( getTermDatabase()->hasTermCurrent( n
) ){
411 if( isHandledTerm( n
) ){
412 getTermDatabase()->computeArgReps( n
);
413 d_op_arg_index
[r
].addTerm( getTermDatabase()->d_arg_reps
[n
], n
);
420 Assert(!d_bool_eqc
[0].isNull());
421 Assert(!d_bool_eqc
[1].isNull());
422 d_urelevant_terms
.clear();
423 Trace("sg-proc") << "...done get eq classes" << std::endl
;
425 Trace("sg-proc") << "Determine ground EQC..." << std::endl
;
429 for( unsigned i
=0; i
<eqcs
.size(); i
++ ){
431 if( d_ground_eqc_map
.find( r
)==d_ground_eqc_map
.end() ){
432 std::vector
< TNode
> args
;
433 Trace("sg-pat-debug") << "******* Get ground term for " << r
<< std::endl
;
435 if (Skolemize::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
, d_false
);
467 eq::EqClassIterator eqc_i
= eq::EqClassIterator( r
, ee
);
468 while( !eqc_i
.isFinished() ){
470 if( getTermDatabase()->hasTermCurrent( n
) && getTermDatabase()->isTermActive( n
) && ( 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 (TNode ar
: getTermDatabase()->d_arg_reps
[n
])
480 Trace("sg-gen-eqc") << " e" << d_em
[ar
];
482 Trace("sg-gen-eqc") << ") :: " << n
<< std::endl
;
484 Trace("sg-gen-eqc") << " " << n
<< std::endl
;
490 Trace("sg-gen-eqc") << "}" << std::endl
;
491 //print out ground term
492 std::map
< TNode
, Node
>::iterator it
= d_ground_eqc_map
.find( r
);
493 if( it
!=d_ground_eqc_map
.end() ){
494 Trace("sg-gen-eqc") << "- Ground term : " << it
->second
<< std::endl
;
500 Trace("sg-proc") << "Compute relevant eqc..." << std::endl
;
501 d_tge
.d_relevant_eqc
[0].clear();
502 d_tge
.d_relevant_eqc
[1].clear();
503 for( unsigned i
=0; i
<eqcs
.size(); i
++ ){
505 std::map
< TNode
, Node
>::iterator it
= d_ground_eqc_map
.find( r
);
507 if( it
==d_ground_eqc_map
.end() ){
510 //based on unproven conjectures? TODO
511 d_tge
.d_relevant_eqc
[index
].push_back( r
);
513 Trace("sg-gen-tg-debug") << "Initial relevant eqc : ";
514 for( unsigned i
=0; i
<d_tge
.d_relevant_eqc
[0].size(); i
++ ){
515 Trace("sg-gen-tg-debug") << "e" << d_em
[d_tge
.d_relevant_eqc
[0][i
]] << " ";
517 Trace("sg-gen-tg-debug") << std::endl
;
518 Trace("sg-proc") << "...done compute relevant eqc" << std::endl
;
521 Trace("sg-proc") << "Collect signature information..." << std::endl
;
522 d_tge
.collectSignatureInformation();
523 if( d_hasAddedLemma
){
524 Trace("sg-proc") << "...added enumeration lemmas." << std::endl
;
526 Trace("sg-proc") << "...done collect signature information" << std::endl
;
530 Trace("sg-proc") << "Build theorem index..." << std::endl
;
533 std::vector
< Node
> provenConj
;
534 quantifiers::FirstOrderModel
* m
= d_quantEngine
->getModel();
535 for( unsigned i
=0; i
<m
->getNumAssertedQuantifiers(); i
++ ){
536 Node q
= m
->getAssertedQuantifier( i
);
537 Trace("thm-db-debug") << "Is " << q
<< " a relevant theorem?" << std::endl
;
539 if( q
[1].getKind()==EQUAL
){
540 bool isSubsume
= false;
542 for( unsigned r
=0; r
<2; r
++ ){
543 TNode nl
= q
[1][r
==0 ? 0 : 1];
544 TNode nr
= q
[1][r
==0 ? 1 : 0];
545 Node eq
= nl
.eqNode( nr
);
546 if( r
==1 || std::find( d_conjectures
.begin(), d_conjectures
.end(), q
)==d_conjectures
.end() ){
547 //check if it contains only relevant functions
548 if( d_tge
.isRelevantTerm( eq
) ){
550 Trace("sg-proc-debug") << "get canonical " << eq
<< std::endl
;
551 eq
= d_termCanon
.getCanonicalTerm(eq
);
558 inEe
= d_ee_conjectures
.find( q
[1] )!=d_ee_conjectures
.end();
560 //add to universal equality engine
561 Node nlu
= getUniversalRepresentative(eq
[0], true);
562 Node nru
= getUniversalRepresentative(eq
[1], true);
563 if (areUniversalEqual(nlu
, nru
))
566 //set inactive (will be ignored by other modules)
567 d_quantEngine
->getModel()->setQuantifierActive( q
, false );
572 d_ee_conjectures
[q
[1]] = true;
573 d_uequalityEngine
.assertEquality(
574 nlu
.eqNode(nru
), true, exp
);
577 Trace("sg-conjecture") << "*** CONJECTURE : currently proven" << (isSubsume
? " and subsumed" : "");
578 Trace("sg-conjecture") << " : " << q
[1] << std::endl
;
579 provenConj
.push_back( q
);
582 Trace("thm-db-debug") << "Adding theorem to database " << eq
[0] << " == " << eq
[1] << std::endl
;
583 d_thm_index
.addTheorem( eq
[0], eq
[1] );
593 //examine status of other conjectures
594 for( unsigned i
=0; i
<d_conjectures
.size(); i
++ ){
595 Node q
= d_conjectures
[i
];
596 if( std::find( provenConj
.begin(), provenConj
.end(), q
)==provenConj
.end() ){
597 //check each skolem variable
598 bool disproven
= true;
599 std::vector
<Node
> skolems
;
600 d_quantEngine
->getSkolemize()->getSkolemConstants(q
, skolems
);
601 Trace("sg-conjecture") << " CONJECTURE : ";
602 std::vector
< Node
> ce
;
603 for (unsigned j
= 0; j
< skolems
.size(); j
++)
605 TNode rk
= getRepresentative(skolems
[j
]);
606 std::map
< TNode
, Node
>::iterator git
= d_ground_eqc_map
.find( rk
);
607 //check if it is a ground term
608 if( git
==d_ground_eqc_map
.end() ){
609 Trace("sg-conjecture") << "ACTIVE : " << q
;
610 if( Trace
.isOn("sg-gen-eqc") ){
611 Trace("sg-conjecture") << " { ";
612 for (unsigned k
= 0; k
< skolems
.size(); k
++)
614 Trace("sg-conjecture") << skolems
[k
] << (j
== k
? "*" : "")
617 Trace("sg-conjecture") << "}";
619 Trace("sg-conjecture") << std::endl
;
623 ce
.push_back( git
->second
);
627 Trace("sg-conjecture") << "disproven : " << q
<< " : ";
628 for (unsigned j
= 0, ceSize
= ce
.size(); j
< ceSize
; j
++)
630 Trace("sg-conjecture") << q
[0][j
] << " -> " << ce
[j
] << " ";
632 Trace("sg-conjecture") << std::endl
;
636 Trace("thm-db") << "Theorem database is : " << std::endl
;
637 d_thm_index
.debugPrint( "thm-db" );
638 Trace("thm-db") << std::endl
;
639 Trace("sg-proc") << "...done build theorem index" << std::endl
;
644 d_pattern_var_id
.clear();
645 d_pattern_var_duplicate
.clear();
646 d_pattern_is_normal
.clear();
647 d_pattern_is_relevant
.clear();
648 d_pattern_fun_id
.clear();
649 d_pattern_fun_sum
.clear();
650 d_rel_patterns
.clear();
651 d_rel_pattern_var_sum
.clear();
652 d_rel_pattern_typ_index
.clear();
653 d_rel_pattern_subs_index
.clear();
655 unsigned rel_term_count
= 0;
656 std::map
< TypeNode
, unsigned > rt_var_max
;
657 std::vector
< TypeNode
> rt_types
;
658 std::map
< TypeNode
, std::map
< int, std::vector
< Node
> > > conj_lhs
;
659 unsigned addedLemmas
= 0;
660 unsigned maxDepth
= options::conjectureGenMaxDepth();
661 for( unsigned depth
=1; depth
<=maxDepth
; depth
++ ){
662 Trace("sg-proc") << "Generate relevant LHS at depth " << depth
<< "..." << std::endl
;
663 Trace("sg-rel-term") << "Relevant terms of depth " << depth
<< " : " << std::endl
;
665 d_tge
.d_var_id
.clear();
666 d_tge
.d_var_limit
.clear();
667 d_tge
.reset( depth
, true, TypeNode::null() );
668 while( d_tge
.getNextTerm() ){
670 Node nn
= d_tge
.getTerm();
671 if( !options::conjectureFilterCanonical() || considerTermCanon( nn
, true ) ){
673 Trace("sg-rel-term") << "*** Relevant term : ";
674 d_tge
.debugPrint( "sg-rel-term", "sg-rel-term-debug2" );
675 Trace("sg-rel-term") << std::endl
;
677 for( unsigned r
=0; r
<2; r
++ ){
678 Trace("sg-rel-term-debug") << "...from equivalence classes (" << r
<< ") : ";
679 int index
= d_tge
.d_ccand_eqc
[r
].size()-1;
680 for( unsigned j
=0; j
<d_tge
.d_ccand_eqc
[r
][index
].size(); j
++ ){
681 Trace("sg-rel-term-debug") << "e" << d_em
[d_tge
.d_ccand_eqc
[r
][index
][j
]] << " ";
683 Trace("sg-rel-term-debug") << std::endl
;
685 TypeNode tnn
= nn
.getType();
686 Trace("sg-gen-tg-debug") << "...term is " << nn
<< std::endl
;
687 conj_lhs
[tnn
][depth
].push_back( nn
);
689 //add information about pattern
690 Trace("sg-gen-tg-debug") << "Collect pattern information..." << std::endl
;
691 Assert(std::find(d_rel_patterns
[tnn
].begin(),
692 d_rel_patterns
[tnn
].end(),
694 == d_rel_patterns
[tnn
].end());
695 d_rel_patterns
[tnn
].push_back( nn
);
696 //build information concerning the variables in this pattern
698 std::map
< TypeNode
, unsigned > typ_to_subs_index
;
699 std::vector
< TNode
> gsubs_vars
;
700 for( std::map
< TypeNode
, unsigned >::iterator it
= d_tge
.d_var_id
.begin(); it
!= d_tge
.d_var_id
.end(); ++it
){
702 typ_to_subs_index
[it
->first
] = sum
;
704 for( unsigned i
=0; i
<it
->second
; i
++ ){
705 gsubs_vars
.push_back(
706 d_termCanon
.getCanonicalFreeVar(it
->first
, i
));
710 d_rel_pattern_var_sum
[nn
] = sum
;
711 //register the pattern
712 registerPattern( nn
, tnn
);
713 Assert(d_pattern_is_normal
[nn
]);
714 Trace("sg-gen-tg-debug") << "...done collect pattern information" << std::endl
;
716 //record information about types
717 Trace("sg-gen-tg-debug") << "Collect type information..." << std::endl
;
718 PatternTypIndex
* pti
= &d_rel_pattern_typ_index
;
719 for( std::map
< TypeNode
, unsigned >::iterator it
= d_tge
.d_var_id
.begin(); it
!= d_tge
.d_var_id
.end(); ++it
){
720 pti
= &pti
->d_children
[it
->first
][it
->second
];
722 if( rt_var_max
.find( it
->first
)==rt_var_max
.end() || it
->second
>rt_var_max
[it
->first
] ){
723 rt_var_max
[it
->first
] = it
->second
;
726 if( std::find( rt_types
.begin(), rt_types
.end(), tnn
)==rt_types
.end() ){
727 rt_types
.push_back( tnn
);
729 pti
->d_terms
.push_back( nn
);
730 Trace("sg-gen-tg-debug") << "...done collect type information" << std::endl
;
732 Trace("sg-gen-tg-debug") << "Build substitutions for ground EQC..." << std::endl
;
733 std::vector
< TNode
> gsubs_terms
;
734 gsubs_terms
.resize( gsubs_vars
.size() );
735 int index
= d_tge
.d_ccand_eqc
[1].size()-1;
736 for( unsigned j
=0; j
<d_tge
.d_ccand_eqc
[1][index
].size(); j
++ ){
737 TNode r
= d_tge
.d_ccand_eqc
[1][index
][j
];
738 Trace("sg-rel-term-debug") << " Matches for e" << d_em
[r
] << ", which is ground term " << d_ground_eqc_map
[r
] << ":" << std::endl
;
739 std::map
< TypeNode
, std::map
< unsigned, TNode
> > subs
;
740 std::map
< TNode
, bool > rev_subs
;
741 //only get ground terms
743 d_tge
.resetMatching( r
, mode
);
744 while( d_tge
.getNextMatch( r
, subs
, rev_subs
) ){
745 //we will be building substitutions
746 bool firstTime
= true;
747 for( std::map
< TypeNode
, std::map
< unsigned, TNode
> >::iterator it
= subs
.begin(); it
!= subs
.end(); ++it
){
748 unsigned tindex
= typ_to_subs_index
[it
->first
];
749 for( std::map
< unsigned, TNode
>::iterator it2
= it
->second
.begin(); it2
!= it
->second
.end(); ++it2
){
751 Trace("sg-rel-term-debug") << ", ";
754 Trace("sg-rel-term-debug") << " ";
756 Trace("sg-rel-term-debug") << it
->first
<< ":x" << it2
->first
<< " -> " << it2
->second
;
757 Assert(tindex
+ it2
->first
< gsubs_terms
.size());
758 gsubs_terms
[tindex
+it2
->first
] = it2
->second
;
761 Trace("sg-rel-term-debug") << std::endl
;
762 d_rel_pattern_subs_index
[nn
].addSubstitution( r
, gsubs_vars
, gsubs_terms
);
765 Trace("sg-gen-tg-debug") << "...done build substitutions for ground EQC" << std::endl
;
767 Trace("sg-gen-tg-debug") << "> not canonical : " << nn
<< std::endl
;
770 Trace("sg-proc") << "...done generate terms at depth " << depth
<< std::endl
;
771 Trace("sg-stats") << "--------> Total LHS of depth " << depth
<< " : " << rel_term_count
<< std::endl
;
772 //Trace("conjecture-count") << "Total LHS of depth " << depth << " : " << conj_lhs[depth].size() << std::endl;
775 for( unsigned i=0; i<rt_types.size(); i++ ){
776 Trace("sg-term-enum") << "Term enumeration for " << rt_types[i] << " : " << std::endl;
777 Trace("sg-term-enum") << "Ground term : " << rt_types[i].mkGroundTerm() << std::endl;
778 for( unsigned j=0; j<150; j++ ){
779 Trace("sg-term-enum") << " " << getEnumerateTerm( rt_types[i], j ) << std::endl;
784 //consider types from relevant terms
785 for( unsigned rdepth
=0; rdepth
<=depth
; rdepth
++ ){
787 d_tge
.d_var_id
.clear();
788 d_tge
.d_var_limit
.clear();
789 for( std::map
< TypeNode
, unsigned >::iterator it
= rt_var_max
.begin(); it
!= rt_var_max
.end(); ++it
){
790 d_tge
.d_var_id
[ it
->first
] = it
->second
;
791 d_tge
.d_var_limit
[ it
->first
] = it
->second
;
793 std::shuffle(rt_types
.begin(), rt_types
.end(), Random::getRandom());
794 std::map
< TypeNode
, std::vector
< Node
> > conj_rhs
;
795 for( unsigned i
=0; i
<rt_types
.size(); i
++ ){
797 Trace("sg-proc") << "Generate relevant RHS terms of type " << rt_types
[i
] << " at depth " << rdepth
<< "..." << std::endl
;
798 d_tge
.reset( rdepth
, false, rt_types
[i
] );
800 while( d_tge
.getNextTerm() ){
801 Node rhs
= d_tge
.getTerm();
802 if( considerTermCanon( rhs
, false ) ){
803 Trace("sg-rel-prop") << "Relevant RHS : " << rhs
<< std::endl
;
805 Assert(rhs
.getType() == rt_types
[i
]);
806 registerPattern( rhs
, rt_types
[i
] );
808 //consider against all LHS at depth
809 for( unsigned j
=0; j
<conj_lhs
[rt_types
[i
]][depth
].size(); j
++ ){
810 processCandidateConjecture( conj_lhs
[rt_types
[i
]][depth
][j
], rhs
, depth
, rdepth
);
813 conj_rhs
[rt_types
[i
]].push_back( rhs
);
818 flushWaitingConjectures( addedLemmas
, depth
, rdepth
);
819 //consider against all LHS up to depth
821 for( unsigned lhs_depth
= 1; lhs_depth
<=depth
; lhs_depth
++ ){
822 if( (int)addedLemmas
<options::conjectureGenPerRound() ){
823 Trace("sg-proc") << "Consider conjectures at depth (" << lhs_depth
<< ", " << rdepth
<< ")..." << std::endl
;
824 for( std::map
< TypeNode
, std::vector
< Node
> >::iterator it
= conj_rhs
.begin(); it
!= conj_rhs
.end(); ++it
){
825 for( unsigned j
=0; j
<it
->second
.size(); j
++ ){
826 for( unsigned k
=0; k
<conj_lhs
[it
->first
][lhs_depth
].size(); k
++ ){
827 processCandidateConjecture( conj_lhs
[it
->first
][lhs_depth
][k
], it
->second
[j
], lhs_depth
, rdepth
);
831 flushWaitingConjectures( addedLemmas
, lhs_depth
, depth
);
835 if( (int)addedLemmas
>=options::conjectureGenPerRound() ){
839 if( (int)addedLemmas
>=options::conjectureGenPerRound() ){
843 Trace("sg-stats") << "Total conjectures considered : " << d_conj_count
<< std::endl
;
844 if( Trace
.isOn("thm-ee") ){
845 Trace("thm-ee") << "Universal equality engine is : " << std::endl
;
846 eq::EqClassesIterator ueqcs_i
= eq::EqClassesIterator( &d_uequalityEngine
);
847 while( !ueqcs_i
.isFinished() ){
848 TNode r
= (*ueqcs_i
);
849 bool firstTime
= true;
850 Node rr
= getUniversalRepresentative(r
);
851 Trace("thm-ee") << " " << rr
;
852 Trace("thm-ee") << " : { ";
853 eq::EqClassIterator ueqc_i
= eq::EqClassIterator( r
, &d_uequalityEngine
);
854 while( !ueqc_i
.isFinished() ){
858 Trace("thm-ee") << std::endl
;
861 Trace("thm-ee") << " " << n
<< std::endl
;
865 if( !firstTime
){ Trace("thm-ee") << " "; }
866 Trace("thm-ee") << "}" << std::endl
;
869 Trace("thm-ee") << std::endl
;
871 if( Trace
.isOn("sg-engine") ){
872 double clSet2
= double(clock())/double(CLOCKS_PER_SEC
);
873 Trace("sg-engine") << "Finished conjecture generator, time = " << (clSet2
-clSet
) << std::endl
;
879 unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas
, int ldepth
, int rdepth
) {
880 if( !d_waiting_conjectures_lhs
.empty() ){
881 Trace("sg-proc") << "Generated " << d_waiting_conjectures_lhs
.size() << " conjectures at depth " << ldepth
<< "/" << rdepth
<< "." << std::endl
;
882 if( (int)addedLemmas
<options::conjectureGenPerRound() ){
884 std::vector< unsigned > indices;
885 for( unsigned i=0; i<d_waiting_conjectures_lhs.size(); i++ ){
886 indices.push_back( i );
890 //sort them based on score
891 sortConjectureScore scs;
892 scs.d_scores.insert( scs.d_scores.begin(), d_waiting_conjectures_score.begin(), d_waiting_conjectures_score.end() );
893 std::sort( indices.begin(), indices.end(), scs );
895 //if( doSort && d_waiting_conjectures_score[indices[0]]<optFilterScoreThreshold() ){
897 unsigned prevCount
= d_conj_count
;
898 for( unsigned i
=0; i
<d_waiting_conjectures_lhs
.size(); i
++ ){
899 if( d_waiting_conjectures_score
[i
]>=optFilterScoreThreshold() ){
900 //we have determined a relevant subgoal
901 Node lhs
= d_waiting_conjectures_lhs
[i
];
902 Node rhs
= d_waiting_conjectures_rhs
[i
];
903 if( options::conjectureFilterCanonical() && ( getUniversalRepresentative( lhs
)!=lhs
|| getUniversalRepresentative( rhs
)!=rhs
) ){
906 Trace("sg-engine") << "*** Consider conjecture : " << lhs
<< " == " << rhs
<< std::endl
;
907 Trace("sg-engine-debug") << " score : " << d_waiting_conjectures_score
[i
] << std::endl
;
908 if( optStatsOnly() ){
911 std::vector
< Node
> bvs
;
912 for (const std::pair
<const TypeNode
, unsigned>& lhs_pattern
:
913 d_pattern_var_id
[lhs
])
915 for (unsigned j
= 0; j
<= lhs_pattern
.second
; j
++)
917 bvs
.push_back(getFreeVar(lhs_pattern
.first
, j
));
922 Node bvl
= NodeManager::currentNM()->mkNode( BOUND_VAR_LIST
, bvs
);
923 rsg
= NodeManager::currentNM()->mkNode( FORALL
, bvl
, lhs
.eqNode( rhs
) );
925 rsg
= lhs
.eqNode( rhs
);
927 rsg
= Rewriter::rewrite( rsg
);
928 d_conjectures
.push_back( rsg
);
929 d_eq_conjectures
[lhs
].push_back( rhs
);
930 d_eq_conjectures
[rhs
].push_back( lhs
);
932 Node lem
= NodeManager::currentNM()->mkNode( OR
, rsg
.negate(), rsg
);
933 d_qim
.addPendingLemma(lem
);
934 d_qim
.addPendingPhaseRequirement(rsg
, false);
936 if( (int)addedLemmas
>=options::conjectureGenPerRound() ){
943 Trace("sg-proc") << "...have now added " << addedLemmas
<< " conjecture lemmas." << std::endl
;
944 if( optStatsOnly() ){
945 Trace("sg-stats") << "Generated " << (d_conj_count
-prevCount
) << " conjectures at depth " << ldepth
<< "/" << rdepth
<< "." << std::endl
;
948 d_waiting_conjectures_lhs
.clear();
949 d_waiting_conjectures_rhs
.clear();
950 d_waiting_conjectures_score
.clear();
951 d_waiting_conjectures
.clear();
956 bool ConjectureGenerator::considerTermCanon( Node ln
, bool genRelevant
){
958 //do not consider if it is non-canonical, and either:
959 // (1) we are not generating relevant terms, or
960 // (2) its canonical form is a generalization.
961 Node lnr
= getUniversalRepresentative(ln
, true);
963 markReportedCanon( ln
);
964 }else if( !genRelevant
|| isGeneralization( lnr
, ln
) ){
965 Trace("sg-gen-consider-term") << "Do not consider term, " << ln
<< " is not canonical representation (which is " << lnr
<< ")." << std::endl
;
969 Trace("sg-gen-tg-debug") << "Will consider term canon " << ln
<< std::endl
;
970 Trace("sg-gen-consider-term-debug") << std::endl
;
974 unsigned ConjectureGenerator::collectFunctions( TNode opat
, TNode pat
, std::map
< TNode
, unsigned >& funcs
,
975 std::map
< TypeNode
, unsigned >& mnvn
, std::map
< TypeNode
, unsigned >& mxvn
){
976 if( pat
.hasOperator() ){
977 funcs
[pat
.getOperator()]++;
978 if( !d_tge
.isRelevantFunc( pat
.getOperator() ) ){
979 d_pattern_is_relevant
[opat
] = false;
982 for( unsigned i
=0; i
<pat
.getNumChildren(); i
++ ){
983 sum
+= collectFunctions( opat
, pat
[i
], funcs
, mnvn
, mxvn
);
987 Assert(pat
.getNumChildren() == 0);
990 if( pat
.getKind()==BOUND_VARIABLE
){
993 d_pattern_var_duplicate
[opat
]++;
996 TypeNode tn
= pat
.getType();
997 unsigned vn
= pat
.getAttribute(InstVarNumAttribute());
998 std::map
< TypeNode
, unsigned >::iterator it
= mnvn
.find( tn
);
999 if( it
!=mnvn
.end() ){
1000 if( vn
<it
->second
){
1001 d_pattern_is_normal
[opat
] = false;
1003 }else if( vn
>mxvn
[tn
] ){
1004 if( vn
!=mxvn
[tn
]+1 ){
1005 d_pattern_is_normal
[opat
] = false;
1010 //first variable of this type
1016 d_pattern_is_relevant
[opat
] = false;
1022 void ConjectureGenerator::registerPattern( Node pat
, TypeNode tpat
) {
1023 if( std::find( d_patterns
[tpat
].begin(), d_patterns
[tpat
].end(), pat
)==d_patterns
[tpat
].end() ){
1024 d_patterns
[TypeNode::null()].push_back( pat
);
1025 d_patterns
[tpat
].push_back( pat
);
1027 Assert(d_pattern_fun_id
.find(pat
) == d_pattern_fun_id
.end());
1028 Assert(d_pattern_var_id
.find(pat
) == d_pattern_var_id
.end());
1031 std::map
< TypeNode
, unsigned > mnvn
;
1032 d_pattern_fun_sum
[pat
] = collectFunctions( pat
, pat
, d_pattern_fun_id
[pat
], mnvn
, d_pattern_var_id
[pat
] );
1033 if( d_pattern_is_normal
.find( pat
)==d_pattern_is_normal
.end() ){
1034 d_pattern_is_normal
[pat
] = true;
1036 if( d_pattern_is_relevant
.find( pat
)==d_pattern_is_relevant
.end() ){
1037 d_pattern_is_relevant
[pat
] = true;
1042 bool ConjectureGenerator::isGeneralization( TNode patg
, TNode pat
, std::map
< TNode
, TNode
>& subs
) {
1043 if( patg
.getKind()==BOUND_VARIABLE
){
1044 std::map
< TNode
, TNode
>::iterator it
= subs
.find( patg
);
1045 if( it
!=subs
.end() ){
1046 return it
->second
==pat
;
1052 Assert(patg
.hasOperator());
1053 if( !pat
.hasOperator() || patg
.getOperator()!=pat
.getOperator() ){
1056 Assert(patg
.getNumChildren() == pat
.getNumChildren());
1057 for( unsigned i
=0; i
<patg
.getNumChildren(); i
++ ){
1058 if( !isGeneralization( patg
[i
], pat
[i
], subs
) ){
1067 int ConjectureGenerator::calculateGeneralizationDepth( TNode n
, std::vector
< TNode
>& fv
) {
1068 if( n
.getKind()==BOUND_VARIABLE
){
1069 if( std::find( fv
.begin(), fv
.end(), n
)==fv
.end() ){
1077 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
1078 depth
+= calculateGeneralizationDepth( n
[i
], fv
);
1084 Node
ConjectureGenerator::getPredicateForType( TypeNode tn
) {
1085 std::map
< TypeNode
, Node
>::iterator it
= d_typ_pred
.find( tn
);
1086 if( it
==d_typ_pred
.end() ){
1087 TypeNode op_tn
= NodeManager::currentNM()->mkFunctionType( tn
, NodeManager::currentNM()->booleanType() );
1088 Node op
= NodeManager::currentNM()->mkSkolem( "PE", op_tn
, "was created by conjecture ground term enumerator." );
1089 d_typ_pred
[tn
] = op
;
1096 void ConjectureGenerator::getEnumerateUfTerm( Node n
, unsigned num
, std::vector
< Node
>& terms
) {
1097 if( n
.getNumChildren()>0 ){
1098 Trace("sg-gt-enum-debug") << "Get enumerate uf terms " << n
<< " (" << num
1099 << ")" << std::endl
;
1100 TermEnumeration
* te
= d_quantEngine
->getTermEnumeration();
1101 // below, we do a fair enumeration of vectors vec of indices whose sum is
1103 std::vector
< int > vec
;
1104 std::vector
< TypeNode
> types
;
1105 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
1107 TypeNode tn
= n
[i
].getType();
1108 if (tn
.isClosedEnumerable())
1110 types
.push_back( tn
);
1115 // the index of the last child is determined by the limit of the sum
1116 // of indices of children (size_limit) and the sum of the indices of the
1117 // other children (vec_sum). Hence, we pop here and add this value at each
1118 // iteration of the loop.
1123 unsigned last_size
= terms
.size();
1124 while( terms
.size()<num
){
1127 // we will construct a new child below
1128 // since sum is 0, the index of last child is limit
1129 vec
.push_back( size_limit
);
1131 else if (index
< vec
.size())
1133 Assert(index
< types
.size());
1134 //see if we can iterate current
1135 if (vec_sum
< size_limit
1136 && !te
->getEnumerateTerm(types
[index
], vec
[index
] + 1).isNull())
1140 // we will construct a new child below
1141 // add the index of the last child, its index is (limit-sum)
1142 vec
.push_back( size_limit
- vec_sum
);
1145 vec_sum
-= vec
[index
];
1150 if (index
< vec
.size())
1152 // if we are ready to construct the term
1153 if( vec
.size()==n
.getNumChildren() ){
1155 te
->getEnumerateTerm(types
[vec
.size() - 1], vec
[vec
.size() - 1]);
1157 for( unsigned i
=0; i
<vec
.size(); i
++ ){
1158 Trace("sg-gt-enum-debug") << vec
[i
] << " ";
1160 Trace("sg-gt-enum-debug") << " / " << size_limit
<< std::endl
;
1161 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
1162 Trace("sg-gt-enum-debug") << n
[i
].getType() << " ";
1164 Trace("sg-gt-enum-debug") << std::endl
;
1165 std::vector
< Node
> children
;
1166 children
.push_back( n
.getOperator() );
1167 for( unsigned i
=0; i
<(vec
.size()-1); i
++ ){
1168 Node nn
= te
->getEnumerateTerm(types
[i
], vec
[i
]);
1169 Assert(!nn
.isNull());
1170 Assert(nn
.getType() == n
[i
].getType());
1171 children
.push_back( nn
);
1173 children
.push_back( lc
);
1174 Node nenum
= NodeManager::currentNM()->mkNode(APPLY_UF
, children
);
1176 << "Ground term enumerate : " << nenum
<< std::endl
;
1177 terms
.push_back(nenum
);
1179 // pop the index for the last child
1184 // no more indices to increment, we reset and increment size_limit
1185 if( terms
.size()>last_size
){
1186 last_size
= terms
.size();
1188 for( unsigned i
=0; i
<vec
.size(); i
++ ){
1193 // No terms were generated at the previous size.
1194 // Thus, we've saturated, no more terms can be enumerated.
1200 terms
.push_back( n
);
1204 void ConjectureGenerator::getEnumeratePredUfTerm( Node n
, unsigned num
, std::vector
< Node
>& terms
) {
1205 std::vector
< Node
> uf_terms
;
1206 getEnumerateUfTerm( n
, num
, uf_terms
);
1207 Node p
= getPredicateForType( n
.getType() );
1208 for( unsigned i
=0; i
<uf_terms
.size(); i
++ ){
1209 terms
.push_back( NodeManager::currentNM()->mkNode( APPLY_UF
, p
, uf_terms
[i
] ) );
1213 void ConjectureGenerator::processCandidateConjecture( TNode lhs
, TNode rhs
, unsigned lhs_depth
, unsigned rhs_depth
) {
1214 int score
= considerCandidateConjecture( lhs
, rhs
);
1216 Trace("sg-conjecture") << "* Candidate conjecture : " << lhs
<< " == " << rhs
<< std::endl
;
1217 Trace("sg-conjecture-debug") << " LHS, RHS generalization depth : " << lhs_depth
<< ", " << rhs_depth
<< std::endl
;
1218 Trace("sg-conjecture-debug") << " confirmed = " << d_subs_confirmCount
<< ", #witnesses range = " << d_subs_confirmWitnessRange
.size() << "." << std::endl
;
1219 Trace("sg-conjecture-debug") << " #witnesses for ";
1220 bool firstTime
= true;
1221 for( std::map
< TNode
, std::vector
< TNode
> >::iterator it
= d_subs_confirmWitnessDomain
.begin(); it
!= d_subs_confirmWitnessDomain
.end(); ++it
){
1223 Trace("sg-conjecture-debug") << ", ";
1225 Trace("sg-conjecture-debug") << it
->first
<< " : " << it
->second
.size();
1226 //if( it->second.size()==1 ){
1227 // Trace("sg-conjecture-debug") << " (" << it->second[0] << ")";
1229 Trace("sg-conjecture-debug2") << " (";
1230 for( unsigned j
=0; j
<it
->second
.size(); j
++ ){
1231 if( j
>0 ){ Trace("sg-conjecture-debug2") << " "; }
1232 Trace("sg-conjecture-debug2") << d_ground_eqc_map
[it
->second
[j
]];
1234 Trace("sg-conjecture-debug2") << ")";
1237 Trace("sg-conjecture-debug") << std::endl
;
1238 Trace("sg-conjecture-debug") << " unknown = " << d_subs_unkCount
<< std::endl
;
1239 //Assert( getUniversalRepresentative( rhs )==rhs );
1240 //Assert( getUniversalRepresentative( lhs )==lhs );
1241 d_waiting_conjectures_lhs
.push_back( lhs
);
1242 d_waiting_conjectures_rhs
.push_back( rhs
);
1243 d_waiting_conjectures_score
.push_back( score
);
1244 d_waiting_conjectures
[lhs
].push_back( rhs
);
1245 d_waiting_conjectures
[rhs
].push_back( lhs
);
1247 Trace("sg-conjecture-debug2") << "...do not consider " << lhs
<< " == " << rhs
<< ", score = " << score
<< std::endl
;
1251 int ConjectureGenerator::considerCandidateConjecture( TNode lhs
, TNode rhs
) {
1252 Assert(lhs
.getType() == rhs
.getType());
1254 Trace("sg-cconj-debug") << "Consider candidate conjecture : " << lhs
<< " == " << rhs
<< "?" << std::endl
;
1256 Trace("sg-cconj-debug") << " -> trivial." << std::endl
;
1259 if( lhs
.getKind()==APPLY_CONSTRUCTOR
&& rhs
.getKind()==APPLY_CONSTRUCTOR
){
1260 Trace("sg-cconj-debug") << " -> irrelevant by syntactic analysis." << std::endl
;
1263 //variables of LHS must subsume variables of RHS
1264 for( std::map
< TypeNode
, unsigned >::iterator it
= d_pattern_var_id
[rhs
].begin(); it
!= d_pattern_var_id
[rhs
].end(); ++it
){
1265 std::map
< TypeNode
, unsigned >::iterator itl
= d_pattern_var_id
[lhs
].find( it
->first
);
1266 if( itl
!=d_pattern_var_id
[lhs
].end() ){
1267 if( itl
->second
<it
->second
){
1268 Trace("sg-cconj-debug") << " -> variables of sort " << it
->first
<< " are not subsumed." << std::endl
;
1271 Trace("sg-cconj-debug2") << " variables of sort " << it
->first
<< " are : " << itl
->second
<< " vs " << it
->second
<< std::endl
;
1274 Trace("sg-cconj-debug") << " -> has no variables of sort " << it
->first
<< "." << std::endl
;
1279 //currently active conjecture?
1280 std::map
< Node
, std::vector
< Node
> >::iterator iteq
= d_eq_conjectures
.find( lhs
);
1281 if( iteq
!=d_eq_conjectures
.end() ){
1282 if( std::find( iteq
->second
.begin(), iteq
->second
.end(), rhs
)!=iteq
->second
.end() ){
1283 Trace("sg-cconj-debug") << " -> this conjecture is already active." << std::endl
;
1287 //current a waiting conjecture?
1288 std::map
< Node
, std::vector
< Node
> >::iterator itw
= d_waiting_conjectures
.find( lhs
);
1289 if( itw
!=d_waiting_conjectures
.end() ){
1290 if( std::find( itw
->second
.begin(), itw
->second
.end(), rhs
)!=itw
->second
.end() ){
1291 Trace("sg-cconj-debug") << " -> already are considering this conjecture." << std::endl
;
1295 //check if canonical representation (should be, but for efficiency this is not guarenteed)
1296 //if( options::conjectureFilterCanonical() && ( getUniversalRepresentative( lhs )!=lhs || getUniversalRepresentative( rhs )!=rhs ) ){
1297 // Trace("sg-cconj") << " -> after processing, not canonical." << std::endl;
1302 bool scoreSet
= false;
1304 Trace("sg-cconj") << "Consider possible candidate conjecture : " << lhs
<< " == " << rhs
<< "?" << std::endl
;
1305 //find witness for counterexample, if possible
1306 if( options::conjectureFilterModel() ){
1307 Assert(d_rel_pattern_var_sum
.find(lhs
) != d_rel_pattern_var_sum
.end());
1308 Trace("sg-cconj-debug") << "Notify substitutions over " << d_rel_pattern_var_sum
[lhs
] << " variables." << std::endl
;
1309 std::map
< TNode
, TNode
> subs
;
1310 d_subs_confirmCount
= 0;
1311 d_subs_confirmWitnessRange
.clear();
1312 d_subs_confirmWitnessDomain
.clear();
1313 d_subs_unkCount
= 0;
1314 if( !d_rel_pattern_subs_index
[lhs
].notifySubstitutions( this, subs
, rhs
, d_rel_pattern_var_sum
[lhs
] ) ){
1315 Trace("sg-cconj") << " -> found witness that falsifies the conjecture." << std::endl
;
1318 //score is the minimum number of distinct substitutions for a variable
1319 for( std::map
< TNode
, std::vector
< TNode
> >::iterator it
= d_subs_confirmWitnessDomain
.begin(); it
!= d_subs_confirmWitnessDomain
.end(); ++it
){
1320 int num
= (int)it
->second
.size();
1321 if( !scoreSet
|| num
<score
){
1329 Trace("sg-cconj") << " confirmed = " << d_subs_confirmCount
<< ", #witnesses range = " << d_subs_confirmWitnessRange
.size() << "." << std::endl
;
1330 for( std::map
< TNode
, std::vector
< TNode
> >::iterator it
= d_subs_confirmWitnessDomain
.begin(); it
!= d_subs_confirmWitnessDomain
.end(); ++it
){
1331 Trace("sg-cconj") << " #witnesses for " << it
->first
<< " : " << it
->second
.size() << std::endl
;
1337 Trace("sg-cconj") << " -> SUCCESS." << std::endl
;
1338 Trace("sg-cconj") << " score : " << score
<< std::endl
;
1344 bool ConjectureGenerator::notifySubstitution( TNode glhs
, std::map
< TNode
, TNode
>& subs
, TNode rhs
) {
1345 if( Trace
.isOn("sg-cconj-debug") ){
1346 Trace("sg-cconj-debug") << "Ground eqc for LHS : " << glhs
<< ", based on substituion: " << std::endl
;
1347 for( std::map
< TNode
, TNode
>::iterator it
= subs
.begin(); it
!= subs
.end(); ++it
){
1348 Assert(getRepresentative(it
->second
) == it
->second
);
1349 Trace("sg-cconj-debug") << " " << it
->first
<< " -> " << it
->second
<< std::endl
;
1352 Trace("sg-cconj-debug") << "Evaluate RHS : : " << rhs
<< std::endl
;
1353 //get the representative of rhs with substitution subs
1354 TNode grhs
= getTermDatabase()->getEntailedTerm( rhs
, subs
, true );
1355 Trace("sg-cconj-debug") << "...done evaluating term, got : " << grhs
<< std::endl
;
1356 if( !grhs
.isNull() ){
1358 Trace("sg-cconj-debug") << "Ground eqc for RHS : " << grhs
<< std::endl
;
1359 //check based on ground terms
1360 std::map
< TNode
, Node
>::iterator itl
= d_ground_eqc_map
.find( glhs
);
1361 if( itl
!=d_ground_eqc_map
.end() ){
1362 std::map
< TNode
, Node
>::iterator itr
= d_ground_eqc_map
.find( grhs
);
1363 if( itr
!=d_ground_eqc_map
.end() ){
1364 Trace("sg-cconj-debug") << "We have ground terms " << itl
->second
<< " and " << itr
->second
<< "." << std::endl
;
1365 if( itl
->second
.isConst() && itr
->second
.isConst() ){
1366 Trace("sg-cconj-debug") << "...disequal constants." << std::endl
;
1367 Trace("sg-cconj-witness") << " Witness of falsification : " << itl
->second
<< " != " << itr
->second
<< ", substutition is : " << std::endl
;
1368 for( std::map
< TNode
, TNode
>::iterator it
= subs
.begin(); it
!= subs
.end(); ++it
){
1369 Trace("sg-cconj-witness") << " " << it
->first
<< " -> " << it
->second
<< std::endl
;
1376 Trace("sg-cconj-debug") << "RHS is identical." << std::endl
;
1377 bool isGroundSubs
= true;
1378 for( std::map
< TNode
, TNode
>::iterator it
= subs
.begin(); it
!= subs
.end(); ++it
){
1379 std::map
< TNode
, Node
>::iterator git
= d_ground_eqc_map
.find( it
->second
);
1380 if( git
==d_ground_eqc_map
.end() ){
1381 isGroundSubs
= false;
1387 Trace("sg-cconj-witness") << " Witnessed " << glhs
<< " == " << grhs
<< ", substutition is : " << std::endl
;
1388 for( std::map
< TNode
, TNode
>::iterator it
= subs
.begin(); it
!= subs
.end(); ++it
){
1389 Trace("sg-cconj-witness") << " " << it
->first
<< " -> " << it
->second
<< std::endl
;
1390 if( std::find( d_subs_confirmWitnessDomain
[it
->first
].begin(), d_subs_confirmWitnessDomain
[it
->first
].end(), it
->second
)==d_subs_confirmWitnessDomain
[it
->first
].end() ){
1391 d_subs_confirmWitnessDomain
[it
->first
].push_back( it
->second
);
1394 d_subs_confirmCount
++;
1395 if( std::find( d_subs_confirmWitnessRange
.begin(), d_subs_confirmWitnessRange
.end(), glhs
)==d_subs_confirmWitnessRange
.end() ){
1396 d_subs_confirmWitnessRange
.push_back( glhs
);
1399 if( optFilterUnknown() ){
1400 Trace("sg-cconj-debug") << "...ground substitution giving terms that are neither equal nor disequal." << std::endl
;
1406 Trace("sg-cconj-debug") << "(could not ground eqc for RHS)." << std::endl
;
1416 void TermGenerator::reset( TermGenEnv
* s
, TypeNode tn
) {
1417 Assert(d_children
.empty());
1422 Trace("sg-gen-tg-debug2") << "...add to context " << this << std::endl
;
1424 s
->changeContext( true );
1427 bool TermGenerator::getNextTerm( TermGenEnv
* s
, unsigned depth
) {
1428 if( Trace
.isOn("sg-gen-tg-debug2") ){
1429 Trace("sg-gen-tg-debug2") << this << " getNextTerm depth " << depth
<< " : status = " << d_status
<< ", num = " << d_status_num
;
1431 TNode f
= s
->getTgFunc( d_typ
, d_status_num
);
1432 Trace("sg-gen-tg-debug2") << ", f = " << f
;
1433 Trace("sg-gen-tg-debug2") << ", #args = " << s
->d_func_args
[f
].size();
1434 Trace("sg-gen-tg-debug2") << ", childNum = " << d_status_child_num
;
1435 Trace("sg-gen-tg-debug2") << ", #children = " << d_children
.size();
1437 Trace("sg-gen-tg-debug2") << std::endl
;
1442 if( !d_typ
.isNull() ){
1443 if( s
->allowVar( d_typ
) ){
1445 d_status_num
= s
->d_var_id
[d_typ
];
1447 Trace("sg-gen-tg-debug2") << this << " ...return unique var #" << d_status_num
<< std::endl
;
1448 return s
->considerCurrentTerm() ? true : getNextTerm( s
, depth
);
1450 //check allocating new variable
1453 if( s
->d_gen_relevant_terms
){
1456 return getNextTerm( s
, depth
);
1461 return getNextTerm( s
, depth
);
1463 }else if( d_status
==2 ){
1464 //cleanup previous information
1465 //if( d_status_num>=0 ){
1466 // s->d_var_eq_tg[d_status_num].pop_back();
1468 //check if there is another variable
1469 if( (d_status_num
+1)<(int)s
->getNumTgVars( d_typ
) ){
1471 //we have equated two variables
1472 //s->d_var_eq_tg[d_status_num].push_back( d_id );
1473 Trace("sg-gen-tg-debug2") << this << "...consider other var #" << d_status_num
<< std::endl
;
1474 return s
->considerCurrentTerm() ? true : getNextTerm( s
, depth
);
1476 if( s
->d_gen_relevant_terms
){
1480 return getNextTerm( s
, depth
);
1482 }else if( d_status
==4 ){
1484 if( depth
>0 && (d_status_num
+1)<(int)s
->getNumTgFuncs( d_typ
) ){
1486 d_status_child_num
= 0;
1487 Trace("sg-gen-tg-debug2") << this << "...consider function " << s
->getTgFunc( d_typ
, d_status_num
) << std::endl
;
1489 if( !s
->considerCurrentTerm() ){
1491 //don't consider this function
1494 //we have decided on a function application
1496 return getNextTerm( s
, depth
);
1498 //do not choose function applications at depth 0
1500 return getNextTerm( s
, depth
);
1502 }else if( d_status
==5 ){
1503 //iterating over arguments
1504 TNode f
= s
->getTgFunc( d_typ
, d_status_num
);
1505 if( d_status_child_num
<0 ){
1509 return getNextTerm( s
, depth
);
1510 }else if( d_status_child_num
==(int)s
->d_func_args
[f
].size() ){
1511 d_status_child_num
--;
1512 return s
->considerCurrentTermCanon( d_id
) ? true : getNextTerm( s
, depth
);
1515 Assert(d_status_child_num
< (int)s
->d_func_args
[f
].size());
1516 if( d_status_child_num
==(int)d_children
.size() ){
1517 d_children
.push_back( s
->d_tg_id
);
1518 Assert(s
->d_tg_alloc
.find(s
->d_tg_id
) == s
->d_tg_alloc
.end());
1519 s
->d_tg_alloc
[d_children
[d_status_child_num
]].reset( s
, s
->d_func_args
[f
][d_status_child_num
] );
1520 return getNextTerm( s
, depth
);
1522 Assert(d_status_child_num
+ 1 == (int)d_children
.size());
1523 if( s
->d_tg_alloc
[d_children
[d_status_child_num
]].getNextTerm( s
, depth
-1 ) ){
1524 d_status_child_num
++;
1525 return getNextTerm( s
, depth
);
1527 Trace("sg-gen-tg-debug2")
1528 << "...remove child from context " << std::endl
;
1529 s
->changeContext(false);
1530 d_children
.pop_back();
1531 d_status_child_num
--;
1532 return getNextTerm( s
, depth
);
1536 }else if( d_status
==1 || d_status
==3 ){
1538 s
->removeVar( d_typ
);
1539 Assert(d_status_num
== (int)s
->d_var_id
[d_typ
]);
1540 //check if there is only one feasible equivalence class. if so, don't make pattern any more specific.
1541 //unsigned i = s->d_ccand_eqc[0].size()-1;
1542 //if( s->d_ccand_eqc[0][i].size()==1 && s->d_ccand_eqc[1][i].empty() ){
1544 // return getNextTerm( s, depth );
1550 return getNextTerm( s
, depth
);
1552 Assert(d_children
.empty());
1557 void TermGenerator::resetMatching( TermGenEnv
* s
, TNode eqc
, unsigned mode
) {
1559 d_match_status_child_num
= 0;
1560 d_match_children
.clear();
1561 d_match_children_end
.clear();
1562 d_match_mode
= mode
;
1563 //if this term generalizes, it must generalize a non-ground term
1564 //if( (d_match_mode & ( 1 << 2 ))!=0 && s->isGroundEqc( eqc ) && d_status==5 ){
1565 // d_match_status = -1;
1569 bool TermGenerator::getNextMatch( TermGenEnv
* s
, TNode eqc
, std::map
< TypeNode
, std::map
< unsigned, TNode
> >& subs
, std::map
< TNode
, bool >& rev_subs
) {
1570 if( d_match_status
<0 ){
1573 if( Trace
.isOn("sg-gen-tg-match") ){
1574 Trace("sg-gen-tg-match") << "Matching ";
1575 debugPrint( s
, "sg-gen-tg-match", "sg-gen-tg-match" );
1576 Trace("sg-gen-tg-match") << " with eqc e" << s
->d_cg
->d_em
[eqc
] << "..." << std::endl
;
1577 Trace("sg-gen-tg-match") << " mstatus = " << d_match_status
;
1579 TNode f
= s
->getTgFunc( d_typ
, d_status_num
);
1580 Trace("sg-gen-tg-debug2") << ", f = " << f
;
1581 Trace("sg-gen-tg-debug2") << ", #args = " << s
->d_func_args
[f
].size();
1582 Trace("sg-gen-tg-debug2") << ", mchildNum = " << d_match_status_child_num
;
1583 Trace("sg-gen-tg-debug2") << ", #mchildren = " << d_match_children
.size();
1585 Trace("sg-gen-tg-debug2") << ", current substitution : {";
1586 for( std::map
< TypeNode
, std::map
< unsigned, TNode
> >::iterator itt
= subs
.begin(); itt
!= subs
.end(); ++itt
){
1587 for( std::map
< unsigned, TNode
>::iterator it
= itt
->second
.begin(); it
!= itt
->second
.end(); ++it
){
1588 Trace("sg-gen-tg-debug2") << " " << it
->first
<< " -> e" << s
->d_cg
->d_em
[it
->second
];
1591 Trace("sg-gen-tg-debug2") << " } " << std::endl
;
1595 if( d_match_status
==0 ){
1597 if( (d_match_mode
& ( 1 << 1 ))!=0 ){
1599 if( !s
->isGroundEqc( eqc
) ){
1602 }else if( (d_match_mode
& ( 1 << 2 ))!=0 ){
1603 //only non-ground terms
1604 //if( s->isGroundEqc( eqc ) ){
1608 //store the match : restricted if match_mode.0 = 1
1609 if( (d_match_mode
& ( 1 << 0 ))!=0 ){
1610 std::map
< TNode
, bool >::iterator it
= rev_subs
.find( eqc
);
1611 if( it
==rev_subs
.end() ){
1612 rev_subs
[eqc
] = true;
1617 Assert(subs
[d_typ
].find(d_status_num
) == subs
[d_typ
].end());
1618 subs
[d_typ
][d_status_num
] = eqc
;
1622 subs
[d_typ
].erase( d_status_num
);
1623 if( (d_match_mode
& ( 1 << 0 ))!=0 ){
1624 rev_subs
.erase( eqc
);
1628 }else if( d_status
==2 ){
1629 if( d_match_status
==0 ){
1631 Assert(d_status_num
< (int)s
->getNumTgVars(d_typ
));
1632 std::map
< unsigned, TNode
>::iterator it
= subs
[d_typ
].find( d_status_num
);
1633 Assert(it
!= subs
[d_typ
].end());
1634 return it
->second
==eqc
;
1638 }else if( d_status
==5 ){
1639 //Assert( d_match_children.size()<=d_children.size() );
1640 //enumerating over f-applications in eqc
1641 if( d_match_status_child_num
<0 ){
1643 }else if( d_match_status
==0 ){
1644 //set up next binding
1645 if( d_match_status_child_num
==(int)d_match_children
.size() ){
1646 if( d_match_status_child_num
==0 ){
1648 TNode f
= s
->getTgFunc( d_typ
, d_status_num
);
1649 Assert(!eqc
.isNull());
1650 TNodeTrie
* tat
= s
->getTermDatabase()->getTermArgTrie(eqc
, f
);
1652 d_match_children
.push_back( tat
->d_data
.begin() );
1653 d_match_children_end
.push_back( tat
->d_data
.end() );
1656 d_match_status_child_num
--;
1657 return getNextMatch( s
, eqc
, subs
, rev_subs
);
1660 d_match_children
.push_back( d_match_children
[d_match_status_child_num
-1]->second
.d_data
.begin() );
1661 d_match_children_end
.push_back( d_match_children
[d_match_status_child_num
-1]->second
.d_data
.end() );
1665 Assert(d_match_status_child_num
+ 1 == (int)d_match_children
.size());
1666 if( d_match_children
[d_match_status_child_num
]==d_match_children_end
[d_match_status_child_num
] ){
1667 //no more arguments to bind
1668 d_match_children
.pop_back();
1669 d_match_children_end
.pop_back();
1670 d_match_status_child_num
--;
1671 return getNextMatch( s
, eqc
, subs
, rev_subs
);
1673 if( d_match_status_child_num
==(int)d_children
.size() ){
1674 //successfully matched all children
1675 d_match_children
.pop_back();
1676 d_match_children_end
.pop_back();
1677 d_match_status_child_num
--;
1678 return true;//return d_match_children[d_match_status]!=d_match_children_end[d_match_status];
1681 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
);
1682 return getNextMatch( s
, eqc
, subs
, rev_subs
);
1686 Assert(d_match_status
== 1);
1687 Assert(d_match_status_child_num
+ 1 == (int)d_match_children
.size());
1688 Assert(d_match_children
[d_match_status_child_num
]
1689 != d_match_children_end
[d_match_status_child_num
]);
1691 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
) ){
1692 d_match_status_child_num
++;
1693 return getNextMatch( s
, eqc
, subs
, rev_subs
);
1696 d_match_children
[d_match_status_child_num
]++;
1697 return getNextMatch( s
, eqc
, subs
, rev_subs
);
1705 unsigned TermGenerator::getDepth( TermGenEnv
* s
) {
1708 for( unsigned i
=0; i
<d_children
.size(); i
++ ){
1709 unsigned d
= s
->d_tg_alloc
[d_children
[i
]].getDepth( s
);
1720 unsigned TermGenerator::calculateGeneralizationDepth( TermGenEnv
* s
, std::map
< TypeNode
, std::vector
< int > >& fvs
) {
1723 for( unsigned i
=0; i
<d_children
.size(); i
++ ){
1724 sum
+= s
->d_tg_alloc
[d_children
[i
]].calculateGeneralizationDepth( s
, fvs
);
1728 Assert(d_status
== 2 || d_status
== 1);
1729 std::map
< TypeNode
, std::vector
< int > >::iterator it
= fvs
.find( d_typ
);
1730 if( it
!=fvs
.end() ){
1731 if( std::find( it
->second
.begin(), it
->second
.end(), d_status_num
)!=it
->second
.end() ){
1735 fvs
[d_typ
].push_back( d_status_num
);
1740 unsigned TermGenerator::getGeneralizationDepth( TermGenEnv
* s
) {
1741 //if( s->d_gen_relevant_terms ){
1742 // return s->d_tg_gdepth;
1744 std::map
< TypeNode
, std::vector
< int > > fvs
;
1745 return calculateGeneralizationDepth( s
, fvs
);
1749 Node
TermGenerator::getTerm( TermGenEnv
* s
) {
1750 if( d_status
==1 || d_status
==2 ){
1751 Assert(!d_typ
.isNull());
1752 return s
->getFreeVar( d_typ
, d_status_num
);
1753 }else if( d_status
==5 ){
1754 Node f
= s
->getTgFunc( d_typ
, d_status_num
);
1755 if( d_children
.size()==s
->d_func_args
[f
].size() ){
1756 std::vector
< Node
> children
;
1757 if( s
->d_tg_func_param
[f
] ){
1758 children
.push_back( f
);
1760 for( unsigned i
=0; i
<d_children
.size(); i
++ ){
1761 Node nc
= s
->d_tg_alloc
[d_children
[i
]].getTerm( s
);
1763 return Node::null();
1765 //Assert( nc.getType()==s->d_func_args[f][i] );
1766 children
.push_back( nc
);
1769 return NodeManager::currentNM()->mkNode( s
->d_func_kind
[f
], children
);
1774 return Node::null();
1777 void TermGenerator::debugPrint( TermGenEnv
* s
, const char * c
, const char * cd
) {
1778 Trace(cd
) << "[*" << d_id
<< "," << d_status
<< "]:";
1779 if( d_status
==1 || d_status
==2 ){
1780 Trace(c
) << s
->getFreeVar( d_typ
, d_status_num
);
1781 }else if( d_status
==5 ){
1782 TNode f
= s
->getTgFunc( d_typ
, d_status_num
);
1783 Trace(c
) << "(" << f
;
1784 for( unsigned i
=0; i
<d_children
.size(); i
++ ){
1786 s
->d_tg_alloc
[d_children
[i
]].debugPrint( s
, c
, cd
);
1788 if( d_children
.size()<s
->d_func_args
[f
].size() ){
1797 void TermGenEnv::collectSignatureInformation() {
1798 d_typ_tg_funcs
.clear();
1800 d_func_kind
.clear();
1801 d_func_args
.clear();
1803 for( std::map
< Node
, std::vector
< Node
> >::iterator it
= getTermDatabase()->d_op_map
.begin(); it
!= getTermDatabase()->d_op_map
.end(); ++it
){
1804 if( !it
->second
.empty() ){
1805 Node nn
= it
->second
[0];
1806 Trace("sg-rel-sig-debug") << "Check in signature : " << nn
<< std::endl
;
1807 if( d_cg
->isHandledTerm( nn
) && nn
.getKind()!=APPLY_SELECTOR_TOTAL
&& !nn
.getType().isBoolean() ){
1808 bool do_enum
= true;
1809 //check if we have enumerated ground terms
1810 if( nn
.getKind()==APPLY_UF
){
1811 Trace("sg-rel-sig-debug") << "Check enumeration..." << std::endl
;
1812 if( !d_cg
->hasEnumeratedUf( nn
) ){
1817 Trace("sg-rel-sig-debug") << "Set enumeration..." << std::endl
;
1818 d_funcs
.push_back( it
->first
);
1819 for( unsigned i
=0; i
<nn
.getNumChildren(); i
++ ){
1820 d_func_args
[it
->first
].push_back( nn
[i
].getType() );
1822 d_func_kind
[it
->first
] = nn
.getKind();
1823 d_typ_tg_funcs
[tnull
].push_back( it
->first
);
1824 d_typ_tg_funcs
[nn
.getType()].push_back( it
->first
);
1825 d_tg_func_param
[it
->first
] = ( nn
.getMetaKind() == kind::metakind::PARAMETERIZED
);
1826 Trace("sg-rel-sig") << "Will enumerate function applications of : " << it
->first
<< ", #args = " << d_func_args
[it
->first
].size() << ", kind = " << nn
.getKind() << std::endl
;
1827 //getTermDatabase()->computeUfEqcTerms( it->first );
1830 Trace("sg-rel-sig-debug") << "Done check in signature : " << nn
<< std::endl
;
1834 for (std::map
<TypeNode
, std::vector
<TNode
> >::iterator it
=
1835 d_typ_tg_funcs
.begin();
1836 it
!= d_typ_tg_funcs
.end();
1839 std::shuffle(it
->second
.begin(), it
->second
.end(), Random::getRandom());
1840 if (it
->first
.isNull())
1842 Trace("sg-gen-tg-debug") << "In this order : ";
1843 for (unsigned i
= 0; i
< it
->second
.size(); i
++)
1845 Trace("sg-gen-tg-debug") << it
->second
[i
] << " ";
1847 Trace("sg-gen-tg-debug") << std::endl
;
1852 void TermGenEnv::reset( unsigned depth
, bool genRelevant
, TypeNode tn
) {
1853 Assert(d_tg_alloc
.empty());
1857 for( unsigned i
=0; i
<2; i
++ ){
1858 d_ccand_eqc
[i
].clear();
1859 d_ccand_eqc
[i
].push_back( d_relevant_eqc
[i
] );
1865 d_tg_gdepth_limit
= depth
;
1866 d_gen_relevant_terms
= genRelevant
;
1867 d_tg_alloc
[0].reset( this, tn
);
1870 bool TermGenEnv::getNextTerm() {
1871 if( d_tg_alloc
[0].getNextTerm( this, d_tg_gdepth_limit
) ){
1872 Assert((int)d_tg_alloc
[0].getGeneralizationDepth(this)
1873 <= d_tg_gdepth_limit
);
1874 if( (int)d_tg_alloc
[0].getGeneralizationDepth( this )!=d_tg_gdepth_limit
){
1875 return getNextTerm();
1880 Trace("sg-gen-tg-debug2") << "...remove from context " << std::endl
;
1881 changeContext(false);
1886 void TermGenEnv::resetMatching( TNode eqc
, unsigned mode
) {
1887 d_tg_alloc
[0].resetMatching( this, eqc
, mode
);
1891 bool TermGenEnv::getNextMatch( TNode eqc
, std::map
< TypeNode
, std::map
< unsigned, TNode
> >& subs
, std::map
< TNode
, bool >& rev_subs
) {
1892 return d_tg_alloc
[0].getNextMatch( this, eqc
, subs
, rev_subs
);
1896 Node
TermGenEnv::getTerm() {
1897 return d_tg_alloc
[0].getTerm( this );
1900 void TermGenEnv::debugPrint( const char * c
, const char * cd
) {
1901 d_tg_alloc
[0].debugPrint( this, c
, cd
);
1904 unsigned TermGenEnv::getNumTgVars( TypeNode tn
) {
1905 return d_var_id
[tn
];
1908 bool TermGenEnv::allowVar( TypeNode tn
) {
1909 std::map
< TypeNode
, unsigned >::iterator it
= d_var_limit
.find( tn
);
1910 if( it
==d_var_limit
.end() ){
1913 return d_var_id
[tn
]<it
->second
;
1917 void TermGenEnv::addVar( TypeNode tn
) {
1921 void TermGenEnv::removeVar( TypeNode tn
) {
1923 //d_var_eq_tg.pop_back();
1924 //d_var_tg.pop_back();
1927 unsigned TermGenEnv::getNumTgFuncs( TypeNode tn
) {
1928 return d_typ_tg_funcs
[tn
].size();
1931 TNode
TermGenEnv::getTgFunc( TypeNode tn
, unsigned i
) {
1932 return d_typ_tg_funcs
[tn
][i
];
1935 Node
TermGenEnv::getFreeVar( TypeNode tn
, unsigned i
) {
1936 return d_cg
->getFreeVar( tn
, i
);
1939 bool TermGenEnv::considerCurrentTerm() {
1940 Assert(!d_tg_alloc
.empty());
1942 //if generalization depth is too large, don't consider it
1943 unsigned i
= d_tg_alloc
.size();
1944 Trace("sg-gen-tg-debug") << "Consider term ";
1945 d_tg_alloc
[0].debugPrint( this, "sg-gen-tg-debug", "sg-gen-tg-debug" );
1946 Trace("sg-gen-tg-debug") << "? curr term size = " << d_tg_alloc
.size() << ", last status = " << d_tg_alloc
[i
-1].d_status
;
1947 Trace("sg-gen-tg-debug") << std::endl
;
1949 if( d_tg_gdepth_limit
>=0 && d_tg_alloc
[0].getGeneralizationDepth( this )>(unsigned)d_tg_gdepth_limit
){
1950 Trace("sg-gen-consider-term") << "-> generalization depth of ";
1951 d_tg_alloc
[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-tg-debug" );
1952 Trace("sg-gen-consider-term") << " is too high " << d_tg_gdepth
<< " " << d_tg_alloc
[0].getGeneralizationDepth( this ) << ", do not consider." << std::endl
;
1958 if( d_tg_alloc[i-1].d_status==1 ){
1959 }else if( d_tg_alloc[i-1].d_status==2 ){
1960 }else if( d_tg_alloc[i-1].d_status==5 ){
1962 Trace("sg-gen-tg-debug") << "Bad tg: " << &d_tg_alloc[i-1] << std::endl;
1966 //if equated two variables, first check if context-independent TODO
1967 //----end optimizations
1970 //check based on which candidate equivalence classes match
1971 if( d_gen_relevant_terms
){
1972 Trace("sg-gen-tg-debug") << "Filter based on relevant ground EQC";
1973 Trace("sg-gen-tg-debug") << ", #eqc to try = " << d_ccand_eqc
[0][i
-1].size() << "/" << d_ccand_eqc
[1][i
-1].size() << std::endl
;
1975 Assert(d_ccand_eqc
[0].size() >= 2);
1976 Assert(d_ccand_eqc
[0].size() == d_ccand_eqc
[1].size());
1977 Assert(d_ccand_eqc
[0].size() == d_tg_id
+ 1);
1978 Assert(d_tg_id
== d_tg_alloc
.size());
1979 for( unsigned r
=0; r
<2; r
++ ){
1980 d_ccand_eqc
[r
][i
].clear();
1983 //re-check feasibility of EQC
1984 for( unsigned r
=0; r
<2; r
++ ){
1985 for( unsigned j
=0; j
<d_ccand_eqc
[r
][i
-1].size(); j
++ ){
1986 std::map
< TypeNode
, std::map
< unsigned, TNode
> > subs
;
1987 std::map
< TNode
, bool > rev_subs
;
1990 mode
= d_cg
->optReqDistinctVarPatterns() ? ( 1 << 0 ) : 0;
1991 mode
= mode
| (1 << 2 );
1995 d_tg_alloc
[0].resetMatching( this, d_ccand_eqc
[r
][i
-1][j
], mode
);
1996 if( d_tg_alloc
[0].getNextMatch( this, d_ccand_eqc
[r
][i
-1][j
], subs
, rev_subs
) ){
1997 d_ccand_eqc
[r
][i
].push_back( d_ccand_eqc
[r
][i
-1][j
] );
2001 for( unsigned r
=0; r
<2; r
++ ){
2002 Trace("sg-gen-tg-debug") << "Current eqc of type " << r
<< " : ";
2003 for( unsigned j
=0; j
<d_ccand_eqc
[r
][i
].size(); j
++ ){
2004 Trace("sg-gen-tg-debug") << "e" << d_cg
->d_em
[d_ccand_eqc
[r
][i
][j
]] << " ";
2006 Trace("sg-gen-tg-debug") << std::endl
;
2008 if( options::conjectureFilterActiveTerms() && d_ccand_eqc
[0][i
].empty() ){
2009 Trace("sg-gen-consider-term") << "Do not consider term of form ";
2010 d_tg_alloc
[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-consider-term-debug" );
2011 Trace("sg-gen-consider-term") << " since no relevant EQC matches it." << std::endl
;
2014 if( options::conjectureFilterModel() && d_ccand_eqc
[1][i
].empty() ){
2015 Trace("sg-gen-consider-term") << "Do not consider term of form ";
2016 d_tg_alloc
[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-consider-term-debug" );
2017 Trace("sg-gen-consider-term") << " since no ground EQC matches it." << std::endl
;
2021 Trace("sg-gen-tg-debug") << "Will consider term ";
2022 d_tg_alloc
[0].debugPrint( this, "sg-gen-tg-debug", "sg-gen-tg-debug" );
2023 Trace("sg-gen-tg-debug") << std::endl
;
2024 Trace("sg-gen-consider-term-debug") << std::endl
;
2028 void TermGenEnv::changeContext( bool add
) {
2030 for( unsigned r
=0; r
<2; r
++ ){
2031 d_ccand_eqc
[r
].push_back( std::vector
< TNode
>() );
2035 for( unsigned r
=0; r
<2; r
++ ){
2036 d_ccand_eqc
[r
].pop_back();
2039 Assert(d_tg_alloc
.find(d_tg_id
) != d_tg_alloc
.end());
2040 d_tg_alloc
.erase( d_tg_id
);
2044 bool TermGenEnv::considerCurrentTermCanon( unsigned tg_id
){
2045 Assert(tg_id
< d_tg_alloc
.size());
2046 if( options::conjectureFilterCanonical() ){
2047 //check based on a canonicity of the term (if there is one)
2048 Trace("sg-gen-tg-debug") << "Consider term canon ";
2049 d_tg_alloc
[0].debugPrint( this, "sg-gen-tg-debug", "sg-gen-tg-debug" );
2050 Trace("sg-gen-tg-debug") << ", tg is [" << tg_id
<< "]..." << std::endl
;
2052 Node ln
= d_tg_alloc
[tg_id
].getTerm( this );
2053 Trace("sg-gen-tg-debug") << "Term is " << ln
<< std::endl
;
2054 return d_cg
->considerTermCanon( ln
, d_gen_relevant_terms
);
2059 bool TermGenEnv::isRelevantFunc( Node f
) {
2060 return std::find( d_funcs
.begin(), d_funcs
.end(), f
)!=d_funcs
.end();
2063 bool TermGenEnv::isRelevantTerm( Node t
) {
2064 if( t
.getKind()!=BOUND_VARIABLE
){
2065 if( t
.getKind()!=EQUAL
){
2066 if( t
.hasOperator() ){
2067 TNode op
= t
.getOperator();
2068 if( !isRelevantFunc( op
) ){
2075 for( unsigned i
=0; i
<t
.getNumChildren(); i
++ ){
2076 if( !isRelevantTerm( t
[i
] ) ){
2084 TermDb
* TermGenEnv::getTermDatabase() {
2085 return d_cg
->getTermDatabase();
2087 Node
TermGenEnv::getGroundEqc( TNode r
) {
2088 return d_cg
->getGroundEqc( r
);
2090 bool TermGenEnv::isGroundEqc( TNode r
){
2091 return d_cg
->isGroundEqc( r
);
2093 bool TermGenEnv::isGroundTerm( TNode n
){
2094 return d_cg
->isGroundTerm( n
);
2098 void SubstitutionIndex::addSubstitution( TNode eqc
, std::vector
< TNode
>& vars
, std::vector
< TNode
>& terms
, unsigned i
) {
2099 if( i
==vars
.size() ){
2102 Assert(d_var
.isNull() || d_var
== vars
[i
]);
2104 d_children
[terms
[i
]].addSubstitution( eqc
, vars
, terms
, i
+1 );
2108 bool SubstitutionIndex::notifySubstitutions( ConjectureGenerator
* s
, std::map
< TNode
, TNode
>& subs
, TNode rhs
, unsigned numVars
, unsigned i
) {
2110 Assert(d_children
.empty());
2111 return s
->notifySubstitution( d_var
, subs
, rhs
);
2113 Assert(i
== 0 || !d_children
.empty());
2114 for( std::map
< TNode
, SubstitutionIndex
>::iterator it
= d_children
.begin(); it
!= d_children
.end(); ++it
){
2115 Trace("sg-cconj-debug2") << "Try " << d_var
<< " -> " << it
->first
<< " (" << i
<< "/" << numVars
<< ")" << std::endl
;
2116 subs
[d_var
] = it
->first
;
2117 if( !it
->second
.notifySubstitutions( s
, subs
, rhs
, numVars
, i
+1 ) ){
2126 void TheoremIndex::addTheorem( std::vector
< TNode
>& lhs_v
, std::vector
< unsigned >& lhs_arg
, TNode rhs
){
2127 if( lhs_v
.empty() ){
2128 if( std::find( d_terms
.begin(), d_terms
.end(), rhs
)==d_terms
.end() ){
2129 d_terms
.push_back( rhs
);
2132 unsigned index
= lhs_v
.size()-1;
2133 if( lhs_arg
[index
]==lhs_v
[index
].getNumChildren() ){
2136 addTheorem( lhs_v
, lhs_arg
, rhs
);
2139 addTheoremNode( lhs_v
[index
][lhs_arg
[index
]-1], lhs_v
, lhs_arg
, rhs
);
2144 void TheoremIndex::addTheoremNode( TNode curr
, std::vector
< TNode
>& lhs_v
, std::vector
< unsigned >& lhs_arg
, TNode rhs
){
2145 Trace("thm-db-debug") << "Adding conjecture for subterm " << curr
<< "..." << std::endl
;
2146 if( curr
.hasOperator() ){
2147 lhs_v
.push_back( curr
);
2148 lhs_arg
.push_back( 0 );
2149 d_children
[curr
.getOperator()].addTheorem( lhs_v
, lhs_arg
, rhs
);
2151 Assert(curr
.getKind() == kind::BOUND_VARIABLE
);
2152 TypeNode tn
= curr
.getType();
2153 Assert(d_var
[tn
].isNull() || d_var
[tn
] == curr
);
2155 d_children
[curr
].addTheorem( lhs_v
, lhs_arg
, rhs
);
2159 void TheoremIndex::getEquivalentTerms( std::vector
< TNode
>& n_v
, std::vector
< unsigned >& n_arg
,
2160 std::map
< TNode
, TNode
>& smap
, std::vector
< TNode
>& vars
, std::vector
< TNode
>& subs
,
2161 std::vector
< Node
>& terms
) {
2162 Trace("thm-db-debug") << "Get equivalent terms " << n_v
.size() << " " << n_arg
.size() << std::endl
;
2164 Trace("thm-db-debug") << "Number of terms : " << d_terms
.size() << std::endl
;
2165 //apply substutitions to RHS's
2166 for( unsigned i
=0; i
<d_terms
.size(); i
++ ){
2167 Node n
= d_terms
[i
].substitute( vars
.begin(), vars
.end(), subs
.begin(), subs
.end() );
2168 terms
.push_back( n
);
2171 unsigned index
= n_v
.size()-1;
2172 if( n_arg
[index
]==n_v
[index
].getNumChildren() ){
2175 getEquivalentTerms( n_v
, n_arg
, smap
, vars
, subs
, terms
);
2178 getEquivalentTermsNode( n_v
[index
][n_arg
[index
]-1], n_v
, n_arg
, smap
, vars
, subs
, terms
);
2183 void TheoremIndex::getEquivalentTermsNode( Node curr
, std::vector
< TNode
>& n_v
, std::vector
< unsigned >& n_arg
,
2184 std::map
< TNode
, TNode
>& smap
, std::vector
< TNode
>& vars
, std::vector
< TNode
>& subs
,
2185 std::vector
< Node
>& terms
) {
2186 Trace("thm-db-debug") << "Get equivalent based on subterm " << curr
<< "..." << std::endl
;
2187 if( curr
.hasOperator() ){
2188 Trace("thm-db-debug") << "Check based on operator..." << std::endl
;
2189 std::map
< TNode
, TheoremIndex
>::iterator it
= d_children
.find( curr
.getOperator() );
2190 if( it
!=d_children
.end() ){
2191 n_v
.push_back( curr
);
2192 n_arg
.push_back( 0 );
2193 it
->second
.getEquivalentTerms( n_v
, n_arg
, smap
, vars
, subs
, terms
);
2195 Trace("thm-db-debug") << "...done check based on operator" << std::endl
;
2197 TypeNode tn
= curr
.getType();
2198 std::map
< TypeNode
, TNode
>::iterator itt
= d_var
.find( tn
);
2199 if( itt
!=d_var
.end() ){
2200 Trace("thm-db-debug") << "Check for substitution with " << itt
->second
<< "..." << std::endl
;
2201 Assert(curr
.getType() == itt
->second
.getType());
2202 //add to substitution if possible
2203 bool success
= false;
2204 std::map
< TNode
, TNode
>::iterator it
= smap
.find( itt
->second
);
2205 if( it
==smap
.end() ){
2206 smap
[itt
->second
] = curr
;
2207 vars
.push_back( itt
->second
);
2208 subs
.push_back( curr
);
2210 }else if( it
->second
==curr
){
2213 //also check modulo equality (in universal equality engine)
2215 Trace("thm-db-debug") << "...check for substitution with " << itt
->second
<< ", success = " << success
<< "." << std::endl
;
2217 d_children
[itt
->second
].getEquivalentTerms( n_v
, n_arg
, smap
, vars
, subs
, terms
);
2222 void TheoremIndex::debugPrint( const char * c
, unsigned ind
) {
2223 for( std::map
< TNode
, TheoremIndex
>::iterator it
= d_children
.begin(); it
!= d_children
.end(); ++it
){
2224 for( unsigned i
=0; i
<ind
; i
++ ){ Trace(c
) << " "; }
2225 Trace(c
) << it
->first
<< std::endl
;
2226 it
->second
.debugPrint( c
, ind
+1 );
2228 if( !d_terms
.empty() ){
2229 for( unsigned i
=0; i
<ind
; i
++ ){ Trace(c
) << " "; }
2231 for( unsigned i
=0; i
<d_terms
.size(); i
++ ){
2232 Trace(c
) << " " << d_terms
[i
];
2234 Trace(c
) << " }" << std::endl
;
2236 //if( !d_var.isNull() ){
2237 // for( unsigned i=0; i<ind; i++ ){ Trace(c) << " "; }
2238 // Trace(c) << "var:" << d_var << std::endl;
2242 bool ConjectureGenerator::optReqDistinctVarPatterns() { return false; }
2243 bool ConjectureGenerator::optFilterUnknown() { return true; } //may change
2244 int ConjectureGenerator::optFilterScoreThreshold() { return 1; }
2245 unsigned ConjectureGenerator::optFullCheckFrequency() { return 1; }
2247 bool ConjectureGenerator::optStatsOnly() { return false; }