Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * conjecture generator class
11 : : */
12 : :
13 : : #include "theory/quantifiers/conjecture_generator.h"
14 : :
15 : : #include "expr/node_algorithm.h"
16 : : #include "expr/skolem_manager.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/rewriter.h"
26 : : #include "util/random.h"
27 : :
28 : : using namespace cvc5::internal;
29 : : using namespace cvc5::internal::kind;
30 : : using namespace cvc5::internal::theory;
31 : : using namespace cvc5::internal::theory::quantifiers;
32 : : using namespace std;
33 : :
34 : : namespace cvc5::internal {
35 : :
36 : : struct sortConjectureScore {
37 : : std::vector< int > d_scores;
38 : : bool operator() (unsigned i, unsigned j) { return d_scores[i]>d_scores[j]; }
39 : : };
40 : :
41 : :
42 : 394775 : void OpArgIndex::addTerm( std::vector< TNode >& terms, TNode n, unsigned index ){
43 [ + + ]: 394775 : if( index==n.getNumChildren() ){
44 [ - + ][ - + ]: 158754 : Assert(n.hasOperator());
[ - - ]
45 [ + + ]: 158754 : if( std::find( d_ops.begin(), d_ops.end(), n.getOperator() )==d_ops.end() ){
46 : 131172 : d_ops.push_back( n.getOperator() );
47 : 131172 : d_op_terms.push_back( n );
48 : : }
49 : : }else{
50 : 236021 : d_child[terms[index]].addTerm( terms, n, index+1 );
51 : : }
52 : 394775 : }
53 : :
54 : 149823 : Node OpArgIndex::getGroundTerm( ConjectureGenerator * s, std::vector< TNode >& args ) {
55 [ + + ]: 149823 : if( d_ops.empty() ){
56 [ + + ]: 159178 : for( std::map< TNode, OpArgIndex >::iterator it = d_child.begin(); it != d_child.end(); ++it ){
57 : 118301 : std::map< TNode, Node >::iterator itf = s->d_ground_eqc_map.find( it->first );
58 [ + + ]: 118301 : if( itf!=s->d_ground_eqc_map.end() ){
59 : 80450 : args.push_back( itf->second );
60 : 80450 : Node n = it->second.getGroundTerm( s, args );
61 : 80450 : args.pop_back();
62 [ + + ]: 80450 : if( !n.isNull() ){
63 : 70116 : return n;
64 : : }
65 [ + + ]: 80450 : }
66 : : }
67 : 40877 : return Node::null();
68 : : }
69 : 38830 : std::vector<TNode> args2;
70 [ + - ]: 38830 : if (d_op_terms[0].getMetaKind() == kind::metakind::PARAMETERIZED)
71 : : {
72 : 38830 : args2.push_back( d_ops[0] );
73 : : }
74 : 38830 : args2.insert(args2.end(), args.begin(), args.end());
75 : 38830 : return s->nodeManager()->mkNode(d_op_terms[0].getKind(), args2);
76 : 38830 : }
77 : :
78 : 224252 : void OpArgIndex::getGroundTerms( ConjectureGenerator * s, std::vector< TNode >& terms ) {
79 : 224252 : terms.insert( terms.end(), d_op_terms.begin(), d_op_terms.end() );
80 [ + + ]: 395353 : for( std::map< TNode, OpArgIndex >::iterator it = d_child.begin(); it != d_child.end(); ++it ){
81 [ + + ]: 171101 : if( s->isGroundEqc( it->first ) ){
82 : 151837 : it->second.getGroundTerms( s, terms );
83 : : }
84 : : }
85 : 224252 : }
86 : :
87 : 68 : ConjectureGenerator::ConjectureGenerator(Env& env,
88 : : QuantifiersState& qs,
89 : : QuantifiersInferenceManager& qim,
90 : : QuantifiersRegistry& qr,
91 : 68 : TermRegistry& tr)
92 : : : QuantifiersModule(env, qs, qim, qr, tr),
93 : 68 : d_notify(*this),
94 : 68 : d_uequalityEngine(
95 : : env, context(), d_notify, "ConjectureGenerator::ee", false),
96 : 68 : d_ee_conjectures(context()),
97 : 68 : d_conj_count(0),
98 : 68 : d_subs_confirmCount(0),
99 : 68 : d_subs_unkCount(0),
100 : 68 : d_fullEffortCount(0),
101 [ + + ]: 340 : d_hasAddedLemma(false)
102 : : {
103 : 68 : d_true = nodeManager()->mkConst(true);
104 : 68 : d_false = nodeManager()->mkConst(false);
105 : 68 : d_uequalityEngine.addFunctionKind(Kind::APPLY_UF);
106 : 68 : d_uequalityEngine.addFunctionKind(Kind::APPLY_CONSTRUCTOR);
107 [ - - ][ - - ]: 68 : }
108 : :
109 : 272 : ConjectureGenerator::~ConjectureGenerator()
110 : : {
111 : 136 : for (std::map<Node, EqcInfo*>::iterator i = d_eqc_info.begin(),
112 : 68 : iend = d_eqc_info.end();
113 [ + + ]: 149 : i != iend;
114 : 81 : ++i)
115 : : {
116 : 81 : EqcInfo* current = (*i).second;
117 [ - + ][ - + ]: 81 : Assert(current != nullptr);
118 [ + - ]: 81 : delete current;
119 : : }
120 [ + - ][ + + ]: 408 : }
121 : :
122 : 33315 : void ConjectureGenerator::eqNotifyNewClass( TNode t ){
123 [ + - ]: 33315 : Trace("thm-ee-debug") << "UEE : new equivalence class " << t << std::endl;
124 : 33315 : d_upendingAdds.push_back( t );
125 : 33315 : }
126 : :
127 : 1118 : void ConjectureGenerator::eqNotifyMerge(TNode t1, TNode t2)
128 : : {
129 : : //get maintained representatives
130 : 1118 : TNode rt1 = t1;
131 : 1118 : TNode rt2 = t2;
132 : 1118 : std::map< Node, EqcInfo* >::iterator it1 = d_eqc_info.find( t1 );
133 [ + + ][ + + ]: 1118 : if( it1!=d_eqc_info.end() && !it1->second->d_rep.get().isNull() ){
[ + + ]
134 : 59 : rt1 = it1->second->d_rep.get();
135 : : }
136 : 1118 : std::map< Node, EqcInfo* >::iterator it2 = d_eqc_info.find( t2 );
137 [ + + ][ - + ]: 1118 : if( it2!=d_eqc_info.end() && !it2->second->d_rep.get().isNull() ){
[ - + ]
138 : 0 : rt2 = it2->second->d_rep.get();
139 : : }
140 [ + - ]: 1118 : Trace("thm-ee-debug") << "UEE : equality holds : " << t1 << " == " << t2 << std::endl;
141 [ + - ]: 1118 : Trace("thm-ee-debug") << " ureps : " << rt1 << " == " << rt2 << std::endl;
142 [ + - ]: 1118 : Trace("thm-ee-debug") << " relevant : " << d_pattern_is_relevant[rt1] << " " << d_pattern_is_relevant[rt2] << std::endl;
143 [ + - ]: 1118 : Trace("thm-ee-debug") << " normal : " << d_pattern_is_normal[rt1] << " " << d_pattern_is_normal[rt2] << std::endl;
144 [ + - ]: 1118 : Trace("thm-ee-debug") << " size : " << d_pattern_fun_sum[rt1] << " " << d_pattern_fun_sum[rt2] << std::endl;
145 : :
146 [ + + ]: 1118 : if( isUniversalLessThan( rt2, rt1 ) ){
147 : : EqcInfo * ei;
148 [ + + ]: 127 : if( it1==d_eqc_info.end() ){
149 : 81 : ei = getOrMakeEqcInfo( t1, true );
150 : : }else{
151 : 46 : ei = it1->second;
152 : : }
153 : 127 : ei->d_rep = t2;
154 : : }
155 : 1118 : }
156 : :
157 : 81 : ConjectureGenerator::EqcInfo::EqcInfo(context::Context* c)
158 : 81 : : d_rep(c, Node::null())
159 : : {
160 : 81 : }
161 : :
162 : 109618 : ConjectureGenerator::EqcInfo* ConjectureGenerator::getOrMakeEqcInfo( TNode n, bool doMake ) {
163 : : //Assert( getUniversalRepresentative( n )==n );
164 : 109618 : std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n );
165 [ + + ]: 109618 : if( eqc_i!=d_eqc_info.end() ){
166 : 1087 : return eqc_i->second;
167 [ + + ]: 108531 : }else if( doMake ){
168 : 81 : EqcInfo* ei = new EqcInfo(context());
169 : 81 : d_eqc_info[n] = ei;
170 : 81 : return ei;
171 : : }else{
172 : 108450 : return NULL;
173 : : }
174 : : }
175 : :
176 : 148498 : void ConjectureGenerator::setUniversalRelevant( TNode n ) {
177 : : //add pattern information
178 : 148498 : registerPattern( n, n.getType() );
179 : 148498 : d_urelevant_terms[n] = true;
180 [ + + ]: 265585 : for( unsigned i=0; i<n.getNumChildren(); i++ ){
181 : 117087 : setUniversalRelevant( n[i] );
182 : : }
183 : 148498 : }
184 : :
185 : 5647 : bool ConjectureGenerator::isUniversalLessThan( TNode rt1, TNode rt2 ) {
186 : : //ensure both patterns are registered so that the following assertions will
187 : : //succeed
188 : 5647 : registerPattern(rt1, rt1.getType());
189 : 5647 : registerPattern(rt2, rt2.getType());
190 : :
191 : : //prefer the one that is (normal, smaller) lexographically
192 [ - + ][ - + ]: 5647 : Assert(d_pattern_is_relevant.find(rt1) != d_pattern_is_relevant.end());
[ - - ]
193 [ - + ][ - + ]: 5647 : Assert(d_pattern_is_relevant.find(rt2) != d_pattern_is_relevant.end());
[ - - ]
194 [ - + ][ - + ]: 5647 : Assert(d_pattern_is_normal.find(rt1) != d_pattern_is_normal.end());
[ - - ]
195 [ - + ][ - + ]: 5647 : Assert(d_pattern_is_normal.find(rt2) != d_pattern_is_normal.end());
[ - - ]
196 [ - + ][ - + ]: 5647 : Assert(d_pattern_fun_sum.find(rt1) != d_pattern_fun_sum.end());
[ - - ]
197 [ - + ][ - + ]: 5647 : Assert(d_pattern_fun_sum.find(rt2) != d_pattern_fun_sum.end());
[ - - ]
198 : :
199 [ + + ][ - + ]: 5647 : if( d_pattern_is_relevant[rt1] && !d_pattern_is_relevant[rt2] ){
[ - + ]
200 [ - - ]: 0 : Trace("thm-ee-debug") << "UEE : LT due to relevant." << std::endl;
201 : 0 : return true;
202 [ + + ]: 5647 : }else if( d_pattern_is_relevant[rt1]==d_pattern_is_relevant[rt2] ){
203 [ + - ][ - + ]: 5629 : if( d_pattern_is_normal[rt1] && !d_pattern_is_normal[rt2] ){
[ - + ]
204 [ - - ]: 0 : Trace("thm-ee-debug") << "UEE : LT due to normal." << std::endl;
205 : 0 : return true;
206 [ + - ]: 5629 : }else if( d_pattern_is_normal[rt1]==d_pattern_is_normal[rt2] ){
207 [ + + ]: 5629 : if( d_pattern_fun_sum[rt1]<d_pattern_fun_sum[rt2] ){
208 [ + - ]: 157 : Trace("thm-ee-debug") << "UEE : LT due to size." << std::endl;
209 : : //decide which representative to use : based on size of the term
210 : 157 : return true;
211 [ + + ]: 5472 : }else if( d_pattern_fun_sum[rt1]==d_pattern_fun_sum[rt2] ){
212 : : //same size : tie goes to term that has already been reported
213 : 703 : return isReportedCanon( rt1 ) && !isReportedCanon( rt2 );
214 : : }
215 : : }
216 : : }
217 : 4787 : return false;
218 : : }
219 : :
220 : :
221 : 108081 : bool ConjectureGenerator::isReportedCanon( TNode n ) {
222 : 108081 : return std::find( d_ue_canon.begin(), d_ue_canon.end(), n )==d_ue_canon.end();
223 : : }
224 : :
225 : 106675 : void ConjectureGenerator::markReportedCanon( TNode n ) {
226 [ - + ]: 106675 : if( !isReportedCanon( n ) ){
227 : 0 : d_ue_canon.push_back( n );
228 : : }
229 : 106675 : }
230 : :
231 : 558 : bool ConjectureGenerator::areUniversalEqual( TNode n1, TNode n2 ) {
232 : 558 : return n1==n2 || ( d_uequalityEngine.hasTerm( n1 ) && d_uequalityEngine.hasTerm( n2 ) && d_uequalityEngine.areEqual( n1, n2 ) );
233 : : }
234 : :
235 : 0 : bool ConjectureGenerator::areUniversalDisequal( TNode n1, TNode n2 ) {
236 : 0 : return n1!=n2 && d_uequalityEngine.hasTerm( n1 ) && d_uequalityEngine.hasTerm( n2 ) && d_uequalityEngine.areDisequal( n1, n2, false );
237 : : }
238 : :
239 : 109537 : Node ConjectureGenerator::getUniversalRepresentative(TNode n, bool add)
240 : : {
241 [ + + ]: 109537 : if( add ){
242 [ + + ]: 109094 : if( d_urelevant_terms.find( n )==d_urelevant_terms.end() ){
243 : 31381 : setUniversalRelevant( n );
244 : : //add term to universal equality engine
245 : 31381 : d_uequalityEngine.addTerm( n );
246 : : // addding this term to equality engine will lead to a set of new terms (the new subterms of n)
247 : : // now, do instantiation-based merging for each of these terms
248 [ + - ]: 31381 : Trace("thm-ee-debug") << "Merge equivalence classes based on instantiations of terms..." << std::endl;
249 : : //merge all pending equalities
250 : 31381 : EntailmentCheck* echeck = d_treg.getEntailmentCheck();
251 [ + + ]: 62395 : while( !d_upendingAdds.empty() ){
252 [ + - ]: 31014 : Trace("sg-pending") << "Add " << d_upendingAdds.size() << " pending terms..." << std::endl;
253 : 31014 : std::vector< Node > pending;
254 : 31014 : pending.insert( pending.end(), d_upendingAdds.begin(), d_upendingAdds.end() );
255 : 31014 : d_upendingAdds.clear();
256 [ + + ]: 64329 : for( unsigned i=0; i<pending.size(); i++ ){
257 : 33315 : Node t = pending[i];
258 : 33315 : TypeNode tn = t.getType();
259 [ + - ]: 33315 : Trace("thm-ee-add") << "UEE : Add universal term " << t << std::endl;
260 : 33315 : std::vector< Node > eq_terms;
261 : : //if occurs modulo equality at ground level, it is equivalent to representative of ground equality engine
262 : 33315 : Node gt = echeck->evaluateTerm(t);
263 [ + - ][ + + ]: 33315 : if( !gt.isNull() && gt!=t ){
[ + + ]
264 : 160 : eq_terms.push_back( gt );
265 : : }
266 : : //get all equivalent terms based on theorem database
267 : 33315 : d_thm_index.getEquivalentTerms( t, eq_terms );
268 [ + + ]: 33315 : if( !eq_terms.empty() ){
269 [ + - ]: 4982 : Trace("thm-ee-add") << "UEE : Based on ground EE/theorem DB, it is equivalent to " << eq_terms.size() << " terms : " << std::endl;
270 : : //add equivalent terms as equalities to universal engine
271 [ + + ]: 9976 : for (const Node& eqt : eq_terms)
272 : : {
273 [ + - ]: 4994 : Trace("thm-ee-add") << " " << eqt << std::endl;
274 : 4994 : bool assertEq = false;
275 [ + + ]: 4994 : if (d_urelevant_terms.find(eqt) != d_urelevant_terms.end())
276 : : {
277 : 465 : assertEq = true;
278 : : }
279 : : else
280 : : {
281 [ - + ][ - + ]: 4529 : Assert(eqt.getType() == tn);
[ - - ]
282 : 4529 : registerPattern(eqt, tn);
283 [ + + ]: 4529 : if (isUniversalLessThan(eqt, t))
284 : : {
285 : 30 : setUniversalRelevant(eqt);
286 : 30 : assertEq = true;
287 : : }
288 : : }
289 [ + + ]: 4994 : if( assertEq ){
290 : 495 : Node exp;
291 : 495 : d_uequalityEngine.assertEquality(t.eqNode(eqt), true, exp);
292 : 495 : }else{
293 [ + - ]: 8998 : Trace("thm-ee-no-add")
294 : 4499 : << "Do not add : " << t << " == " << eqt << std::endl;
295 : : }
296 : : }
297 : : }else{
298 [ + - ]: 28333 : Trace("thm-ee-add") << "UEE : No equivalent terms." << std::endl;
299 : : }
300 : 33315 : }
301 : 31014 : }
302 : : }
303 : : }
304 : :
305 [ + - ]: 109537 : if( d_uequalityEngine.hasTerm( n ) ){
306 : 219074 : Node r = d_uequalityEngine.getRepresentative( n );
307 : 109537 : EqcInfo * ei = getOrMakeEqcInfo( r );
308 [ + + ][ + + ]: 109537 : if( ei && !ei->d_rep.get().isNull() ){
[ + + ]
309 : 1054 : return ei->d_rep.get();
310 : : }else{
311 : 108483 : return r;
312 : : }
313 : 109537 : }else{
314 : 0 : return n;
315 : : }
316 : : }
317 : :
318 : 250428 : Node ConjectureGenerator::getFreeVar( TypeNode tn, unsigned i ) {
319 : 250428 : return d_termCanon.getCanonicalFreeVar(tn, i);
320 : : }
321 : :
322 : 299872 : bool ConjectureGenerator::isHandledTerm( TNode n ){
323 [ - - ]: 599744 : return getTermDatabase()->isTermActive(n)
324 [ + + ][ + - ]: 571047 : && inst::TriggerTermInfo::isAtomicTrigger(n)
[ - - ]
325 [ + + ][ + + ]: 994065 : && (n.getKind() != Kind::APPLY_UF
326 [ + + ][ + + ]: 722890 : || n.getOperator().getKind() != Kind::SKOLEM);
[ + + ][ - - ]
327 : : }
328 : :
329 : 0 : Node ConjectureGenerator::getGroundEqc( TNode r ) {
330 : 0 : std::map< TNode, Node >::iterator it = d_ground_eqc_map.find( r );
331 [ - - ]: 0 : return it!=d_ground_eqc_map.end() ? it->second : Node::null();
332 : : }
333 : :
334 : 4565903 : bool ConjectureGenerator::isGroundEqc( TNode r ) {
335 : 4565903 : return d_ground_eqc_map.find( r )!=d_ground_eqc_map.end();
336 : : }
337 : :
338 : 0 : bool ConjectureGenerator::isGroundTerm( TNode n ) {
339 : 0 : return std::find( d_ground_terms.begin(), d_ground_terms.end(), n )!=d_ground_terms.end();
340 : : }
341 : :
342 : 6756 : bool ConjectureGenerator::needsCheck( Theory::Effort e ) {
343 : : // synchonized with instantiation engine
344 : 6756 : return d_qstate.getInstWhenNeedsCheck(e);
345 : : }
346 : :
347 : 1205 : bool ConjectureGenerator::hasEnumeratedUf( Node n ) {
348 [ + - ]: 1205 : if (options().quantifiers.conjectureGenGtEnum > 0)
349 : : {
350 : 1205 : std::map< Node, bool >::iterator it = d_uf_enum.find( n.getOperator() );
351 [ + + ]: 1205 : if( it==d_uf_enum.end() ){
352 : 252 : d_uf_enum[n.getOperator()] = true;
353 : 252 : std::vector< Node > lem;
354 : 252 : getEnumeratePredUfTerm(n, options().quantifiers.conjectureGenGtEnum, lem);
355 [ + - ]: 252 : if( !lem.empty() ){
356 [ + + ]: 12852 : for (const Node& l : lem)
357 : : {
358 : 12600 : d_qim.addPendingLemma(l, InferenceId::QUANTIFIERS_CONJ_GEN_GT_ENUM);
359 : : }
360 : 252 : d_hasAddedLemma = true;
361 : 252 : return false;
362 : : }
363 [ - + ]: 252 : }
364 : : }
365 : 953 : return true;
366 : : }
367 : :
368 : 1402 : void ConjectureGenerator::reset_round(CVC5_UNUSED Theory::Effort e) {}
369 : 1037 : void ConjectureGenerator::check(CVC5_UNUSED Theory::Effort e, QEffort quant_e)
370 : : {
371 [ + + ]: 1037 : if (quant_e == QEFFORT_STANDARD)
372 : : {
373 : 320 : d_fullEffortCount++;
374 [ + - ]: 320 : if( d_fullEffortCount%optFullCheckFrequency()==0 ){
375 : 320 : d_hasAddedLemma = false;
376 : 320 : d_tge.d_cg = this;
377 : 320 : beginCallDebug();
378 : 320 : d_conj_count = 0;
379 : 320 : std::vector<TNode> eqcs;
380 : 320 : getEquivalenceClasses(eqcs);
381 : 320 : computeIrrelevantEqcs(eqcs);
382 : : //debug printing
383 [ - + ]: 320 : if( TraceIsOn("sg-gen-eqc") )
384 : : {
385 : 0 : debugPrintIrrelevantEqcs(eqcs);
386 : : }
387 : :
388 : 320 : computeRelevantEqcs(eqcs);
389 : :
390 : :
391 [ + - ]: 320 : Trace("sg-proc") << "Collect signature information..." << std::endl;
392 : 320 : d_tge.collectSignatureInformation();
393 [ + + ]: 320 : if( d_hasAddedLemma ){
394 [ + - ]: 76 : Trace("sg-proc") << "...added enumeration lemmas." << std::endl;
395 : : }
396 [ + - ]: 320 : Trace("sg-proc") << "...done collect signature information" << std::endl;
397 : :
398 : :
399 : :
400 : 320 : std::vector<Node> provenConj = buildTheoremIndex();
401 : 320 : debugPrintUnprovenConjectures(provenConj);
402 : :
403 [ - + ]: 320 : if (TraceIsOn("thm-db"))
404 : : {
405 : 0 : debugPrintTheoremIndex();
406 : : }
407 : :
408 : : //clear patterns
409 : 320 : d_patterns.clear();
410 : 320 : d_pattern_var_id.clear();
411 : 320 : d_pattern_var_duplicate.clear();
412 : 320 : d_pattern_is_normal.clear();
413 : 320 : d_pattern_is_relevant.clear();
414 : 320 : d_pattern_fun_id.clear();
415 : 320 : d_pattern_fun_sum.clear();
416 : 320 : d_rel_patterns.clear();
417 : 320 : d_rel_pattern_var_sum.clear();
418 : 320 : d_rel_pattern_typ_index.clear();
419 : 320 : d_rel_pattern_subs_index.clear();
420 : :
421 : 320 : generateConjectures();
422 : :
423 [ + - ]: 320 : Trace("sg-stats") << "Total conjectures considered : " << d_conj_count << std::endl;
424 [ - + ]: 320 : if( TraceIsOn("thm-ee") ){
425 [ - - ]: 0 : Trace("thm-ee") << "Universal equality engine is : " << std::endl;
426 : 0 : eq::EqClassesIterator ueqcs_i = eq::EqClassesIterator( &d_uequalityEngine );
427 [ - - ]: 0 : while( !ueqcs_i.isFinished() ){
428 : 0 : TNode r = (*ueqcs_i);
429 : 0 : bool firstTime = true;
430 : 0 : Node rr = getUniversalRepresentative(r);
431 [ - - ]: 0 : Trace("thm-ee") << " " << rr;
432 [ - - ]: 0 : Trace("thm-ee") << " : { ";
433 : 0 : eq::EqClassIterator ueqc_i = eq::EqClassIterator( r, &d_uequalityEngine );
434 [ - - ]: 0 : while( !ueqc_i.isFinished() ){
435 : 0 : TNode n = (*ueqc_i);
436 [ - - ]: 0 : if( rr!=n ){
437 [ - - ]: 0 : if( firstTime ){
438 [ - - ]: 0 : Trace("thm-ee") << std::endl;
439 : 0 : firstTime = false;
440 : : }
441 [ - - ]: 0 : Trace("thm-ee") << " " << n << std::endl;
442 : : }
443 : 0 : ++ueqc_i;
444 : 0 : }
445 : 0 : if( !firstTime ){ Trace("thm-ee") << " "; }
446 [ - - ]: 0 : Trace("thm-ee") << "}" << std::endl;
447 : 0 : ++ueqcs_i;
448 : 0 : }
449 [ - - ]: 0 : Trace("thm-ee") << std::endl;
450 : : }
451 : 320 : endCallDebug();
452 : 320 : }
453 : : }
454 : 1037 : }
455 : :
456 : 320 : void ConjectureGenerator::getEquivalenceClasses(std::vector<TNode>& eqcs)
457 : : {
458 [ + - ]: 320 : Trace("sg-proc") << "Get eq classes..." << std::endl;
459 : 320 : d_op_arg_index.clear();
460 : 320 : d_ground_eqc_map.clear();
461 : 320 : d_bool_eqc[0] = Node::null();
462 : 320 : d_bool_eqc[1] = Node::null();
463 : 320 : d_em.clear();
464 : 320 : eq::EqualityEngine* ee = getEqualityEngine();
465 : 320 : eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
466 [ + + ]: 72735 : while( !eqcs_i.isFinished() ){
467 : 72415 : TNode r = (*eqcs_i);
468 [ + - ]: 72415 : Trace("sg-proc-debug") << "...eqc : " << r << std::endl;
469 : 72415 : eqcs.push_back( r );
470 [ + + ]: 72415 : if( r.getType().isBoolean() ){
471 [ + + ]: 15791 : if (areEqual(r, d_true))
472 : : {
473 : 320 : d_ground_eqc_map[r] = d_true;
474 : 320 : d_bool_eqc[0] = r;
475 : : }
476 [ + + ]: 15471 : else if (areEqual(r, d_false))
477 : : {
478 : 320 : d_ground_eqc_map[r] = d_false;
479 : 320 : d_bool_eqc[1] = r;
480 : : }
481 : : }
482 : 72415 : d_em[r] = eqcs.size();
483 : 72415 : eq::EqClassIterator ieqc_i = eq::EqClassIterator( r, ee );
484 [ + + ]: 386124 : while( !ieqc_i.isFinished() ){
485 : 313709 : TNode n = (*ieqc_i);
486 [ + - ]: 313709 : Trace("sg-proc-debug") << "......term : " << n << std::endl;
487 [ + + ]: 313709 : if( getTermDatabase()->hasTermCurrent( n ) ){
488 [ + + ]: 294812 : if( isHandledTerm( n ) ){
489 : 158754 : std::vector<TNode> areps;
490 [ + + ]: 394775 : for (const Node& nc : n)
491 : : {
492 : 236021 : areps.push_back(d_qstate.getRepresentative(nc));
493 : 236021 : }
494 : 158754 : d_op_arg_index[r].addTerm(areps, n);
495 : 158754 : }
496 : : }
497 : 313709 : ++ieqc_i;
498 : 313709 : }
499 : 72415 : ++eqcs_i;
500 : 72415 : }
501 [ - + ][ - + ]: 320 : Assert(!d_bool_eqc[0].isNull());
[ - - ]
502 [ - + ][ - + ]: 320 : Assert(!d_bool_eqc[1].isNull());
[ - - ]
503 : 320 : d_urelevant_terms.clear();
504 [ + - ]: 320 : Trace("sg-proc") << "...done get eq classes" << std::endl;
505 : 320 : }
506 : :
507 : 320 : void ConjectureGenerator::computeIrrelevantEqcs(const std::vector<TNode>& eqcs)
508 : : {
509 [ + - ]: 320 : Trace("sg-proc") << "Determine ground EQC..." << std::endl;
510 : : bool success;
511 [ + + ]: 738 : do
512 : : {
513 : 738 : success = false;
514 [ + + ]: 187938 : for (unsigned i = 0; i < eqcs.size(); i++)
515 : : {
516 : 187200 : TNode r = eqcs[i];
517 [ + + ]: 187200 : if (d_ground_eqc_map.find(r) == d_ground_eqc_map.end())
518 : : {
519 : 88761 : std::vector<TNode> args;
520 [ + - ]: 177522 : Trace("sg-pat-debug")
521 : 88761 : << "******* Get ground term for " << r << std::endl;
522 : 88761 : Node n;
523 [ + + ]: 88761 : if (Skolemize::isInductionTerm(options(), r))
524 : : {
525 : 69373 : n = d_op_arg_index[r].getGroundTerm(this, args);
526 : : }
527 : : else
528 : : {
529 : 19388 : n = r;
530 : : }
531 [ + + ]: 88761 : if (!n.isNull())
532 : : {
533 [ + - ]: 58218 : Trace("sg-pat") << "Ground term for eqc " << r << " : " << std::endl;
534 [ + - ]: 58218 : Trace("sg-pat") << " " << n << std::endl;
535 : 58218 : d_ground_eqc_map[r] = n;
536 : 58218 : success = true;
537 : : }
538 : : else
539 : : {
540 [ + - ]: 61086 : Trace("sg-pat-debug")
541 : 30543 : << "...could not find ground term." << std::endl;
542 : : }
543 : 88761 : }
544 : 187200 : }
545 : : } while (success);
546 : : // also get ground terms
547 : 320 : d_ground_terms.clear();
548 [ + + ]: 72735 : for (unsigned i = 0; i < eqcs.size(); i++)
549 : : {
550 : 72415 : TNode r = eqcs[i];
551 : 72415 : d_op_arg_index[r].getGroundTerms(this, d_ground_terms);
552 : 72415 : }
553 [ + - ]: 320 : Trace("sg-proc") << "...done determine ground EQC" << std::endl;
554 : 320 : }
555 : :
556 : 0 : void ConjectureGenerator::debugPrintIrrelevantEqcs(
557 : : const std::vector<TNode>& eqcs)
558 : : {
559 : 0 : eq::EqualityEngine* ee = getEqualityEngine();
560 [ - - ]: 0 : for (unsigned i = 0; i < eqcs.size(); i++)
561 : : {
562 : 0 : TNode r = eqcs[i];
563 : : // print out members
564 : 0 : bool firstTime = true;
565 : 0 : bool isFalse = areEqual(r, d_false);
566 : 0 : eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee);
567 [ - - ]: 0 : while (!eqc_i.isFinished())
568 : : {
569 : 0 : TNode n = (*eqc_i);
570 : 0 : if (getTermDatabase()->hasTermCurrent(n)
571 : 0 : && getTermDatabase()->isTermActive(n)
572 : 0 : && (n.getKind() != Kind::EQUAL || isFalse))
573 : : {
574 [ - - ]: 0 : if (firstTime)
575 : : {
576 [ - - ]: 0 : Trace("sg-gen-eqc") << "e" << d_em[r] << " : { " << std::endl;
577 : 0 : firstTime = false;
578 : : }
579 [ - - ]: 0 : if (n.hasOperator())
580 : : {
581 : 0 : Trace("sg-gen-eqc") << " (" << n.getOperator();
582 [ - - ]: 0 : for (const Node& nc : n)
583 : : {
584 : 0 : TNode ar = d_qstate.getRepresentative(nc);
585 [ - - ]: 0 : Trace("sg-gen-eqc") << " e" << d_em[ar];
586 : 0 : }
587 [ - - ]: 0 : Trace("sg-gen-eqc") << ") :: " << n << std::endl;
588 : : }
589 : : else
590 : : {
591 [ - - ]: 0 : Trace("sg-gen-eqc") << " " << n << std::endl;
592 : : }
593 : : }
594 : 0 : ++eqc_i;
595 : 0 : }
596 [ - - ]: 0 : if (!firstTime)
597 : : {
598 [ - - ]: 0 : Trace("sg-gen-eqc") << "}" << std::endl;
599 : : // print out ground term
600 : 0 : std::map<TNode, Node>::iterator it = d_ground_eqc_map.find(r);
601 [ - - ]: 0 : if (it != d_ground_eqc_map.end())
602 : : {
603 [ - - ]: 0 : Trace("sg-gen-eqc") << "- Ground term : " << it->second << std::endl;
604 : : }
605 : : }
606 : 0 : }
607 : 0 : }
608 : :
609 : 320 : void ConjectureGenerator::computeRelevantEqcs(const std::vector<TNode>& eqcs)
610 : : {
611 [ + - ]: 320 : Trace("sg-proc") << "Compute relevant eqc..." << std::endl;
612 : 320 : d_tge.d_relevant_eqc[0].clear();
613 : 320 : d_tge.d_relevant_eqc[1].clear();
614 [ + + ]: 72735 : for (unsigned i = 0; i < eqcs.size(); i++)
615 : : {
616 : 72415 : TNode r = eqcs[i];
617 : 72415 : std::map<TNode, Node>::iterator it = d_ground_eqc_map.find(r);
618 : 72415 : unsigned index = 1;
619 [ + + ]: 72415 : if (it == d_ground_eqc_map.end())
620 : : {
621 : 13557 : index = 0;
622 : : }
623 : : // based on unproven conjectures? TODO
624 : 72415 : d_tge.d_relevant_eqc[index].push_back(r);
625 : 72415 : }
626 [ + - ]: 320 : Trace("sg-gen-tg-debug") << "Initial relevant eqc : ";
627 [ + + ]: 13877 : for (unsigned i = 0; i < d_tge.d_relevant_eqc[0].size(); i++)
628 : : {
629 [ + - ]: 13557 : Trace("sg-gen-tg-debug") << "e" << d_em[d_tge.d_relevant_eqc[0][i]] << " ";
630 : : }
631 [ + - ]: 320 : Trace("sg-gen-tg-debug") << std::endl;
632 [ + - ]: 320 : Trace("sg-proc") << "...done compute relevant eqc" << std::endl;
633 : 320 : }
634 : :
635 : 320 : std::vector<Node> ConjectureGenerator::buildTheoremIndex()
636 : : {
637 [ + - ]: 320 : Trace("sg-proc") << "Build theorem index..." << std::endl;
638 : 320 : d_ue_canon.clear();
639 : 320 : d_thm_index.clear();
640 : 320 : std::vector<Node> provenConj;
641 : 320 : quantifiers::FirstOrderModel* m = d_treg.getModel();
642 [ + + ]: 3278 : for (unsigned i = 0; i < m->getNumAssertedQuantifiers(); i++)
643 : : {
644 : 2958 : Node q = m->getAssertedQuantifier(i);
645 [ + - ]: 2958 : Trace("thm-db-debug") << "Is " << q << " a relevant theorem?" << std::endl;
646 : 2958 : Node conjEq;
647 [ + + ]: 2958 : if (q[1].getKind() == Kind::EQUAL)
648 : : {
649 : 2669 : bool isSubsume = false;
650 : 2669 : bool inEe = false;
651 [ + + ]: 3959 : for (unsigned r = 0; r < 2; r++)
652 : : {
653 : 6628 : TNode nl = q[1][r == 0 ? 0 : 1];
654 [ + + ]: 6628 : TNode nr = q[1][r == 0 ? 1 : 0];
655 : 3314 : Node eq;
656 : 3314 : if (r == 1
657 [ + + ][ + + ]: 8652 : || std::find(d_conjectures.begin(), d_conjectures.end(), q)
658 [ + + ]: 8652 : == d_conjectures.end())
659 : : {
660 : 2882 : eq = nl.eqNode(nr);
661 : : // check if it contains only relevant functions
662 [ + + ]: 2882 : if (d_tge.isRelevantTerm(eq))
663 : : {
664 : : // make it canonical
665 [ + - ]: 1290 : Trace("sg-proc-debug") << "get canonical " << eq << std::endl;
666 : 1290 : eq = d_termCanon.getCanonicalTerm(eq);
667 : : }
668 : : else
669 : : {
670 : 1592 : eq = Node::null();
671 : : }
672 : : }
673 [ + + ]: 3314 : if (!eq.isNull())
674 : : {
675 [ + + ]: 1290 : if (r == 0)
676 : : {
677 : 645 : inEe = d_ee_conjectures.find(q[1]) != d_ee_conjectures.end();
678 [ + + ]: 645 : if (!inEe)
679 : : {
680 : : // add to universal equality engine
681 : 1116 : Node nlu = getUniversalRepresentative(eq[0], true);
682 : 1116 : Node nru = getUniversalRepresentative(eq[1], true);
683 [ - + ]: 558 : if (areUniversalEqual(nlu, nru))
684 : : {
685 : 0 : isSubsume = true;
686 : : // set inactive (will be ignored by other modules)
687 : 0 : m->setQuantifierActive(q, false);
688 : : }
689 : : else
690 : : {
691 : 558 : Node exp;
692 : 558 : d_ee_conjectures[q[1]] = true;
693 : 558 : d_uequalityEngine.assertEquality(nlu.eqNode(nru), true, exp);
694 : 558 : }
695 : 558 : }
696 [ + - ]: 1290 : Trace("sg-conjecture") << "*** CONJECTURE : currently proven"
697 [ - - ]: 645 : << (isSubsume ? " and subsumed" : "");
698 [ + - ][ - + ]: 645 : Trace("sg-conjecture") << " : " << q[1] << std::endl;
[ - - ]
699 : 645 : provenConj.push_back(q);
700 : : }
701 [ + - ]: 1290 : if (!isSubsume)
702 : : {
703 [ + - ][ - - ]: 2580 : Trace("thm-db-debug") << "Adding theorem to database " << eq[0]
704 [ - + ][ - + ]: 1290 : << " == " << eq[1] << std::endl;
[ - - ]
705 : 1290 : d_thm_index.addTheorem(eq[0], eq[1]);
706 : : }
707 : : else
708 : : {
709 : 0 : break;
710 : : }
711 : : }
712 : : else
713 : : {
714 : 2024 : break;
715 : : }
716 [ + + ][ + + ]: 7362 : }
[ + + ]
717 : : }
718 : 2958 : }
719 : 320 : return provenConj;
720 : 0 : }
721 : :
722 : 320 : void ConjectureGenerator::debugPrintUnprovenConjectures(
723 : : const std::vector<Node>& provenConj)
724 : : {
725 [ - + ]: 320 : if (TraceIsOn("sg-conjecture"))
726 : : {
727 : : // examine status of other conjectures
728 [ - - ]: 0 : for (unsigned i = 0; i < d_conjectures.size(); i++)
729 : : {
730 : 0 : Node q = d_conjectures[i];
731 [ - - ]: 0 : if (std::find(provenConj.begin(), provenConj.end(), q) == provenConj.end())
732 : : {
733 : : // check each skolem variable
734 : 0 : bool disproven = true;
735 : 0 : std::vector<Node> skolems;
736 : 0 : d_qim.getSkolemize()->getSkolemConstantsInduction(q, skolems);
737 [ - - ]: 0 : Trace("sg-conjecture") << " CONJECTURE : ";
738 : 0 : std::vector<Node> ce;
739 [ - - ]: 0 : for (unsigned j = 0; j < skolems.size(); j++)
740 : : {
741 : 0 : TNode rk = getRepresentative(skolems[j]);
742 : 0 : std::map<TNode, Node>::iterator git = d_ground_eqc_map.find(rk);
743 : : // check if it is a ground term
744 [ - - ]: 0 : if (git == d_ground_eqc_map.end())
745 : : {
746 [ - - ]: 0 : Trace("sg-conjecture") << "ACTIVE : " << q;
747 [ - - ]: 0 : if (TraceIsOn("sg-gen-eqc"))
748 : : {
749 [ - - ]: 0 : Trace("sg-conjecture") << " { ";
750 [ - - ]: 0 : for (unsigned k = 0; k < skolems.size(); k++)
751 : : {
752 [ - - ]: 0 : Trace("sg-conjecture")
753 [ - - ]: 0 : << skolems[k] << (j == k ? "*" : "") << " ";
754 : : }
755 [ - - ]: 0 : Trace("sg-conjecture") << "}";
756 : : }
757 [ - - ]: 0 : Trace("sg-conjecture") << std::endl;
758 : 0 : disproven = false;
759 : 0 : break;
760 : : }
761 : : else
762 : : {
763 : 0 : ce.push_back(git->second);
764 : : }
765 [ - - ]: 0 : }
766 [ - - ]: 0 : if (disproven)
767 : : {
768 [ - - ]: 0 : Trace("sg-conjecture") << "disproven : " << q << " : ";
769 [ - - ]: 0 : for (unsigned j = 0, ceSize = ce.size(); j < ceSize; j++)
770 : : {
771 : 0 : Trace("sg-conjecture") << q[0][j] << " -> " << ce[j] << " ";
772 : : }
773 [ - - ]: 0 : Trace("sg-conjecture") << std::endl;
774 : : }
775 : 0 : }
776 : 0 : }
777 : : }
778 : 320 : }
779 : :
780 : 0 : void ConjectureGenerator::debugPrintTheoremIndex()
781 : : {
782 [ - - ]: 0 : Trace("thm-db") << "Theorem database is : " << std::endl;
783 : 0 : d_thm_index.debugPrint("thm-db");
784 [ - - ]: 0 : Trace("thm-db") << std::endl;
785 : :
786 [ - - ]: 0 : Trace("sg-proc") << "...done build theorem index" << std::endl;
787 : 0 : }
788 : :
789 : 320 : void ConjectureGenerator::generateConjectures()
790 : : {
791 : 320 : unsigned rel_term_count = 0;
792 : 320 : std::map<TypeNode, unsigned> rt_var_max;
793 : 320 : std::vector<TypeNode> rt_types;
794 : 320 : std::map<TypeNode, std::map<int, std::vector<Node> > > conj_lhs;
795 : 320 : unsigned addedLemmas = 0;
796 : 320 : unsigned maxDepth = options().quantifiers.conjectureGenMaxDepth;
797 [ + + ]: 907 : for (unsigned depth = 1; depth <= maxDepth; depth++)
798 : : {
799 [ + - ]: 1566 : Trace("sg-proc") << "Generate relevant LHS at depth " << depth << "..."
800 : 783 : << std::endl;
801 [ + - ]: 1566 : Trace("sg-rel-term") << "Relevant terms of depth " << depth << " : "
802 : 783 : << std::endl;
803 : : // set up environment
804 : 783 : d_tge.d_var_id.clear();
805 : 783 : d_tge.d_var_limit.clear();
806 : 783 : d_tge.reset(depth, true, TypeNode::null());
807 [ + + ]: 6722 : while (d_tge.getNextTerm())
808 : : {
809 : : // construct term
810 : 5939 : Node nn = d_tge.getTerm();
811 [ + - ]: 5939 : if (considerTermCanon(nn, true))
812 : : {
813 : 5939 : rel_term_count++;
814 [ + - ]: 5939 : Trace("sg-rel-term") << "*** Relevant term : ";
815 : 5939 : d_tge.debugPrint("sg-rel-term", "sg-rel-term-debug2");
816 [ + - ]: 5939 : Trace("sg-rel-term") << std::endl;
817 : :
818 [ + + ]: 17817 : for (unsigned r = 0; r < 2; r++)
819 : : {
820 [ + - ]: 23756 : Trace("sg-rel-term-debug")
821 : 11878 : << "...from equivalence classes (" << r << ") : ";
822 : 11878 : int index = d_tge.d_ccand_eqc[r].size() - 1;
823 [ + + ]: 246918 : for (unsigned j = 0; j < d_tge.d_ccand_eqc[r][index].size(); j++)
824 : : {
825 [ + - ]: 470080 : Trace("sg-rel-term-debug")
826 : 235040 : << "e" << d_em[d_tge.d_ccand_eqc[r][index][j]] << " ";
827 : : }
828 [ + - ]: 11878 : Trace("sg-rel-term-debug") << std::endl;
829 : : }
830 : 5939 : TypeNode tnn = nn.getType();
831 [ + - ]: 5939 : Trace("sg-gen-tg-debug") << "...term is " << nn << std::endl;
832 : 5939 : conj_lhs[tnn][depth].push_back(nn);
833 : :
834 : : // add information about pattern
835 [ + - ]: 11878 : Trace("sg-gen-tg-debug")
836 : 5939 : << "Collect pattern information..." << std::endl;
837 [ - + ][ - + ]: 5939 : Assert(std::find(
[ - - ]
838 : : d_rel_patterns[tnn].begin(), d_rel_patterns[tnn].end(), nn)
839 : : == d_rel_patterns[tnn].end());
840 : 5939 : d_rel_patterns[tnn].push_back(nn);
841 : : // build information concerning the variables in this pattern
842 : 5939 : unsigned sum = 0;
843 : 5939 : std::map<TypeNode, unsigned> typ_to_subs_index;
844 : 5939 : std::vector<TNode> gsubs_vars;
845 : 5939 : for (std::map<TypeNode, unsigned>::iterator it = d_tge.d_var_id.begin();
846 [ + + ]: 15456 : it != d_tge.d_var_id.end();
847 : 9517 : ++it)
848 : : {
849 [ + + ]: 9517 : if (it->second > 0)
850 : : {
851 : 7180 : typ_to_subs_index[it->first] = sum;
852 : 7180 : sum += it->second;
853 [ + + ]: 19678 : for (unsigned i = 0; i < it->second; i++)
854 : : {
855 : 12498 : gsubs_vars.push_back(
856 : 24996 : d_termCanon.getCanonicalFreeVar(it->first, i));
857 : : }
858 : : }
859 : : }
860 : 5939 : d_rel_pattern_var_sum[nn] = sum;
861 : : // register the pattern
862 : 5939 : registerPattern(nn, tnn);
863 [ - + ][ - + ]: 5939 : Assert(d_pattern_is_normal[nn]);
[ - - ]
864 [ + - ]: 11878 : Trace("sg-gen-tg-debug")
865 : 5939 : << "...done collect pattern information" << std::endl;
866 : :
867 : : // record information about types
868 [ + - ]: 5939 : Trace("sg-gen-tg-debug") << "Collect type information..." << std::endl;
869 : 5939 : PatternTypIndex* pti = &d_rel_pattern_typ_index;
870 : 5939 : for (std::map<TypeNode, unsigned>::iterator it = d_tge.d_var_id.begin();
871 [ + + ]: 15456 : it != d_tge.d_var_id.end();
872 : 9517 : ++it)
873 : : {
874 : 9517 : pti = &pti->d_children[it->first][it->second];
875 : : // record maximum
876 : 9517 : if (rt_var_max.find(it->first) == rt_var_max.end()
877 [ + + ][ + + ]: 9517 : || it->second > rt_var_max[it->first])
[ + + ]
878 : : {
879 : 735 : rt_var_max[it->first] = it->second;
880 : : }
881 : : }
882 [ + + ]: 5939 : if (std::find(rt_types.begin(), rt_types.end(), tnn) == rt_types.end())
883 : : {
884 : 365 : rt_types.push_back(tnn);
885 : : }
886 : 5939 : pti->d_terms.push_back(nn);
887 [ + - ]: 11878 : Trace("sg-gen-tg-debug")
888 : 5939 : << "...done collect type information" << std::endl;
889 : :
890 [ + - ]: 11878 : Trace("sg-gen-tg-debug")
891 : 5939 : << "Build substitutions for ground EQC..." << std::endl;
892 : 5939 : std::vector<TNode> gsubs_terms;
893 : 5939 : gsubs_terms.resize(gsubs_vars.size());
894 : 5939 : int index = d_tge.d_ccand_eqc[1].size() - 1;
895 [ + + ]: 181597 : for (unsigned j = 0; j < d_tge.d_ccand_eqc[1][index].size(); j++)
896 : : {
897 : 175658 : TNode r = d_tge.d_ccand_eqc[1][index][j];
898 [ + - ]: 351316 : Trace("sg-rel-term-debug")
899 : 0 : << " Matches for e" << d_em[r] << ", which is ground term "
900 : 175658 : << d_ground_eqc_map[r] << ":" << std::endl;
901 : 175658 : std::map<TypeNode, std::map<unsigned, TNode> > subs;
902 : 175658 : std::map<TNode, bool> rev_subs;
903 : : // only get ground terms
904 : 175658 : unsigned mode = 2;
905 : 175658 : d_tge.resetMatching(mode);
906 [ + + ]: 1329470 : while (d_tge.getNextMatch(r, subs, rev_subs))
907 : : {
908 : : // we will be building substitutions
909 : 1153812 : bool firstTime = true;
910 : 1153812 : for (std::map<TypeNode, std::map<unsigned, TNode> >::iterator it =
911 : 1153812 : subs.begin();
912 [ + + ]: 2531330 : it != subs.end();
913 : 1377518 : ++it)
914 : : {
915 : 1377518 : unsigned tindex = typ_to_subs_index[it->first];
916 : 1377518 : for (std::map<unsigned, TNode>::iterator it2 = it->second.begin();
917 [ + + ]: 4707328 : it2 != it->second.end();
918 : 3329810 : ++it2)
919 : : {
920 [ + + ]: 3329810 : if (!firstTime)
921 : : {
922 [ + - ]: 2175998 : Trace("sg-rel-term-debug") << ", ";
923 : : }
924 : : else
925 : : {
926 : 1153812 : firstTime = false;
927 [ + - ]: 1153812 : Trace("sg-rel-term-debug") << " ";
928 : : }
929 [ + - ]: 6659620 : Trace("sg-rel-term-debug")
930 : 3329810 : << it->first << ":x" << it2->first << " -> " << it2->second;
931 [ - + ][ - + ]: 3329810 : Assert(tindex + it2->first < gsubs_terms.size());
[ - - ]
932 : 3329810 : gsubs_terms[tindex + it2->first] = it2->second;
933 : : }
934 : : }
935 [ + - ]: 1153812 : Trace("sg-rel-term-debug") << std::endl;
936 : 1153812 : d_rel_pattern_subs_index[nn].addSubstitution(
937 : : r, gsubs_vars, gsubs_terms);
938 : : }
939 : 175658 : }
940 [ + - ]: 11878 : Trace("sg-gen-tg-debug")
941 : 5939 : << "...done build substitutions for ground EQC" << std::endl;
942 : 5939 : }
943 : : else
944 : : {
945 [ - - ]: 0 : Trace("sg-gen-tg-debug") << "> not canonical : " << nn << std::endl;
946 : : }
947 : 5939 : }
948 [ + - ]: 1566 : Trace("sg-proc") << "...done generate terms at depth " << depth
949 : 783 : << std::endl;
950 [ + - ]: 1566 : Trace("sg-stats") << "--------> Total LHS of depth " << depth << " : "
951 : 783 : << rel_term_count << std::endl;
952 : :
953 : : // consider types from relevant terms
954 [ + + ]: 2545 : for (unsigned rdepth = 0; rdepth <= depth; rdepth++)
955 : : {
956 : : // set up environment
957 : 1958 : d_tge.d_var_id.clear();
958 : 1958 : d_tge.d_var_limit.clear();
959 : 1958 : for (std::map<TypeNode, unsigned>::iterator it = rt_var_max.begin();
960 [ + + ]: 3865 : it != rt_var_max.end();
961 : 1907 : ++it)
962 : : {
963 : 1907 : d_tge.d_var_id[it->first] = it->second;
964 : 1907 : d_tge.d_var_limit[it->first] = it->second;
965 : : }
966 : 1958 : std::shuffle(rt_types.begin(), rt_types.end(), Random::getRandom());
967 : 1958 : std::map<TypeNode, std::vector<Node> > conj_rhs;
968 [ + + ]: 3851 : for (unsigned i = 0; i < rt_types.size(); i++)
969 : : {
970 [ + - ]: 3786 : Trace("sg-proc") << "Generate relevant RHS terms of type "
971 : 0 : << rt_types[i] << " at depth " << rdepth << "..."
972 : 1893 : << std::endl;
973 : 1893 : d_tge.reset(rdepth, false, rt_types[i]);
974 : :
975 [ + + ]: 34382 : while (d_tge.getNextTerm())
976 : : {
977 : 32489 : Node rhs = d_tge.getTerm();
978 [ + - ]: 32489 : if (considerTermCanon(rhs, false))
979 : : {
980 [ + - ]: 32489 : Trace("sg-rel-prop") << "Relevant RHS : " << rhs << std::endl;
981 : : // register pattern
982 [ - + ][ - + ]: 32489 : Assert(rhs.getType() == rt_types[i]);
[ - - ]
983 : 32489 : registerPattern(rhs, rt_types[i]);
984 [ + + ]: 32489 : if (rdepth < depth)
985 : : {
986 : : // consider against all LHS at depth
987 [ + + ]: 161070 : for (unsigned j = 0; j < conj_lhs[rt_types[i]][depth].size(); j++)
988 : : {
989 : 458394 : processCandidateConjecture(
990 : 305596 : conj_lhs[rt_types[i]][depth][j], rhs, depth, rdepth);
991 : : }
992 : : }
993 : : else
994 : : {
995 : 24217 : conj_rhs[rt_types[i]].push_back(rhs);
996 : : }
997 : : }
998 : 32489 : }
999 : : }
1000 : 1958 : flushWaitingConjectures(addedLemmas, depth, rdepth);
1001 : : // consider against all LHS up to depth
1002 [ + + ]: 1958 : if (rdepth == depth)
1003 : : {
1004 [ + + ]: 1705 : for (unsigned lhs_depth = 1; lhs_depth <= depth; lhs_depth++)
1005 : : {
1006 [ + - ]: 1076 : if ((int)addedLemmas < options().quantifiers.conjectureGenPerRound)
1007 : : {
1008 [ + - ]: 2152 : Trace("sg-proc") << "Consider conjectures at depth (" << lhs_depth
1009 : 1076 : << ", " << rdepth << ")..." << std::endl;
1010 : 1076 : for (std::map<TypeNode, std::vector<Node> >::iterator it =
1011 : 1076 : conj_rhs.begin();
1012 [ + + ]: 1944 : it != conj_rhs.end();
1013 : 868 : ++it)
1014 : : {
1015 [ + + ]: 48537 : for (unsigned j = 0; j < it->second.size(); j++)
1016 : : {
1017 [ + + ]: 733880 : for (unsigned k = 0; k < conj_lhs[it->first][lhs_depth].size();
1018 : : k++)
1019 : : {
1020 : 686211 : processCandidateConjecture(conj_lhs[it->first][lhs_depth][k],
1021 : 686211 : it->second[j],
1022 : : lhs_depth,
1023 : : rdepth);
1024 : : }
1025 : : }
1026 : : }
1027 : 1076 : flushWaitingConjectures(addedLemmas, lhs_depth, depth);
1028 : : }
1029 : : }
1030 : : }
1031 [ + + ]: 1958 : if ((int)addedLemmas >= options().quantifiers.conjectureGenPerRound)
1032 : : {
1033 : 196 : break;
1034 : : }
1035 [ + + ]: 1958 : }
1036 [ + + ]: 783 : if ((int)addedLemmas >= options().quantifiers.conjectureGenPerRound)
1037 : : {
1038 : 196 : break;
1039 : : }
1040 : : }
1041 : 320 : }
1042 : :
1043 : 0 : std::string ConjectureGenerator::identify() const { return "induction-cg"; }
1044 : :
1045 : 3034 : unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth ) {
1046 [ + + ]: 3034 : if( !d_waiting_conjectures_lhs.empty() ){
1047 [ + - ]: 220 : Trace("sg-proc") << "Generated " << d_waiting_conjectures_lhs.size() << " conjectures at depth " << ldepth << "/" << rdepth << "." << std::endl;
1048 [ + - ]: 220 : if ((int)addedLemmas < options().quantifiers.conjectureGenPerRound)
1049 : : {
1050 : : /*
1051 : : std::vector< unsigned > indices;
1052 : : for( unsigned i=0; i<d_waiting_conjectures_lhs.size(); i++ ){
1053 : : indices.push_back( i );
1054 : : }
1055 : : bool doSort = false;
1056 : : if( doSort ){
1057 : : //sort them based on score
1058 : : sortConjectureScore scs;
1059 : : scs.d_scores.insert( scs.d_scores.begin(), d_waiting_conjectures_score.begin(), d_waiting_conjectures_score.end() );
1060 : : std::sort( indices.begin(), indices.end(), scs );
1061 : : }
1062 : : //if( doSort && d_waiting_conjectures_score[indices[0]]<optFilterScoreThreshold() ){
1063 : : */
1064 : 220 : unsigned prevCount = d_conj_count;
1065 [ + + ]: 271 : for( unsigned i=0; i<d_waiting_conjectures_lhs.size(); i++ ){
1066 [ + - ]: 247 : if( d_waiting_conjectures_score[i]>=optFilterScoreThreshold() ){
1067 : : //we have determined a relevant subgoal
1068 : 247 : Node lhs = d_waiting_conjectures_lhs[i];
1069 : 247 : Node rhs = d_waiting_conjectures_rhs[i];
1070 : 494 : if (getUniversalRepresentative(lhs) != lhs
1071 : 494 : || getUniversalRepresentative(rhs) != rhs)
1072 : : {
1073 : : //skip
1074 : : }
1075 : : else
1076 : : {
1077 [ + - ]: 196 : Trace("sg-engine") << "*** Consider conjecture : " << lhs << " == " << rhs << std::endl;
1078 [ + - ]: 196 : Trace("sg-engine-debug") << " score : " << d_waiting_conjectures_score[i] << std::endl;
1079 [ - + ]: 196 : if( optStatsOnly() ){
1080 : 0 : d_conj_count++;
1081 : : }else{
1082 : 196 : Node body = lhs.eqNode(rhs);
1083 : 196 : std::unordered_set<Node> fvs;
1084 : 196 : expr::getFreeVariables(body, fvs);
1085 : 196 : std::vector<Node> bvs;
1086 : 196 : bvs.insert(bvs.begin(), fvs.begin(), fvs.end());
1087 : 196 : Node bvl = nodeManager()->mkNode(Kind::BOUND_VAR_LIST, bvs);
1088 : 392 : Node rsg = NodeManager::mkNode(Kind::FORALL, bvl, body);
1089 : :
1090 : 196 : rsg = rewrite(rsg);
1091 : 196 : d_conjectures.push_back( rsg );
1092 : 196 : d_eq_conjectures[lhs].push_back( rhs );
1093 : 196 : d_eq_conjectures[rhs].push_back( lhs );
1094 : :
1095 : 392 : Node lem = NodeManager::mkNode(Kind::OR, rsg.negate(), rsg);
1096 : 196 : d_qim.addPendingLemma(lem,
1097 : : InferenceId::QUANTIFIERS_CONJ_GEN_SPLIT);
1098 : 196 : d_qim.addPendingPhaseRequirement(rsg, false);
1099 : 196 : addedLemmas++;
1100 : 392 : if ((int)addedLemmas
1101 [ + - ]: 196 : >= options().quantifiers.conjectureGenPerRound)
1102 : : {
1103 : 196 : break;
1104 : : }
1105 [ - + ][ - + ]: 1176 : }
[ - + ][ - + ]
[ - + ][ - + ]
1106 : : }
1107 [ + + ][ + + ]: 443 : }
1108 : : }
1109 [ + - ]: 220 : Trace("sg-proc") << "...have now added " << addedLemmas << " conjecture lemmas." << std::endl;
1110 [ - + ]: 220 : if( optStatsOnly() ){
1111 [ - - ]: 0 : Trace("sg-stats") << "Generated " << (d_conj_count-prevCount) << " conjectures at depth " << ldepth << "/" << rdepth << "." << std::endl;
1112 : : }
1113 : : }
1114 : 220 : d_waiting_conjectures_lhs.clear();
1115 : 220 : d_waiting_conjectures_rhs.clear();
1116 : 220 : d_waiting_conjectures_score.clear();
1117 : 220 : d_waiting_conjectures.clear();
1118 : : }
1119 : 3034 : return addedLemmas;
1120 : : }
1121 : :
1122 : 107978 : bool ConjectureGenerator::considerTermCanon( Node ln, bool genRelevant ){
1123 [ + - ]: 107978 : if( !ln.isNull() ){
1124 : : //do not consider if it is non-canonical, and either:
1125 : : // (1) we are not generating relevant terms, or
1126 : : // (2) its canonical form is a generalization.
1127 : 107978 : Node lnr = getUniversalRepresentative(ln, true);
1128 [ + + ]: 107978 : if( lnr==ln ){
1129 : 106675 : markReportedCanon( ln );
1130 : 1303 : }else if( !genRelevant || isGeneralization( lnr, ln ) ){
1131 [ + - ]: 623 : Trace("sg-gen-consider-term") << "Do not consider term, " << ln << " is not canonical representation (which is " << lnr << ")." << std::endl;
1132 : 623 : return false;
1133 : : }
1134 [ + + ]: 107978 : }
1135 [ + - ]: 107355 : Trace("sg-gen-tg-debug") << "Will consider term canon " << ln << std::endl;
1136 [ + - ]: 107355 : Trace("sg-gen-consider-term-debug") << std::endl;
1137 : 107355 : return true;
1138 : : }
1139 : :
1140 : 183414 : unsigned ConjectureGenerator::collectFunctions( TNode opat, TNode pat, std::map< TNode, unsigned >& funcs,
1141 : : std::map< TypeNode, unsigned >& mnvn, std::map< TypeNode, unsigned >& mxvn ){
1142 [ + + ]: 183414 : if( pat.hasOperator() ){
1143 : 81930 : funcs[pat.getOperator()]++;
1144 [ - + ]: 81930 : if( !d_tge.isRelevantFunc( pat.getOperator() ) ){
1145 : 0 : d_pattern_is_relevant[opat] = false;
1146 : : }
1147 : 81930 : unsigned sum = 1;
1148 [ + + ]: 228055 : for( unsigned i=0; i<pat.getNumChildren(); i++ ){
1149 : 146125 : sum += collectFunctions( opat, pat[i], funcs, mnvn, mxvn );
1150 : : }
1151 : 81930 : return sum;
1152 : : }else{
1153 [ - + ][ - + ]: 101484 : Assert(pat.getNumChildren() == 0);
[ - - ]
1154 : 101484 : funcs[pat]++;
1155 : : //for variables
1156 [ + + ]: 101484 : if (pat.getKind() == Kind::BOUND_VARIABLE)
1157 : : {
1158 [ + + ]: 101466 : if( funcs[pat]>1 ){
1159 : : //duplicate variable
1160 : 861 : d_pattern_var_duplicate[opat]++;
1161 : : }else{
1162 : : //check for max/min
1163 : 100605 : TypeNode tn = pat.getType();
1164 : 100605 : unsigned vn = pat.getAttribute(InstVarNumAttribute());
1165 : 100605 : std::map< TypeNode, unsigned >::iterator it = mnvn.find( tn );
1166 [ + + ]: 100605 : if( it!=mnvn.end() ){
1167 [ - + ]: 58473 : if( vn<it->second ){
1168 : 0 : d_pattern_is_normal[opat] = false;
1169 : 0 : mnvn[tn] = vn;
1170 [ - + ]: 58473 : }else if( vn>mxvn[tn] ){
1171 [ - - ]: 0 : if( vn!=mxvn[tn]+1 ){
1172 : 0 : d_pattern_is_normal[opat] = false;
1173 : : }
1174 : 0 : mxvn[tn] = vn;
1175 : : }
1176 : : }else{
1177 : : //first variable of this type
1178 : 42132 : mnvn[tn] = vn;
1179 : 42132 : mxvn[tn] = vn;
1180 : : }
1181 : 100605 : }
1182 : : }
1183 : : else
1184 : : {
1185 : 18 : d_pattern_is_relevant[opat] = false;
1186 : : }
1187 : 101484 : return 1;
1188 : : }
1189 : : }
1190 : :
1191 : 202749 : void ConjectureGenerator::registerPattern( Node pat, TypeNode tpat ) {
1192 [ + + ]: 202749 : if( std::find( d_patterns[tpat].begin(), d_patterns[tpat].end(), pat )==d_patterns[tpat].end() ){
1193 : 37289 : d_patterns[TypeNode::null()].push_back( pat );
1194 : 37289 : d_patterns[tpat].push_back( pat );
1195 : :
1196 [ - + ][ - + ]: 37289 : Assert(d_pattern_fun_id.find(pat) == d_pattern_fun_id.end());
[ - - ]
1197 [ - + ][ - + ]: 37289 : Assert(d_pattern_var_id.find(pat) == d_pattern_var_id.end());
[ - - ]
1198 : :
1199 : : //collect functions
1200 : 37289 : std::map< TypeNode, unsigned > mnvn;
1201 : 37289 : d_pattern_fun_sum[pat] = collectFunctions( pat, pat, d_pattern_fun_id[pat], mnvn, d_pattern_var_id[pat] );
1202 [ + - ]: 37289 : if( d_pattern_is_normal.find( pat )==d_pattern_is_normal.end() ){
1203 : 37289 : d_pattern_is_normal[pat] = true;
1204 : : }
1205 [ + + ]: 37289 : if( d_pattern_is_relevant.find( pat )==d_pattern_is_relevant.end() ){
1206 : 37271 : d_pattern_is_relevant[pat] = true;
1207 : : }
1208 : 37289 : }
1209 : 202749 : }
1210 : :
1211 : 794 : bool ConjectureGenerator::isGeneralization( TNode patg, TNode pat, std::map< TNode, TNode >& subs ) {
1212 [ + + ]: 794 : if (patg.getKind() == Kind::BOUND_VARIABLE)
1213 : : {
1214 : 24 : std::map< TNode, TNode >::iterator it = subs.find( patg );
1215 [ - + ]: 24 : if( it!=subs.end() ){
1216 : 0 : return it->second==pat;
1217 : : }else{
1218 : 24 : subs[patg] = pat;
1219 : 24 : return true;
1220 : : }
1221 : : }
1222 : : else
1223 : : {
1224 [ - + ][ - + ]: 770 : Assert(patg.hasOperator());
[ - - ]
1225 : 770 : if( !pat.hasOperator() || patg.getOperator()!=pat.getOperator() ){
1226 : 680 : return false;
1227 : : }else{
1228 [ - + ][ - + ]: 90 : Assert(patg.getNumChildren() == pat.getNumChildren());
[ - - ]
1229 [ + - ]: 114 : for( unsigned i=0; i<patg.getNumChildren(); i++ ){
1230 [ + + ]: 114 : if( !isGeneralization( patg[i], pat[i], subs ) ){
1231 : 90 : return false;
1232 : : }
1233 : : }
1234 : 0 : return true;
1235 : : }
1236 : : }
1237 : : }
1238 : :
1239 : 0 : int ConjectureGenerator::calculateGeneralizationDepth( TNode n, std::vector< TNode >& fv ) {
1240 [ - - ]: 0 : if (n.getKind() == Kind::BOUND_VARIABLE)
1241 : : {
1242 [ - - ]: 0 : if( std::find( fv.begin(), fv.end(), n )==fv.end() ){
1243 : 0 : fv.push_back( n );
1244 : 0 : return 0;
1245 : : }else{
1246 : 0 : return 1;
1247 : : }
1248 : : }
1249 : : else
1250 : : {
1251 : 0 : int depth = 1;
1252 [ - - ]: 0 : for( unsigned i=0; i<n.getNumChildren(); i++ ){
1253 : 0 : depth += calculateGeneralizationDepth( n[i], fv );
1254 : : }
1255 : 0 : return depth;
1256 : : }
1257 : : }
1258 : :
1259 : 252 : Node ConjectureGenerator::getPredicateForType( TypeNode tn ) {
1260 : 252 : std::map< TypeNode, Node >::iterator it = d_typ_pred.find( tn );
1261 [ + + ]: 252 : if( it==d_typ_pred.end() ){
1262 : 140 : NodeManager* nm = nodeManager();
1263 : 140 : TypeNode op_tn = nm->mkFunctionType(tn, nm->booleanType());
1264 : 280 : Node op = NodeManager::mkDummySkolem("PE", op_tn);
1265 : 140 : d_typ_pred[tn] = op;
1266 : 140 : return op;
1267 : 140 : }else{
1268 : 112 : return it->second;
1269 : : }
1270 : : }
1271 : :
1272 : 252 : void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< Node >& terms ) {
1273 [ + - ]: 252 : if( n.getNumChildren()>0 ){
1274 [ + - ]: 504 : Trace("sg-gt-enum-debug") << "Get enumerate uf terms " << n << " (" << num
1275 : 252 : << ")" << std::endl;
1276 : 252 : TermEnumeration* te = d_treg.getTermEnumeration();
1277 : : // below, we do a fair enumeration of vectors vec of indices whose sum is
1278 : : // 1,2,3, ...
1279 : 252 : std::vector< int > vec;
1280 : 252 : std::vector< TypeNode > types;
1281 [ + + ]: 667 : for( unsigned i=0; i<n.getNumChildren(); i++ ){
1282 : 415 : vec.push_back( 0 );
1283 : 415 : TypeNode tn = n[i].getType();
1284 [ + - ]: 415 : if (tn.isClosedEnumerable())
1285 : : {
1286 : 415 : types.push_back( tn );
1287 : : }else{
1288 : 0 : return;
1289 : : }
1290 [ + - ]: 415 : }
1291 : : // the index of the last child is determined by the limit of the sum
1292 : : // of indices of children (size_limit) and the sum of the indices of the
1293 : : // other children (vec_sum). Hence, we pop here and add this value at each
1294 : : // iteration of the loop.
1295 : 252 : vec.pop_back();
1296 : 252 : int size_limit = 0;
1297 : 252 : int vec_sum = -1;
1298 : 252 : unsigned index = 0;
1299 : 252 : unsigned last_size = terms.size();
1300 [ + + ]: 19422 : while( terms.size()<num ){
1301 [ + + ]: 19170 : if( vec_sum==-1 ){
1302 : 6584 : vec_sum = 0;
1303 : : // we will construct a new child below
1304 : : // since sum is 0, the index of last child is limit
1305 : 6584 : vec.push_back( size_limit );
1306 : : }
1307 [ + + ]: 12586 : else if (index < vec.size())
1308 : : {
1309 [ - + ][ - + ]: 7539 : Assert(index < types.size());
[ - - ]
1310 : : //see if we can iterate current
1311 : 15078 : if (vec_sum < size_limit
1312 : 7539 : && !te->getEnumerateTerm(types[index], vec[index] + 1).isNull())
1313 : : {
1314 : 6016 : vec[index]++;
1315 : 6016 : vec_sum++;
1316 : : // we will construct a new child below
1317 : : // add the index of the last child, its index is (limit-sum)
1318 : 6016 : vec.push_back( size_limit - vec_sum );
1319 : : }else{
1320 : : // reset the index
1321 : 1523 : vec_sum -= vec[index];
1322 : 1523 : vec[index] = 0;
1323 : 1523 : index++;
1324 : : }
1325 : : }
1326 [ + + ]: 19170 : if (index < vec.size())
1327 : : {
1328 : : // if we are ready to construct the term
1329 [ + + ]: 12838 : if( vec.size()==n.getNumChildren() ){
1330 : : Node lc =
1331 : 12600 : te->getEnumerateTerm(types[vec.size() - 1], vec[vec.size() - 1]);
1332 [ + - ]: 12600 : if( !lc.isNull() ){
1333 [ + + ]: 33350 : for( unsigned i=0; i<vec.size(); i++ ){
1334 [ + - ]: 20750 : Trace("sg-gt-enum-debug") << vec[i] << " ";
1335 : : }
1336 [ + - ]: 12600 : Trace("sg-gt-enum-debug") << " / " << size_limit << std::endl;
1337 [ + + ]: 33350 : for( unsigned i=0; i<n.getNumChildren(); i++ ){
1338 : 20750 : Trace("sg-gt-enum-debug") << n[i].getType() << " ";
1339 : : }
1340 [ + - ]: 12600 : Trace("sg-gt-enum-debug") << std::endl;
1341 : 12600 : std::vector< Node > children;
1342 : 12600 : children.push_back( n.getOperator() );
1343 [ + + ]: 20750 : for( unsigned i=0; i<(vec.size()-1); i++ ){
1344 : 8150 : Node nn = te->getEnumerateTerm(types[i], vec[i]);
1345 [ - + ][ - + ]: 8150 : Assert(!nn.isNull());
[ - - ]
1346 [ - + ][ - + ]: 8150 : Assert(nn.getType() == n[i].getType());
[ - - ]
1347 : 8150 : children.push_back( nn );
1348 : 8150 : }
1349 : 12600 : children.push_back( lc );
1350 : : Node nenum =
1351 : 12600 : nodeManager()->mkNode(Kind::APPLY_UF, children);
1352 [ + - ]: 25200 : Trace("sg-gt-enum")
1353 : 12600 : << "Ground term enumerate : " << nenum << std::endl;
1354 : 12600 : terms.push_back(nenum);
1355 : 12600 : }
1356 : : // pop the index for the last child
1357 : 12600 : vec.pop_back();
1358 : 12600 : index = 0;
1359 : 12600 : }
1360 : : }else{
1361 : : // no more indices to increment, we reset and increment size_limit
1362 [ + - ]: 6332 : if( terms.size()>last_size ){
1363 : 6332 : last_size = terms.size();
1364 : 6332 : size_limit++;
1365 [ + + ]: 7687 : for( unsigned i=0; i<vec.size(); i++ ){
1366 : 1355 : vec[i] = 0;
1367 : : }
1368 : 6332 : vec_sum = -1;
1369 : : }else{
1370 : : // No terms were generated at the previous size.
1371 : : // Thus, we've saturated, no more terms can be enumerated.
1372 : 0 : return;
1373 : : }
1374 : : }
1375 : : }
1376 [ + - ][ + - ]: 252 : }else{
1377 : 0 : terms.push_back( n );
1378 : : }
1379 : : }
1380 : :
1381 : 252 : void ConjectureGenerator::getEnumeratePredUfTerm( Node n, unsigned num, std::vector< Node >& terms ) {
1382 : 252 : std::vector< Node > uf_terms;
1383 : 252 : getEnumerateUfTerm( n, num, uf_terms );
1384 : 252 : Node p = getPredicateForType( n.getType() );
1385 [ + + ]: 12852 : for( unsigned i=0; i<uf_terms.size(); i++ ){
1386 : 12600 : terms.push_back(NodeManager::mkNode(Kind::APPLY_UF, p, uf_terms[i]));
1387 : : }
1388 : 252 : }
1389 : :
1390 : 839009 : void ConjectureGenerator::processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth ) {
1391 : 839009 : int score = considerCandidateConjecture( lhs, rhs );
1392 [ + + ]: 839009 : if( score>0 ){
1393 [ + - ]: 852 : Trace("sg-conjecture") << "* Candidate conjecture : " << lhs << " == " << rhs << std::endl;
1394 [ + - ]: 852 : Trace("sg-conjecture-debug") << " LHS, RHS generalization depth : " << lhs_depth << ", " << rhs_depth << std::endl;
1395 [ + - ]: 852 : Trace("sg-conjecture-debug") << " confirmed = " << d_subs_confirmCount << ", #witnesses range = " << d_subs_confirmWitnessRange.size() << "." << std::endl;
1396 [ + - ]: 852 : Trace("sg-conjecture-debug") << " #witnesses for ";
1397 : 852 : bool firstTime = true;
1398 [ + + ]: 3203 : for( std::map< TNode, std::vector< TNode > >::iterator it = d_subs_confirmWitnessDomain.begin(); it != d_subs_confirmWitnessDomain.end(); ++it ){
1399 [ + + ]: 2351 : if( !firstTime ){
1400 [ + - ]: 1499 : Trace("sg-conjecture-debug") << ", ";
1401 : : }
1402 [ + - ]: 2351 : Trace("sg-conjecture-debug") << it->first << " : " << it->second.size();
1403 : : //if( it->second.size()==1 ){
1404 : : // Trace("sg-conjecture-debug") << " (" << it->second[0] << ")";
1405 : : //}
1406 [ + - ]: 2351 : Trace("sg-conjecture-debug2") << " (";
1407 [ + + ]: 23376 : for( unsigned j=0; j<it->second.size(); j++ ){
1408 [ + + ][ + - ]: 21025 : if( j>0 ){ Trace("sg-conjecture-debug2") << " "; }
1409 [ + - ]: 21025 : Trace("sg-conjecture-debug2") << d_ground_eqc_map[it->second[j]];
1410 : : }
1411 [ + - ]: 2351 : Trace("sg-conjecture-debug2") << ")";
1412 : 2351 : firstTime = false;
1413 : : }
1414 [ + - ]: 852 : Trace("sg-conjecture-debug") << std::endl;
1415 [ + - ]: 852 : Trace("sg-conjecture-debug") << " unknown = " << d_subs_unkCount << std::endl;
1416 : : //Assert( getUniversalRepresentative( rhs )==rhs );
1417 : : //Assert( getUniversalRepresentative( lhs )==lhs );
1418 : 852 : d_waiting_conjectures_lhs.push_back( lhs );
1419 : 852 : d_waiting_conjectures_rhs.push_back( rhs );
1420 : 852 : d_waiting_conjectures_score.push_back( score );
1421 : 852 : d_waiting_conjectures[lhs].push_back( rhs );
1422 : 852 : d_waiting_conjectures[rhs].push_back( lhs );
1423 : : }else{
1424 [ + - ]: 838157 : Trace("sg-conjecture-debug2") << "...do not consider " << lhs << " == " << rhs << ", score = " << score << std::endl;
1425 : : }
1426 : 839009 : }
1427 : :
1428 : 839009 : int ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) {
1429 [ - + ][ - + ]: 839009 : Assert(lhs.getType() == rhs.getType());
[ - - ]
1430 : :
1431 [ + - ]: 839009 : Trace("sg-cconj-debug") << "Consider candidate conjecture : " << lhs << " == " << rhs << "?" << std::endl;
1432 [ + + ]: 839009 : if( lhs==rhs ){
1433 [ + - ]: 2149 : Trace("sg-cconj-debug") << " -> trivial." << std::endl;
1434 : 2149 : return -1;
1435 : : }
1436 : 836860 : if (lhs.getKind() == Kind::APPLY_CONSTRUCTOR
1437 [ + + ][ + + ]: 836860 : && rhs.getKind() == Kind::APPLY_CONSTRUCTOR)
[ + + ]
1438 : : {
1439 [ + - ]: 51326 : Trace("sg-cconj-debug")
1440 : 25663 : << " -> irrelevant by syntactic analysis." << std::endl;
1441 : 25663 : return -1;
1442 : : }
1443 : : // variables of LHS must subsume variables of RHS
1444 [ + + ]: 1623566 : for (std::pair<const TypeNode, unsigned>& p : d_pattern_var_id[rhs])
1445 : : {
1446 : : std::map<TypeNode, unsigned>::iterator itl =
1447 : 844029 : d_pattern_var_id[lhs].find(p.first);
1448 [ + + ]: 844029 : if (itl == d_pattern_var_id[lhs].end())
1449 : : {
1450 [ + - ]: 63320 : Trace("sg-cconj-debug")
1451 : 31660 : << " -> has no variables of sort " << p.first << "." << std::endl;
1452 : 31660 : return -1;
1453 : : }
1454 [ - + ]: 812369 : if (itl->second < p.second)
1455 : : {
1456 [ - - ]: 0 : Trace("sg-cconj-debug") << " -> variables of sort " << p.first
1457 : 0 : << " are not subsumed." << std::endl;
1458 : 0 : return -1;
1459 : : }
1460 [ + - ]: 1624738 : Trace("sg-cconj-debug2")
1461 : 0 : << " variables of sort " << p.first << " are : " << itl->second
1462 : 812369 : << " vs " << p.second << std::endl;
1463 : : }
1464 : :
1465 : : // currently active conjecture?
1466 : : std::map<Node, std::vector<Node> >::iterator iteq =
1467 : 779537 : d_eq_conjectures.find(lhs);
1468 [ + + ]: 779537 : if (iteq != d_eq_conjectures.end())
1469 : : {
1470 : 352604 : if (std::find(iteq->second.begin(), iteq->second.end(), rhs)
1471 [ + + ]: 705208 : != iteq->second.end())
1472 : : {
1473 [ + - ]: 2118 : Trace("sg-cconj-debug")
1474 : 1059 : << " -> this conjecture is already active." << std::endl;
1475 : 1059 : return -1;
1476 : : }
1477 : : }
1478 : : // current a waiting conjecture?
1479 : : std::map<Node, std::vector<Node> >::iterator itw =
1480 : 778478 : d_waiting_conjectures.find(lhs);
1481 [ + + ]: 778478 : if (itw != d_waiting_conjectures.end())
1482 : : {
1483 : 40071 : if (std::find(itw->second.begin(), itw->second.end(), rhs)
1484 [ + + ]: 80142 : != itw->second.end())
1485 : : {
1486 [ + - ]: 26 : Trace("sg-cconj-debug")
1487 : 13 : << " -> already are considering this conjecture." << std::endl;
1488 : 13 : return -1;
1489 : : }
1490 : : }
1491 : :
1492 : : size_t score;
1493 : 778465 : bool scoreSet = false;
1494 : :
1495 [ + - ]: 1556930 : Trace("sg-cconj") << "Consider possible candidate conjecture : " << lhs
1496 : 778465 : << " == " << rhs << "?" << std::endl;
1497 : : // find witness for counterexample, if possible
1498 [ - + ][ - + ]: 778465 : Assert(d_rel_pattern_var_sum.find(lhs) != d_rel_pattern_var_sum.end());
[ - - ]
1499 [ + - ]: 1556930 : Trace("sg-cconj-debug") << "Notify substitutions over "
1500 : 0 : << d_rel_pattern_var_sum[lhs] << " variables."
1501 : 778465 : << std::endl;
1502 : 778465 : std::map<TNode, TNode> subs;
1503 : 778465 : d_subs_confirmCount = 0;
1504 : 778465 : d_subs_confirmWitnessRange.clear();
1505 : 778465 : d_subs_confirmWitnessDomain.clear();
1506 : 778465 : d_subs_unkCount = 0;
1507 [ + + ]: 1556930 : if (!d_rel_pattern_subs_index[lhs].notifySubstitutions(
1508 : 778465 : this, subs, rhs, d_rel_pattern_var_sum[lhs]))
1509 : : {
1510 [ + - ]: 255438 : Trace("sg-cconj") << " -> found witness that falsifies the conjecture."
1511 : 127719 : << std::endl;
1512 : 127719 : return -1;
1513 : : }
1514 : : // score is the minimum number of distinct substitutions for a variable
1515 : 650746 : for (std::pair<const TNode, std::vector<TNode> >& w :
1516 [ + + ]: 1303843 : d_subs_confirmWitnessDomain)
1517 : : {
1518 : 2351 : size_t num = w.second.size();
1519 [ + + ][ + + ]: 2351 : if (!scoreSet || num < score)
1520 : : {
1521 : 887 : score = num;
1522 : 887 : scoreSet = true;
1523 : : }
1524 : : }
1525 [ + + ]: 650746 : if (!scoreSet)
1526 : : {
1527 : 649894 : score = 0;
1528 : : }
1529 [ - + ]: 650746 : if (TraceIsOn("sg-cconj"))
1530 : : {
1531 [ - - ]: 0 : Trace("sg-cconj") << " confirmed = " << d_subs_confirmCount
1532 : 0 : << ", #witnesses range = "
1533 : 0 : << d_subs_confirmWitnessRange.size() << "." << std::endl;
1534 : 0 : for (std::pair<const TNode, std::vector<TNode> >& w :
1535 [ - - ]: 0 : d_subs_confirmWitnessDomain)
1536 : : {
1537 [ - - ]: 0 : Trace("sg-cconj") << " #witnesses for " << w.first << " : "
1538 : 0 : << w.second.size() << std::endl;
1539 : : }
1540 [ - - ]: 0 : Trace("sg-cconj") << " -> SUCCESS." << std::endl;
1541 [ - - ]: 0 : Trace("sg-cconj") << " score : " << score << std::endl;
1542 : : }
1543 : 650746 : return static_cast<int>(score);
1544 : 778465 : }
1545 : :
1546 : 101627113 : bool ConjectureGenerator::notifySubstitution( TNode glhs, std::map< TNode, TNode >& subs, TNode rhs ) {
1547 [ - + ]: 101627113 : if( TraceIsOn("sg-cconj-debug") ){
1548 [ - - ]: 0 : Trace("sg-cconj-debug") << "Ground eqc for LHS : " << glhs << ", based on substitution: " << std::endl;
1549 [ - - ]: 0 : for( std::map< TNode, TNode >::iterator it = subs.begin(); it != subs.end(); ++it ){
1550 : 0 : Assert(getRepresentative(it->second) == it->second);
1551 [ - - ]: 0 : Trace("sg-cconj-debug") << " " << it->first << " -> " << it->second << std::endl;
1552 : : }
1553 : : }
1554 [ + - ]: 101627113 : Trace("sg-cconj-debug") << "Evaluate RHS : : " << rhs << std::endl;
1555 : : //get the representative of rhs with substitution subs
1556 : 101627113 : EntailmentCheck* echeck = d_treg.getEntailmentCheck();
1557 : 101627113 : TNode grhs = echeck->getEntailedTerm(rhs, subs, true);
1558 [ + - ]: 101627113 : Trace("sg-cconj-debug") << "...done evaluating term, got : " << grhs << std::endl;
1559 [ + + ]: 101627113 : if( !grhs.isNull() ){
1560 [ + + ]: 279806 : if( glhs!=grhs ){
1561 [ + - ]: 127719 : Trace("sg-cconj-debug") << "Ground eqc for RHS : " << grhs << std::endl;
1562 : : //check based on ground terms
1563 : 127719 : std::map< TNode, Node >::iterator itl = d_ground_eqc_map.find( glhs );
1564 [ + - ]: 127719 : if( itl!=d_ground_eqc_map.end() ){
1565 : 127719 : std::map< TNode, Node >::iterator itr = d_ground_eqc_map.find( grhs );
1566 [ + + ]: 127719 : if( itr!=d_ground_eqc_map.end() ){
1567 [ + - ]: 46744 : Trace("sg-cconj-debug") << "We have ground terms " << itl->second << " and " << itr->second << "." << std::endl;
1568 [ + + ][ + + ]: 46744 : if( itl->second.isConst() && itr->second.isConst() ){
[ + + ]
1569 [ + - ]: 20179 : Trace("sg-cconj-debug") << "...disequal constants." << std::endl;
1570 [ + - ]: 20179 : Trace("sg-cconj-witness") << " Witness of falsification : " << itl->second << " != " << itr->second << ", substutition is : " << std::endl;
1571 [ + + ]: 75935 : for( std::map< TNode, TNode >::iterator it = subs.begin(); it != subs.end(); ++it ){
1572 [ + - ]: 55756 : Trace("sg-cconj-witness") << " " << it->first << " -> " << it->second << std::endl;
1573 : : }
1574 : 20179 : return false;
1575 : : }
1576 : : }
1577 : : }
1578 : : }
1579 [ + - ]: 259627 : Trace("sg-cconj-debug") << "RHS is identical." << std::endl;
1580 : 259627 : bool isGroundSubs = true;
1581 [ + + ]: 1072871 : for( std::map< TNode, TNode >::iterator it = subs.begin(); it != subs.end(); ++it ){
1582 : 813244 : std::map< TNode, Node >::iterator git = d_ground_eqc_map.find( it->second );
1583 [ - + ]: 813244 : if( git==d_ground_eqc_map.end() ){
1584 : 0 : isGroundSubs = false;
1585 : 0 : break;
1586 : : }
1587 : : }
1588 [ + - ]: 259627 : if( isGroundSubs ){
1589 [ + + ]: 259627 : if( glhs==grhs ){
1590 [ + - ]: 152087 : Trace("sg-cconj-witness") << " Witnessed " << glhs << " == " << grhs << ", substutition is : " << std::endl;
1591 [ + + ]: 575224 : for( std::map< TNode, TNode >::iterator it = subs.begin(); it != subs.end(); ++it ){
1592 [ + - ]: 423137 : Trace("sg-cconj-witness") << " " << it->first << " -> " << it->second << std::endl;
1593 [ + + ]: 423137 : if( std::find( d_subs_confirmWitnessDomain[it->first].begin(), d_subs_confirmWitnessDomain[it->first].end(), it->second )==d_subs_confirmWitnessDomain[it->first].end() ){
1594 : 68014 : d_subs_confirmWitnessDomain[it->first].push_back( it->second );
1595 : : }
1596 : : }
1597 : 152087 : d_subs_confirmCount++;
1598 [ + + ]: 152087 : if( std::find( d_subs_confirmWitnessRange.begin(), d_subs_confirmWitnessRange.end(), glhs )==d_subs_confirmWitnessRange.end() ){
1599 : 42031 : d_subs_confirmWitnessRange.push_back( glhs );
1600 : : }
1601 : : }else{
1602 [ + - ]: 107540 : if( optFilterUnknown() ){
1603 [ + - ]: 107540 : Trace("sg-cconj-debug") << "...ground substitution giving terms that are neither equal nor disequal." << std::endl;
1604 : 107540 : return false;
1605 : : }
1606 : : }
1607 : : }
1608 : : }else{
1609 [ + - ]: 101347307 : Trace("sg-cconj-debug") << "(could not ground eqc for RHS)." << std::endl;
1610 : : }
1611 : 101499394 : return true;
1612 : 101627113 : }
1613 : :
1614 : :
1615 : :
1616 : :
1617 : :
1618 : :
1619 : 42566 : void TermGenerator::reset( TermGenEnv * s, TypeNode tn ) {
1620 [ - + ][ - + ]: 42566 : Assert(d_children.empty());
[ - - ]
1621 : 42566 : d_typ = tn;
1622 : 42566 : d_status = 0;
1623 : 42566 : d_status_num = 0;
1624 : 42566 : d_children.clear();
1625 [ + - ]: 42566 : Trace("sg-gen-tg-debug2") << "...add to context " << this << std::endl;
1626 : 42566 : d_id = s->d_tg_id;
1627 : 42566 : s->changeContext( true );
1628 : 42566 : }
1629 : :
1630 : 652871 : bool TermGenerator::getNextTerm( TermGenEnv * s, unsigned depth ) {
1631 [ - + ]: 652871 : if( TraceIsOn("sg-gen-tg-debug2") ){
1632 [ - - ]: 0 : Trace("sg-gen-tg-debug2") << this << " getNextTerm depth " << depth << " : status = " << d_status << ", num = " << d_status_num;
1633 [ - - ]: 0 : if( d_status==5 ){
1634 : 0 : TNode f = s->getTgFunc( d_typ, d_status_num );
1635 [ - - ]: 0 : Trace("sg-gen-tg-debug2") << ", f = " << f;
1636 [ - - ]: 0 : Trace("sg-gen-tg-debug2") << ", #args = " << s->d_func_args[f].size();
1637 [ - - ]: 0 : Trace("sg-gen-tg-debug2") << ", childNum = " << d_status_child_num;
1638 [ - - ]: 0 : Trace("sg-gen-tg-debug2") << ", #children = " << d_children.size();
1639 : 0 : }
1640 [ - - ]: 0 : Trace("sg-gen-tg-debug2") << std::endl;
1641 : : }
1642 : :
1643 [ + + ]: 652871 : if( d_status==0 ){
1644 : 42566 : d_status++;
1645 [ + + ]: 42566 : if( !d_typ.isNull() ){
1646 [ + + ]: 41783 : if( s->allowVar( d_typ ) ){
1647 : : //allocate variable
1648 : 14216 : d_status_num = s->d_var_id[d_typ];
1649 : 14216 : s->addVar( d_typ );
1650 [ + - ]: 14216 : Trace("sg-gen-tg-debug2") << this << " ...return unique var #" << d_status_num << std::endl;
1651 [ + + ]: 14216 : return s->considerCurrentTerm() ? true : getNextTerm( s, depth );
1652 : : }else{
1653 : : //check allocating new variable
1654 : 27567 : d_status++;
1655 : 27567 : d_status_num = -1;
1656 [ - + ]: 27567 : if( s->d_gen_relevant_terms ){
1657 : 0 : s->d_tg_gdepth++;
1658 : : }
1659 : 27567 : return getNextTerm( s, depth );
1660 : : }
1661 : : }else{
1662 : 783 : d_status = 4;
1663 : 783 : d_status_num = -1;
1664 : 783 : return getNextTerm( s, depth );
1665 : : }
1666 [ + + ]: 610305 : }else if( d_status==2 ){
1667 : : //cleanup previous information
1668 : : //if( d_status_num>=0 ){
1669 : : // s->d_var_eq_tg[d_status_num].pop_back();
1670 : : //}
1671 : : //check if there is another variable
1672 [ + + ]: 136168 : if( (d_status_num+1)<(int)s->getNumTgVars( d_typ ) ){
1673 : 94385 : d_status_num++;
1674 : : //we have equated two variables
1675 : : //s->d_var_eq_tg[d_status_num].push_back( d_id );
1676 [ + - ]: 94385 : Trace("sg-gen-tg-debug2") << this << "...consider other var #" << d_status_num << std::endl;
1677 [ + + ]: 94385 : return s->considerCurrentTerm() ? true : getNextTerm( s, depth );
1678 : : }else{
1679 [ + + ]: 41783 : if( s->d_gen_relevant_terms ){
1680 : 13613 : s->d_tg_gdepth--;
1681 : : }
1682 : 41783 : d_status++;
1683 : 41783 : return getNextTerm( s, depth );
1684 : : }
1685 [ + + ]: 474137 : }else if( d_status==4 ){
1686 : 116802 : d_status++;
1687 [ + + ][ + + ]: 116802 : if( depth>0 && (d_status_num+1)<(int)s->getNumTgFuncs( d_typ ) ){
[ + + ][ + + ]
[ - - ]
1688 : 74236 : d_status_num++;
1689 : 74236 : d_status_child_num = 0;
1690 : 74236 : Trace("sg-gen-tg-debug2") << this << "...consider function " << s->getTgFunc( d_typ, d_status_num ) << std::endl;
1691 : 74236 : s->d_tg_gdepth++;
1692 [ + + ]: 74236 : if( !s->considerCurrentTerm() ){
1693 : 55799 : s->d_tg_gdepth--;
1694 : : //don't consider this function
1695 : 55799 : d_status--;
1696 : : }else{
1697 : : //we have decided on a function application
1698 : : }
1699 : 74236 : return getNextTerm( s, depth );
1700 : : }else{
1701 : : //do not choose function applications at depth 0
1702 : 42566 : d_status++;
1703 : 42566 : return getNextTerm( s, depth );
1704 : : }
1705 [ + + ]: 357335 : }else if( d_status==5 ){
1706 : : //iterating over arguments
1707 : 258770 : TNode f = s->getTgFunc( d_typ, d_status_num );
1708 [ + + ]: 258770 : if( d_status_child_num<0 ){
1709 : : //no more arguments
1710 : 18437 : s->d_tg_gdepth--;
1711 : 18437 : d_status--;
1712 : 18437 : return getNextTerm( s, depth );
1713 [ + + ]: 240333 : }else if( d_status_child_num==(int)s->d_func_args[f].size() ){
1714 : 69550 : d_status_child_num--;
1715 [ + + ]: 69550 : return s->considerCurrentTermCanon( d_id ) ? true : getNextTerm( s, depth );
1716 : : //return true;
1717 : : }else{
1718 [ - + ][ - + ]: 170783 : Assert(d_status_child_num < (int)s->d_func_args[f].size());
[ - - ]
1719 [ + + ]: 170783 : if( d_status_child_num==(int)d_children.size() ){
1720 : 39890 : d_children.push_back( s->d_tg_id );
1721 [ - + ][ - + ]: 39890 : Assert(s->d_tg_alloc.find(s->d_tg_id) == s->d_tg_alloc.end());
[ - - ]
1722 : 39890 : s->d_tg_alloc[d_children[d_status_child_num]].reset( s, s->d_func_args[f][d_status_child_num] );
1723 : 39890 : return getNextTerm( s, depth );
1724 : : }else{
1725 [ - + ][ - + ]: 130893 : Assert(d_status_child_num + 1 == (int)d_children.size());
[ - - ]
1726 [ + + ]: 130893 : if( s->d_tg_alloc[d_children[d_status_child_num]].getNextTerm( s, depth-1 ) ){
1727 : 91003 : d_status_child_num++;
1728 : 91003 : return getNextTerm( s, depth );
1729 : : }else{
1730 [ + - ]: 79780 : Trace("sg-gen-tg-debug2")
1731 : 39890 : << "...remove child from context " << std::endl;
1732 : 39890 : s->changeContext(false);
1733 : 39890 : d_children.pop_back();
1734 : 39890 : d_status_child_num--;
1735 : 39890 : return getNextTerm( s, depth );
1736 : : }
1737 : : }
1738 : : }
1739 [ + + ][ + + ]: 357335 : }else if( d_status==1 || d_status==3 ){
1740 [ + + ]: 55999 : if( d_status==1 ){
1741 : 14216 : s->removeVar( d_typ );
1742 [ - + ][ - + ]: 14216 : Assert(d_status_num == (int)s->d_var_id[d_typ]);
[ - - ]
1743 : : //check if there is only one feasible equivalence class. if so, don't make pattern any more specific.
1744 : : //unsigned i = s->d_ccand_eqc[0].size()-1;
1745 : : //if( s->d_ccand_eqc[0][i].size()==1 && s->d_ccand_eqc[1][i].empty() ){
1746 : : // d_status = 6;
1747 : : // return getNextTerm( s, depth );
1748 : : //}
1749 : 14216 : s->d_tg_gdepth++;
1750 : : }
1751 : 55999 : d_status++;
1752 : 55999 : d_status_num = -1;
1753 : 55999 : return getNextTerm( s, depth );
1754 : : }else{
1755 [ - + ][ - + ]: 42566 : Assert(d_children.empty());
[ - - ]
1756 : 42566 : return false;
1757 : : }
1758 : : }
1759 : :
1760 : 10721921 : void TermGenerator::resetMatching(unsigned mode)
1761 : : {
1762 : 10721921 : d_match_status = 0;
1763 : 10721921 : d_match_status_child_num = 0;
1764 : 10721921 : d_match_children.clear();
1765 : 10721921 : d_match_children_end.clear();
1766 : 10721921 : d_match_mode = mode;
1767 : : //if this term generalizes, it must generalize a non-ground term
1768 : : //if( (d_match_mode & ( 1 << 2 ))!=0 && s->isGroundEqc( eqc ) && d_status==5 ){
1769 : : // d_match_status = -1;
1770 : : //}
1771 : 10721921 : }
1772 : :
1773 : 43029623 : bool TermGenerator::getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode, std::map< unsigned, TNode > >& subs, std::map< TNode, bool >& rev_subs ) {
1774 [ - + ]: 43029623 : if( d_match_status<0 ){
1775 : 0 : return false;
1776 : : }
1777 [ - + ]: 43029623 : if( TraceIsOn("sg-gen-tg-match") ){
1778 [ - - ]: 0 : Trace("sg-gen-tg-match") << "Matching ";
1779 : 0 : debugPrint( s, "sg-gen-tg-match", "sg-gen-tg-match" );
1780 [ - - ]: 0 : Trace("sg-gen-tg-match") << " with eqc e" << s->d_cg->d_em[eqc] << "..." << std::endl;
1781 [ - - ]: 0 : Trace("sg-gen-tg-match") << " mstatus = " << d_match_status;
1782 [ - - ]: 0 : if( d_status==5 ){
1783 : 0 : TNode f = s->getTgFunc( d_typ, d_status_num );
1784 [ - - ]: 0 : Trace("sg-gen-tg-debug2") << ", f = " << f;
1785 [ - - ]: 0 : Trace("sg-gen-tg-debug2") << ", #args = " << s->d_func_args[f].size();
1786 [ - - ]: 0 : Trace("sg-gen-tg-debug2") << ", mchildNum = " << d_match_status_child_num;
1787 [ - - ]: 0 : Trace("sg-gen-tg-debug2") << ", #mchildren = " << d_match_children.size();
1788 : 0 : }
1789 [ - - ]: 0 : Trace("sg-gen-tg-debug2") << ", current substitution : {";
1790 [ - - ]: 0 : for( std::map< TypeNode, std::map< unsigned, TNode > >::iterator itt = subs.begin(); itt != subs.end(); ++itt ){
1791 [ - - ]: 0 : for( std::map< unsigned, TNode >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
1792 [ - - ]: 0 : Trace("sg-gen-tg-debug2") << " " << it->first << " -> e" << s->d_cg->d_em[it->second];
1793 : : }
1794 : : }
1795 [ - - ]: 0 : Trace("sg-gen-tg-debug2") << " } " << std::endl;
1796 : : }
1797 [ + + ]: 43029623 : if( d_status==1 ){
1798 : : //a variable
1799 [ + + ]: 8252883 : if( d_match_status==0 ){
1800 : 4807388 : d_match_status++;
1801 [ + + ]: 4807388 : if( (d_match_mode & ( 1 << 1 ))!=0 ){
1802 : : //only ground terms
1803 [ + + ]: 4394802 : if( !s->isGroundEqc( eqc ) ){
1804 : 64023 : return false;
1805 : : }
1806 : 412586 : }else if( (d_match_mode & ( 1 << 2 ))!=0 ){
1807 : : //only non-ground terms
1808 : : //if( s->isGroundEqc( eqc ) ){
1809 : : // return false;
1810 : : //}
1811 : : }
1812 : : //store the match : restricted if match_mode.0 = 1
1813 [ - + ]: 4743365 : if( (d_match_mode & ( 1 << 0 ))!=0 ){
1814 : 0 : std::map< TNode, bool >::iterator it = rev_subs.find( eqc );
1815 [ - - ]: 0 : if( it==rev_subs.end() ){
1816 : 0 : rev_subs[eqc] = true;
1817 : : }else{
1818 : 0 : return false;
1819 : : }
1820 : : }
1821 [ - + ][ - + ]: 4743365 : Assert(subs[d_typ].find(d_status_num) == subs[d_typ].end());
[ - - ]
1822 : 4743365 : subs[d_typ][d_status_num] = eqc;
1823 : 4743365 : return true;
1824 : : }else{
1825 : : //clean up
1826 : 3445495 : subs[d_typ].erase( d_status_num );
1827 [ - + ]: 3445495 : if( (d_match_mode & ( 1 << 0 ))!=0 ){
1828 : 0 : rev_subs.erase( eqc );
1829 : : }
1830 : 3445495 : return false;
1831 : : }
1832 [ + + ]: 34776740 : }else if( d_status==2 ){
1833 [ + + ]: 195938 : if( d_match_status==0 ){
1834 : 188814 : d_match_status++;
1835 [ - + ][ - + ]: 188814 : Assert(d_status_num < (int)s->getNumTgVars(d_typ));
[ - - ]
1836 : 188814 : std::map< unsigned, TNode >::iterator it = subs[d_typ].find( d_status_num );
1837 [ - + ][ - + ]: 188814 : Assert(it != subs[d_typ].end());
[ - - ]
1838 : 188814 : return it->second==eqc;
1839 : : }else{
1840 : 7124 : return false;
1841 : : }
1842 [ + - ]: 34580802 : }else if( d_status==5 ){
1843 : : //Assert( d_match_children.size()<=d_children.size() );
1844 : : //enumerating over f-applications in eqc
1845 [ + + ]: 34580802 : if( d_match_status_child_num<0 ){
1846 : 3634035 : return false;
1847 [ + + ]: 30946767 : }else if( d_match_status==0 ){
1848 : : //set up next binding
1849 [ + + ]: 18336243 : if( d_match_status_child_num==(int)d_match_children.size() ){
1850 [ + + ]: 13349410 : if( d_match_status_child_num==0 ){
1851 : : //initial binding
1852 : 5725719 : TNode f = s->getTgFunc( d_typ, d_status_num );
1853 [ - + ][ - + ]: 5725719 : Assert(!eqc.isNull());
[ - - ]
1854 : 5725719 : TNodeTrie* tat = s->getTermDatabase()->getTermArgTrie(eqc, f);
1855 [ + + ]: 5725719 : if( tat ){
1856 : 3218145 : d_match_children.push_back( tat->d_data.begin() );
1857 : 3218145 : d_match_children_end.push_back( tat->d_data.end() );
1858 : : }else{
1859 : 2507574 : d_match_status++;
1860 : 2507574 : d_match_status_child_num--;
1861 : 2507574 : return getNextMatch( s, eqc, subs, rev_subs );
1862 : : }
1863 [ + + ]: 5725719 : }else{
1864 : 7623691 : d_match_children.push_back( d_match_children[d_match_status_child_num-1]->second.d_data.begin() );
1865 : 7623691 : d_match_children_end.push_back( d_match_children[d_match_status_child_num-1]->second.d_data.end() );
1866 : : }
1867 : : }
1868 : 15828669 : d_match_status++;
1869 [ - + ][ - + ]: 15828669 : Assert(d_match_status_child_num + 1 == (int)d_match_children.size());
[ - - ]
1870 [ + + ]: 15828669 : if( d_match_children[d_match_status_child_num]==d_match_children_end[d_match_status_child_num] ){
1871 : : //no more arguments to bind
1872 : 3425268 : d_match_children.pop_back();
1873 : 3425268 : d_match_children_end.pop_back();
1874 : 3425268 : d_match_status_child_num--;
1875 : 3425268 : return getNextMatch( s, eqc, subs, rev_subs );
1876 : : }else{
1877 [ + + ]: 12403401 : if( d_match_status_child_num==(int)d_children.size() ){
1878 : : //successfully matched all children
1879 : 5101671 : d_match_children.pop_back();
1880 : 5101671 : d_match_children_end.pop_back();
1881 : 5101671 : d_match_status_child_num--;
1882 : 5101671 : return true;//return d_match_children[d_match_status]!=d_match_children_end[d_match_status];
1883 : : }else{
1884 : : //do next binding
1885 : 7301730 : s->d_tg_alloc[d_children[d_match_status_child_num]].resetMatching(
1886 : : d_match_mode);
1887 : 7301730 : return getNextMatch( s, eqc, subs, rev_subs );
1888 : : }
1889 : : }
1890 : : }else{
1891 [ - + ][ - + ]: 12610524 : Assert(d_match_status == 1);
[ - - ]
1892 [ - + ][ - + ]: 12610524 : Assert(d_match_status_child_num + 1 == (int)d_match_children.size());
[ - - ]
1893 [ - + ][ - + ]: 12610524 : Assert(d_match_children[d_match_status_child_num]
[ - - ]
1894 : : != d_match_children_end[d_match_status_child_num]);
1895 : 12610524 : d_match_status--;
1896 [ + + ]: 12610524 : 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 ) ){
1897 : 7623691 : d_match_status_child_num++;
1898 : 7623691 : return getNextMatch( s, eqc, subs, rev_subs );
1899 : : }else{
1900 : : //iterate
1901 : 4986833 : d_match_children[d_match_status_child_num]++;
1902 : 4986833 : return getNextMatch( s, eqc, subs, rev_subs );
1903 : : }
1904 : : }
1905 : : }
1906 : 0 : DebugUnhandled();
1907 : : return false;
1908 : : }
1909 : :
1910 : 0 : unsigned TermGenerator::getDepth( TermGenEnv * s ) {
1911 [ - - ]: 0 : if( d_status==5 ){
1912 : 0 : unsigned maxd = 0;
1913 [ - - ]: 0 : for( unsigned i=0; i<d_children.size(); i++ ){
1914 : 0 : unsigned d = s->d_tg_alloc[d_children[i]].getDepth( s );
1915 [ - - ]: 0 : if( d>maxd ){
1916 : 0 : maxd = d;
1917 : : }
1918 : : }
1919 : 0 : return 1+maxd;
1920 : : }else{
1921 : 0 : return 0;
1922 : : }
1923 : : }
1924 : :
1925 : 1178594 : unsigned TermGenerator::calculateGeneralizationDepth( TermGenEnv * s, std::map< TypeNode, std::vector< int > >& fvs ) {
1926 [ + + ]: 1178594 : if( d_status==5 ){
1927 : 546268 : unsigned sum = 1;
1928 [ + + ]: 1452249 : for( unsigned i=0; i<d_children.size(); i++ ){
1929 : 905981 : sum += s->d_tg_alloc[d_children[i]].calculateGeneralizationDepth( s, fvs );
1930 : : }
1931 : 546268 : return sum;
1932 : : }else{
1933 [ + + ][ + - ]: 632326 : Assert(d_status == 2 || d_status == 1);
[ - + ][ - + ]
[ - - ]
1934 : 632326 : std::map< TypeNode, std::vector< int > >::iterator it = fvs.find( d_typ );
1935 [ + + ]: 632326 : if( it!=fvs.end() ){
1936 [ + + ]: 351673 : if( std::find( it->second.begin(), it->second.end(), d_status_num )!=it->second.end() ){
1937 : 44500 : return 1;
1938 : : }
1939 : : }
1940 : 587826 : fvs[d_typ].push_back( d_status_num );
1941 : 587826 : return 0;
1942 : : }
1943 : : }
1944 : :
1945 : 272613 : unsigned TermGenerator::getGeneralizationDepth( TermGenEnv * s ) {
1946 : : //if( s->d_gen_relevant_terms ){
1947 : : // return s->d_tg_gdepth;
1948 : : //}else{
1949 : 272613 : std::map< TypeNode, std::vector< int > > fvs;
1950 : 545226 : return calculateGeneralizationDepth( s, fvs );
1951 : : //}
1952 : 272613 : }
1953 : :
1954 : 423860 : Node TermGenerator::getTerm( TermGenEnv * s ) {
1955 [ + + ][ + + ]: 423860 : if( d_status==1 || d_status==2 ){
1956 [ - + ][ - + ]: 250428 : Assert(!d_typ.isNull());
[ - - ]
1957 : 250428 : return s->getFreeVar( d_typ, d_status_num );
1958 [ + - ]: 173432 : }else if( d_status==5 ){
1959 : 346864 : Node f = s->getTgFunc( d_typ, d_status_num );
1960 [ + - ]: 173432 : if( d_children.size()==s->d_func_args[f].size() ){
1961 : 173432 : std::vector< Node > children;
1962 [ + - ]: 173432 : if( s->d_tg_func_param[f] ){
1963 : 173432 : children.push_back( f );
1964 : : }
1965 [ + + ]: 489314 : for( unsigned i=0; i<d_children.size(); i++ ){
1966 : 315882 : Node nc = s->d_tg_alloc[d_children[i]].getTerm( s );
1967 [ - + ]: 315882 : if( nc.isNull() ){
1968 : 0 : return Node::null();
1969 : : }else{
1970 : : //Assert( nc.getType()==s->d_func_args[f][i] );
1971 : 315882 : children.push_back( nc );
1972 : : }
1973 [ + - ]: 315882 : }
1974 : 346864 : return s->d_cg->nodeManager()->mkNode(s->d_func_kind[f], children);
1975 : 173432 : }
1976 [ - + ]: 173432 : }else{
1977 : 0 : DebugUnhandled();
1978 : : }
1979 : 0 : return Node::null();
1980 : : }
1981 : :
1982 : 1957159 : void TermGenerator::debugPrint( TermGenEnv * s, const char * c, const char * cd ) {
1983 [ + - ]: 1957159 : Trace(cd) << "[*" << d_id << "," << d_status << "]:";
1984 [ + + ][ + + ]: 1957159 : if( d_status==1 || d_status==2 ){
1985 : 1013372 : Trace(c) << s->getFreeVar( d_typ, d_status_num );
1986 [ + - ]: 943787 : }else if( d_status==5 ){
1987 : 943787 : TNode f = s->getTgFunc( d_typ, d_status_num );
1988 [ + - ]: 943787 : Trace(c) << "(" << f;
1989 [ + + ]: 2459783 : for( unsigned i=0; i<d_children.size(); i++ ){
1990 [ + - ]: 1515996 : Trace(c) << " ";
1991 : 1515996 : s->d_tg_alloc[d_children[i]].debugPrint( s, c, cd );
1992 : : }
1993 [ + + ]: 943787 : if( d_children.size()<s->d_func_args[f].size() ){
1994 [ + - ]: 224201 : Trace(c) << " ...";
1995 : : }
1996 [ + - ]: 943787 : Trace(c) << ")";
1997 : 943787 : }else{
1998 [ - - ]: 0 : Trace(c) << "???";
1999 : : }
2000 : 1957159 : }
2001 : :
2002 : 320 : void TermGenEnv::collectSignatureInformation() {
2003 : 320 : d_typ_tg_funcs.clear();
2004 : 320 : d_funcs.clear();
2005 : 320 : d_func_kind.clear();
2006 : 320 : d_func_args.clear();
2007 : 320 : TypeNode tnull;
2008 : 320 : TermDb* tdb = getTermDatabase();
2009 [ + + ]: 5436 : for (size_t i = 0, nops = tdb->getNumOperators(); i < nops; i++)
2010 : : {
2011 : 5116 : Node op = tdb->getOperator(i);
2012 : 5116 : DbList* dbl = tdb->getOrMkDbListForOp(op);
2013 [ + + ]: 5116 : if (!dbl->d_list.empty())
2014 : : {
2015 : 5060 : Node nn = dbl->d_list[0];
2016 [ + - ]: 5060 : Trace("sg-rel-sig-debug") << "Check in signature : " << nn << std::endl;
2017 [ + + ][ + + ]: 10116 : if (d_cg->isHandledTerm(nn) && nn.getKind() != Kind::APPLY_SELECTOR
[ - - ]
2018 [ + + ][ + + ]: 10116 : && !nn.getType().isBoolean())
[ + + ][ + - ]
[ - - ]
2019 : : {
2020 : 2400 : bool do_enum = true;
2021 : : //check if we have enumerated ground terms
2022 [ + + ]: 2400 : if (nn.getKind() == Kind::APPLY_UF)
2023 : : {
2024 [ + - ]: 1205 : Trace("sg-rel-sig-debug") << "Check enumeration..." << std::endl;
2025 [ + + ]: 1205 : if( !d_cg->hasEnumeratedUf( nn ) ){
2026 : 252 : do_enum = false;
2027 : : }
2028 : : }
2029 [ + + ]: 2400 : if( do_enum ){
2030 [ + - ]: 2148 : Trace("sg-rel-sig-debug") << "Set enumeration..." << std::endl;
2031 : 2148 : d_funcs.push_back(op);
2032 [ + + ]: 4748 : for (const Node& nnc : nn)
2033 : : {
2034 : 2600 : d_func_args[op].push_back(nnc.getType());
2035 : 2600 : }
2036 : 2148 : d_func_kind[op] = nn.getKind();
2037 : 2148 : d_typ_tg_funcs[tnull].push_back(op);
2038 : 2148 : d_typ_tg_funcs[nn.getType()].push_back(op);
2039 : 2148 : d_tg_func_param[op] =
2040 : 2148 : (nn.getMetaKind() == kind::metakind::PARAMETERIZED);
2041 [ + - ]: 4296 : Trace("sg-rel-sig")
2042 : 0 : << "Will enumerate function applications of : " << op
2043 [ - - ]: 2148 : << ", #args = " << d_func_args[op].size()
2044 [ - + ]: 2148 : << ", kind = " << nn.getKind() << std::endl;
2045 : : }
2046 : : }
2047 [ + - ]: 5060 : Trace("sg-rel-sig-debug") << "Done check in signature : " << nn << std::endl;
2048 : 5060 : }
2049 : 5116 : }
2050 : : //shuffle functions
2051 : 320 : for (std::map<TypeNode, std::vector<TNode> >::iterator it =
2052 : 320 : d_typ_tg_funcs.begin();
2053 [ + + ]: 1363 : it != d_typ_tg_funcs.end();
2054 : 1043 : ++it)
2055 : : {
2056 : 1043 : std::shuffle(it->second.begin(), it->second.end(), Random::getRandom());
2057 [ + + ]: 1043 : if (it->first.isNull())
2058 : : {
2059 [ + - ]: 304 : Trace("sg-gen-tg-debug") << "In this order : ";
2060 [ + + ]: 2452 : for (unsigned i = 0; i < it->second.size(); i++)
2061 : : {
2062 [ + - ]: 2148 : Trace("sg-gen-tg-debug") << it->second[i] << " ";
2063 : : }
2064 [ + - ]: 304 : Trace("sg-gen-tg-debug") << std::endl;
2065 : : }
2066 : : }
2067 : 320 : }
2068 : :
2069 : 2676 : void TermGenEnv::reset( unsigned depth, bool genRelevant, TypeNode tn ) {
2070 [ - + ][ - + ]: 2676 : Assert(d_tg_alloc.empty());
[ - - ]
2071 : 2676 : d_tg_alloc.clear();
2072 : :
2073 [ + + ]: 2676 : if( genRelevant ){
2074 [ + + ]: 2349 : for( unsigned i=0; i<2; i++ ){
2075 : 1566 : d_ccand_eqc[i].clear();
2076 : 1566 : d_ccand_eqc[i].push_back( d_relevant_eqc[i] );
2077 : : }
2078 : : }
2079 : :
2080 : 2676 : d_tg_id = 0;
2081 : 2676 : d_tg_gdepth = 0;
2082 : 2676 : d_tg_gdepth_limit = depth;
2083 : 2676 : d_gen_relevant_terms = genRelevant;
2084 : 2676 : d_tg_alloc[0].reset( this, tn );
2085 : 2676 : }
2086 : :
2087 : 47564 : bool TermGenEnv::getNextTerm() {
2088 [ + + ]: 47564 : if( d_tg_alloc[0].getNextTerm( this, d_tg_gdepth_limit ) ){
2089 [ - + ][ - + ]: 44888 : Assert((int)d_tg_alloc[0].getGeneralizationDepth(this)
[ - - ]
2090 : : <= d_tg_gdepth_limit);
2091 [ + + ]: 44888 : if( (int)d_tg_alloc[0].getGeneralizationDepth( this )!=d_tg_gdepth_limit ){
2092 : 6460 : return getNextTerm();
2093 : : }else{
2094 : 38428 : return true;
2095 : : }
2096 : : }
2097 [ + - ]: 2676 : Trace("sg-gen-tg-debug2") << "...remove from context " << std::endl;
2098 : 2676 : changeContext(false);
2099 : 2676 : return false;
2100 : : }
2101 : :
2102 : : //reset matching
2103 : 175658 : void TermGenEnv::resetMatching(unsigned mode)
2104 : : {
2105 : 175658 : d_tg_alloc[0].resetMatching(mode);
2106 : 175658 : }
2107 : :
2108 : : //get next match
2109 : 1329470 : bool TermGenEnv::getNextMatch( TNode eqc, std::map< TypeNode, std::map< unsigned, TNode > >& subs, std::map< TNode, bool >& rev_subs ) {
2110 : 1329470 : return d_tg_alloc[0].getNextMatch( this, eqc, subs, rev_subs );
2111 : : }
2112 : :
2113 : : //get term
2114 : 38428 : Node TermGenEnv::getTerm() {
2115 : 76856 : return d_tg_alloc[0].getTerm( this );
2116 : : }
2117 : :
2118 : 5939 : void TermGenEnv::debugPrint( const char * c, const char * cd ) {
2119 : 5939 : d_tg_alloc[0].debugPrint( this, c, cd );
2120 : 5939 : }
2121 : :
2122 : 324982 : unsigned TermGenEnv::getNumTgVars( TypeNode tn ) {
2123 : 324982 : return d_var_id[tn];
2124 : : }
2125 : :
2126 : 41783 : bool TermGenEnv::allowVar( TypeNode tn ) {
2127 : 41783 : std::map< TypeNode, unsigned >::iterator it = d_var_limit.find( tn );
2128 [ + + ]: 41783 : if( it==d_var_limit.end() ){
2129 : 14216 : return true;
2130 : : }else{
2131 : 27567 : return d_var_id[tn]<it->second;
2132 : : }
2133 : : }
2134 : :
2135 : 14216 : void TermGenEnv::addVar( TypeNode tn ) {
2136 : 14216 : d_var_id[tn]++;
2137 : 14216 : }
2138 : :
2139 : 14216 : void TermGenEnv::removeVar( TypeNode tn ) {
2140 : 14216 : d_var_id[tn]--;
2141 : : //d_var_eq_tg.pop_back();
2142 : : //d_var_tg.pop_back();
2143 : 14216 : }
2144 : :
2145 : 91288 : unsigned TermGenEnv::getNumTgFuncs( TypeNode tn ) {
2146 : 91288 : return d_typ_tg_funcs[tn].size();
2147 : : }
2148 : :
2149 : 7101708 : TNode TermGenEnv::getTgFunc( TypeNode tn, unsigned i ) {
2150 : 7101708 : return d_typ_tg_funcs[tn][i];
2151 : : }
2152 : :
2153 : 250428 : Node TermGenEnv::getFreeVar( TypeNode tn, unsigned i ) {
2154 : 250428 : return d_cg->getFreeVar( tn, i );
2155 : : }
2156 : :
2157 : 182837 : bool TermGenEnv::considerCurrentTerm() {
2158 [ - + ][ - + ]: 182837 : Assert(!d_tg_alloc.empty());
[ - - ]
2159 : :
2160 : : //if generalization depth is too large, don't consider it
2161 : 182837 : unsigned i = d_tg_alloc.size();
2162 [ + - ]: 182837 : Trace("sg-gen-tg-debug") << "Consider term ";
2163 : 182837 : d_tg_alloc[0].debugPrint( this, "sg-gen-tg-debug", "sg-gen-tg-debug" );
2164 [ + - ]: 182837 : Trace("sg-gen-tg-debug") << "? curr term size = " << d_tg_alloc.size() << ", last status = " << d_tg_alloc[i-1].d_status;
2165 [ + - ]: 182837 : Trace("sg-gen-tg-debug") << std::endl;
2166 : :
2167 [ + - ][ + + ]: 182837 : if( d_tg_gdepth_limit>=0 && d_tg_alloc[0].getGeneralizationDepth( this )>(unsigned)d_tg_gdepth_limit ){
[ + + ]
2168 [ + - ]: 88739 : Trace("sg-gen-consider-term") << "-> generalization depth of ";
2169 : 88739 : d_tg_alloc[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-tg-debug" );
2170 [ + - ]: 88739 : Trace("sg-gen-consider-term") << " is too high " << d_tg_gdepth << " " << d_tg_alloc[0].getGeneralizationDepth( this ) << ", do not consider." << std::endl;
2171 : 88739 : return false;
2172 : : }
2173 : :
2174 : : //----optimizations
2175 : : /*
2176 : : if( d_tg_alloc[i-1].d_status==1 ){
2177 : : }else if( d_tg_alloc[i-1].d_status==2 ){
2178 : : }else if( d_tg_alloc[i-1].d_status==5 ){
2179 : : }else{
2180 : : Trace("sg-gen-tg-debug") << "Bad tg: " << &d_tg_alloc[i-1] << std::endl;
2181 : : Assert( false );
2182 : : }
2183 : : */
2184 : : //if equated two variables, first check if context-independent TODO
2185 : : //----end optimizations
2186 : :
2187 : :
2188 : : //check based on which candidate equivalence classes match
2189 [ + + ]: 94098 : if( d_gen_relevant_terms ){
2190 [ + - ]: 30040 : Trace("sg-gen-tg-debug") << "Filter based on relevant ground EQC";
2191 [ + - ]: 30040 : Trace("sg-gen-tg-debug") << ", #eqc to try = " << d_ccand_eqc[0][i-1].size() << "/" << d_ccand_eqc[1][i-1].size() << std::endl;
2192 : :
2193 [ - + ][ - + ]: 30040 : Assert(d_ccand_eqc[0].size() >= 2);
[ - - ]
2194 [ - + ][ - + ]: 30040 : Assert(d_ccand_eqc[0].size() == d_ccand_eqc[1].size());
[ - - ]
2195 [ - + ][ - + ]: 30040 : Assert(d_ccand_eqc[0].size() == d_tg_id + 1);
[ - - ]
2196 [ - + ][ - + ]: 30040 : Assert(d_tg_id == d_tg_alloc.size());
[ - - ]
2197 [ + + ]: 90120 : for( unsigned r=0; r<2; r++ ){
2198 : 60080 : d_ccand_eqc[r][i].clear();
2199 : : }
2200 : :
2201 : : //re-check feasibility of EQC
2202 [ + + ]: 90120 : for( unsigned r=0; r<2; r++ ){
2203 [ + + ]: 3304613 : for( unsigned j=0; j<d_ccand_eqc[r][i-1].size(); j++ ){
2204 : 3244533 : std::map< TypeNode, std::map< unsigned, TNode > > subs;
2205 : 3244533 : std::map< TNode, bool > rev_subs;
2206 : : unsigned mode;
2207 [ + + ]: 3244533 : if( r==0 ){
2208 [ - + ]: 486310 : mode = d_cg->optReqDistinctVarPatterns() ? ( 1 << 0 ) : 0;
2209 : 486310 : mode = mode | (1 << 2 );
2210 : : }else{
2211 : 2758223 : mode = 1 << 1;
2212 : : }
2213 : 3244533 : d_tg_alloc[0].resetMatching(mode);
2214 [ + + ]: 3244533 : if( d_tg_alloc[0].getNextMatch( this, d_ccand_eqc[r][i-1][j], subs, rev_subs ) ){
2215 : 1084765 : d_ccand_eqc[r][i].push_back( d_ccand_eqc[r][i-1][j] );
2216 : : }
2217 : 3244533 : }
2218 : : }
2219 [ + + ]: 90120 : for( unsigned r=0; r<2; r++ ){
2220 [ + - ]: 60080 : Trace("sg-gen-tg-debug") << "Current eqc of type " << r << " : ";
2221 [ + + ]: 1144845 : for( unsigned j=0; j<d_ccand_eqc[r][i].size(); j++ ){
2222 [ + - ]: 1084765 : Trace("sg-gen-tg-debug") << "e" << d_cg->d_em[d_ccand_eqc[r][i][j]] << " ";
2223 : : }
2224 [ + - ]: 60080 : Trace("sg-gen-tg-debug") << std::endl;
2225 : : }
2226 : : // filter based active terms
2227 [ + + ]: 30040 : if (d_ccand_eqc[0][i].empty())
2228 : : {
2229 [ + - ]: 8179 : Trace("sg-gen-consider-term") << "Do not consider term of form ";
2230 : 8179 : d_tg_alloc[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-consider-term-debug" );
2231 [ + - ]: 8179 : Trace("sg-gen-consider-term") << " since no relevant EQC matches it." << std::endl;
2232 : 8179 : return false;
2233 : : }
2234 : : // filter based on model
2235 [ + + ]: 21861 : if (d_ccand_eqc[1][i].empty())
2236 : : {
2237 [ + - ]: 518 : Trace("sg-gen-consider-term") << "Do not consider term of form ";
2238 : 518 : d_tg_alloc[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-consider-term-debug" );
2239 [ + - ]: 518 : Trace("sg-gen-consider-term") << " since no ground EQC matches it." << std::endl;
2240 : 518 : return false;
2241 : : }
2242 : : }
2243 [ + - ]: 85401 : Trace("sg-gen-tg-debug") << "Will consider term ";
2244 : 85401 : d_tg_alloc[0].debugPrint( this, "sg-gen-tg-debug", "sg-gen-tg-debug" );
2245 [ + - ]: 85401 : Trace("sg-gen-tg-debug") << std::endl;
2246 [ + - ]: 85401 : Trace("sg-gen-consider-term-debug") << std::endl;
2247 : 85401 : return true;
2248 : : }
2249 : :
2250 : 85132 : void TermGenEnv::changeContext( bool add ) {
2251 [ + + ]: 85132 : if( add ){
2252 [ + + ]: 127698 : for( unsigned r=0; r<2; r++ ){
2253 : 85132 : d_ccand_eqc[r].push_back( std::vector< TNode >() );
2254 : : }
2255 : 42566 : d_tg_id++;
2256 : : }else{
2257 [ + + ]: 127698 : for( unsigned r=0; r<2; r++ ){
2258 : 85132 : d_ccand_eqc[r].pop_back();
2259 : : }
2260 : 42566 : d_tg_id--;
2261 [ - + ][ - + ]: 42566 : Assert(d_tg_alloc.find(d_tg_id) != d_tg_alloc.end());
[ - - ]
2262 : 42566 : d_tg_alloc.erase( d_tg_id );
2263 : : }
2264 : 85132 : }
2265 : :
2266 : 69550 : bool TermGenEnv::considerCurrentTermCanon( unsigned tg_id ){
2267 [ - + ][ - + ]: 69550 : Assert(tg_id < d_tg_alloc.size());
[ - - ]
2268 : : // filter based on canonical
2269 : : // check based on a canonicity of the term (if there is one)
2270 [ + - ]: 69550 : Trace("sg-gen-tg-debug") << "Consider term canon ";
2271 : 69550 : d_tg_alloc[0].debugPrint(this, "sg-gen-tg-debug", "sg-gen-tg-debug");
2272 [ + - ]: 69550 : Trace("sg-gen-tg-debug") << ", tg is [" << tg_id << "]..." << std::endl;
2273 : :
2274 : 69550 : Node ln = d_tg_alloc[tg_id].getTerm(this);
2275 [ + - ]: 69550 : Trace("sg-gen-tg-debug") << "Term is " << ln << std::endl;
2276 : 139100 : return d_cg->considerTermCanon(ln, d_gen_relevant_terms);
2277 : 69550 : }
2278 : :
2279 : 89410 : bool TermGenEnv::isRelevantFunc( Node f ) {
2280 : 89410 : return std::find( d_funcs.begin(), d_funcs.end(), f )!=d_funcs.end();
2281 : : }
2282 : :
2283 : 14989 : bool TermGenEnv::isRelevantTerm( Node t ) {
2284 [ + + ]: 14989 : if (t.getKind() != Kind::BOUND_VARIABLE)
2285 : : {
2286 [ + + ]: 10889 : if (t.getKind() != Kind::EQUAL)
2287 : : {
2288 [ + + ]: 8003 : if( t.hasOperator() ){
2289 : 7480 : TNode op = t.getOperator();
2290 [ + + ]: 7480 : if( !isRelevantFunc( op ) ){
2291 : 1069 : return false;
2292 : : }
2293 [ + + ]: 7480 : }else{
2294 : 523 : return false;
2295 : : }
2296 : : }
2297 [ + + ]: 18944 : for( unsigned i=0; i<t.getNumChildren(); i++ ){
2298 [ + + ]: 12107 : if( !isRelevantTerm( t[i] ) ){
2299 : 2460 : return false;
2300 : : }
2301 : : }
2302 : : }
2303 : 10937 : return true;
2304 : : }
2305 : :
2306 : 5726039 : TermDb * TermGenEnv::getTermDatabase() {
2307 : 5726039 : return d_cg->getTermDatabase();
2308 : : }
2309 : 0 : Node TermGenEnv::getGroundEqc( TNode r ) {
2310 : 0 : return d_cg->getGroundEqc( r );
2311 : : }
2312 : 4394802 : bool TermGenEnv::isGroundEqc( TNode r ){
2313 : 4394802 : return d_cg->isGroundEqc( r );
2314 : : }
2315 : 0 : bool TermGenEnv::isGroundTerm( TNode n ){
2316 : 0 : return d_cg->isGroundTerm( n );
2317 : : }
2318 : :
2319 : :
2320 : 4483622 : void SubstitutionIndex::addSubstitution( TNode eqc, std::vector< TNode >& vars, std::vector< TNode >& terms, unsigned i ) {
2321 [ + + ]: 4483622 : if( i==vars.size() ){
2322 : 1153812 : d_var = eqc;
2323 : : }else{
2324 [ + + ][ + - ]: 3329810 : Assert(d_var.isNull() || d_var == vars[i]);
[ - + ][ - + ]
[ - - ]
2325 : 3329810 : d_var = vars[i];
2326 : 3329810 : d_children[terms[i]].addSubstitution( eqc, vars, terms, i+1 );
2327 : : }
2328 : 4483622 : }
2329 : :
2330 : 132245726 : bool SubstitutionIndex::notifySubstitutions( ConjectureGenerator * s, std::map< TNode, TNode >& subs, TNode rhs, unsigned numVars, unsigned i ) {
2331 [ + + ]: 132245726 : if( i==numVars ){
2332 [ - + ][ - + ]: 101627113 : Assert(d_children.empty());
[ - - ]
2333 : 101627113 : return s->notifySubstitution( d_var, subs, rhs );
2334 : : }else{
2335 [ + + ][ + - ]: 30618613 : Assert(i == 0 || !d_children.empty());
[ - + ][ - + ]
[ - - ]
2336 [ + + ]: 161640011 : for( std::map< TNode, SubstitutionIndex >::iterator it = d_children.begin(); it != d_children.end(); ++it ){
2337 [ + - ]: 131467261 : Trace("sg-cconj-debug2") << "Try " << d_var << " -> " << it->first << " (" << i << "/" << numVars << ")" << std::endl;
2338 : 131467261 : subs[d_var] = it->first;
2339 [ + + ]: 131467261 : if( !it->second.notifySubstitutions( s, subs, rhs, numVars, i+1 ) ){
2340 : 445863 : return false;
2341 : : }
2342 : : }
2343 : 30172750 : return true;
2344 : : }
2345 : : }
2346 : :
2347 : :
2348 : 6650 : void TheoremIndex::addTheorem( std::vector< TNode >& lhs_v, std::vector< unsigned >& lhs_arg, TNode rhs ){
2349 [ + + ]: 6650 : if( lhs_v.empty() ){
2350 [ + - ]: 1290 : if( std::find( d_terms.begin(), d_terms.end(), rhs )==d_terms.end() ){
2351 : 1290 : d_terms.push_back( rhs );
2352 : : }
2353 : : }else{
2354 : 5360 : unsigned index = lhs_v.size()-1;
2355 [ + + ]: 5360 : if( lhs_arg[index]==lhs_v[index].getNumChildren() ){
2356 : 2565 : lhs_v.pop_back();
2357 : 2565 : lhs_arg.pop_back();
2358 : 2565 : addTheorem( lhs_v, lhs_arg, rhs );
2359 : : }else{
2360 : 2795 : lhs_arg[index]++;
2361 : 2795 : addTheoremNode( lhs_v[index][lhs_arg[index]-1], lhs_v, lhs_arg, rhs );
2362 : : }
2363 : : }
2364 : 6650 : }
2365 : :
2366 : 4085 : void TheoremIndex::addTheoremNode( TNode curr, std::vector< TNode >& lhs_v, std::vector< unsigned >& lhs_arg, TNode rhs ){
2367 [ + - ]: 4085 : Trace("thm-db-debug") << "Adding conjecture for subterm " << curr << "..." << std::endl;
2368 [ + + ]: 4085 : if( curr.hasOperator() ){
2369 : 2565 : lhs_v.push_back( curr );
2370 : 2565 : lhs_arg.push_back( 0 );
2371 : 2565 : d_children[curr.getOperator()].addTheorem( lhs_v, lhs_arg, rhs );
2372 : : }else{
2373 [ - + ][ - + ]: 1520 : Assert(curr.getKind() == Kind::BOUND_VARIABLE);
[ - - ]
2374 : 1520 : TypeNode tn = curr.getType();
2375 [ + + ][ + - ]: 1520 : Assert(d_var[tn].isNull() || d_var[tn] == curr);
[ - + ][ - + ]
[ - - ]
2376 : 1520 : d_var[tn] = curr;
2377 : 1520 : d_children[curr].addTheorem( lhs_v, lhs_arg, rhs );
2378 : 1520 : }
2379 : 4085 : }
2380 : :
2381 : 44963 : void TheoremIndex::getEquivalentTerms( std::vector< TNode >& n_v, std::vector< unsigned >& n_arg,
2382 : : std::map< TNode, TNode >& smap, std::vector< TNode >& vars, std::vector< TNode >& subs,
2383 : : std::vector< Node >& terms ) {
2384 [ + - ]: 44963 : Trace("thm-db-debug") << "Get equivalent terms " << n_v.size() << " " << n_arg.size() << std::endl;
2385 [ + + ]: 44963 : if( n_v.empty() ){
2386 [ + - ]: 4834 : Trace("thm-db-debug") << "Number of terms : " << d_terms.size() << std::endl;
2387 : : //apply substutitions to RHS's
2388 [ + + ]: 9668 : for( unsigned i=0; i<d_terms.size(); i++ ){
2389 : 4834 : Node n = d_terms[i].substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
2390 : 4834 : terms.push_back( n );
2391 : 4834 : }
2392 : : }else{
2393 : 40129 : unsigned index = n_v.size()-1;
2394 [ + + ]: 40129 : if( n_arg[index]==n_v[index].getNumChildren() ){
2395 : 2066 : n_v.pop_back();
2396 : 2066 : n_arg.pop_back();
2397 : 2066 : getEquivalentTerms( n_v, n_arg, smap, vars, subs, terms );
2398 : : }else{
2399 : 38063 : n_arg[index]++;
2400 : 38063 : getEquivalentTermsNode( n_v[index][n_arg[index]-1], n_v, n_arg, smap, vars, subs, terms );
2401 : : }
2402 : : }
2403 : 44963 : }
2404 : :
2405 : 71378 : void TheoremIndex::getEquivalentTermsNode( Node curr, std::vector< TNode >& n_v, std::vector< unsigned >& n_arg,
2406 : : std::map< TNode, TNode >& smap, std::vector< TNode >& vars, std::vector< TNode >& subs,
2407 : : std::vector< Node >& terms ) {
2408 [ + - ]: 71378 : Trace("thm-db-debug") << "Get equivalent based on subterm " << curr << "..." << std::endl;
2409 [ + + ]: 71378 : if( curr.hasOperator() ){
2410 [ + - ]: 46191 : Trace("thm-db-debug") << "Check based on operator..." << std::endl;
2411 : 46191 : std::map< TNode, TheoremIndex >::iterator it = d_children.find( curr.getOperator() );
2412 [ + + ]: 46191 : if( it!=d_children.end() ){
2413 : 20531 : n_v.push_back( curr );
2414 : 20531 : n_arg.push_back( 0 );
2415 : 20531 : it->second.getEquivalentTerms( n_v, n_arg, smap, vars, subs, terms );
2416 : : }
2417 [ + - ]: 46191 : Trace("thm-db-debug") << "...done check based on operator" << std::endl;
2418 : : }
2419 : 71378 : TypeNode tn = curr.getType();
2420 : 71378 : std::map< TypeNode, TNode >::iterator itt = d_var.find( tn );
2421 [ + + ]: 71378 : if( itt!=d_var.end() ){
2422 [ + - ]: 29411 : Trace("thm-db-debug") << "Check for substitution with " << itt->second << "..." << std::endl;
2423 [ - + ][ - + ]: 29411 : Assert(curr.getType() == itt->second.getType());
[ - - ]
2424 : : //add to substitution if possible
2425 : 29411 : bool success = false;
2426 : 29411 : std::map< TNode, TNode >::iterator it = smap.find( itt->second );
2427 [ + + ]: 29411 : if( it==smap.end() ){
2428 : 22366 : smap[itt->second] = curr;
2429 : 22366 : vars.push_back( itt->second );
2430 : 22366 : subs.push_back( curr );
2431 : 22366 : success = true;
2432 [ - + ]: 7045 : }else if( it->second==curr ){
2433 : 0 : success = true;
2434 : : }else{
2435 : : //also check modulo equality (in universal equality engine)
2436 : : }
2437 [ + - ]: 29411 : Trace("thm-db-debug") << "...check for substitution with " << itt->second << ", success = " << success << "." << std::endl;
2438 [ + + ]: 29411 : if( success ){
2439 : 22366 : d_children[itt->second].getEquivalentTerms( n_v, n_arg, smap, vars, subs, terms );
2440 : : }
2441 : : }
2442 : 71378 : }
2443 : :
2444 : 0 : void TheoremIndex::debugPrint( const char * c, unsigned ind ) {
2445 [ - - ]: 0 : for( std::map< TNode, TheoremIndex >::iterator it = d_children.begin(); it != d_children.end(); ++it ){
2446 : 0 : for( unsigned i=0; i<ind; i++ ){ Trace(c) << " "; }
2447 [ - - ]: 0 : Trace(c) << it->first << std::endl;
2448 : 0 : it->second.debugPrint( c, ind+1 );
2449 : : }
2450 [ - - ]: 0 : if( !d_terms.empty() ){
2451 : 0 : for( unsigned i=0; i<ind; i++ ){ Trace(c) << " "; }
2452 [ - - ]: 0 : Trace(c) << "{";
2453 [ - - ]: 0 : for( unsigned i=0; i<d_terms.size(); i++ ){
2454 [ - - ]: 0 : Trace(c) << " " << d_terms[i];
2455 : : }
2456 [ - - ]: 0 : Trace(c) << " }" << std::endl;
2457 : : }
2458 : : //if( !d_var.isNull() ){
2459 : : // for( unsigned i=0; i<ind; i++ ){ Trace(c) << " "; }
2460 : : // Trace(c) << "var:" << d_var << std::endl;
2461 : : //}
2462 : 0 : }
2463 : :
2464 : 486310 : bool ConjectureGenerator::optReqDistinctVarPatterns() { return false; }
2465 : 107540 : bool ConjectureGenerator::optFilterUnknown() { return true; } //may change
2466 : 247 : int ConjectureGenerator::optFilterScoreThreshold() { return 1; }
2467 : 320 : unsigned ConjectureGenerator::optFullCheckFrequency() { return 1; }
2468 : :
2469 : 416 : bool ConjectureGenerator::optStatsOnly() { return false; }
2470 : :
2471 : : } // namespace cvc5::internal
|
