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