1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Morgan Deters, Mathias Preiner |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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 |
|
* Implementation of the theory of datatypes. |
14 |
|
*/ |
15 |
|
#include "theory/datatypes/theory_datatypes.h" |
16 |
|
|
17 |
|
#include <map> |
18 |
|
#include <sstream> |
19 |
|
|
20 |
|
#include "base/check.h" |
21 |
|
#include "expr/dtype.h" |
22 |
|
#include "expr/dtype_cons.h" |
23 |
|
#include "expr/kind.h" |
24 |
|
#include "expr/skolem_manager.h" |
25 |
|
#include "options/datatypes_options.h" |
26 |
|
#include "options/quantifiers_options.h" |
27 |
|
#include "options/smt_options.h" |
28 |
|
#include "options/theory_options.h" |
29 |
|
#include "proof/proof_node_manager.h" |
30 |
|
#include "smt/logic_exception.h" |
31 |
|
#include "theory/datatypes/datatypes_rewriter.h" |
32 |
|
#include "theory/datatypes/theory_datatypes_type_rules.h" |
33 |
|
#include "theory/datatypes/theory_datatypes_utils.h" |
34 |
|
#include "theory/logic_info.h" |
35 |
|
#include "theory/quantifiers_engine.h" |
36 |
|
#include "theory/rewriter.h" |
37 |
|
#include "theory/theory_model.h" |
38 |
|
#include "theory/theory_state.h" |
39 |
|
#include "theory/type_enumerator.h" |
40 |
|
#include "theory/valuation.h" |
41 |
|
|
42 |
|
using namespace std; |
43 |
|
using namespace cvc5::kind; |
44 |
|
using namespace cvc5::context; |
45 |
|
|
46 |
|
namespace cvc5 { |
47 |
|
namespace theory { |
48 |
|
namespace datatypes { |
49 |
|
|
50 |
9940 |
TheoryDatatypes::TheoryDatatypes(Env& env, |
51 |
|
OutputChannel& out, |
52 |
9940 |
Valuation valuation) |
53 |
|
: Theory(THEORY_DATATYPES, env, out, valuation), |
54 |
9940 |
d_term_sk(userContext()), |
55 |
|
d_labels(context()), |
56 |
|
d_selector_apps(context()), |
57 |
|
d_collectTermsCache(context()), |
58 |
9940 |
d_collectTermsCacheU(userContext()), |
59 |
|
d_functionTerms(context()), |
60 |
9940 |
d_singleton_eq(userContext()), |
61 |
|
d_sygusExtension(nullptr), |
62 |
|
d_state(env, valuation), |
63 |
|
d_im(env, *this, d_state, d_pnm), |
64 |
39760 |
d_notify(d_im, *this) |
65 |
|
{ |
66 |
|
|
67 |
9940 |
d_true = NodeManager::currentNM()->mkConst( true ); |
68 |
9940 |
d_zero = NodeManager::currentNM()->mkConst( Rational(0) ); |
69 |
9940 |
d_dtfCounter = 0; |
70 |
|
|
71 |
|
// indicate we are using the default theory state object |
72 |
9940 |
d_theoryState = &d_state; |
73 |
9940 |
d_inferManager = &d_im; |
74 |
9940 |
} |
75 |
|
|
76 |
29811 |
TheoryDatatypes::~TheoryDatatypes() { |
77 |
35661 |
for(std::map< Node, EqcInfo* >::iterator i = d_eqc_info.begin(), iend = d_eqc_info.end(); |
78 |
35661 |
i != iend; ++i){ |
79 |
25724 |
EqcInfo* current = (*i).second; |
80 |
25724 |
Assert(current != NULL); |
81 |
25724 |
delete current; |
82 |
|
} |
83 |
19874 |
} |
84 |
|
|
85 |
9940 |
TheoryRewriter* TheoryDatatypes::getTheoryRewriter() { return &d_rewriter; } |
86 |
|
|
87 |
3794 |
ProofRuleChecker* TheoryDatatypes::getProofChecker() { return &d_checker; } |
88 |
|
|
89 |
9940 |
bool TheoryDatatypes::needsEqualityEngine(EeSetupInfo& esi) |
90 |
|
{ |
91 |
9940 |
esi.d_notify = &d_notify; |
92 |
9940 |
esi.d_name = "theory::datatypes::ee"; |
93 |
|
// need notifications on new constructors, merging datatype eqcs |
94 |
9940 |
esi.d_notifyNewClass = true; |
95 |
9940 |
esi.d_notifyMerge = true; |
96 |
9940 |
return true; |
97 |
|
} |
98 |
|
|
99 |
9940 |
void TheoryDatatypes::finishInit() |
100 |
|
{ |
101 |
9940 |
Assert(d_equalityEngine != nullptr); |
102 |
|
// The kinds we are treating as function application in congruence |
103 |
9940 |
d_equalityEngine->addFunctionKind(kind::APPLY_CONSTRUCTOR); |
104 |
9940 |
d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR_TOTAL); |
105 |
9940 |
d_equalityEngine->addFunctionKind(kind::APPLY_TESTER); |
106 |
|
// We could but don't do congruence for DT_SIZE and DT_HEIGHT_BOUND here. |
107 |
|
// It also could make sense in practice to do congruence for APPLY_UF, but |
108 |
|
// this is not done. |
109 |
9940 |
if (getQuantifiersEngine() && options::sygus()) |
110 |
|
{ |
111 |
|
quantifiers::TermDbSygus* tds = |
112 |
1233 |
getQuantifiersEngine()->getTermDatabaseSygus(); |
113 |
1233 |
d_sygusExtension.reset(new SygusExtension(d_env, d_state, d_im, tds)); |
114 |
|
// do congruence on evaluation functions |
115 |
1233 |
d_equalityEngine->addFunctionKind(kind::DT_SYGUS_EVAL); |
116 |
|
} |
117 |
|
// testers are not relevant for model building |
118 |
9940 |
d_valuation.setIrrelevantKind(APPLY_TESTER); |
119 |
9940 |
} |
120 |
|
|
121 |
2711361 |
TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( TNode n, bool doMake ){ |
122 |
2711361 |
if( !hasEqcInfo( n ) ){ |
123 |
493836 |
if( doMake ){ |
124 |
|
//add to labels |
125 |
149892 |
d_labels[ n ] = 0; |
126 |
|
|
127 |
149892 |
std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n ); |
128 |
|
EqcInfo* ei; |
129 |
149892 |
if( eqc_i != d_eqc_info.end() ){ |
130 |
124168 |
ei = eqc_i->second; |
131 |
|
}else{ |
132 |
25724 |
ei = new EqcInfo(context()); |
133 |
25724 |
d_eqc_info[n] = ei; |
134 |
|
} |
135 |
149892 |
if( n.getKind()==APPLY_CONSTRUCTOR ){ |
136 |
100154 |
ei->d_constructor = n; |
137 |
|
} |
138 |
|
|
139 |
|
//add to selectors |
140 |
149892 |
d_selector_apps[n] = 0; |
141 |
|
|
142 |
149892 |
return ei; |
143 |
|
}else{ |
144 |
343944 |
return NULL; |
145 |
|
} |
146 |
|
}else{ |
147 |
2217525 |
std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n ); |
148 |
2217525 |
return (*eqc_i).second; |
149 |
|
} |
150 |
|
} |
151 |
|
|
152 |
510936 |
TNode TheoryDatatypes::getEqcConstructor( TNode r ) { |
153 |
510936 |
if( r.getKind()==APPLY_CONSTRUCTOR ){ |
154 |
336209 |
return r; |
155 |
|
}else{ |
156 |
174727 |
EqcInfo * ei = getOrMakeEqcInfo( r, false ); |
157 |
174727 |
if( ei && !ei->d_constructor.get().isNull() ){ |
158 |
56147 |
return ei->d_constructor.get(); |
159 |
|
}else{ |
160 |
118580 |
return r; |
161 |
|
} |
162 |
|
} |
163 |
|
} |
164 |
|
|
165 |
541030 |
bool TheoryDatatypes::preCheck(Effort level) |
166 |
|
{ |
167 |
1082060 |
Trace("datatypes-check") << "TheoryDatatypes::preCheck: " << level |
168 |
541030 |
<< std::endl; |
169 |
541030 |
d_im.process(); |
170 |
541030 |
d_im.reset(); |
171 |
541030 |
return false; |
172 |
|
} |
173 |
|
|
174 |
541030 |
void TheoryDatatypes::postCheck(Effort level) |
175 |
|
{ |
176 |
1082060 |
Trace("datatypes-check") << "TheoryDatatypes::postCheck: " << level |
177 |
541030 |
<< std::endl; |
178 |
|
// Apply any last pending inferences, which may occur if the last processed |
179 |
|
// fact was an internal one and triggered further internal inferences. |
180 |
541030 |
d_im.process(); |
181 |
541030 |
if (level == EFFORT_LAST_CALL) |
182 |
|
{ |
183 |
5316 |
Assert(d_sygusExtension != nullptr); |
184 |
5316 |
d_sygusExtension->check(); |
185 |
|
} |
186 |
1103772 |
else if (level == EFFORT_FULL && !d_state.isInConflict() |
187 |
567783 |
&& !d_im.hasSentLemma() && !d_valuation.needCheck()) |
188 |
|
{ |
189 |
|
//check for cycles |
190 |
28321 |
Assert(!d_im.hasPendingFact()); |
191 |
4 |
do { |
192 |
28325 |
d_im.reset(); |
193 |
28325 |
Trace("datatypes-proc") << "Check cycles..." << std::endl; |
194 |
28325 |
checkCycles(); |
195 |
28325 |
Trace("datatypes-proc") << "...finish check cycles" << std::endl; |
196 |
28325 |
d_im.process(); |
197 |
28325 |
if (d_state.isInConflict() || d_im.hasSentLemma()) |
198 |
|
{ |
199 |
143 |
return; |
200 |
|
} |
201 |
28182 |
} while (d_im.hasSentFact()); |
202 |
|
|
203 |
|
//check for splits |
204 |
28178 |
Trace("datatypes-debug") << "Check for splits " << endl; |
205 |
1089 |
do { |
206 |
29267 |
d_im.reset(); |
207 |
58534 |
std::map< TypeNode, Node > rec_singletons; |
208 |
29267 |
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine); |
209 |
936617 |
while( !eqcs_i.isFinished() ){ |
210 |
908655 |
Node n = (*eqcs_i); |
211 |
|
//TODO : avoid irrelevant (pre-registered but not asserted) terms here? |
212 |
908655 |
TypeNode tn = n.getType(); |
213 |
454980 |
if( tn.isDatatype() ){ |
214 |
134142 |
Trace("datatypes-debug") << "Process equivalence class " << n << std::endl; |
215 |
134142 |
EqcInfo* eqc = getOrMakeEqcInfo( n ); |
216 |
|
//if there are more than 1 possible constructors for eqc |
217 |
134142 |
if( !hasLabel( eqc, n ) ){ |
218 |
33646 |
Trace("datatypes-debug") << "No constructor..." << std::endl; |
219 |
65987 |
TypeNode tt = tn; |
220 |
33646 |
const DType& dt = tt.getDType(); |
221 |
67292 |
Trace("datatypes-debug") |
222 |
67292 |
<< "Datatype " << dt.getName() << " is " |
223 |
67292 |
<< dt.getCardinalityClass(tt) << " " |
224 |
33646 |
<< dt.isRecursiveSingleton(tt) << std::endl; |
225 |
33646 |
bool continueProc = true; |
226 |
33646 |
if( dt.isRecursiveSingleton( tt ) ){ |
227 |
8 |
Trace("datatypes-debug") << "Check recursive singleton..." << std::endl; |
228 |
|
//handle recursive singleton case |
229 |
8 |
std::map< TypeNode, Node >::iterator itrs = rec_singletons.find( tn ); |
230 |
8 |
if( itrs!=rec_singletons.end() ){ |
231 |
8 |
Node eq = n.eqNode( itrs->second ); |
232 |
4 |
if( d_singleton_eq.find( eq )==d_singleton_eq.end() ){ |
233 |
4 |
d_singleton_eq[eq] = true; |
234 |
|
// get assumptions |
235 |
4 |
bool success = true; |
236 |
8 |
std::vector< Node > assumptions; |
237 |
|
//if there is at least one uninterpreted sort occurring within the datatype and the logic is not quantified, add lemmas ensuring cardinality is more than one, |
238 |
|
// do not infer the equality if at least one sort was processed. |
239 |
|
//otherwise, if the logic is quantified, under the assumption that all uninterpreted sorts have cardinality one, |
240 |
|
// infer the equality. |
241 |
4 |
for( unsigned i=0; i<dt.getNumRecursiveSingletonArgTypes( tt ); i++ ){ |
242 |
|
TypeNode type = dt.getRecursiveSingletonArgType(tt, i); |
243 |
|
if( getQuantifiersEngine() ){ |
244 |
|
// under the assumption that the cardinality of this type is one |
245 |
|
Node a = getSingletonLemma(type, true); |
246 |
|
assumptions.push_back( a.negate() ); |
247 |
|
}else{ |
248 |
|
success = false; |
249 |
|
// assert that the cardinality of this type is more than one |
250 |
|
getSingletonLemma(type, false); |
251 |
|
} |
252 |
|
} |
253 |
4 |
if( success ){ |
254 |
8 |
Node assumption = n.eqNode(itrs->second); |
255 |
4 |
assumptions.push_back(assumption); |
256 |
8 |
Node lemma = assumptions.size()==1 ? assumptions[0] : NodeManager::currentNM()->mkNode( OR, assumptions ); |
257 |
4 |
Trace("dt-singleton") << "*************Singleton equality lemma " << lemma << std::endl; |
258 |
4 |
d_im.lemma(lemma, InferenceId::DATATYPES_REC_SINGLETON_EQ); |
259 |
|
} |
260 |
|
} |
261 |
|
}else{ |
262 |
4 |
rec_singletons[tn] = n; |
263 |
|
} |
264 |
|
//do splitting for quantified logics (incomplete anyways) |
265 |
8 |
continueProc = ( getQuantifiersEngine()!=NULL ); |
266 |
|
} |
267 |
33646 |
if( continueProc ){ |
268 |
33646 |
Trace("datatypes-debug") << "Get possible cons..." << std::endl; |
269 |
|
//all other cases |
270 |
65987 |
std::vector< bool > pcons; |
271 |
33646 |
getPossibleCons( eqc, n, pcons ); |
272 |
|
//check if we do not need to resolve the constructor type for this equivalence class. |
273 |
|
// this is if there are no selectors for this equivalence class, and its possible values are infinite, |
274 |
|
// then do not split. |
275 |
33646 |
int consIndex = -1; |
276 |
33646 |
int fconsIndex = -1; |
277 |
33646 |
bool needSplit = true; |
278 |
129185 |
for (size_t j = 0, psize = pcons.size(); j < psize; j++) |
279 |
|
{ |
280 |
95539 |
if( pcons[j] ) { |
281 |
94129 |
if( consIndex==-1 ){ |
282 |
33549 |
consIndex = j; |
283 |
|
} |
284 |
188258 |
Trace("datatypes-debug") << j << " compute finite..." |
285 |
94129 |
<< std::endl; |
286 |
|
// Notice that we split here on all datatypes except the |
287 |
|
// truly infinite ones. It is possible to also not split |
288 |
|
// on those that are interpreted-finite when finite model |
289 |
|
// finding is disabled, but as a heuristic we choose to split |
290 |
|
// on those too. |
291 |
188258 |
bool ifin = dt[j].getCardinalityClass(tt) |
292 |
94129 |
!= CardinalityClass::INFINITE; |
293 |
188258 |
Trace("datatypes-debug") << "...returned " << ifin |
294 |
94129 |
<< std::endl; |
295 |
94129 |
if (!ifin) |
296 |
|
{ |
297 |
54543 |
if( !eqc || !eqc->d_selectors ){ |
298 |
52094 |
needSplit = false; |
299 |
|
} |
300 |
|
}else{ |
301 |
39586 |
if( fconsIndex==-1 ){ |
302 |
30809 |
fconsIndex = j; |
303 |
|
} |
304 |
|
} |
305 |
|
} |
306 |
|
} |
307 |
|
//if we want to force an assignment of constructors to all ground eqc |
308 |
|
//d_dtfCounter++; |
309 |
33646 |
if( !needSplit && options::dtForceAssignment() && d_dtfCounter%2==0 ){ |
310 |
|
Trace("datatypes-force-assign") << "Force assignment for " << n << std::endl; |
311 |
|
needSplit = true; |
312 |
|
consIndex = fconsIndex!=-1 ? fconsIndex : consIndex; |
313 |
|
} |
314 |
|
|
315 |
33646 |
if( needSplit ) { |
316 |
16122 |
if( dt.getNumConstructors()==1 ){ |
317 |
|
//this may not be necessary? |
318 |
|
//if only one constructor, then this term must be this constructor |
319 |
29634 |
Node t = utils::mkTester(n, 0, dt); |
320 |
14817 |
d_im.addPendingInference( |
321 |
|
t, InferenceId::DATATYPES_SPLIT, d_true); |
322 |
14817 |
Trace("datatypes-infer") << "DtInfer : 1-cons (full) : " << t << std::endl; |
323 |
|
}else{ |
324 |
1305 |
Assert(consIndex != -1 || dt.isSygus()); |
325 |
1305 |
if( options::dtBinarySplit() && consIndex!=-1 ){ |
326 |
|
Node test = utils::mkTester(n, consIndex, dt); |
327 |
|
Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n << endl; |
328 |
|
test = Rewriter::rewrite( test ); |
329 |
|
NodeBuilder nb(kind::OR); |
330 |
|
nb << test << test.notNode(); |
331 |
|
Node lemma = nb; |
332 |
|
d_im.lemma(lemma, InferenceId::DATATYPES_BINARY_SPLIT); |
333 |
|
d_im.requirePhase(test, true); |
334 |
|
}else{ |
335 |
1305 |
Trace("dt-split") << "*************Split for constructors on " << n << endl; |
336 |
2610 |
Node lemma = utils::mkSplit(n, dt); |
337 |
1305 |
Trace("dt-split-debug") << "Split lemma is : " << lemma << std::endl; |
338 |
1305 |
d_im.sendDtLemma(lemma, |
339 |
|
InferenceId::DATATYPES_SPLIT, |
340 |
|
LemmaProperty::SEND_ATOMS); |
341 |
|
} |
342 |
1305 |
if( !options::dtBlastSplits() ){ |
343 |
1305 |
break; |
344 |
|
} |
345 |
|
} |
346 |
|
}else{ |
347 |
17524 |
Trace("dt-split-debug") << "Do not split constructor for " << n << " : " << n.getType() << " " << dt.getNumConstructors() << std::endl; |
348 |
|
} |
349 |
|
} |
350 |
|
}else{ |
351 |
100496 |
Trace("datatypes-debug") << "Has constructor " << eqc->d_constructor.get() << std::endl; |
352 |
|
} |
353 |
|
} |
354 |
453675 |
++eqcs_i; |
355 |
|
} |
356 |
29267 |
if (d_im.hasSentLemma()) |
357 |
|
{ |
358 |
|
// clear pending facts: we added a lemma, so internal inferences are |
359 |
|
// no longer necessary |
360 |
1290 |
d_im.clearPendingFacts(); |
361 |
|
} |
362 |
|
else |
363 |
|
{ |
364 |
|
// we did not add a lemma, process internal inferences. This loop |
365 |
|
// will repeat. |
366 |
27977 |
Trace("datatypes-debug") << "Flush pending facts..." << std::endl; |
367 |
27977 |
d_im.process(); |
368 |
|
} |
369 |
57722 |
} while (!d_state.isInConflict() && !d_im.hasSentLemma() |
370 |
56190 |
&& d_im.hasSentFact()); |
371 |
56356 |
Trace("datatypes-debug") |
372 |
56356 |
<< "Finished, conflict=" << d_state.isInConflict() |
373 |
28178 |
<< ", lemmas=" << d_im.hasSentLemma() << std::endl; |
374 |
28178 |
if (!d_state.isInConflict()) |
375 |
|
{ |
376 |
27366 |
Trace("dt-model-debug") << std::endl; |
377 |
27366 |
printModelDebug("dt-model-debug"); |
378 |
|
} |
379 |
|
} |
380 |
|
|
381 |
540887 |
Trace("datatypes-check") << "Finished check effort " << level << std::endl; |
382 |
540887 |
if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") ) { |
383 |
|
Notice() << "TheoryDatatypes::check(): done" << endl; |
384 |
|
} |
385 |
|
} |
386 |
|
|
387 |
10898 |
bool TheoryDatatypes::needsCheckLastEffort() { |
388 |
10898 |
return d_sygusExtension != nullptr; |
389 |
|
} |
390 |
|
|
391 |
2380168 |
void TheoryDatatypes::notifyFact(TNode atom, |
392 |
|
bool polarity, |
393 |
|
TNode fact, |
394 |
|
bool isInternal) |
395 |
|
{ |
396 |
4760336 |
Trace("datatypes-debug") << "TheoryDatatypes::assertFact : " << fact |
397 |
2380168 |
<< ", isInternal = " << isInternal << std::endl; |
398 |
|
// could be sygus-specific |
399 |
2380168 |
if (d_sygusExtension) |
400 |
|
{ |
401 |
1994647 |
d_sygusExtension->assertFact(atom, polarity); |
402 |
|
} |
403 |
|
//add to tester if applicable |
404 |
4760336 |
Node t_arg; |
405 |
2380168 |
int tindex = utils::isTester(atom, t_arg); |
406 |
2380168 |
if (tindex >= 0) |
407 |
|
{ |
408 |
1219214 |
Trace("dt-tester") << "Assert tester : " << atom << " for " << t_arg << std::endl; |
409 |
2438428 |
Node rep = getRepresentative( t_arg ); |
410 |
1219214 |
EqcInfo* eqc = getOrMakeEqcInfo( rep, true ); |
411 |
|
Node tst = |
412 |
2438428 |
isInternal ? (polarity ? Node(atom) : atom.notNode()) : Node(fact); |
413 |
1219214 |
addTester(tindex, tst, eqc, rep, t_arg); |
414 |
1219214 |
Trace("dt-tester") << "Done assert tester." << std::endl; |
415 |
1219214 |
Trace("dt-tester") << "Done pending merges." << std::endl; |
416 |
1219214 |
if (!d_state.isInConflict() && polarity) |
417 |
|
{ |
418 |
355873 |
if (d_sygusExtension) |
419 |
|
{ |
420 |
308376 |
Trace("dt-tester") << "Assert tester to sygus : " << atom << std::endl; |
421 |
308376 |
d_sygusExtension->assertTester(tindex, t_arg, atom); |
422 |
308376 |
Trace("dt-tester") << "Done assert tester to sygus." << std::endl; |
423 |
|
} |
424 |
|
} |
425 |
|
}else{ |
426 |
1160954 |
Trace("dt-tester-debug") << "Assert (non-tester) : " << atom << std::endl; |
427 |
|
} |
428 |
2380168 |
Trace("datatypes-debug") << "TheoryDatatypes::assertFact : finished " << fact << std::endl; |
429 |
|
// now, flush pending facts if this wasn't an internal call |
430 |
2380168 |
if (!isInternal) |
431 |
|
{ |
432 |
2054582 |
d_im.process(); |
433 |
|
} |
434 |
2380168 |
} |
435 |
|
|
436 |
187010 |
void TheoryDatatypes::preRegisterTerm(TNode n) |
437 |
|
{ |
438 |
374020 |
Trace("datatypes-prereg") |
439 |
187010 |
<< "TheoryDatatypes::preRegisterTerm() " << n << endl; |
440 |
|
// external selectors should be preprocessed away by now |
441 |
187010 |
Assert(n.getKind() != APPLY_SELECTOR); |
442 |
|
// must ensure the type is well founded and has no nested recursion if |
443 |
|
// the option dtNestedRec is not set to true. |
444 |
374020 |
TypeNode tn = n.getType(); |
445 |
187010 |
if (tn.isDatatype()) |
446 |
|
{ |
447 |
74493 |
const DType& dt = tn.getDType(); |
448 |
74493 |
Trace("dt-expand") << "Check properties of " << dt.getName() << std::endl; |
449 |
74493 |
if (!dt.isWellFounded()) |
450 |
|
{ |
451 |
|
std::stringstream ss; |
452 |
|
ss << "Cannot handle non-well-founded datatype " << dt.getName(); |
453 |
|
throw LogicException(ss.str()); |
454 |
|
} |
455 |
74493 |
Trace("dt-expand") << "...well-founded ok" << std::endl; |
456 |
74493 |
if (!options::dtNestedRec()) |
457 |
|
{ |
458 |
74265 |
if (dt.hasNestedRecursion()) |
459 |
|
{ |
460 |
2 |
std::stringstream ss; |
461 |
1 |
ss << "Cannot handle nested-recursive datatype " << dt.getName(); |
462 |
1 |
throw LogicException(ss.str()); |
463 |
|
} |
464 |
74264 |
Trace("dt-expand") << "...nested recursion ok" << std::endl; |
465 |
|
} |
466 |
|
} |
467 |
187009 |
collectTerms( n ); |
468 |
187009 |
switch (n.getKind()) { |
469 |
85759 |
case kind::EQUAL: |
470 |
|
case kind::APPLY_TESTER: |
471 |
|
// add predicate trigger for testers and equalities |
472 |
|
// Get triggered for both equal and dis-equal |
473 |
85759 |
d_equalityEngine->addTriggerPredicate(n); |
474 |
85759 |
break; |
475 |
101250 |
default: |
476 |
|
// Function applications/predicates |
477 |
101250 |
d_equalityEngine->addTerm(n); |
478 |
101250 |
if (d_sygusExtension) |
479 |
|
{ |
480 |
23756 |
d_sygusExtension->preRegisterTerm(n); |
481 |
|
} |
482 |
101250 |
break; |
483 |
|
} |
484 |
187009 |
d_im.process(); |
485 |
187009 |
} |
486 |
|
|
487 |
81749 |
TrustNode TheoryDatatypes::ppRewrite(TNode in, std::vector<SkolemLemma>& lems) |
488 |
|
{ |
489 |
81749 |
Debug("tuprec") << "TheoryDatatypes::ppRewrite(" << in << ")" << endl; |
490 |
|
// first, see if we need to expand definitions |
491 |
163498 |
TrustNode texp = d_rewriter.expandDefinition(in); |
492 |
81749 |
if (!texp.isNull()) |
493 |
|
{ |
494 |
3954 |
return texp; |
495 |
|
} |
496 |
77795 |
if( in.getKind()==EQUAL ){ |
497 |
8286 |
Node nn; |
498 |
8286 |
std::vector< Node > rew; |
499 |
4189 |
if (utils::checkClash(in[0], in[1], rew)) |
500 |
|
{ |
501 |
|
nn = NodeManager::currentNM()->mkConst(false); |
502 |
|
} |
503 |
|
else |
504 |
|
{ |
505 |
12495 |
nn = rew.size()==0 ? d_true : |
506 |
8306 |
( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) ); |
507 |
|
} |
508 |
4189 |
if (in != nn) |
509 |
|
{ |
510 |
92 |
return TrustNode::mkTrustRewrite(in, nn, nullptr); |
511 |
|
} |
512 |
|
} |
513 |
|
|
514 |
|
// nothing to do |
515 |
77703 |
return TrustNode::null(); |
516 |
|
} |
517 |
|
|
518 |
61627 |
TrustNode TheoryDatatypes::explain(TNode literal) |
519 |
|
{ |
520 |
61627 |
return d_im.explainLit(literal); |
521 |
|
} |
522 |
|
|
523 |
|
/** called when a new equivalance class is created */ |
524 |
296918 |
void TheoryDatatypes::eqNotifyNewClass(TNode t){ |
525 |
296918 |
if( t.getKind()==APPLY_CONSTRUCTOR ){ |
526 |
100154 |
getOrMakeEqcInfo( t, true ); |
527 |
|
} |
528 |
296918 |
} |
529 |
|
|
530 |
|
/** called when two equivalance classes have merged */ |
531 |
2514147 |
void TheoryDatatypes::eqNotifyMerge(TNode t1, TNode t2) |
532 |
|
{ |
533 |
2514147 |
if( t1.getType().isDatatype() ){ |
534 |
1177416 |
Trace("datatypes-merge") |
535 |
588708 |
<< "NotifyMerge : " << t1 << " " << t2 << std::endl; |
536 |
588708 |
merge(t1, t2); |
537 |
|
} |
538 |
2514147 |
} |
539 |
|
|
540 |
588708 |
void TheoryDatatypes::merge( Node t1, Node t2 ){ |
541 |
588708 |
if (d_state.isInConflict()) |
542 |
|
{ |
543 |
182293 |
return; |
544 |
|
} |
545 |
588571 |
Trace("datatypes-merge") << "Merge " << t1 << " " << t2 << std::endl; |
546 |
588571 |
Assert(areEqual(t1, t2)); |
547 |
995123 |
TNode trep1 = t1; |
548 |
995123 |
TNode trep2 = t2; |
549 |
588571 |
EqcInfo* eqc2 = getOrMakeEqcInfo(t2); |
550 |
588571 |
if (eqc2 == nullptr) |
551 |
|
{ |
552 |
180298 |
return; |
553 |
|
} |
554 |
408273 |
bool checkInst = false; |
555 |
408273 |
if (!eqc2->d_constructor.get().isNull()) |
556 |
|
{ |
557 |
104887 |
trep2 = eqc2->d_constructor.get(); |
558 |
|
} |
559 |
408273 |
EqcInfo* eqc1 = getOrMakeEqcInfo(t1); |
560 |
408273 |
if (eqc1) |
561 |
|
{ |
562 |
780164 |
Trace("datatypes-debug") |
563 |
390082 |
<< " merge eqc info " << eqc2 << " into " << eqc1 << std::endl; |
564 |
390082 |
if (!eqc1->d_constructor.get().isNull()) |
565 |
|
{ |
566 |
309720 |
trep1 = eqc1->d_constructor.get(); |
567 |
|
} |
568 |
|
// check for clash |
569 |
779153 |
TNode cons1 = eqc1->d_constructor.get(); |
570 |
779153 |
TNode cons2 = eqc2->d_constructor.get(); |
571 |
|
// if both have constructor, then either clash or unification |
572 |
390082 |
if (!cons1.isNull() && !cons2.isNull()) |
573 |
|
{ |
574 |
115294 |
Trace("datatypes-debug") |
575 |
57647 |
<< " constructors : " << cons1 << " " << cons2 << std::endl; |
576 |
114298 |
Node unifEq = cons1.eqNode(cons2); |
577 |
114298 |
std::vector<Node> rew; |
578 |
57647 |
if (utils::checkClash(cons1, cons2, rew)) |
579 |
|
{ |
580 |
1992 |
std::vector<Node> conf; |
581 |
996 |
conf.push_back(unifEq); |
582 |
1992 |
Trace("dt-conflict") |
583 |
996 |
<< "CONFLICT: Clash conflict : " << conf << std::endl; |
584 |
996 |
d_im.sendDtConflict(conf, InferenceId::DATATYPES_CLASH_CONFLICT); |
585 |
996 |
return; |
586 |
|
} |
587 |
|
else |
588 |
|
{ |
589 |
56651 |
Assert(areEqual(cons1, cons2)); |
590 |
|
// do unification |
591 |
166323 |
for (size_t i = 0, nchild = cons1.getNumChildren(); i < nchild; i++) |
592 |
|
{ |
593 |
109672 |
if (!areEqual(cons1[i], cons2[i])) |
594 |
|
{ |
595 |
56464 |
Node eq = cons1[i].eqNode(cons2[i]); |
596 |
28232 |
d_im.addPendingInference(eq, InferenceId::DATATYPES_UNIF, unifEq); |
597 |
56464 |
Trace("datatypes-infer") << "DtInfer : cons-inj : " << eq << " by " |
598 |
28232 |
<< unifEq << std::endl; |
599 |
|
} |
600 |
|
} |
601 |
|
} |
602 |
|
} |
603 |
778172 |
Trace("datatypes-debug") << " instantiated : " << eqc1->d_inst << " " |
604 |
389086 |
<< eqc2->d_inst << std::endl; |
605 |
389086 |
eqc1->d_inst = eqc1->d_inst || eqc2->d_inst; |
606 |
389086 |
if (!cons2.isNull()) |
607 |
|
{ |
608 |
95191 |
if (cons1.isNull()) |
609 |
|
{ |
610 |
77080 |
Trace("datatypes-debug") |
611 |
38540 |
<< " must check if it is okay to set the constructor." |
612 |
38540 |
<< std::endl; |
613 |
38540 |
checkInst = true; |
614 |
38540 |
addConstructor(eqc2->d_constructor.get(), eqc1, t1); |
615 |
38540 |
if (d_state.isInConflict()) |
616 |
|
{ |
617 |
15 |
return; |
618 |
|
} |
619 |
|
} |
620 |
|
} |
621 |
|
} |
622 |
|
else |
623 |
|
{ |
624 |
36382 |
Trace("datatypes-debug") |
625 |
18191 |
<< " no eqc info for " << t1 << ", must create" << std::endl; |
626 |
|
// just copy the equivalence class information |
627 |
18191 |
eqc1 = getOrMakeEqcInfo(t1, true); |
628 |
18191 |
eqc1->d_inst.set(eqc2->d_inst); |
629 |
18191 |
eqc1->d_constructor.set(eqc2->d_constructor); |
630 |
18191 |
eqc1->d_selectors.set(eqc2->d_selectors); |
631 |
|
} |
632 |
|
|
633 |
|
// merge labels |
634 |
407262 |
NodeUIntMap::iterator lbl_i = d_labels.find(t2); |
635 |
407262 |
if (lbl_i != d_labels.end()) |
636 |
|
{ |
637 |
814524 |
Trace("datatypes-debug") |
638 |
407262 |
<< " merge labels from " << eqc2 << " " << t2 << std::endl; |
639 |
407262 |
size_t n_label = (*lbl_i).second; |
640 |
699454 |
for (size_t i = 0; i < n_label; i++) |
641 |
|
{ |
642 |
292902 |
Assert(i < d_labels_data[t2].size()); |
643 |
585094 |
Node t = d_labels_data[t2][i]; |
644 |
585094 |
Node t_arg = d_labels_args[t2][i]; |
645 |
292902 |
unsigned tindex = d_labels_tindex[t2][i]; |
646 |
292902 |
addTester(tindex, t, eqc1, t1, t_arg); |
647 |
292902 |
if (d_state.isInConflict()) |
648 |
|
{ |
649 |
710 |
Trace("datatypes-debug") << " conflict!" << std::endl; |
650 |
710 |
return; |
651 |
|
} |
652 |
|
} |
653 |
|
} |
654 |
|
// merge selectors |
655 |
406552 |
if (!eqc1->d_selectors && eqc2->d_selectors) |
656 |
|
{ |
657 |
50300 |
eqc1->d_selectors = true; |
658 |
50300 |
checkInst = true; |
659 |
|
} |
660 |
406552 |
NodeUIntMap::iterator sel_i = d_selector_apps.find(t2); |
661 |
406552 |
if (sel_i != d_selector_apps.end()) |
662 |
|
{ |
663 |
813104 |
Trace("datatypes-debug") |
664 |
406552 |
<< " merge selectors from " << eqc2 << " " << t2 << std::endl; |
665 |
406552 |
size_t n_sel = (*sel_i).second; |
666 |
993170 |
for (size_t j = 0; j < n_sel; j++) |
667 |
|
{ |
668 |
586618 |
addSelector(d_selector_apps_data[t2][j], |
669 |
|
eqc1, |
670 |
|
t1, |
671 |
586618 |
eqc2->d_constructor.get().isNull()); |
672 |
|
} |
673 |
|
} |
674 |
406552 |
if (checkInst) |
675 |
|
{ |
676 |
88825 |
Trace("datatypes-debug") << " checking instantiate" << std::endl; |
677 |
88825 |
instantiate(eqc1, t1); |
678 |
|
} |
679 |
406552 |
Trace("datatypes-debug") << "Finished Merge " << t1 << " " << t2 << std::endl; |
680 |
|
} |
681 |
|
|
682 |
25724 |
TheoryDatatypes::EqcInfo::EqcInfo(context::Context* c) |
683 |
|
: d_inst(c, false), |
684 |
51448 |
d_constructor(c, Node::null()), |
685 |
77172 |
d_selectors(c, false) |
686 |
25724 |
{} |
687 |
|
|
688 |
134142 |
bool TheoryDatatypes::hasLabel( EqcInfo* eqc, Node n ){ |
689 |
134142 |
return ( eqc && !eqc->d_constructor.get().isNull() ) || !getLabel( n ).isNull(); |
690 |
|
} |
691 |
|
|
692 |
724792 |
Node TheoryDatatypes::getLabel( Node n ) { |
693 |
724792 |
NodeUIntMap::iterator lbl_i = d_labels.find(n); |
694 |
724792 |
if( lbl_i != d_labels.end() ){ |
695 |
668292 |
size_t n_lbl = (*lbl_i).second; |
696 |
668292 |
if( n_lbl>0 && d_labels_data[n][ n_lbl-1 ].getKind()!=kind::NOT ){ |
697 |
216502 |
return d_labels_data[n][ n_lbl-1 ]; |
698 |
|
} |
699 |
|
} |
700 |
508290 |
return Node::null(); |
701 |
|
} |
702 |
|
|
703 |
1785420 |
int TheoryDatatypes::getLabelIndex( EqcInfo* eqc, Node n ){ |
704 |
1785420 |
if( eqc && !eqc->d_constructor.get().isNull() ){ |
705 |
1201769 |
return utils::indexOf(eqc->d_constructor.get().getOperator()); |
706 |
|
}else{ |
707 |
1167302 |
Node lbl = getLabel( n ); |
708 |
583651 |
if( lbl.isNull() ){ |
709 |
474644 |
return -1; |
710 |
|
}else{ |
711 |
109007 |
int tindex = utils::isTester(lbl); |
712 |
218014 |
Trace("datatypes-debug") << "Label of " << n << " is " << lbl |
713 |
109007 |
<< " with tindex " << tindex << std::endl; |
714 |
109007 |
Assert(tindex != -1); |
715 |
109007 |
return tindex; |
716 |
|
} |
717 |
|
} |
718 |
|
} |
719 |
|
|
720 |
8422 |
bool TheoryDatatypes::hasTester( Node n ) { |
721 |
8422 |
NodeUIntMap::iterator lbl_i = d_labels.find(n); |
722 |
8422 |
if( lbl_i != d_labels.end() ){ |
723 |
3 |
return (*lbl_i).second>0; |
724 |
|
}else{ |
725 |
8419 |
return false; |
726 |
|
} |
727 |
|
} |
728 |
|
|
729 |
77444 |
void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >& pcons ){ |
730 |
154888 |
TypeNode tn = n.getType(); |
731 |
77444 |
const DType& dt = tn.getDType(); |
732 |
77444 |
int lindex = getLabelIndex( eqc, n ); |
733 |
77444 |
pcons.resize( dt.getNumConstructors(), lindex==-1 ); |
734 |
77444 |
if( lindex!=-1 ){ |
735 |
|
pcons[ lindex ] = true; |
736 |
|
}else{ |
737 |
77444 |
NodeUIntMap::iterator lbl_i = d_labels.find(n); |
738 |
77444 |
if( lbl_i != d_labels.end() ){ |
739 |
49194 |
size_t n_lbl = (*lbl_i).second; |
740 |
262121 |
for (size_t i = 0; i < n_lbl; i++) |
741 |
|
{ |
742 |
212927 |
Assert(d_labels_data[n][i].getKind() == NOT); |
743 |
212927 |
unsigned tindex = d_labels_tindex[n][i]; |
744 |
212927 |
pcons[ tindex ] = false; |
745 |
|
} |
746 |
|
} |
747 |
|
} |
748 |
77444 |
} |
749 |
|
|
750 |
118190 |
Node TheoryDatatypes::getTermSkolemFor( Node n ) { |
751 |
118190 |
if( n.getKind()==APPLY_CONSTRUCTOR ){ |
752 |
11155 |
NodeMap::const_iterator it = d_term_sk.find( n ); |
753 |
11155 |
if( it==d_term_sk.end() ){ |
754 |
1235 |
NodeManager* nm = NodeManager::currentNM(); |
755 |
1235 |
SkolemManager* sm = nm->getSkolemManager(); |
756 |
|
//add purification unit lemma ( k = n ) |
757 |
2470 |
Node k = sm->mkPurifySkolem(n, "kdt"); |
758 |
1235 |
d_term_sk[n] = k; |
759 |
2470 |
Node eq = k.eqNode( n ); |
760 |
1235 |
Trace("datatypes-infer") << "DtInfer : ref : " << eq << std::endl; |
761 |
1235 |
d_im.addPendingLemma(eq, InferenceId::DATATYPES_PURIFY); |
762 |
1235 |
return k; |
763 |
|
}else{ |
764 |
9920 |
return (*it).second; |
765 |
|
} |
766 |
|
}else{ |
767 |
107035 |
return n; |
768 |
|
} |
769 |
|
} |
770 |
|
|
771 |
1512116 |
void TheoryDatatypes::addTester( |
772 |
|
unsigned ttindex, Node t, EqcInfo* eqc, Node n, Node t_arg) |
773 |
|
{ |
774 |
1512116 |
Trace("datatypes-debug") << "Add tester : " << t << " to eqc(" << n << ")" << std::endl; |
775 |
1512116 |
Debug("datatypes-labels") << "Add tester " << t << " " << n << " " << eqc << std::endl; |
776 |
1512116 |
bool tpolarity = t.getKind()!=NOT; |
777 |
1512116 |
Assert((tpolarity ? t : t[0]).getKind() == APPLY_TESTER); |
778 |
1832169 |
Node j, jt; |
779 |
1512116 |
bool makeConflict = false; |
780 |
1512116 |
int prevTIndex = getLabelIndex(eqc, n); |
781 |
1512116 |
if (prevTIndex >= 0) |
782 |
|
{ |
783 |
1115470 |
unsigned ptu = static_cast<unsigned>(prevTIndex); |
784 |
|
//if we already know the constructor type, check whether it is in conflict or redundant |
785 |
1115470 |
if ((ptu == ttindex) != tpolarity) |
786 |
|
{ |
787 |
1619 |
if( !eqc->d_constructor.get().isNull() ){ |
788 |
|
//conflict because equivalence class contains a constructor |
789 |
3238 |
std::vector<Node> conf; |
790 |
1619 |
conf.push_back(t); |
791 |
1619 |
conf.push_back(t_arg.eqNode(eqc->d_constructor.get())); |
792 |
3238 |
Trace("dt-conflict") |
793 |
1619 |
<< "CONFLICT: Tester eq conflict " << conf << std::endl; |
794 |
1619 |
d_im.sendDtConflict(conf, InferenceId::DATATYPES_TESTER_CONFLICT); |
795 |
1619 |
return; |
796 |
|
}else{ |
797 |
|
makeConflict = true; |
798 |
|
//conflict because the existing label is contradictory |
799 |
|
j = getLabel( n ); |
800 |
|
jt = j; |
801 |
|
} |
802 |
|
}else{ |
803 |
1113851 |
return; |
804 |
|
} |
805 |
|
}else{ |
806 |
|
//otherwise, scan list of labels |
807 |
396646 |
NodeUIntMap::iterator lbl_i = d_labels.find(n); |
808 |
396646 |
Assert(lbl_i != d_labels.end()); |
809 |
396646 |
size_t n_lbl = (*lbl_i).second; |
810 |
716699 |
std::map< int, bool > neg_testers; |
811 |
1466698 |
for (size_t i = 0; i < n_lbl; i++) |
812 |
|
{ |
813 |
1103031 |
Assert(d_labels_data[n][i].getKind() == NOT); |
814 |
1103031 |
unsigned jtindex = d_labels_tindex[n][i]; |
815 |
1103031 |
if( jtindex==ttindex ){ |
816 |
32979 |
if( tpolarity ){ //we are in conflict |
817 |
181 |
j = d_labels_data[n][i]; |
818 |
181 |
jt = j[0]; |
819 |
181 |
makeConflict = true; |
820 |
181 |
break; |
821 |
|
}else{ //it is redundant |
822 |
32798 |
return; |
823 |
|
} |
824 |
|
}else{ |
825 |
1070052 |
neg_testers[jtindex] = true; |
826 |
|
} |
827 |
|
} |
828 |
363848 |
if( !makeConflict ){ |
829 |
363667 |
Debug("datatypes-labels") << "Add to labels " << t << std::endl; |
830 |
363667 |
d_labels[n] = n_lbl + 1; |
831 |
363667 |
if (n_lbl < d_labels_data[n].size()) |
832 |
|
{ |
833 |
|
// reuse spot in the vector |
834 |
352421 |
d_labels_data[n][n_lbl] = t; |
835 |
352421 |
d_labels_args[n][n_lbl] = t_arg; |
836 |
352421 |
d_labels_tindex[n][n_lbl] = ttindex; |
837 |
|
}else{ |
838 |
11246 |
d_labels_data[n].push_back(t); |
839 |
11246 |
d_labels_args[n].push_back(t_arg); |
840 |
11246 |
d_labels_tindex[n].push_back(ttindex); |
841 |
|
} |
842 |
363667 |
n_lbl++; |
843 |
|
|
844 |
363667 |
const DType& dt = t_arg.getType().getDType(); |
845 |
363667 |
Debug("datatypes-labels") << "Labels at " << n_lbl << " / " << dt.getNumConstructors() << std::endl; |
846 |
363667 |
if( tpolarity ){ |
847 |
107035 |
instantiate(eqc, n); |
848 |
|
// We could propagate is-C1(x) => not is-C2(x) here for all other |
849 |
|
// constructors, but empirically this hurts performance. |
850 |
|
}else{ |
851 |
|
//check if we have reached the maximum number of testers |
852 |
|
// in this case, add the positive tester |
853 |
256632 |
if (n_lbl == dt.getNumConstructors() - 1) |
854 |
|
{ |
855 |
87590 |
std::vector< bool > pcons; |
856 |
43795 |
getPossibleCons( eqc, n, pcons ); |
857 |
43795 |
int testerIndex = -1; |
858 |
139914 |
for( unsigned i=0; i<pcons.size(); i++ ) { |
859 |
139914 |
if( pcons[i] ){ |
860 |
43795 |
testerIndex = i; |
861 |
43795 |
break; |
862 |
|
} |
863 |
|
} |
864 |
43795 |
Assert(testerIndex != -1); |
865 |
|
//we must explain why each term in the set of testers for this equivalence class is equal |
866 |
87590 |
std::vector< Node > eq_terms; |
867 |
87590 |
NodeBuilder nb(kind::AND); |
868 |
255307 |
for (unsigned i = 0; i < n_lbl; i++) |
869 |
|
{ |
870 |
423024 |
Node ti = d_labels_data[n][i]; |
871 |
211512 |
nb << ti; |
872 |
211512 |
Assert(ti.getKind() == NOT); |
873 |
423024 |
Node t_arg2 = d_labels_args[n][i]; |
874 |
211512 |
if( std::find( eq_terms.begin(), eq_terms.end(), t_arg2 )==eq_terms.end() ){ |
875 |
54658 |
eq_terms.push_back( t_arg2 ); |
876 |
54658 |
if( t_arg2!=t_arg ){ |
877 |
10863 |
nb << t_arg2.eqNode( t_arg ); |
878 |
|
} |
879 |
|
} |
880 |
|
} |
881 |
|
Node t_concl = testerIndex == -1 |
882 |
|
? NodeManager::currentNM()->mkConst(false) |
883 |
87590 |
: utils::mkTester(t_arg, testerIndex, dt); |
884 |
87590 |
Node t_concl_exp = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb; |
885 |
43795 |
d_im.addPendingInference( |
886 |
|
t_concl, InferenceId::DATATYPES_LABEL_EXH, t_concl_exp); |
887 |
43795 |
Trace("datatypes-infer") << "DtInfer : label : " << t_concl << " by " << t_concl_exp << std::endl; |
888 |
43795 |
return; |
889 |
|
} |
890 |
|
} |
891 |
|
} |
892 |
|
} |
893 |
320053 |
if( makeConflict ){ |
894 |
181 |
Debug("datatypes-labels") << "Explain " << j << " " << t << std::endl; |
895 |
362 |
std::vector<Node> conf; |
896 |
181 |
conf.push_back(j); |
897 |
181 |
conf.push_back(t); |
898 |
181 |
conf.push_back(jt[0].eqNode(t_arg)); |
899 |
181 |
Trace("dt-conflict") << "CONFLICT: Tester conflict : " << conf << std::endl; |
900 |
181 |
d_im.sendDtConflict(conf, InferenceId::DATATYPES_TESTER_MERGE_CONFLICT); |
901 |
|
} |
902 |
|
} |
903 |
|
|
904 |
611033 |
void TheoryDatatypes::addSelector( Node s, EqcInfo* eqc, Node n, bool assertFacts ) { |
905 |
611033 |
Trace("dt-collapse-sel") << "Add selector : " << s << " to eqc(" << n << ")" << std::endl; |
906 |
|
//check to see if it is redundant |
907 |
611033 |
NodeUIntMap::iterator sel_i = d_selector_apps.find(n); |
908 |
611033 |
Assert(sel_i != d_selector_apps.end()); |
909 |
611033 |
if( sel_i != d_selector_apps.end() ){ |
910 |
611033 |
size_t n_sel = (*sel_i).second; |
911 |
1277724 |
for (size_t j = 0; j < n_sel; j++) |
912 |
|
{ |
913 |
1744786 |
Node ss = d_selector_apps_data[n][j]; |
914 |
1078095 |
if( s.getOperator()==ss.getOperator() && ( s.getKind()!=DT_HEIGHT_BOUND || s[1]==ss[1] ) ){ |
915 |
411404 |
Trace("dt-collapse-sel") << "...redundant." << std::endl; |
916 |
411404 |
return; |
917 |
|
} |
918 |
|
} |
919 |
|
//add it to the vector |
920 |
|
//sel->push_back( s ); |
921 |
199629 |
d_selector_apps[n] = n_sel + 1; |
922 |
199629 |
if (n_sel < d_selector_apps_data[n].size()) |
923 |
|
{ |
924 |
181609 |
d_selector_apps_data[n][n_sel] = s; |
925 |
|
}else{ |
926 |
18020 |
d_selector_apps_data[n].push_back( s ); |
927 |
|
} |
928 |
|
|
929 |
199629 |
eqc->d_selectors = true; |
930 |
|
} |
931 |
199629 |
if( assertFacts && !eqc->d_constructor.get().isNull() ){ |
932 |
|
//conclude the collapsed merge |
933 |
140659 |
collapseSelector( s, eqc->d_constructor.get() ); |
934 |
|
} |
935 |
|
} |
936 |
|
|
937 |
38540 |
void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){ |
938 |
38540 |
Trace("datatypes-debug") << "Add constructor : " << c << " to eqc(" << n << ")" << std::endl; |
939 |
38540 |
Assert(eqc->d_constructor.get().isNull()); |
940 |
|
//check labels |
941 |
38540 |
NodeUIntMap::iterator lbl_i = d_labels.find(n); |
942 |
38540 |
if( lbl_i != d_labels.end() ){ |
943 |
38540 |
size_t constructorIndex = utils::indexOf(c.getOperator()); |
944 |
38540 |
size_t n_lbl = (*lbl_i).second; |
945 |
184393 |
for (size_t i = 0; i < n_lbl; i++) |
946 |
|
{ |
947 |
291721 |
Node t = d_labels_data[n][i]; |
948 |
145868 |
if (d_labels_data[n][i].getKind() == NOT) |
949 |
|
{ |
950 |
109585 |
unsigned tindex = d_labels_tindex[n][i]; |
951 |
109585 |
if (tindex == constructorIndex) |
952 |
|
{ |
953 |
30 |
std::vector<Node> conf; |
954 |
15 |
conf.push_back(t); |
955 |
15 |
conf.push_back(t[0][0].eqNode(c)); |
956 |
30 |
Trace("dt-conflict") |
957 |
15 |
<< "CONFLICT: Tester merge eq conflict : " << conf << std::endl; |
958 |
15 |
d_im.sendDtConflict(conf, InferenceId::DATATYPES_TESTER_CONFLICT); |
959 |
15 |
return; |
960 |
|
} |
961 |
|
} |
962 |
|
} |
963 |
|
} |
964 |
|
//check selectors |
965 |
38525 |
NodeUIntMap::iterator sel_i = d_selector_apps.find(n); |
966 |
38525 |
if( sel_i != d_selector_apps.end() ){ |
967 |
38525 |
size_t n_sel = (*sel_i).second; |
968 |
170091 |
for (size_t j = 0; j < n_sel; j++) |
969 |
|
{ |
970 |
263132 |
Node s = d_selector_apps_data[n][j]; |
971 |
|
//collapse the selector |
972 |
131566 |
collapseSelector( s, c ); |
973 |
|
} |
974 |
|
} |
975 |
38525 |
eqc->d_constructor.set( c ); |
976 |
|
} |
977 |
|
|
978 |
272225 |
void TheoryDatatypes::collapseSelector( Node s, Node c ) { |
979 |
272225 |
Assert(c.getKind() == APPLY_CONSTRUCTOR); |
980 |
272225 |
Trace("dt-collapse-sel") << "collapse selector : " << s << " " << c << std::endl; |
981 |
544450 |
Node r; |
982 |
272225 |
bool wrong = false; |
983 |
544450 |
Node eq_exp = s[0].eqNode(c); |
984 |
272225 |
if( s.getKind()==kind::APPLY_SELECTOR_TOTAL ){ |
985 |
415306 |
Node selector = s.getOperator(); |
986 |
207653 |
size_t constructorIndex = utils::indexOf(c.getOperator()); |
987 |
207653 |
const DType& dt = utils::datatypeOf(selector); |
988 |
207653 |
const DTypeConstructor& dtc = dt[constructorIndex]; |
989 |
207653 |
int selectorIndex = dtc.getSelectorIndexInternal(selector); |
990 |
207653 |
wrong = selectorIndex<0; |
991 |
207653 |
r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), c ); |
992 |
|
} |
993 |
272225 |
if( !r.isNull() ){ |
994 |
415306 |
Node rrs; |
995 |
207653 |
if (wrong) |
996 |
|
{ |
997 |
|
// Must use make ground term here instead of the rewriter, since we |
998 |
|
// do not want to introduce arbitrary values. This is important so that |
999 |
|
// we avoid constants for types that are not "closed enumerable", e.g. |
1000 |
|
// uninterpreted sorts and arrays, where the solver does not fully |
1001 |
|
// handle values of the sort. The call to mkGroundTerm does not introduce |
1002 |
|
// values for these sorts. |
1003 |
116239 |
rrs = r.getType().mkGroundTerm(); |
1004 |
232478 |
Trace("datatypes-wrong-sel") |
1005 |
116239 |
<< "Bad apply " << r << " term = " << rrs |
1006 |
116239 |
<< ", value = " << r.getType().mkGroundValue() << std::endl; |
1007 |
|
} |
1008 |
|
else |
1009 |
|
{ |
1010 |
91414 |
rrs = Rewriter::rewrite(r); |
1011 |
|
} |
1012 |
207653 |
if (s != rrs) |
1013 |
|
{ |
1014 |
286312 |
Node eq = s.eqNode(rrs); |
1015 |
|
// Since collapsing selectors may generate new terms, we must send |
1016 |
|
// this out as a lemma if it is of an external type, or otherwise we |
1017 |
|
// may ask for the equality status of terms that only datatypes knows |
1018 |
|
// about, see issue #5344. |
1019 |
143156 |
bool forceLemma = !s.getType().isDatatype(); |
1020 |
143156 |
Trace("datatypes-infer") << "DtInfer : collapse sel"; |
1021 |
143156 |
Trace("datatypes-infer") << " : " << eq << " by " << eq_exp << std::endl; |
1022 |
143156 |
d_im.addPendingInference( |
1023 |
|
eq, InferenceId::DATATYPES_COLLAPSE_SEL, eq_exp, forceLemma); |
1024 |
|
} |
1025 |
|
} |
1026 |
272225 |
} |
1027 |
|
|
1028 |
125255 |
EqualityStatus TheoryDatatypes::getEqualityStatus(TNode a, TNode b){ |
1029 |
125255 |
Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b)); |
1030 |
125255 |
if (d_equalityEngine->areEqual(a, b)) |
1031 |
|
{ |
1032 |
|
// The terms are implied to be equal |
1033 |
4706 |
return EQUALITY_TRUE; |
1034 |
|
} |
1035 |
120549 |
if (d_equalityEngine->areDisequal(a, b, false)) |
1036 |
|
{ |
1037 |
|
// The terms are implied to be dis-equal |
1038 |
|
return EQUALITY_FALSE; |
1039 |
|
} |
1040 |
120549 |
return EQUALITY_FALSE_IN_MODEL; |
1041 |
|
} |
1042 |
|
|
1043 |
74589 |
void TheoryDatatypes::addCarePairs(TNodeTrie* t1, |
1044 |
|
TNodeTrie* t2, |
1045 |
|
unsigned arity, |
1046 |
|
unsigned depth, |
1047 |
|
unsigned& n_pairs) |
1048 |
|
{ |
1049 |
74589 |
if( depth==arity ){ |
1050 |
7104 |
if( t2!=NULL ){ |
1051 |
14208 |
Node f1 = t1->getData(); |
1052 |
14208 |
Node f2 = t2->getData(); |
1053 |
7104 |
if( !areEqual( f1, f2 ) ){ |
1054 |
7104 |
Trace("dt-cg") << "Check " << f1 << " and " << f2 << std::endl; |
1055 |
14208 |
vector< pair<TNode, TNode> > currentPairs; |
1056 |
21514 |
for (unsigned k = 0; k < f1.getNumChildren(); ++ k) { |
1057 |
28820 |
TNode x = f1[k]; |
1058 |
28820 |
TNode y = f2[k]; |
1059 |
14410 |
Assert(d_equalityEngine->hasTerm(x)); |
1060 |
14410 |
Assert(d_equalityEngine->hasTerm(y)); |
1061 |
14410 |
Assert(!areDisequal(x, y)); |
1062 |
14410 |
Assert(!areCareDisequal(x, y)); |
1063 |
14410 |
if (!d_equalityEngine->areEqual(x, y)) |
1064 |
|
{ |
1065 |
8316 |
Trace("dt-cg") << "Arg #" << k << " is " << x << " " << y << std::endl; |
1066 |
24948 |
if (d_equalityEngine->isTriggerTerm(x, THEORY_DATATYPES) |
1067 |
24948 |
&& d_equalityEngine->isTriggerTerm(y, THEORY_DATATYPES)) |
1068 |
|
{ |
1069 |
1696 |
TNode x_shared = d_equalityEngine->getTriggerTermRepresentative( |
1070 |
3392 |
x, THEORY_DATATYPES); |
1071 |
1696 |
TNode y_shared = d_equalityEngine->getTriggerTermRepresentative( |
1072 |
3392 |
y, THEORY_DATATYPES); |
1073 |
1696 |
currentPairs.push_back(make_pair(x_shared, y_shared)); |
1074 |
|
} |
1075 |
|
} |
1076 |
|
} |
1077 |
8800 |
for (unsigned c = 0; c < currentPairs.size(); ++ c) { |
1078 |
1696 |
Trace("dt-cg-pair") << "Pair : " << currentPairs[c].first << " " << currentPairs[c].second << std::endl; |
1079 |
1696 |
addCarePair(currentPairs[c].first, currentPairs[c].second); |
1080 |
1696 |
n_pairs++; |
1081 |
|
} |
1082 |
|
} |
1083 |
|
} |
1084 |
|
}else{ |
1085 |
67485 |
if( t2==NULL ){ |
1086 |
63473 |
if( depth<(arity-1) ){ |
1087 |
|
//add care pairs internal to each child |
1088 |
25277 |
for (std::pair<const TNode, TNodeTrie>& tt : t1->d_data) |
1089 |
|
{ |
1090 |
14418 |
addCarePairs(&tt.second, nullptr, arity, depth + 1, n_pairs); |
1091 |
|
} |
1092 |
|
} |
1093 |
|
//add care pairs based on each pair of non-disequal arguments |
1094 |
162807 |
for (std::map<TNode, TNodeTrie>::iterator it = t1->d_data.begin(); |
1095 |
162807 |
it != t1->d_data.end(); |
1096 |
|
++it) |
1097 |
|
{ |
1098 |
99334 |
std::map<TNode, TNodeTrie>::iterator it2 = it; |
1099 |
99334 |
++it2; |
1100 |
265186 |
for( ; it2 != t1->d_data.end(); ++it2 ){ |
1101 |
82926 |
if (!d_equalityEngine->areDisequal(it->first, it2->first, false)) |
1102 |
|
{ |
1103 |
45488 |
if( !areCareDisequal(it->first, it2->first) ){ |
1104 |
7239 |
addCarePairs( &it->second, &it2->second, arity, depth+1, n_pairs ); |
1105 |
|
} |
1106 |
|
} |
1107 |
|
} |
1108 |
|
} |
1109 |
|
}else{ |
1110 |
|
//add care pairs based on product of indices, non-disequal arguments |
1111 |
10886 |
for (std::pair<const TNode, TNodeTrie>& tt1 : t1->d_data) |
1112 |
|
{ |
1113 |
19284 |
for (std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data) |
1114 |
|
{ |
1115 |
12410 |
if (!d_equalityEngine->areDisequal(tt1.first, tt2.first, false)) |
1116 |
|
{ |
1117 |
11713 |
if (!areCareDisequal(tt1.first, tt2.first)) |
1118 |
|
{ |
1119 |
3877 |
addCarePairs(&tt1.second, &tt2.second, arity, depth + 1, n_pairs); |
1120 |
|
} |
1121 |
|
} |
1122 |
|
} |
1123 |
|
} |
1124 |
|
} |
1125 |
|
} |
1126 |
74589 |
} |
1127 |
|
|
1128 |
11611 |
void TheoryDatatypes::computeCareGraph(){ |
1129 |
11611 |
unsigned n_pairs = 0; |
1130 |
11611 |
Trace("dt-cg-summary") << "Compute graph for dt..." << d_functionTerms.size() << " " << d_sharedTerms.size() << std::endl; |
1131 |
11611 |
Trace("dt-cg") << "Build indices..." << std::endl; |
1132 |
23222 |
std::map<TypeNode, std::map<Node, TNodeTrie> > index; |
1133 |
23222 |
std::map< Node, unsigned > arity; |
1134 |
|
//populate indices |
1135 |
11611 |
unsigned functionTerms = d_functionTerms.size(); |
1136 |
247295 |
for( unsigned i=0; i<functionTerms; i++ ){ |
1137 |
471368 |
TNode f1 = d_functionTerms[i]; |
1138 |
235684 |
Assert(d_equalityEngine->hasTerm(f1)); |
1139 |
235684 |
Trace("dt-cg-debug") << "...build for " << f1 << std::endl; |
1140 |
|
//break into index based on operator, and type of first argument (since some operators are parametric) |
1141 |
471368 |
Node op = f1.getOperator(); |
1142 |
471368 |
TypeNode tn = f1[0].getType(); |
1143 |
471368 |
std::vector< TNode > reps; |
1144 |
235684 |
bool has_trigger_arg = false; |
1145 |
496932 |
for( unsigned j=0; j<f1.getNumChildren(); j++ ){ |
1146 |
261248 |
reps.push_back(d_equalityEngine->getRepresentative(f1[j])); |
1147 |
261248 |
if (d_equalityEngine->isTriggerTerm(f1[j], THEORY_DATATYPES)) |
1148 |
|
{ |
1149 |
222949 |
has_trigger_arg = true; |
1150 |
|
} |
1151 |
|
} |
1152 |
|
//only may contribute to care pairs if has at least one trigger argument |
1153 |
235684 |
if( has_trigger_arg ){ |
1154 |
204790 |
index[tn][op].addTerm( f1, reps ); |
1155 |
204790 |
arity[op] = reps.size(); |
1156 |
|
} |
1157 |
|
} |
1158 |
|
//for each index |
1159 |
27380 |
for (std::pair<const TypeNode, std::map<Node, TNodeTrie> >& tt : index) |
1160 |
|
{ |
1161 |
64824 |
for (std::pair<const Node, TNodeTrie>& t : tt.second) |
1162 |
|
{ |
1163 |
98110 |
Trace("dt-cg") << "Process index " << tt.first << ", " << t.first << "..." |
1164 |
49055 |
<< std::endl; |
1165 |
49055 |
addCarePairs(&t.second, nullptr, arity[t.first], 0, n_pairs); |
1166 |
|
} |
1167 |
|
} |
1168 |
11611 |
Trace("dt-cg-summary") << "...done, # pairs = " << n_pairs << std::endl; |
1169 |
11611 |
} |
1170 |
|
|
1171 |
9717 |
bool TheoryDatatypes::collectModelValues(TheoryModel* m, |
1172 |
|
const std::set<Node>& termSet) |
1173 |
|
{ |
1174 |
19434 |
Trace("dt-cmi") << "Datatypes : Collect model values " |
1175 |
9717 |
<< d_equalityEngine->consistent() << std::endl; |
1176 |
9717 |
Trace("dt-model") << std::endl; |
1177 |
9717 |
printModelDebug( "dt-model" ); |
1178 |
9717 |
Trace("dt-model") << std::endl; |
1179 |
|
|
1180 |
|
//get all constructors |
1181 |
9717 |
eq::EqClassesIterator eqccs_i = eq::EqClassesIterator(d_equalityEngine); |
1182 |
19434 |
std::vector< Node > cons; |
1183 |
19434 |
std::vector< Node > nodes; |
1184 |
19434 |
std::map< Node, Node > eqc_cons; |
1185 |
542673 |
while( !eqccs_i.isFinished() ){ |
1186 |
532956 |
Node eqc = (*eqccs_i); |
1187 |
|
//for all equivalence classes that are datatypes |
1188 |
|
//if( termSet.find( eqc )==termSet.end() ){ |
1189 |
|
// Trace("dt-cmi-debug") << "Irrelevant eqc : " << eqc << std::endl; |
1190 |
|
//} |
1191 |
266478 |
if( eqc.getType().isDatatype() ){ |
1192 |
43671 |
EqcInfo* ei = getOrMakeEqcInfo( eqc ); |
1193 |
43671 |
if( ei && !ei->d_constructor.get().isNull() ){ |
1194 |
70498 |
Node c = ei->d_constructor.get(); |
1195 |
35249 |
cons.push_back( c ); |
1196 |
35249 |
eqc_cons[ eqc ] = c; |
1197 |
|
}else{ |
1198 |
|
//if eqc contains a symbol known to datatypes (a selector), then we must assign |
1199 |
|
//should assign constructors to EQC if they have a selector or a tester |
1200 |
8422 |
bool shouldConsider = ( ei && ei->d_selectors ) || hasTester( eqc ); |
1201 |
8422 |
if( shouldConsider ){ |
1202 |
3 |
nodes.push_back( eqc ); |
1203 |
|
} |
1204 |
|
} |
1205 |
|
} |
1206 |
|
//} |
1207 |
266478 |
++eqccs_i; |
1208 |
|
} |
1209 |
|
|
1210 |
|
//unsigned orig_size = nodes.size(); |
1211 |
19434 |
std::map< TypeNode, int > typ_enum_map; |
1212 |
19434 |
std::vector< TypeEnumerator > typ_enum; |
1213 |
9717 |
unsigned index = 0; |
1214 |
9723 |
while( index<nodes.size() ){ |
1215 |
6 |
Node eqc = nodes[index]; |
1216 |
6 |
Node neqc; |
1217 |
3 |
bool addCons = false; |
1218 |
6 |
TypeNode tt = eqc.getType(); |
1219 |
3 |
const DType& dt = tt.getDType(); |
1220 |
3 |
if (!d_equalityEngine->hasTerm(eqc)) |
1221 |
|
{ |
1222 |
|
Assert(false); |
1223 |
|
}else{ |
1224 |
3 |
Trace("dt-cmi") << "NOTICE : Datatypes: no constructor in equivalence class " << eqc << std::endl; |
1225 |
3 |
Trace("dt-cmi") << " Type : " << eqc.getType() << std::endl; |
1226 |
3 |
EqcInfo* ei = getOrMakeEqcInfo( eqc ); |
1227 |
6 |
std::vector< bool > pcons; |
1228 |
3 |
getPossibleCons( ei, eqc, pcons ); |
1229 |
3 |
Trace("dt-cmi") << "Possible constructors : "; |
1230 |
18 |
for( unsigned i=0; i<pcons.size(); i++ ){ |
1231 |
15 |
Trace("dt-cmi") << pcons[i] << " "; |
1232 |
|
} |
1233 |
3 |
Trace("dt-cmi") << std::endl; |
1234 |
9 |
for( unsigned r=0; r<2; r++ ){ |
1235 |
6 |
if( neqc.isNull() ){ |
1236 |
7 |
for( unsigned i=0; i<pcons.size(); i++ ){ |
1237 |
|
// must try the infinite ones first |
1238 |
|
bool cfinite = |
1239 |
7 |
d_state.isFiniteType(dt[i].getSpecializedConstructorType(tt)); |
1240 |
7 |
if( pcons[i] && (r==1)==cfinite ){ |
1241 |
3 |
neqc = utils::getInstCons(eqc, dt, i); |
1242 |
3 |
break; |
1243 |
|
} |
1244 |
|
} |
1245 |
|
} |
1246 |
|
} |
1247 |
3 |
addCons = true; |
1248 |
|
} |
1249 |
3 |
if( !neqc.isNull() ){ |
1250 |
3 |
Trace("dt-cmi") << "Assign : " << neqc << std::endl; |
1251 |
3 |
if (!m->assertEquality(eqc, neqc, true)) |
1252 |
|
{ |
1253 |
|
return false; |
1254 |
|
} |
1255 |
3 |
eqc_cons[ eqc ] = neqc; |
1256 |
|
} |
1257 |
3 |
if( addCons ){ |
1258 |
3 |
cons.push_back( neqc ); |
1259 |
|
} |
1260 |
3 |
++index; |
1261 |
|
} |
1262 |
|
|
1263 |
44985 |
for( std::map< Node, Node >::iterator it = eqc_cons.begin(); it != eqc_cons.end(); ++it ){ |
1264 |
70536 |
Node eqc = it->first; |
1265 |
35268 |
if( eqc.getType().isCodatatype() ){ |
1266 |
|
//until models are implemented for codatatypes |
1267 |
|
//throw Exception("Models for codatatypes are not supported in this version."); |
1268 |
|
//must proactive expand to avoid looping behavior in model builder |
1269 |
67 |
if( !it->second.isNull() ){ |
1270 |
108 |
std::map< Node, int > vmap; |
1271 |
108 |
Node v = getCodatatypesValue( it->first, eqc_cons, vmap, 0 ); |
1272 |
54 |
Trace("dt-cmi") << " EQC(" << it->first << "), constructor is " << it->second << ", value is " << v << ", const = " << v.isConst() << std::endl; |
1273 |
54 |
if (!m->assertEquality(eqc, v, true)) |
1274 |
|
{ |
1275 |
|
return false; |
1276 |
|
} |
1277 |
54 |
m->assertSkeleton(v); |
1278 |
|
} |
1279 |
|
}else{ |
1280 |
35201 |
Trace("dt-cmi") << "Datatypes : assert representative " << it->second << " for " << it->first << std::endl; |
1281 |
35201 |
m->assertSkeleton(it->second); |
1282 |
|
} |
1283 |
|
} |
1284 |
9717 |
return true; |
1285 |
|
} |
1286 |
|
|
1287 |
|
|
1288 |
179 |
Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_cons, std::map< Node, int >& vmap, int depth ){ |
1289 |
179 |
std::map< Node, int >::iterator itv = vmap.find( n ); |
1290 |
179 |
if( itv!=vmap.end() ){ |
1291 |
6 |
int debruijn = depth - 1 - itv->second; |
1292 |
|
return NodeManager::currentNM()->mkConst( |
1293 |
6 |
UninterpretedConstant(n.getType(), debruijn)); |
1294 |
173 |
}else if( n.getType().isDatatype() ){ |
1295 |
155 |
Node nc = eqc_cons[n]; |
1296 |
125 |
if( !nc.isNull() ){ |
1297 |
95 |
vmap[n] = depth; |
1298 |
95 |
Trace("dt-cmi-cdt-debug") << " map " << n << " -> " << depth << std::endl; |
1299 |
95 |
Assert(nc.getKind() == APPLY_CONSTRUCTOR); |
1300 |
190 |
std::vector< Node > children; |
1301 |
95 |
children.push_back( nc.getOperator() ); |
1302 |
220 |
for( unsigned i=0; i<nc.getNumChildren(); i++ ){ |
1303 |
250 |
Node r = getRepresentative( nc[i] ); |
1304 |
250 |
Node rv = getCodatatypesValue( r, eqc_cons, vmap, depth+1 ); |
1305 |
125 |
children.push_back( rv ); |
1306 |
|
} |
1307 |
95 |
vmap.erase( n ); |
1308 |
95 |
return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); |
1309 |
|
} |
1310 |
|
} |
1311 |
78 |
return n; |
1312 |
|
} |
1313 |
|
|
1314 |
|
Node TheoryDatatypes::getSingletonLemma( TypeNode tn, bool pol ) { |
1315 |
|
NodeManager* nm = NodeManager::currentNM(); |
1316 |
|
SkolemManager* sm = nm->getSkolemManager(); |
1317 |
|
int index = pol ? 0 : 1; |
1318 |
|
std::map< TypeNode, Node >::iterator it = d_singleton_lemma[index].find( tn ); |
1319 |
|
if( it==d_singleton_lemma[index].end() ){ |
1320 |
|
Node a; |
1321 |
|
if( pol ){ |
1322 |
|
Node v1 = nm->mkBoundVar(tn); |
1323 |
|
Node v2 = nm->mkBoundVar(tn); |
1324 |
|
a = nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, v1, v2), v1.eqNode(v2)); |
1325 |
|
}else{ |
1326 |
|
Node v1 = sm->mkDummySkolem("k1", tn); |
1327 |
|
Node v2 = sm->mkDummySkolem("k2", tn); |
1328 |
|
a = v1.eqNode( v2 ).negate(); |
1329 |
|
//send out immediately as lemma |
1330 |
|
d_im.lemma(a, InferenceId::DATATYPES_REC_SINGLETON_FORCE_DEQ); |
1331 |
|
Trace("dt-singleton") << "******** assert " << a << " to avoid singleton cardinality for type " << tn << std::endl; |
1332 |
|
} |
1333 |
|
d_singleton_lemma[index][tn] = a; |
1334 |
|
return a; |
1335 |
|
}else{ |
1336 |
|
return it->second; |
1337 |
|
} |
1338 |
|
} |
1339 |
|
|
1340 |
305199 |
void TheoryDatatypes::collectTerms( Node n ) { |
1341 |
305199 |
if (d_collectTermsCache.find(n) != d_collectTermsCache.end()) |
1342 |
|
{ |
1343 |
|
// already processed |
1344 |
46081 |
return; |
1345 |
|
} |
1346 |
259118 |
d_collectTermsCache[n] = true; |
1347 |
259118 |
Kind nk = n.getKind(); |
1348 |
259118 |
if (nk == APPLY_CONSTRUCTOR) |
1349 |
|
{ |
1350 |
94600 |
Debug("datatypes") << " Found constructor " << n << endl; |
1351 |
94600 |
if (n.getNumChildren() > 0) |
1352 |
|
{ |
1353 |
68712 |
d_functionTerms.push_back(n); |
1354 |
|
} |
1355 |
94600 |
return; |
1356 |
|
} |
1357 |
164518 |
if (nk == APPLY_SELECTOR_TOTAL || nk == DT_SIZE || nk == DT_HEIGHT_BOUND) |
1358 |
|
{ |
1359 |
24415 |
d_functionTerms.push_back(n); |
1360 |
|
// we must also record which selectors exist |
1361 |
24415 |
Trace("dt-collapse-sel") << " Found selector " << n << endl; |
1362 |
48830 |
Node rep = getRepresentative(n[0]); |
1363 |
|
// record it in the selectors |
1364 |
24415 |
EqcInfo* eqc = getOrMakeEqcInfo(rep, true); |
1365 |
|
// add it to the eqc info |
1366 |
24415 |
addSelector(n, eqc, rep); |
1367 |
|
} |
1368 |
|
|
1369 |
|
// now, do user-context-dependent lemmas |
1370 |
164518 |
if (nk != DT_SIZE && nk != DT_HEIGHT_BOUND) |
1371 |
|
{ |
1372 |
|
// if not one of these kinds, there are no lemmas |
1373 |
159217 |
return; |
1374 |
|
} |
1375 |
5301 |
if (d_collectTermsCacheU.find(n) != d_collectTermsCacheU.end()) |
1376 |
|
{ |
1377 |
2563 |
return; |
1378 |
|
} |
1379 |
2738 |
d_collectTermsCacheU[n] = true; |
1380 |
|
|
1381 |
2738 |
NodeManager* nm = NodeManager::currentNM(); |
1382 |
|
|
1383 |
2738 |
if (nk == DT_SIZE) |
1384 |
|
{ |
1385 |
5476 |
Node lem = nm->mkNode(LEQ, d_zero, n); |
1386 |
5476 |
Trace("datatypes-infer") |
1387 |
2738 |
<< "DtInfer : size geq zero : " << lem << std::endl; |
1388 |
2738 |
d_im.addPendingLemma(lem, InferenceId::DATATYPES_SIZE_POS); |
1389 |
|
} |
1390 |
|
else if (nk == DT_HEIGHT_BOUND && n[1].getConst<Rational>().isZero()) |
1391 |
|
{ |
1392 |
|
std::vector<Node> children; |
1393 |
|
const DType& dt = n[0].getType().getDType(); |
1394 |
|
for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) |
1395 |
|
{ |
1396 |
|
if (utils::isNullaryConstructor(dt[i])) |
1397 |
|
{ |
1398 |
|
Node test = utils::mkTester(n[0], i, dt); |
1399 |
|
children.push_back(test); |
1400 |
|
} |
1401 |
|
} |
1402 |
|
Node lem; |
1403 |
|
if (children.empty()) |
1404 |
|
{ |
1405 |
|
lem = n.negate(); |
1406 |
|
} |
1407 |
|
else |
1408 |
|
{ |
1409 |
|
lem = n.eqNode(children.size() == 1 ? children[0] |
1410 |
|
: nm->mkNode(OR, children)); |
1411 |
|
} |
1412 |
|
Trace("datatypes-infer") << "DtInfer : zero height : " << lem << std::endl; |
1413 |
|
d_im.addPendingLemma(lem, InferenceId::DATATYPES_HEIGHT_ZERO); |
1414 |
|
} |
1415 |
|
} |
1416 |
|
|
1417 |
129181 |
Node TheoryDatatypes::getInstantiateCons(Node n, const DType& dt, int index) |
1418 |
|
{ |
1419 |
129181 |
if( n.getKind()==APPLY_CONSTRUCTOR && n.getNumChildren()==0 ){ |
1420 |
10991 |
return n; |
1421 |
|
} |
1422 |
|
//add constructor to equivalence class |
1423 |
236380 |
Node k = getTermSkolemFor( n ); |
1424 |
236380 |
Node n_ic = utils::getInstCons(k, dt, index); |
1425 |
118190 |
n_ic = Rewriter::rewrite( n_ic ); |
1426 |
|
// it may be a new term, so we collect terms and add it to the equality engine |
1427 |
118190 |
collectTerms( n_ic ); |
1428 |
118190 |
d_equalityEngine->addTerm(n_ic); |
1429 |
118190 |
Debug("dt-enum") << "Made instantiate cons " << n_ic << std::endl; |
1430 |
118190 |
return n_ic; |
1431 |
|
} |
1432 |
|
|
1433 |
195860 |
bool TheoryDatatypes::instantiate(EqcInfo* eqc, Node n) |
1434 |
|
{ |
1435 |
195860 |
Trace("datatypes-debug") << "Instantiate: " << n << std::endl; |
1436 |
|
//add constructor to equivalence class if not done so already |
1437 |
195860 |
int index = getLabelIndex( eqc, n ); |
1438 |
195860 |
if (index == -1 || eqc->d_inst) |
1439 |
|
{ |
1440 |
66679 |
return false; |
1441 |
|
} |
1442 |
258362 |
Node exp; |
1443 |
258362 |
Node tt; |
1444 |
129181 |
if (!eqc->d_constructor.get().isNull()) |
1445 |
|
{ |
1446 |
22146 |
exp = d_true; |
1447 |
22146 |
tt = eqc->d_constructor; |
1448 |
|
} |
1449 |
|
else |
1450 |
|
{ |
1451 |
107035 |
exp = getLabel(n); |
1452 |
107035 |
tt = exp[0]; |
1453 |
|
} |
1454 |
258362 |
TypeNode ttn = tt.getType(); |
1455 |
129181 |
const DType& dt = ttn.getDType(); |
1456 |
|
// instantiate this equivalence class |
1457 |
129181 |
eqc->d_inst = true; |
1458 |
258362 |
Node tt_cons = getInstantiateCons(tt, dt, index); |
1459 |
258362 |
Node eq; |
1460 |
129181 |
if (tt == tt_cons) |
1461 |
|
{ |
1462 |
|
// not necessary |
1463 |
10991 |
return false; |
1464 |
|
} |
1465 |
118190 |
eq = tt.eqNode(tt_cons); |
1466 |
|
// Determine if the equality must be sent out as a lemma. Notice that |
1467 |
|
// we keep new equalities from the instantiate rule internal |
1468 |
|
// as long as they are for datatype constructors that have no arguments that |
1469 |
|
// have finite external type, which corresponds to: |
1470 |
|
// forceLemma = dt[index].hasFiniteExternalArgType(ttn); |
1471 |
|
// Such equalities must be sent because they introduce selector terms that |
1472 |
|
// may contribute to conflicts due to cardinality (good examples of this are |
1473 |
|
// regress0/datatypes/dt-param-card4-bool-sat.smt2 and |
1474 |
|
// regress0/datatypes/list-bool.smt2). |
1475 |
|
bool forceLemma; |
1476 |
118190 |
if (options::dtPoliteOptimize()) |
1477 |
|
{ |
1478 |
118190 |
forceLemma = dt[index].hasFiniteExternalArgType(ttn); |
1479 |
|
} |
1480 |
|
else |
1481 |
|
{ |
1482 |
|
forceLemma = dt.involvesExternalType(); |
1483 |
|
} |
1484 |
236380 |
Trace("datatypes-infer-debug") << "DtInstantiate : " << eqc << " " << eq |
1485 |
118190 |
<< " forceLemma = " << forceLemma << std::endl; |
1486 |
236380 |
Trace("datatypes-infer") << "DtInfer : instantiate : " << eq << " by " << exp |
1487 |
118190 |
<< std::endl; |
1488 |
118190 |
d_im.addPendingInference(eq, InferenceId::DATATYPES_INST, exp, forceLemma); |
1489 |
118190 |
return true; |
1490 |
|
} |
1491 |
|
|
1492 |
28325 |
void TheoryDatatypes::checkCycles() { |
1493 |
28325 |
Trace("datatypes-cycle-check") << "Check acyclicity" << std::endl; |
1494 |
56513 |
std::vector< Node > cdt_eqc; |
1495 |
28325 |
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine); |
1496 |
985469 |
while( !eqcs_i.isFinished() ){ |
1497 |
957281 |
Node eqc = (*eqcs_i); |
1498 |
957281 |
TypeNode tn = eqc.getType(); |
1499 |
478709 |
if( tn.isDatatype() ) { |
1500 |
141785 |
if( !tn.isCodatatype() ){ |
1501 |
140647 |
if( options::dtCyclic() ){ |
1502 |
|
//do cycle checks |
1503 |
281157 |
std::map< TNode, bool > visited; |
1504 |
281157 |
std::map< TNode, bool > proc; |
1505 |
281157 |
std::vector<Node> expl; |
1506 |
140647 |
Trace("datatypes-cycle-check") << "...search for cycle starting at " << eqc << std::endl; |
1507 |
281157 |
Node cn = searchForCycle( eqc, eqc, visited, proc, expl ); |
1508 |
140647 |
Trace("datatypes-cycle-check") << "...finish." << std::endl; |
1509 |
|
//if we discovered a different cycle while searching this one |
1510 |
140647 |
if( !cn.isNull() && cn!=eqc ){ |
1511 |
19 |
visited.clear(); |
1512 |
19 |
proc.clear(); |
1513 |
19 |
expl.clear(); |
1514 |
38 |
Node prev = cn; |
1515 |
19 |
cn = searchForCycle( cn, cn, visited, proc, expl ); |
1516 |
19 |
Assert(prev == cn); |
1517 |
|
} |
1518 |
|
|
1519 |
140647 |
if( !cn.isNull() ) { |
1520 |
137 |
Assert(expl.size() > 0); |
1521 |
274 |
Trace("dt-conflict") |
1522 |
137 |
<< "CONFLICT: Cycle conflict : " << expl << std::endl; |
1523 |
137 |
d_im.sendDtConflict(expl, InferenceId::DATATYPES_CYCLE); |
1524 |
137 |
return; |
1525 |
|
} |
1526 |
|
} |
1527 |
|
}else{ |
1528 |
|
//indexing |
1529 |
1138 |
cdt_eqc.push_back( eqc ); |
1530 |
|
} |
1531 |
|
} |
1532 |
478572 |
++eqcs_i; |
1533 |
|
} |
1534 |
28188 |
Trace("datatypes-cycle-check") << "Check uniqueness" << std::endl; |
1535 |
|
//process codatatypes |
1536 |
28188 |
if( cdt_eqc.size()>1 && options::cdtBisimilar() ){ |
1537 |
87 |
printModelDebug("dt-cdt-debug"); |
1538 |
87 |
Trace("dt-cdt-debug") << "Process " << cdt_eqc.size() << " co-datatypes" << std::endl; |
1539 |
174 |
std::vector< std::vector< Node > > part_out; |
1540 |
174 |
std::vector<Node> exp; |
1541 |
174 |
std::map< Node, Node > cn; |
1542 |
174 |
std::map< Node, std::map< Node, int > > dni; |
1543 |
1221 |
for( unsigned i=0; i<cdt_eqc.size(); i++ ){ |
1544 |
1134 |
cn[cdt_eqc[i]] = cdt_eqc[i]; |
1545 |
|
} |
1546 |
87 |
separateBisimilar( cdt_eqc, part_out, exp, cn, dni, 0, false ); |
1547 |
87 |
Trace("dt-cdt-debug") << "Done separate bisimilar." << std::endl; |
1548 |
87 |
if( !part_out.empty() ){ |
1549 |
10 |
Trace("dt-cdt-debug") << "Process partition size " << part_out.size() << std::endl; |
1550 |
20 |
for( unsigned i=0; i<part_out.size(); i++ ){ |
1551 |
20 |
std::vector< Node > part; |
1552 |
10 |
part.push_back( part_out[i][0] ); |
1553 |
20 |
for( unsigned j=1; j<part_out[i].size(); j++ ){ |
1554 |
10 |
Trace("dt-cdt") << "Codatatypes : " << part_out[i][0] << " and " << part_out[i][j] << " must be equal!!" << std::endl; |
1555 |
10 |
part.push_back( part_out[i][j] ); |
1556 |
20 |
std::vector< std::vector< Node > > tpart_out; |
1557 |
10 |
exp.clear(); |
1558 |
10 |
cn.clear(); |
1559 |
10 |
cn[part_out[i][0]] = part_out[i][0]; |
1560 |
10 |
cn[part_out[i][j]] = part_out[i][j]; |
1561 |
10 |
dni.clear(); |
1562 |
10 |
separateBisimilar( part, tpart_out, exp, cn, dni, 0, true ); |
1563 |
10 |
Assert(tpart_out.size() == 1 && tpart_out[0].size() == 2); |
1564 |
10 |
part.pop_back(); |
1565 |
|
//merge based on explanation |
1566 |
10 |
Trace("dt-cdt") << " exp is : "; |
1567 |
38 |
for( unsigned k=0; k<exp.size(); k++ ){ |
1568 |
28 |
Trace("dt-cdt") << exp[k] << " "; |
1569 |
|
} |
1570 |
10 |
Trace("dt-cdt") << std::endl; |
1571 |
20 |
Node eq = part_out[i][0].eqNode( part_out[i][j] ); |
1572 |
20 |
Node eqExp = NodeManager::currentNM()->mkAnd(exp); |
1573 |
10 |
d_im.addPendingInference(eq, InferenceId::DATATYPES_BISIMILAR, eqExp); |
1574 |
10 |
Trace("datatypes-infer") << "DtInfer : cdt-bisimilar : " << eq << " by " << eqExp << std::endl; |
1575 |
|
} |
1576 |
|
} |
1577 |
|
} |
1578 |
|
} |
1579 |
|
} |
1580 |
|
|
1581 |
|
//everything is in terms of representatives |
1582 |
269 |
void TheoryDatatypes::separateBisimilar( |
1583 |
|
std::vector<Node>& part, |
1584 |
|
std::vector<std::vector<Node> >& part_out, |
1585 |
|
std::vector<Node>& exp, |
1586 |
|
std::map<Node, Node>& cn, |
1587 |
|
std::map<Node, std::map<Node, int> >& dni, |
1588 |
|
int dniLvl, |
1589 |
|
bool mkExp) |
1590 |
|
{ |
1591 |
269 |
if( !mkExp ){ |
1592 |
231 |
Trace("dt-cdt-debug") << "Separate bisimilar : " << std::endl; |
1593 |
1776 |
for( unsigned i=0; i<part.size(); i++ ){ |
1594 |
1545 |
Trace("dt-cdt-debug") << " " << part[i] << ", current = " << cn[part[i]] << std::endl; |
1595 |
|
} |
1596 |
|
} |
1597 |
269 |
Assert(part.size() > 1); |
1598 |
538 |
std::map< Node, std::vector< Node > > new_part; |
1599 |
538 |
std::map< Node, std::vector< Node > > new_part_c; |
1600 |
538 |
std::map< int, std::vector< Node > > new_part_rec; |
1601 |
|
|
1602 |
538 |
std::map< Node, Node > cn_cons; |
1603 |
1890 |
for( unsigned j=0; j<part.size(); j++ ){ |
1604 |
3242 |
Node c = cn[part[j]]; |
1605 |
1621 |
std::map< Node, int >::iterator it_rec = dni[part[j]].find( c ); |
1606 |
1621 |
if( it_rec!=dni[part[j]].end() ){ |
1607 |
|
//looped |
1608 |
46 |
if( !mkExp ){ Trace("dt-cdt-debug") << " - " << part[j] << " is looping at index " << it_rec->second << std::endl; } |
1609 |
46 |
new_part_rec[ it_rec->second ].push_back( part[j] ); |
1610 |
|
}else{ |
1611 |
1575 |
if( c.getType().isDatatype() ){ |
1612 |
2620 |
Node ncons = getEqcConstructor( c ); |
1613 |
1310 |
if( ncons.getKind()==APPLY_CONSTRUCTOR ) { |
1614 |
816 |
Node cc = ncons.getOperator(); |
1615 |
408 |
cn_cons[part[j]] = ncons; |
1616 |
408 |
if (mkExp && c != ncons) |
1617 |
|
{ |
1618 |
20 |
exp.push_back(c.eqNode(ncons)); |
1619 |
|
} |
1620 |
408 |
new_part[cc].push_back( part[j] ); |
1621 |
408 |
if( !mkExp ){ Trace("dt-cdt-debug") << " - " << part[j] << " is datatype " << ncons << "." << std::endl; } |
1622 |
|
}else{ |
1623 |
902 |
new_part_c[c].push_back( part[j] ); |
1624 |
902 |
if( !mkExp ){ Trace("dt-cdt-debug") << " - " << part[j] << " is unspecified datatype." << std::endl; } |
1625 |
|
} |
1626 |
|
}else{ |
1627 |
|
//add equivalences |
1628 |
265 |
if( !mkExp ){ Trace("dt-cdt-debug") << " - " << part[j] << " is term " << c << "." << std::endl; } |
1629 |
265 |
new_part_c[c].push_back( part[j] ); |
1630 |
|
} |
1631 |
|
} |
1632 |
|
} |
1633 |
|
//direct add for constants |
1634 |
1334 |
for( std::map< Node, std::vector< Node > >::iterator it = new_part_c.begin(); it != new_part_c.end(); ++it ){ |
1635 |
1065 |
if( it->second.size()>1 ){ |
1636 |
180 |
std::vector< Node > vec; |
1637 |
90 |
vec.insert( vec.begin(), it->second.begin(), it->second.end() ); |
1638 |
90 |
part_out.push_back( vec ); |
1639 |
|
} |
1640 |
|
} |
1641 |
|
//direct add for recursive |
1642 |
295 |
for( std::map< int, std::vector< Node > >::iterator it = new_part_rec.begin(); it != new_part_rec.end(); ++it ){ |
1643 |
26 |
if( it->second.size()>1 ){ |
1644 |
40 |
std::vector< Node > vec; |
1645 |
20 |
vec.insert( vec.begin(), it->second.begin(), it->second.end() ); |
1646 |
20 |
part_out.push_back( vec ); |
1647 |
|
}else{ |
1648 |
|
//add back : could match a datatype? |
1649 |
|
} |
1650 |
|
} |
1651 |
|
//recurse for the datatypes |
1652 |
484 |
for( std::map< Node, std::vector< Node > >::iterator it = new_part.begin(); it != new_part.end(); ++it ){ |
1653 |
215 |
if( it->second.size()>1 ){ |
1654 |
|
//set dni to check for loops |
1655 |
164 |
std::map< Node, Node > dni_rem; |
1656 |
357 |
for( unsigned i=0; i<it->second.size(); i++ ){ |
1657 |
550 |
Node n = it->second[i]; |
1658 |
275 |
dni[n][cn[n]] = dniLvl; |
1659 |
275 |
dni_rem[n] = cn[n]; |
1660 |
|
} |
1661 |
|
|
1662 |
|
//we will split based on the arguments of the datatype |
1663 |
164 |
std::vector< std::vector< Node > > split_new_part; |
1664 |
82 |
split_new_part.push_back( it->second ); |
1665 |
|
|
1666 |
82 |
unsigned nChildren = cn_cons[it->second[0]].getNumChildren(); |
1667 |
|
//for each child of constructor |
1668 |
82 |
unsigned cindex = 0; |
1669 |
390 |
while( cindex<nChildren && !split_new_part.empty() ){ |
1670 |
154 |
if( !mkExp ){ Trace("dt-cdt-debug") << "Split argument #" << cindex << " of " << it->first << "..." << std::endl; } |
1671 |
308 |
std::vector< std::vector< Node > > next_split_new_part; |
1672 |
326 |
for( unsigned j=0; j<split_new_part.size(); j++ ){ |
1673 |
|
//set current node |
1674 |
639 |
for( unsigned k=0; k<split_new_part[j].size(); k++ ){ |
1675 |
934 |
Node n = split_new_part[j][k]; |
1676 |
934 |
Node cnc = cn_cons[n][cindex]; |
1677 |
934 |
Node nr = getRepresentative(cnc); |
1678 |
467 |
cn[n] = nr; |
1679 |
467 |
if (mkExp && cnc != nr) |
1680 |
|
{ |
1681 |
8 |
exp.push_back(nr.eqNode(cnc)); |
1682 |
|
} |
1683 |
|
} |
1684 |
344 |
std::vector< std::vector< Node > > c_part_out; |
1685 |
172 |
separateBisimilar( split_new_part[j], c_part_out, exp, cn, dni, dniLvl+1, mkExp ); |
1686 |
172 |
next_split_new_part.insert( next_split_new_part.end(), c_part_out.begin(), c_part_out.end() ); |
1687 |
|
} |
1688 |
154 |
split_new_part.clear(); |
1689 |
154 |
split_new_part.insert( split_new_part.end(), next_split_new_part.begin(), next_split_new_part.end() ); |
1690 |
154 |
cindex++; |
1691 |
|
} |
1692 |
82 |
part_out.insert( part_out.end(), split_new_part.begin(), split_new_part.end() ); |
1693 |
|
|
1694 |
357 |
for( std::map< Node, Node >::iterator it2 = dni_rem.begin(); it2 != dni_rem.end(); ++it2 ){ |
1695 |
275 |
dni[it2->first].erase( it2->second ); |
1696 |
|
} |
1697 |
|
} |
1698 |
|
} |
1699 |
269 |
} |
1700 |
|
|
1701 |
|
//postcondition: if cycle detected, explanation is why n is a subterm of on |
1702 |
647375 |
Node TheoryDatatypes::searchForCycle(TNode n, |
1703 |
|
TNode on, |
1704 |
|
std::map<TNode, bool>& visited, |
1705 |
|
std::map<TNode, bool>& proc, |
1706 |
|
std::vector<Node>& explanation, |
1707 |
|
bool firstTime) |
1708 |
|
{ |
1709 |
647375 |
Trace("datatypes-cycle-check2") << "Search for cycle " << n << " " << on << endl; |
1710 |
1294750 |
TNode ncons; |
1711 |
1294750 |
TNode nn; |
1712 |
647375 |
if( !firstTime ){ |
1713 |
506709 |
nn = getRepresentative( n ); |
1714 |
506709 |
if( nn==on ){ |
1715 |
137 |
if (n != nn) |
1716 |
|
{ |
1717 |
98 |
explanation.push_back(n.eqNode(nn)); |
1718 |
|
} |
1719 |
137 |
return on; |
1720 |
|
} |
1721 |
|
}else{ |
1722 |
140666 |
nn = getRepresentative( n ); |
1723 |
|
} |
1724 |
647238 |
if( proc.find( nn )!=proc.end() ){ |
1725 |
137593 |
return Node::null(); |
1726 |
|
} |
1727 |
509645 |
Trace("datatypes-cycle-check2") << "...representative : " << nn << " " << ( visited.find( nn ) == visited.end() ) << " " << visited.size() << std::endl; |
1728 |
509645 |
if( visited.find( nn ) == visited.end() ) { |
1729 |
509626 |
Trace("datatypes-cycle-check2") << " visit : " << nn << std::endl; |
1730 |
509626 |
visited[nn] = true; |
1731 |
1019252 |
TNode nncons = getEqcConstructor(nn); |
1732 |
509626 |
if (nncons.getKind() == APPLY_CONSTRUCTOR) |
1733 |
|
{ |
1734 |
897696 |
for (unsigned i = 0; i < nncons.getNumChildren(); i++) |
1735 |
|
{ |
1736 |
|
TNode cn = |
1737 |
1012457 |
searchForCycle(nncons[i], on, visited, proc, explanation, false); |
1738 |
506709 |
if( cn==on ) { |
1739 |
|
//add explanation for why the constructor is connected |
1740 |
850 |
if (n != nncons) |
1741 |
|
{ |
1742 |
465 |
explanation.push_back(n.eqNode(nncons)); |
1743 |
|
} |
1744 |
850 |
return on; |
1745 |
505859 |
}else if( !cn.isNull() ){ |
1746 |
111 |
return cn; |
1747 |
|
} |
1748 |
|
} |
1749 |
|
} |
1750 |
508665 |
Trace("datatypes-cycle-check2") << " unvisit : " << nn << std::endl; |
1751 |
508665 |
proc[nn] = true; |
1752 |
508665 |
visited.erase( nn ); |
1753 |
508665 |
return Node::null(); |
1754 |
|
}else{ |
1755 |
38 |
TypeNode tn = nn.getType(); |
1756 |
19 |
if( tn.isDatatype() ) { |
1757 |
19 |
if( !tn.isCodatatype() ){ |
1758 |
19 |
return nn; |
1759 |
|
} |
1760 |
|
} |
1761 |
|
return Node::null(); |
1762 |
|
} |
1763 |
|
} |
1764 |
|
|
1765 |
3416500 |
bool TheoryDatatypes::hasTerm(TNode a) { return d_equalityEngine->hasTerm(a); } |
1766 |
|
|
1767 |
761998 |
bool TheoryDatatypes::areEqual( TNode a, TNode b ){ |
1768 |
761998 |
if( a==b ){ |
1769 |
9472 |
return true; |
1770 |
752526 |
}else if( hasTerm( a ) && hasTerm( b ) ){ |
1771 |
752526 |
return d_equalityEngine->areEqual(a, b); |
1772 |
|
}else{ |
1773 |
|
return false; |
1774 |
|
} |
1775 |
|
} |
1776 |
|
|
1777 |
14410 |
bool TheoryDatatypes::areDisequal( TNode a, TNode b ){ |
1778 |
14410 |
if( a==b ){ |
1779 |
4484 |
return false; |
1780 |
9926 |
}else if( hasTerm( a ) && hasTerm( b ) ){ |
1781 |
9926 |
return d_equalityEngine->areDisequal(a, b, false); |
1782 |
|
}else{ |
1783 |
|
//TODO : constants here? |
1784 |
|
return false; |
1785 |
|
} |
1786 |
|
} |
1787 |
|
|
1788 |
71611 |
bool TheoryDatatypes::areCareDisequal( TNode x, TNode y ) { |
1789 |
71611 |
Trace("datatypes-cg") << "areCareDisequal: " << x << " " << y << std::endl; |
1790 |
71611 |
Assert(d_equalityEngine->hasTerm(x)); |
1791 |
71611 |
Assert(d_equalityEngine->hasTerm(y)); |
1792 |
214833 |
if (d_equalityEngine->isTriggerTerm(x, THEORY_DATATYPES) |
1793 |
214833 |
&& d_equalityEngine->isTriggerTerm(y, THEORY_DATATYPES)) |
1794 |
|
{ |
1795 |
|
TNode x_shared = |
1796 |
69327 |
d_equalityEngine->getTriggerTermRepresentative(x, THEORY_DATATYPES); |
1797 |
|
TNode y_shared = |
1798 |
69327 |
d_equalityEngine->getTriggerTermRepresentative(y, THEORY_DATATYPES); |
1799 |
57706 |
EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared); |
1800 |
57706 |
if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){ |
1801 |
46085 |
return true; |
1802 |
|
} |
1803 |
|
} |
1804 |
25526 |
return false; |
1805 |
|
} |
1806 |
|
|
1807 |
1891596 |
TNode TheoryDatatypes::getRepresentative( TNode a ){ |
1808 |
1891596 |
if( hasTerm( a ) ){ |
1809 |
1891579 |
return d_equalityEngine->getRepresentative(a); |
1810 |
|
}else{ |
1811 |
17 |
return a; |
1812 |
|
} |
1813 |
|
} |
1814 |
|
|
1815 |
37170 |
void TheoryDatatypes::printModelDebug( const char* c ){ |
1816 |
37170 |
if(! (Trace.isOn(c))) { |
1817 |
37170 |
return; |
1818 |
|
} |
1819 |
|
|
1820 |
|
Trace( c ) << "Datatypes model : " << std::endl; |
1821 |
|
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine); |
1822 |
|
while( !eqcs_i.isFinished() ){ |
1823 |
|
Node eqc = (*eqcs_i); |
1824 |
|
//if( !eqc.getType().isBoolean() ){ |
1825 |
|
if( eqc.getType().isDatatype() ){ |
1826 |
|
Trace( c ) << "DATATYPE : "; |
1827 |
|
} |
1828 |
|
Trace( c ) << eqc << " : " << eqc.getType() << " : " << std::endl; |
1829 |
|
Trace( c ) << " { "; |
1830 |
|
//add terms to model |
1831 |
|
eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, d_equalityEngine); |
1832 |
|
while( !eqc_i.isFinished() ){ |
1833 |
|
if( (*eqc_i)!=eqc ){ |
1834 |
|
Trace( c ) << (*eqc_i) << " "; |
1835 |
|
} |
1836 |
|
++eqc_i; |
1837 |
|
} |
1838 |
|
Trace( c ) << "}" << std::endl; |
1839 |
|
if( eqc.getType().isDatatype() ){ |
1840 |
|
EqcInfo* ei = getOrMakeEqcInfo( eqc ); |
1841 |
|
if( ei ){ |
1842 |
|
Trace( c ) << " Instantiated : " << ei->d_inst.get() << std::endl; |
1843 |
|
Trace( c ) << " Constructor : "; |
1844 |
|
if( !ei->d_constructor.get().isNull() ){ |
1845 |
|
Trace( c )<< ei->d_constructor.get(); |
1846 |
|
} |
1847 |
|
Trace( c ) << std::endl << " Labels : "; |
1848 |
|
if( hasLabel( ei, eqc ) ){ |
1849 |
|
Trace( c ) << getLabel( eqc ); |
1850 |
|
}else{ |
1851 |
|
NodeUIntMap::iterator lbl_i = d_labels.find(eqc); |
1852 |
|
if( lbl_i != d_labels.end() ){ |
1853 |
|
for (size_t j = 0; j < (*lbl_i).second; j++) |
1854 |
|
{ |
1855 |
|
Trace( c ) << d_labels_data[eqc][j] << " "; |
1856 |
|
} |
1857 |
|
} |
1858 |
|
} |
1859 |
|
Trace( c ) << std::endl; |
1860 |
|
Trace( c ) << " Selectors : " << ( ei->d_selectors ? "yes, " : "no " ); |
1861 |
|
NodeUIntMap::iterator sel_i = d_selector_apps.find(eqc); |
1862 |
|
if( sel_i != d_selector_apps.end() ){ |
1863 |
|
for (size_t j = 0; j < (*sel_i).second; j++) |
1864 |
|
{ |
1865 |
|
Trace( c ) << d_selector_apps_data[eqc][j] << " "; |
1866 |
|
} |
1867 |
|
} |
1868 |
|
Trace( c ) << std::endl; |
1869 |
|
} |
1870 |
|
} |
1871 |
|
//} |
1872 |
|
++eqcs_i; |
1873 |
|
} |
1874 |
|
} |
1875 |
|
|
1876 |
9717 |
void TheoryDatatypes::computeRelevantTerms(std::set<Node>& termSet) |
1877 |
|
{ |
1878 |
19434 |
Trace("dt-cmi") << "Have " << termSet.size() << " relevant terms..." |
1879 |
9717 |
<< std::endl; |
1880 |
|
|
1881 |
|
//also include non-singleton dt equivalence classes TODO : revisit this |
1882 |
9717 |
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine); |
1883 |
542673 |
while( !eqcs_i.isFinished() ){ |
1884 |
532956 |
TNode r = (*eqcs_i); |
1885 |
266478 |
if (r.getType().isDatatype()) |
1886 |
|
{ |
1887 |
43671 |
eq::EqClassIterator eqc_i = eq::EqClassIterator(r, d_equalityEngine); |
1888 |
422385 |
while (!eqc_i.isFinished()) |
1889 |
|
{ |
1890 |
189357 |
termSet.insert(*eqc_i); |
1891 |
189357 |
++eqc_i; |
1892 |
|
} |
1893 |
|
} |
1894 |
266478 |
++eqcs_i; |
1895 |
|
} |
1896 |
9717 |
} |
1897 |
|
|
1898 |
|
std::pair<bool, Node> TheoryDatatypes::entailmentCheck(TNode lit) |
1899 |
|
{ |
1900 |
|
Trace("dt-entail") << "Check entailed : " << lit << std::endl; |
1901 |
|
Node atom = lit.getKind()==NOT ? lit[0] : lit; |
1902 |
|
bool pol = lit.getKind()!=NOT; |
1903 |
|
if( atom.getKind()==APPLY_TESTER ){ |
1904 |
|
Node n = atom[0]; |
1905 |
|
if( hasTerm( n ) ){ |
1906 |
|
Node r = d_equalityEngine->getRepresentative(n); |
1907 |
|
EqcInfo * ei = getOrMakeEqcInfo( r, false ); |
1908 |
|
int l_index = getLabelIndex( ei, r ); |
1909 |
|
int t_index = static_cast<int>(utils::indexOf(atom.getOperator())); |
1910 |
|
Trace("dt-entail") << " Tester indices are " << t_index << " and " << l_index << std::endl; |
1911 |
|
if( l_index!=-1 && (l_index==t_index)==pol ){ |
1912 |
|
std::vector< TNode > exp_c; |
1913 |
|
Node eqToExplain; |
1914 |
|
if( ei && !ei->d_constructor.get().isNull() ){ |
1915 |
|
eqToExplain = n.eqNode(ei->d_constructor.get()); |
1916 |
|
}else{ |
1917 |
|
Node lbl = getLabel( n ); |
1918 |
|
Assert(!lbl.isNull()); |
1919 |
|
exp_c.push_back( lbl ); |
1920 |
|
Assert(areEqual(n, lbl[0])); |
1921 |
|
eqToExplain = n.eqNode(lbl[0]); |
1922 |
|
} |
1923 |
|
d_equalityEngine->explainLit(eqToExplain, exp_c); |
1924 |
|
Node exp = NodeManager::currentNM()->mkAnd(exp_c); |
1925 |
|
Trace("dt-entail") << " entailed, explanation is " << exp << std::endl; |
1926 |
|
return make_pair(true, exp); |
1927 |
|
} |
1928 |
|
} |
1929 |
|
} |
1930 |
|
return make_pair(false, Node::null()); |
1931 |
|
} |
1932 |
|
|
1933 |
|
} // namespace datatypes |
1934 |
|
} // namespace theory |
1935 |
29574 |
} // namespace cvc5 |