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