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