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