projects / cvc5.git / blob
? search:


c8d7338a7edbae94d4c81e82ed49aee69b9098e9
[cvc5.git] / src / theory / datatypes / theory_datatypes.cpp
1 /********************* */
2 /*! \file theory_datatypes.cpp
3 ** \verbatim
4 ** Original author: Morgan Deters
5 ** Major contributors: Andrew Reynolds
6 ** Minor contributors (to current version): Dejan Jovanovic
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
11 **
12 ** \brief Implementation of the theory of datatypes
13 **
14 ** Implementation of the theory of datatypes.
15 **/
16 #include "theory/datatypes/theory_datatypes.h"
17
18 #include <map>
19
20 #include "base/cvc4_assert.h"
21 #include "expr/datatype.h"
22 #include "expr/kind.h"
23 #include "options/datatypes_options.h"
24 #include "options/quantifiers_options.h"
25 #include "options/smt_options.h"
26 #include "smt/boolean_terms.h"
27 #include "theory/datatypes/datatypes_rewriter.h"
28 #include "theory/datatypes/theory_datatypes_type_rules.h"
29 #include "theory/quantifiers_engine.h"
30 #include "theory/theory_model.h"
31 #include "theory/type_enumerator.h"
32 #include "theory/valuation.h"
33
34 using namespace std;
35 using namespace CVC4::kind;
36 using namespace CVC4::context;
37
38 namespace CVC4 {
39 namespace theory {
40 namespace datatypes {
41
42 TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
43 Valuation valuation, const LogicInfo& logicInfo)
44 : Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo),
45 //d_cycle_check(c),
46 d_hasSeenCycle(c, false),
47 d_infer(c),
48 d_infer_exp(c),
49 d_term_sk( u ),
50 d_notify( *this ),
51 d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes", true),
52 d_labels( c ),
53 d_selector_apps( c ),
54 //d_consEqc( c ),
55 d_conflict( c, false ),
56 d_collectTermsCache( c ),
57 d_consTerms( c ),
58 d_selTerms( c ),
59 d_singleton_eq( u ),
60 d_lemmas_produced_c( u )
61 {
62 // The kinds we are treating as function application in congruence
63 d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR);
64 d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
65 d_equalityEngine.addFunctionKind(kind::DT_SIZE);
66 d_equalityEngine.addFunctionKind(kind::DT_HEIGHT_BOUND);
67 d_equalityEngine.addFunctionKind(kind::APPLY_TESTER);
68 //d_equalityEngine.addFunctionKind(kind::APPLY_UF);
69
70 d_true = NodeManager::currentNM()->mkConst( true );
71 d_dtfCounter = 0;
72
73 d_sygus_split = NULL;
74 d_sygus_sym_break = NULL;
75 }
76
77 TheoryDatatypes::~TheoryDatatypes() {
78 }
79
80 void TheoryDatatypes::setMasterEqualityEngine(eq::EqualityEngine* eq) {
81 d_equalityEngine.setMasterEqualityEngine(eq);
82 }
83
84 TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( TNode n, bool doMake ){
85 if( !hasEqcInfo( n ) ){
86 if( doMake ){
87 //add to labels
88 NodeList* lbl = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
89 ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
90 d_labels.insertDataFromContextMemory( n, lbl );
91
92 std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n );
93 EqcInfo* ei;
94 if( eqc_i!=d_eqc_info.end() ){
95 ei = eqc_i->second;
96 }else{
97 ei = new EqcInfo( getSatContext() );
98 d_eqc_info[n] = ei;
99 }
100 if( n.getKind()==APPLY_CONSTRUCTOR ){
101 ei->d_constructor = n;
102 }
103 //add to selectors
104 NodeList* sel = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
105 ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
106 d_selector_apps.insertDataFromContextMemory( n, sel );
107 return ei;
108 }else{
109 return NULL;
110 }
111 }else{
112 std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n );
113 return (*eqc_i).second;
114 }
115 }
116
117 TNode TheoryDatatypes::getEqcConstructor( TNode r ) {
118 if( r.getKind()==APPLY_CONSTRUCTOR ){
119 return r;
120 }else{
121 EqcInfo * ei = getOrMakeEqcInfo( r, false );
122 if( ei && !ei->d_constructor.get().isNull() ){
123 return ei->d_constructor.get();
124 }else{
125 return r;
126 }
127 }
128 }
129
130 void TheoryDatatypes::check(Effort e) {
131 if (done() && !fullEffort(e)) {
132 return;
133 }
134 Assert( d_pending.empty() && d_pending_merge.empty() );
135 d_addedLemma = false;
136
137 TimerStat::CodeTimer checkTimer(d_checkTime);
138
139 Trace("datatypes-check") << "Check effort " << e << std::endl;
140 while(!done() && !d_conflict) {
141 // Get all the assertions
142 Assertion assertion = get();
143 TNode fact = assertion.assertion;
144 Trace("datatypes-assert") << "Assert " << fact << std::endl;
145
146 TNode atom CVC4_UNUSED = fact.getKind() == kind::NOT ? fact[0] : fact;
147
148 // extra debug check to make sure that the rewriter did its job correctly
149 Assert( atom.getKind() != kind::EQUAL ||
150 ( atom[0].getKind() != kind::TUPLE && atom[1].getKind() != kind::TUPLE &&
151 atom[0].getKind() != kind::RECORD && atom[1].getKind() != kind::RECORD &&
152 atom[0].getKind() != kind::TUPLE_UPDATE && atom[1].getKind() != kind::TUPLE_UPDATE &&
153 atom[0].getKind() != kind::RECORD_UPDATE && atom[1].getKind() != kind::RECORD_UPDATE &&
154 atom[0].getKind() != kind::TUPLE_SELECT && atom[1].getKind() != kind::TUPLE_SELECT &&
155 atom[0].getKind() != kind::RECORD_SELECT && atom[1].getKind() != kind::RECORD_SELECT ),
156 "tuple/record escaped into datatypes decision procedure; should have been rewritten away" );
157
158 //assert the fact
159 assertFact( fact, fact );
160 flushPendingFacts();
161 }
162
163 if( e == EFFORT_FULL && !d_conflict && !d_addedLemma && !d_valuation.needCheck() ) {
164 //check for cycles
165 Assert( d_pending.empty() && d_pending_merge.empty() );
166 bool addedFact;
167 do {
168 checkCycles();
169 addedFact = !d_pending.empty() || !d_pending_merge.empty();
170 flushPendingFacts();
171 if( d_conflict || d_addedLemma ){
172 return;
173 }
174 }while( addedFact );
175
176 //check for splits
177 Trace("datatypes-debug") << "Check for splits " << e << endl;
178 addedFact = false;
179 do {
180 std::map< TypeNode, Node > rec_singletons;
181 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
182 while( !eqcs_i.isFinished() ){
183 Node n = (*eqcs_i);
184 TypeNode tn = n.getType();
185 if( DatatypesRewriter::isTypeDatatype( tn ) ){
186 Trace("datatypes-debug") << "Process equivalence class " << n << std::endl;
187 EqcInfo* eqc = getOrMakeEqcInfo( n );
188 //if there are more than 1 possible constructors for eqc
189 if( !hasLabel( eqc, n ) ){
190 Trace("datatypes-debug") << "No constructor..." << std::endl;
191 const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
192 Trace("datatypes-debug") << "Datatype " << dt << " is " << dt.isFinite() << " " << dt.isUFinite() << " " << dt.isRecursiveSingleton() << std::endl;
193 bool continueProc = true;
194 if( dt.isRecursiveSingleton() ){
195 Trace("datatypes-debug") << "Check recursive singleton..." << std::endl;
196 //handle recursive singleton case
197 std::map< TypeNode, Node >::iterator itrs = rec_singletons.find( tn );
198 if( itrs!=rec_singletons.end() ){
199 Node eq = n.eqNode( itrs->second );
200 if( d_singleton_eq.find( eq )==d_singleton_eq.end() ){
201 d_singleton_eq[eq] = true;
202 // get assumptions
203 bool success = true;
204 std::vector< Node > assumptions;
205 //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,
206 // do not infer the equality if at least one sort was processed.
207 //otherwise, if the logic is quantified, under the assumption that all uninterpreted sorts have cardinality one,
208 // infer the equality.
209 for( unsigned i=0; i<dt.getNumRecursiveSingletonArgTypes(); i++ ){
210 TypeNode tn = TypeNode::fromType( dt.getRecursiveSingletonArgType( i ) );
211 if( getQuantifiersEngine() ){
212 // under the assumption that the cardinality of this type is one
213 Node a = getSingletonLemma( tn, true );
214 assumptions.push_back( a.negate() );
215 }else{
216 success = false;
217 // assert that the cardinality of this type is more than one
218 getSingletonLemma( tn, false );
219 }
220 }
221 if( success ){
222 Node eq = n.eqNode( itrs->second );
223 assumptions.push_back( eq );
224 Node lemma = assumptions.size()==1 ? assumptions[0] : NodeManager::currentNM()->mkNode( OR, assumptions );
225 Trace("dt-singleton") << "*************Singleton equality lemma " << lemma << std::endl;
226 doSendLemma( lemma );
227 }
228 }
229 }else{
230 rec_singletons[tn] = n;
231 }
232 //do splitting for quantified logics (incomplete anyways)
233 continueProc = ( getQuantifiersEngine()!=NULL );
234 }
235 if( continueProc ){
236 Trace("datatypes-debug") << "Get possible cons..." << std::endl;
237 //all other cases
238 std::vector< bool > pcons;
239 getPossibleCons( eqc, n, pcons );
240 //check if we do not need to resolve the constructor type for this equivalence class.
241 // this is if there are no selectors for this equivalence class, its possible values are infinite,
242 // and we are not producing a model, then do not split.
243 int consIndex = -1;
244 int fconsIndex = -1;
245 bool needSplit = true;
246 for( unsigned int j=0; j<pcons.size(); j++ ) {
247 if( pcons[j] ) {
248 if( consIndex==-1 ){
249 consIndex = j;
250 }
251 if( options::finiteModelFind() ? !dt[ j ].isUFinite() : !dt[ j ].isFinite() ) {
252 if( !eqc || !eqc->d_selectors ){
253 needSplit = false;
254 }
255 }else{
256 if( fconsIndex==-1 ){
257 fconsIndex = j;
258 }
259 }
260 }
261 }
262 //if we want to force an assignment of constructors to all ground eqc
263 //d_dtfCounter++;
264 if( !needSplit && options::dtForceAssignment() && d_dtfCounter%2==0 ){
265 Trace("datatypes-force-assign") << "Force assignment for " << n << std::endl;
266 needSplit = true;
267 consIndex = fconsIndex!=-1 ? fconsIndex : consIndex;
268 }
269
270 if( needSplit && consIndex!=-1 ) {
271 if( dt.getNumConstructors()==1 ){
272 //this may not be necessary?
273 //if only one constructor, then this term must be this constructor
274 Node t = DatatypesRewriter::mkTester( n, 0, dt );
275 d_pending.push_back( t );
276 d_pending_exp[ t ] = d_true;
277 Trace("datatypes-infer") << "DtInfer : 1-cons (full) : " << t << std::endl;
278 d_infer.push_back( t );
279 }else{
280 if( options::dtBinarySplit() ){
281 Node test = DatatypesRewriter::mkTester( n, consIndex, dt );
282 Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n << endl;
283 test = Rewriter::rewrite( test );
284 NodeBuilder<> nb(kind::OR);
285 nb << test << test.notNode();
286 Node lemma = nb;
287 doSendLemma( lemma );
288 d_out->requirePhase( test, true );
289 }else{
290 Trace("dt-split") << "*************Split for constructors on " << n << endl;
291 std::vector< Node > children;
292 if( dt.isSygus() && d_sygus_split ){
293 std::vector< Node > lemmas;
294 d_sygus_split->getSygusSplits( n, dt, children, lemmas );
295 for( unsigned i=0; i<lemmas.size(); i++ ){
296 Trace("dt-lemma-sygus") << "Dt sygus lemma : " << lemmas[i] << std::endl;
297 doSendLemma( lemmas[i] );
298 }
299 }else{
300 for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
301 Node test = DatatypesRewriter::mkTester( n, i, dt );
302 children.push_back( test );
303 }
304 }
305 Assert( !children.empty() );
306 Node lemma = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::OR, children );
307 Trace("dt-split-debug") << "Split lemma is : " << lemma << std::endl;
308 //doSendLemma( lemma );
309 d_out->lemma( lemma, false, false, true );
310 }
311 return;
312 }
313 }else{
314 Trace("dt-split-debug") << "Do not split constructor for " << n << " : " << n.getType() << " " << dt.getNumConstructors() << std::endl;
315 }
316 }
317 }else{
318 Trace("datatypes-debug") << "Has constructor " << eqc->d_constructor.get() << std::endl;
319 }
320 }
321 ++eqcs_i;
322 }
323 Trace("datatypes-debug") << "Flush pending facts..." << std::endl;
324 addedFact = !d_pending.empty() || !d_pending_merge.empty();
325 flushPendingFacts();
326 /*
327 if( !d_conflict ){
328 if( options::dtRewriteErrorSel() ){
329 bool innerAddedFact = false;
330 do {
331 collapseSelectors();
332 innerAddedFact = !d_pending.empty() || !d_pending_merge.empty();
333 flushPendingFacts();
334 }while( !d_conflict && innerAddedFact );
335 }
336 }
337 */
338 }while( !d_conflict && !d_addedLemma && addedFact );
339 Trace("datatypes-debug") << "Finished. " << d_conflict << std::endl;
340 if( !d_conflict ){
341 Trace("dt-model-debug") << std::endl;
342 printModelDebug("dt-model-debug");
343 }
344 }
345
346 Trace("datatypes-check") << "Finished check effort " << e << std::endl;
347 if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") ) {
348 Notice() << "TheoryDatatypes::check(): done" << endl;
349 }
350 }
351
352 void TheoryDatatypes::flushPendingFacts(){
353 doPendingMerges();
354 if( !d_pending_lem.empty() ){
355 int i = 0;
356 while( i<(int)d_pending_lem.size() ){
357 doSendLemma( d_pending_lem[i] );
358 i++;
359 }
360 d_pending_lem.clear();
361 doPendingMerges();
362 }
363 int i = 0;
364 while( !d_conflict && i<(int)d_pending.size() ){
365 Node fact = d_pending[i];
366 Node exp = d_pending_exp[ fact ];
367 Trace("datatypes-debug") << "Assert fact (#" << (i+1) << "/" << d_pending.size() << ") " << fact << " with explanation " << exp << std::endl;
368 //check to see if we have to communicate it to the rest of the system
369 if( mustCommunicateFact( fact, exp ) ){
370 Node lem = fact;
371 if( exp.isNull() || exp==d_true ){
372 Trace("dt-lemma-debug") << "Trivial explanation." << std::endl;
373 }else{
374 Trace("dt-lemma-debug") << "Get explanation..." << std::endl;
375 Node ee_exp = explain( exp );
376 Trace("dt-lemma-debug") << "Explanation : " << ee_exp << std::endl;
377 lem = NodeManager::currentNM()->mkNode( OR, ee_exp.negate(), fact );
378 lem = Rewriter::rewrite( lem );
379 }
380 Trace("dt-lemma") << "Datatypes lemma : " << lem << std::endl;
381 doSendLemma( lem );
382 d_addedLemma = true;
383 }else{
384 assertFact( fact, exp );
385 }
386 Trace("datatypes-debug") << "Finished fact " << fact << ", now = " << d_conflict << " " << d_pending.size() << std::endl;
387 i++;
388 }
389 d_pending.clear();
390 d_pending_exp.clear();
391 }
392
393 void TheoryDatatypes::doPendingMerges(){
394 if( !d_conflict ){
395 //do all pending merges
396 int i=0;
397 while( i<(int)d_pending_merge.size() ){
398 Assert( d_pending_merge[i].getKind()==EQUAL || d_pending_merge[i].getKind()==IFF );
399 merge( d_pending_merge[i][0], d_pending_merge[i][1] );
400 i++;
401 }
402 }
403 d_pending_merge.clear();
404 }
405
406 bool TheoryDatatypes::doSendLemma( Node lem ) {
407 if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){
408 Trace("dt-lemma-send") << "TheoryDatatypes::doSendLemma : " << lem << std::endl;
409 d_lemmas_produced_c[lem] = true;
410 d_out->lemma( lem );
411 return true;
412 }else{
413 return false;
414 }
415 }
416
417 void TheoryDatatypes::assertFact( Node fact, Node exp ){
418 Assert( d_pending_merge.empty() );
419 Trace("datatypes-debug") << "TheoryDatatypes::assertFact : " << fact << std::endl;
420 bool polarity = fact.getKind() != kind::NOT;
421 TNode atom = polarity ? fact : fact[0];
422 if (atom.getKind() == kind::EQUAL) {
423 d_equalityEngine.assertEquality( atom, polarity, exp );
424 }else{
425 d_equalityEngine.assertPredicate( atom, polarity, exp );
426 }
427 doPendingMerges();
428 //add to tester if applicable
429 Node t_arg;
430 int tindex = DatatypesRewriter::isTester( atom, t_arg );
431 if( tindex!=-1 ){
432 Trace("dt-tester") << "Assert tester : " << atom << " for " << t_arg << std::endl;
433 Node rep = getRepresentative( t_arg );
434 EqcInfo* eqc = getOrMakeEqcInfo( rep, true );
435 addTester( tindex, fact, eqc, rep, t_arg );
436 Trace("dt-tester") << "Done assert tester." << std::endl;
437 if( !d_conflict && polarity ){
438 if( d_sygus_sym_break ){
439 //Assert( !d_sygus_util->d_conflict );
440 Trace("dt-tester") << "Assert tester to sygus : " << atom << std::endl;
441 d_sygus_sym_break->addTester( tindex, t_arg, atom );
442 Trace("dt-tester") << "Done assert tester to sygus." << std::endl;
443 for( unsigned i=0; i<d_sygus_sym_break->d_lemmas.size(); i++ ){
444 Trace("dt-lemma-sygus") << "Sygus symmetry breaking lemma : " << d_sygus_sym_break->d_lemmas[i] << std::endl;
445 doSendLemma( d_sygus_sym_break->d_lemmas[i] );
446 }
447 d_sygus_sym_break->d_lemmas.clear();
448 /*
449 if( d_sygus_util->d_conflict ){
450 //d_conflict = true;
451 if( !d_sygus_util->d_conflictNode.isNull() ){
452 std::vector< TNode > assumptions;
453 explain( d_sygus_util->d_conflictNode, assumptions );
454 d_conflictNode = mkAnd( assumptions );
455 Trace("dt-conflict") << "CONFLICT: sygus symmetry breaking conflict : " << d_conflictNode << std::endl;
456 d_out->conflict( d_conflictNode );
457 }
458 return;
459 }
460 */
461 }
462 }
463 }else{
464 Trace("dt-tester-debug") << "Assert (non-tester) : " << atom << std::endl;
465 }
466 doPendingMerges();
467 Trace("datatypes-debug") << "TheoryDatatypes::assertFact : finished " << fact << std::endl;
468 }
469
470 void TheoryDatatypes::preRegisterTerm(TNode n) {
471 Debug("datatypes-prereg") << "TheoryDatatypes::preRegisterTerm() " << n << endl;
472 collectTerms( n );
473 switch (n.getKind()) {
474 case kind::EQUAL:
475 // Add the trigger for equality
476 d_equalityEngine.addTriggerEquality(n);
477 break;
478 case kind::APPLY_TESTER:
479 // Get triggered for both equal and dis-equal
480 d_equalityEngine.addTriggerPredicate(n);
481 break;
482 default:
483 // Maybe it's a predicate
484 if (n.getType().isBoolean()) {
485 // Get triggered for both equal and dis-equal
486 d_equalityEngine.addTriggerPredicate(n);
487 } else {
488 // Function applications/predicates
489 d_equalityEngine.addTerm(n);
490 //d_equalityEngine.addTriggerTerm(n, THEORY_DATATYPES);
491 }
492 break;
493 }
494 flushPendingFacts();
495 }
496
497 void TheoryDatatypes::finishInit() {
498 if( getQuantifiersEngine() && options::ceGuidedInst() ){
499 quantifiers::TermDbSygus * tds = getQuantifiersEngine()->getTermDatabaseSygus();
500 Assert( tds!=NULL );
501 d_sygus_split = new SygusSplit( tds );
502 d_sygus_sym_break = new SygusSymBreak( tds, getSatContext() );
503 }
504 }
505
506 Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) {
507 switch( n.getKind() ){
508 case kind::APPLY_SELECTOR: {
509 Node selector = n.getOperator();
510 Expr selectorExpr = selector.toExpr();
511 Node sel = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( selectorExpr ), n[0] );
512 if( options::dtRewriteErrorSel() ){
513 return sel;
514 }else{
515 size_t selectorIndex = Datatype::cindexOf(selectorExpr);
516 const Datatype& dt = Datatype::datatypeOf(selectorExpr);
517 const DatatypeConstructor& c = dt[selectorIndex];
518 Expr tester = c.getTester();
519 Node tst = NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( tester ), n[0] );
520 tst = Rewriter::rewrite( tst );
521 Node n_ret;
522 if( tst==d_true ){
523 n_ret = sel;
524 }else{
525 mkExpDefSkolem( selector, n[0].getType(), n.getType() );
526 Node sk = NodeManager::currentNM()->mkNode( kind::APPLY_UF, d_exp_def_skolem[ selector ], n[0] );
527 if( tst==NodeManager::currentNM()->mkConst( false ) ){
528 n_ret = sk;
529 }else{
530 n_ret = NodeManager::currentNM()->mkNode( kind::ITE, tst, sel, sk );
531 }
532 }
533 //n_ret = Rewriter::rewrite( n_ret );
534 Trace("dt-expand") << "Expand def : " << n << " to " << n_ret << std::endl;
535 return n_ret;
536 }
537 }
538 break;
539 default:
540 return n;
541 break;
542 }
543 Unreachable();
544 }
545
546 void TheoryDatatypes::presolve() {
547 Debug("datatypes") << "TheoryDatatypes::presolve()" << endl;
548 }
549
550 Node TheoryDatatypes::ppRewrite(TNode in) {
551 Debug("tuprec") << "TheoryDatatypes::ppRewrite(" << in << ")" << endl;
552
553 if(in.getKind() == kind::TUPLE_SELECT) {
554 TypeNode t = in[0].getType();
555 if(t.hasAttribute(expr::DatatypeTupleAttr())) {
556 t = t.getAttribute(expr::DatatypeTupleAttr());
557 }
558 TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t);
559 const Datatype& dt = DatatypeType(dtt.toType()).getDatatype();
560 return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][in.getOperator().getConst<TupleSelect>().getIndex()].getSelector()), in[0]);
561 } else if(in.getKind() == kind::RECORD_SELECT) {
562 TypeNode t = in[0].getType();
563 if(t.hasAttribute(expr::DatatypeRecordAttr())) {
564 t = t.getAttribute(expr::DatatypeRecordAttr());
565 }
566 TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t);
567 const Datatype& dt = DatatypeType(dtt.toType()).getDatatype();
568 return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][in.getOperator().getConst<RecordSelect>().getField()].getSelector()), in[0]);
569 }
570
571 TypeNode t = in.getType();
572
573 // we only care about tuples and records here
574 if(in.getKind() != kind::TUPLE && in.getKind() != kind::TUPLE_UPDATE &&
575 in.getKind() != kind::RECORD && in.getKind() != kind::RECORD_UPDATE) {
576 if((t.isTuple() || t.isRecord()) && in.hasAttribute(smt::BooleanTermAttr())) {
577 Debug("tuprec") << "should map " << in << " of type " << t << " back to " << in.getAttribute(smt::BooleanTermAttr()).getType() << endl;
578 Debug("tuprec") << "so " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getDatatype() << " goes to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getDatatype() << endl;
579 if(t.isTuple()) {
580 Debug("tuprec") << "current datatype-tuple-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getAttribute(expr::DatatypeTupleAttr()) << endl;
581 Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr()) << endl;
582 NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeTupleAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr()));
583 } else {
584 Debug("tuprec") << "current datatype-record-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getAttribute(expr::DatatypeRecordAttr()) << endl;
585 Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()) << endl;
586 NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeRecordAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()));
587 }
588 }
589
590 if( in.getKind()==EQUAL ){
591 Node nn;
592 std::vector< Node > rew;
593 if( DatatypesRewriter::checkClash(in[0], in[1], rew) ){
594 nn = NodeManager::currentNM()->mkConst(false);
595 }else{
596 nn = rew.size()==0 ? d_true :
597 ( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) );
598 }
599 return nn;
600 }
601
602 // nothing to do
603 return in;
604 }
605
606 if(t.hasAttribute(expr::DatatypeTupleAttr())) {
607 t = t.getAttribute(expr::DatatypeTupleAttr());
608 } else if(t.hasAttribute(expr::DatatypeRecordAttr())) {
609 t = t.getAttribute(expr::DatatypeRecordAttr());
610 }
611
612 // if the type doesn't have an associated datatype, then make one for it
613 TypeNode dtt = (t.isTuple() || t.isRecord()) ? NodeManager::currentNM()->getDatatypeForTupleRecord(t) : t;
614
615 const Datatype& dt = DatatypeType(dtt.toType()).getDatatype();
616
617 // now rewrite the expression
618 Node n;
619 if(in.getKind() == kind::TUPLE || in.getKind() == kind::RECORD) {
620 NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
621 b << Node::fromExpr(dt[0].getConstructor());
622 b.append(in.begin(), in.end());
623 n = b;
624 } else if(in.getKind() == kind::TUPLE_UPDATE || in.getKind() == kind::RECORD_UPDATE) {
625 NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
626 b << Node::fromExpr(dt[0].getConstructor());
627 size_t size, updateIndex;
628 if(in.getKind() == kind::TUPLE_UPDATE) {
629 size = t.getNumChildren();
630 updateIndex = in.getOperator().getConst<TupleUpdate>().getIndex();
631 } else { // kind::RECORD_UPDATE
632 const Record& record = t.getConst<Record>();
633 size = record.getNumFields();
634 updateIndex = record.getIndex(in.getOperator().getConst<RecordUpdate>().getField());
635 }
636 Debug("tuprec") << "expr is " << in << std::endl;
637 Debug("tuprec") << "updateIndex is " << updateIndex << std::endl;
638 Debug("tuprec") << "t is " << t << std::endl;
639 Debug("tuprec") << "t has arity " << size << std::endl;
640 for(size_t i = 0; i < size; ++i) {
641 if(i == updateIndex) {
642 b << in[1];
643 Debug("tuprec") << "arg " << i << " gets updated to " << in[1] << std::endl;
644 } else {
645 b << NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][i].getSelector()), in[0]);
646 Debug("tuprec") << "arg " << i << " copies " << b[b.getNumChildren() - 1] << std::endl;
647 }
648 }
649 Debug("tuprec") << "builder says " << b << std::endl;
650 n = b;
651 }
652
653 Assert(!n.isNull());
654
655
656 Debug("tuprec") << "REWROTE " << in << " to " << n << std::endl;
657
658 return n;
659 }
660
661 void TheoryDatatypes::addSharedTerm(TNode t) {
662 Debug("datatypes") << "TheoryDatatypes::addSharedTerm(): "
663 << t << " " << t.getType().isBoolean() << endl;
664 //if( t.getType().isBoolean() ){
665 //d_equalityEngine.addTriggerPredicate(t, THEORY_DATATYPES);
666 //}else{
667 d_equalityEngine.addTriggerTerm(t, THEORY_DATATYPES);
668 //}
669 Debug("datatypes") << "TheoryDatatypes::addSharedTerm() finished" << std::endl;
670 }
671
672 /** propagate */
673 void TheoryDatatypes::propagate(Effort effort){
674
675 }
676
677 /** propagate */
678 bool TheoryDatatypes::propagate(TNode literal){
679 Debug("dt::propagate") << "TheoryDatatypes::propagate(" << literal << ")" << std::endl;
680 // If already in conflict, no more propagation
681 if (d_conflict) {
682 Debug("dt::propagate") << "TheoryDatatypes::propagate(" << literal << "): already in conflict" << std::endl;
683 return false;
684 }
685 Trace("dt-prop") << "dtPropagate " << literal << std::endl;
686 // Propagate out
687 bool ok = d_out->propagate(literal);
688 if (!ok) {
689 Trace("dt-conflict") << "CONFLICT: Eq engine propagate conflict " << std::endl;
690 d_conflict = true;
691 }
692 return ok;
693 }
694
695 void TheoryDatatypes::addAssumptions( std::vector<TNode>& assumptions, std::vector<TNode>& tassumptions ) {
696 std::vector<TNode> ntassumptions;
697 for( unsigned i=0; i<tassumptions.size(); i++ ){
698 //flatten AND
699 if( tassumptions[i].getKind()==AND ){
700 for( unsigned j=0; j<tassumptions[i].getNumChildren(); j++ ){
701 explain( tassumptions[i][j], ntassumptions );
702 }
703 }else{
704 if( std::find( assumptions.begin(), assumptions.end(), tassumptions[i] )==assumptions.end() ){
705 assumptions.push_back( tassumptions[i] );
706 }
707 }
708 }
709 if( !ntassumptions.empty() ){
710 addAssumptions( assumptions, ntassumptions );
711 }
712 }
713
714 void TheoryDatatypes::explainEquality( TNode a, TNode b, bool polarity, std::vector<TNode>& assumptions ) {
715 if( a!=b ){
716 std::vector<TNode> tassumptions;
717 d_equalityEngine.explainEquality(a, b, polarity, tassumptions);
718 addAssumptions( assumptions, tassumptions );
719 }
720 }
721
722 void TheoryDatatypes::explainPredicate( TNode p, bool polarity, std::vector<TNode>& assumptions ) {
723 std::vector<TNode> tassumptions;
724 d_equalityEngine.explainPredicate(p, polarity, tassumptions);
725 addAssumptions( assumptions, tassumptions );
726 }
727
728 /** explain */
729 void TheoryDatatypes::explain(TNode literal, std::vector<TNode>& assumptions){
730 Debug("datatypes-explain") << "Explain " << literal << std::endl;
731 bool polarity = literal.getKind() != kind::NOT;
732 TNode atom = polarity ? literal : literal[0];
733 if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
734 explainEquality( atom[0], atom[1], polarity, assumptions );
735 } else if( atom.getKind() == kind::AND && polarity ){
736 for( unsigned i=0; i<atom.getNumChildren(); i++ ){
737 explain( atom[i], assumptions );
738 }
739 } else {
740 Assert( atom.getKind()!=kind::AND );
741 explainPredicate( atom, polarity, assumptions );
742 }
743 }
744
745 Node TheoryDatatypes::explain( TNode literal ){
746 std::vector< TNode > assumptions;
747 explain( literal, assumptions );
748 return mkAnd( assumptions );
749 }
750
751 Node TheoryDatatypes::explain( std::vector< Node >& lits ) {
752 std::vector< TNode > assumptions;
753 for( unsigned i=0; i<lits.size(); i++ ){
754 explain( lits[i], assumptions );
755 }
756 return mkAnd( assumptions );
757 }
758
759 /** Conflict when merging two constants */
760 void TheoryDatatypes::conflict(TNode a, TNode b){
761 if (a.getKind() == kind::CONST_BOOLEAN) {
762 d_conflictNode = explain( a.iffNode(b) );
763 } else {
764 d_conflictNode = explain( a.eqNode(b) );
765 }
766 Trace("dt-conflict") << "CONFLICT: Eq engine conflict : " << d_conflictNode << std::endl;
767 d_out->conflict( d_conflictNode );
768 d_conflict = true;
769 }
770
771 /** called when a new equivalance class is created */
772 void TheoryDatatypes::eqNotifyNewClass(TNode t){
773 if( t.getKind()==APPLY_CONSTRUCTOR ){
774 getOrMakeEqcInfo( t, true );
775 //look at all equivalence classes with constructor terms
776 /*
777 for( BoolMap::const_iterator it = d_consEqc.begin(); it != d_consEqc.end(); ++it ){
778 if( (*it).second ){
779 TNode r = (*it).first;
780 if( r.getType()==t.getType() ){
781 EqcInfo * ei = getOrMakeEqcInfo( r, false );
782 if( ei && !ei->d_constructor.get().isNull() && ei->d_constructor.get().getOperator()!=t.getOperator() ){
783 Node deq = ei->d_constructor.get().eqNode( t ).negate();
784 d_pending.push_back( deq );
785 d_pending_exp[ deq ] = d_true;
786 Trace("datatypes-infer") << "DtInfer : diff constructor : " << deq << std::endl;
787 d_infer.push_back( deq );
788 }
789 }
790 }
791 }
792 */
793 //d_consEqc[t] = true;
794 }
795 }
796
797 /** called when two equivalance classes will merge */
798 void TheoryDatatypes::eqNotifyPreMerge(TNode t1, TNode t2){
799
800 }
801
802 /** called when two equivalance classes have merged */
803 void TheoryDatatypes::eqNotifyPostMerge(TNode t1, TNode t2){
804 if( DatatypesRewriter::isTermDatatype( t1 ) ){
805 Trace("datatypes-debug") << "NotifyPostMerge : " << t1 << " " << t2 << std::endl;
806 d_pending_merge.push_back( t1.eqNode( t2 ) );
807 }
808 }
809
810 void TheoryDatatypes::merge( Node t1, Node t2 ){
811 if( !d_conflict ){
812 TNode trep1 = t1;
813 TNode trep2 = t2;
814 Trace("datatypes-debug") << "Merge " << t1 << " " << t2 << std::endl;
815 EqcInfo* eqc2 = getOrMakeEqcInfo( t2 );
816 if( eqc2 ){
817 bool checkInst = false;
818 if( !eqc2->d_constructor.get().isNull() ){
819 trep2 = eqc2->d_constructor.get();
820 }
821 EqcInfo* eqc1 = getOrMakeEqcInfo( t1 );
822 if( eqc1 ){
823 Trace("datatypes-debug") << " merge eqc info " << eqc2 << " into " << eqc1 << std::endl;
824 if( !eqc1->d_constructor.get().isNull() ){
825 trep1 = eqc1->d_constructor.get();
826 }
827 //check for clash
828 TNode cons1 = eqc1->d_constructor.get();
829 TNode cons2 = eqc2->d_constructor.get();
830 //if both have constructor, then either clash or unification
831 if( !cons1.isNull() && !cons2.isNull() ){
832 Trace("datatypes-debug") << " constructors : " << cons1 << " " << cons2 << std::endl;
833 Node unifEq = cons1.eqNode( cons2 );
834 /*
835 std::vector< Node > exp;
836 std::vector< std::pair< TNode, TNode > > deq_cand;
837 bool conf = checkClashModEq( cons1, cons2, exp, deq_cand );
838 if( !conf ){
839 for( unsigned i=0; i<deq_cand.size(); i++ ){
840 if( d_equalityEngine.areDisequal( deq_cand[i].first, deq_cand[i].second, true ) ){
841 conf = true;
842 Node eq = NodeManager::currentNM()->mkNode( deq_cand[i].first.getType().isBoolean() ? kind::IFF : kind::EQUAL,
843 deq_cand[i].first, deq_cand[i].second );
844 exp.push_back( eq.negate() );
845 }
846 }
847 }
848 if( conf ){
849 exp.push_back( unifEq );
850 d_conflictNode = explain( exp );
851 }
852 */
853 std::vector< Node > rew;
854 if( DatatypesRewriter::checkClash( cons1, cons2, rew ) ){
855 d_conflictNode = explain( unifEq );
856 Trace("dt-conflict") << "CONFLICT: Clash conflict : " << d_conflictNode << std::endl;
857 d_out->conflict( d_conflictNode );
858 d_conflict = true;
859 return;
860 }else{
861
862 //do unification
863 for( int i=0; i<(int)cons1.getNumChildren(); i++ ) {
864 if( !areEqual( cons1[i], cons2[i] ) ){
865 Node eq = cons1[i].getType().isBoolean() ? cons1[i].iffNode( cons2[i] ) : cons1[i].eqNode( cons2[i] );
866 d_pending.push_back( eq );
867 d_pending_exp[ eq ] = unifEq;
868 Trace("datatypes-infer") << "DtInfer : cons-inj : " << eq << " by " << unifEq << std::endl;
869 d_infer.push_back( eq );
870 d_infer_exp.push_back( unifEq );
871 }
872 }
873 /*
874 for( unsigned i=0; i<rew.size(); i++ ){
875 d_pending.push_back( rew[i] );
876 d_pending_exp[ rew[i] ] = unifEq;
877 Trace("datatypes-infer") << "DtInfer : cons-inj : " << rew[i] << " by " << unifEq << std::endl;
878 d_infer.push_back( rew[i] );
879 d_infer_exp.push_back( unifEq );
880 }
881 */
882 }
883 }
884 Trace("datatypes-debug") << " instantiated : " << eqc1->d_inst << " " << eqc2->d_inst << std::endl;
885 eqc1->d_inst = eqc1->d_inst || eqc2->d_inst;
886 if( !cons2.isNull() ){
887 if( cons1.isNull() ){
888 Trace("datatypes-debug") << " must check if it is okay to set the constructor." << std::endl;
889 checkInst = true;
890 addConstructor( eqc2->d_constructor.get(), eqc1, t1 );
891 if( d_conflict ){
892 return;
893 }
894 //d_consEqc[t1] = true;
895 }
896 //d_consEqc[t2] = false;
897 }
898 }else{
899 Trace("datatypes-debug") << " no eqc info for " << t1 << ", must create" << std::endl;
900 //just copy the equivalence class information
901 eqc1 = getOrMakeEqcInfo( t1, true );
902 eqc1->d_inst.set( eqc2->d_inst );
903 eqc1->d_constructor.set( eqc2->d_constructor );
904 eqc1->d_selectors.set( eqc2->d_selectors );
905 }
906
907
908 //merge labels
909 NodeListMap::iterator lbl_i = d_labels.find( t2 );
910 if( lbl_i != d_labels.end() ){
911 Trace("datatypes-debug") << " merge labels from " << eqc2 << " " << t2 << std::endl;
912 NodeList* lbl = (*lbl_i).second;
913 for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); ++j ){
914 Node tt = (*j).getKind()==kind::NOT ? (*j)[0] : (*j);
915 Node t_arg;
916 int tindex = DatatypesRewriter::isTester( tt, t_arg );
917 Assert( tindex!=-1 );
918 addTester( tindex, *j, eqc1, t1, t_arg );
919 if( d_conflict ){
920 Trace("datatypes-debug") << " conflict!" << std::endl;
921 return;
922 }
923 }
924 }
925 //merge selectors
926 if( !eqc1->d_selectors && eqc2->d_selectors ){
927 eqc1->d_selectors = true;
928 checkInst = true;
929 }
930 NodeListMap::iterator sel_i = d_selector_apps.find( t2 );
931 if( sel_i != d_selector_apps.end() ){
932 Trace("datatypes-debug") << " merge selectors from " << eqc2 << " " << t2 << std::endl;
933 NodeList* sel = (*sel_i).second;
934 for( NodeList::const_iterator j = sel->begin(); j != sel->end(); ++j ){
935 addSelector( *j, eqc1, t1, eqc2->d_constructor.get().isNull() );
936 }
937 }
938 if( checkInst ){
939 Trace("datatypes-debug") << " checking instantiate" << std::endl;
940 instantiate( eqc1, t1 );
941 if( d_conflict ){
942 return;
943 }
944 }
945 }
946 Trace("datatypes-debug") << "Finished Merge " << t1 << " " << t2 << std::endl;
947 }
948 }
949
950 /** called when two equivalence classes are made disequal */
951 void TheoryDatatypes::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){
952
953 }
954
955 TheoryDatatypes::EqcInfo::EqcInfo( context::Context* c ) :
956 d_inst( c, false ), d_constructor( c, Node::null() ), d_selectors( c, false ){
957
958 }
959
960 bool TheoryDatatypes::hasLabel( EqcInfo* eqc, Node n ){
961 return ( eqc && !eqc->d_constructor.get().isNull() ) || !getLabel( n ).isNull();
962 }
963
964 Node TheoryDatatypes::getLabel( Node n ) {
965 NodeListMap::iterator lbl_i = d_labels.find( n );
966 if( lbl_i != d_labels.end() ){
967 NodeList* lbl = (*lbl_i).second;
968 if( !(*lbl).empty() && (*lbl)[ (*lbl).size() - 1 ].getKind()!=kind::NOT ){
969 return (*lbl)[ (*lbl).size() - 1 ];
970 }
971 }
972 return Node::null();
973 }
974
975 int TheoryDatatypes::getLabelIndex( EqcInfo* eqc, Node n ){
976 if( eqc && !eqc->d_constructor.get().isNull() ){
977 return Datatype::indexOf( eqc->d_constructor.get().getOperator().toExpr() );
978 }else{
979 Node lbl = getLabel( n );
980 if( lbl.isNull() ){
981 return -1;
982 }else{
983 int tindex = DatatypesRewriter::isTester( lbl );
984 Assert( tindex!=-1 );
985 return tindex;
986 //return Datatype::indexOf( getLabel( n ).getOperator().toExpr() );
987 }
988 }
989 }
990
991 bool TheoryDatatypes::hasTester( Node n ) {
992 NodeListMap::iterator lbl_i = d_labels.find( n );
993 if( lbl_i != d_labels.end() ){
994 return !(*(*lbl_i).second).empty();
995 }else{
996 return false;
997 }
998 }
999
1000 void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >& pcons ){
1001 const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype();
1002 int lindex = getLabelIndex( eqc, n );
1003 pcons.resize( dt.getNumConstructors(), lindex==-1 );
1004 if( lindex!=-1 ){
1005 pcons[ lindex ] = true;
1006 }else{
1007 NodeListMap::iterator lbl_i = d_labels.find( n );
1008 if( lbl_i != d_labels.end() ){
1009 NodeList* lbl = (*lbl_i).second;
1010 for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
1011 Assert( (*i).getKind()==NOT );
1012 //pcons[ Datatype::indexOf( (*i)[0].getOperator().toExpr() ) ] = false;
1013 int tindex = DatatypesRewriter::isTester( (*i)[0] );
1014 Assert( tindex!=-1 );
1015 pcons[ tindex ] = false;
1016 }
1017 }
1018 }
1019 }
1020
1021 void TheoryDatatypes::mkExpDefSkolem( Node sel, TypeNode dt, TypeNode rt ) {
1022 if( d_exp_def_skolem.find( sel )==d_exp_def_skolem.end() ){
1023 std::stringstream ss;
1024 ss << sel << "_uf";
1025 d_exp_def_skolem[ sel ] = NodeManager::currentNM()->mkSkolem( ss.str().c_str(),
1026 NodeManager::currentNM()->mkFunctionType( dt, rt ) );
1027 }
1028 }
1029
1030 Node TheoryDatatypes::getTermSkolemFor( Node n ) {
1031 if( n.getKind()==APPLY_CONSTRUCTOR ){
1032 NodeMap::const_iterator it = d_term_sk.find( n );
1033 if( it==d_term_sk.end() ){
1034 //add purification unit lemma ( k = n )
1035 Node k = NodeManager::currentNM()->mkSkolem( "k", n.getType(), "reference skolem for datatypes" );
1036 d_term_sk[n] = k;
1037 Node eq = k.eqNode( n );
1038 Trace("datatypes-infer") << "DtInfer : ref : " << eq << std::endl;
1039 d_pending_lem.push_back( eq );
1040 //doSendLemma( eq );
1041 //d_pending_exp[ eq ] = d_true;
1042 return k;
1043 }else{
1044 return (*it).second;
1045 }
1046 }else{
1047 return n;
1048 }
1049 }
1050
1051 void TheoryDatatypes::addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node t_arg ){
1052 Trace("datatypes-debug") << "Add tester : " << t << " to eqc(" << n << ")" << std::endl;
1053 Debug("datatypes-labels") << "Add tester " << t << " " << n << " " << eqc << std::endl;
1054 bool tpolarity = t.getKind()!=NOT;
1055 Node j, jt;
1056 bool makeConflict = false;
1057 int jtindex0 = getLabelIndex( eqc, n );
1058 if( jtindex0!=-1 ){
1059 //if we already know the constructor type, check whether it is in conflict or redundant
1060 if( (jtindex0==ttindex)!=tpolarity ){
1061 if( !eqc->d_constructor.get().isNull() ){
1062 //conflict because equivalence class contains a constructor
1063 std::vector< TNode > assumptions;
1064 explain( t, assumptions );
1065 explainEquality( eqc->d_constructor.get(), t_arg, true, assumptions );
1066 d_conflictNode = mkAnd( assumptions );
1067 Trace("dt-conflict") << "CONFLICT: Tester eq conflict : " << d_conflictNode << std::endl;
1068 d_out->conflict( d_conflictNode );
1069 d_conflict = true;
1070 return;
1071 }else{
1072 makeConflict = true;
1073 //conflict because the existing label is contradictory
1074 j = getLabel( n );
1075 jt = j;
1076 }
1077 }else{
1078 return;
1079 }
1080 }else{
1081 //otherwise, scan list of labels
1082 NodeListMap::iterator lbl_i = d_labels.find( n );
1083 Assert( lbl_i != d_labels.end() );
1084 NodeList* lbl = (*lbl_i).second;
1085 for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
1086 Assert( (*i).getKind()==NOT );
1087 j = *i;
1088 jt = j[0];
1089 //int jtindex = Datatype::indexOf( jt.getOperator().toExpr() );
1090 int jtindex = DatatypesRewriter::isTester( jt );
1091 Assert( jtindex!=-1 );
1092 if( jtindex==ttindex ){
1093 if( tpolarity ){ //we are in conflict
1094 makeConflict = true;
1095 break;
1096 }else{ //it is redundant
1097 return;
1098 }
1099 }
1100 }
1101 if( !makeConflict ){
1102 Debug("datatypes-labels") << "Add to labels " << t << std::endl;
1103 lbl->push_back( t );
1104 const Datatype& dt = ((DatatypeType)(t_arg.getType()).toType()).getDatatype();
1105 Debug("datatypes-labels") << "Labels at " << lbl->size() << " / " << dt.getNumConstructors() << std::endl;
1106 if( tpolarity ){
1107 instantiate( eqc, n );
1108 }else{
1109 //check if we have reached the maximum number of testers
1110 // in this case, add the positive tester
1111 //this should not be done for sygus, since cases may be limited
1112 if( lbl->size()==dt.getNumConstructors()-1 && !dt.isSygus() ){
1113 std::vector< bool > pcons;
1114 getPossibleCons( eqc, n, pcons );
1115 int testerIndex = -1;
1116 for( unsigned i=0; i<pcons.size(); i++ ) {
1117 if( pcons[i] ){
1118 testerIndex = i;
1119 break;
1120 }
1121 }
1122 Assert( testerIndex!=-1 );
1123 //we must explain why each term in the set of testers for this equivalence class is equal
1124 std::vector< Node > eq_terms;
1125 NodeBuilder<> nb(kind::AND);
1126 for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
1127 nb << (*i);
1128 Assert( (*i).getKind()==NOT );
1129 Node t_arg2;
1130 DatatypesRewriter::isTester( (*i)[0], t_arg2 );
1131 //Assert( tindex!=-1 );
1132 if( std::find( eq_terms.begin(), eq_terms.end(), t_arg2 )==eq_terms.end() ){
1133 eq_terms.push_back( t_arg2 );
1134 if( t_arg2!=t_arg ){
1135 nb << t_arg2.eqNode( t_arg );
1136 }
1137 }
1138 }
1139 Node t_concl = DatatypesRewriter::mkTester( t_arg, testerIndex, dt );
1140 Node t_concl_exp = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb;
1141 d_pending.push_back( t_concl );
1142 d_pending_exp[ t_concl ] = t_concl_exp;
1143 Trace("datatypes-infer") << "DtInfer : label : " << t_concl << " by " << t_concl_exp << std::endl;
1144 d_infer.push_back( t_concl );
1145 d_infer_exp.push_back( t_concl_exp );
1146 return;
1147 }
1148 }
1149 }
1150 }
1151 if( makeConflict ){
1152 d_conflict = true;
1153 Debug("datatypes-labels") << "Explain " << j << " " << t << std::endl;
1154 std::vector< TNode > assumptions;
1155 explain( j, assumptions );
1156 explain( t, assumptions );
1157 explainEquality( jt[0], t_arg, true, assumptions );
1158 d_conflictNode = mkAnd( assumptions );
1159 Trace("dt-conflict") << "CONFLICT: Tester conflict : " << d_conflictNode << std::endl;
1160 d_out->conflict( d_conflictNode );
1161 }
1162 }
1163
1164 void TheoryDatatypes::addSelector( Node s, EqcInfo* eqc, Node n, bool assertFacts ) {
1165 Trace("dt-collapse-sel") << "Add selector : " << s << " to eqc(" << n << ")" << std::endl;
1166 //check to see if it is redundant
1167 NodeListMap::iterator sel_i = d_selector_apps.find( n );
1168 Assert( sel_i != d_selector_apps.end() );
1169 if( sel_i != d_selector_apps.end() ){
1170 NodeList* sel = (*sel_i).second;
1171 for( NodeList::const_iterator j = sel->begin(); j != sel->end(); ++j ){
1172 Node ss = *j;
1173 if( s.getOperator()==ss.getOperator() && ( s.getKind()!=DT_HEIGHT_BOUND || s[1]==ss[1] ) ){
1174 Trace("dt-collapse-sel") << "...redundant." << std::endl;
1175 return;
1176 }
1177 }
1178 //add it to the vector
1179 sel->push_back( s );
1180 eqc->d_selectors = true;
1181 }
1182 if( assertFacts && !eqc->d_constructor.get().isNull() ){
1183 //conclude the collapsed merge
1184 collapseSelector( s, eqc->d_constructor.get() );
1185 }
1186 }
1187
1188 void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){
1189 Trace("datatypes-debug") << "Add constructor : " << c << " to eqc(" << n << ")" << std::endl;
1190 Assert( eqc->d_constructor.get().isNull() );
1191 //check labels
1192 NodeListMap::iterator lbl_i = d_labels.find( n );
1193 if( lbl_i != d_labels.end() ){
1194 size_t constructorIndex = Datatype::indexOf(c.getOperator().toExpr());
1195 NodeList* lbl = (*lbl_i).second;
1196 for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
1197 if( (*i).getKind()==NOT ){
1198 int tindex = DatatypesRewriter::isTester( (*i)[0] );
1199 Assert( tindex!=-1 );
1200 if( tindex==(int)constructorIndex ){
1201 Node n = *i;
1202 std::vector< TNode > assumptions;
1203 explain( *i, assumptions );
1204 explainEquality( c, (*i)[0][0], true, assumptions );
1205 d_conflictNode = mkAnd( assumptions );
1206 Trace("dt-conflict") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl;
1207 d_out->conflict( d_conflictNode );
1208 d_conflict = true;
1209 return;
1210 }
1211 }
1212 }
1213 }
1214 //check selectors
1215 NodeListMap::iterator sel_i = d_selector_apps.find( n );
1216 if( sel_i != d_selector_apps.end() ){
1217 NodeList* sel = (*sel_i).second;
1218 for( NodeList::const_iterator j = sel->begin(); j != sel->end(); ++j ){
1219 //collapse the selector
1220 collapseSelector( *j, c );
1221 }
1222 }
1223 eqc->d_constructor.set( c );
1224 }
1225
1226 void TheoryDatatypes::collapseSelector( Node s, Node c ) {
1227 Assert( c.getKind()==APPLY_CONSTRUCTOR );
1228 Trace("dt-collapse-sel") << "collapse selector : " << s << " " << c << std::endl;
1229 Node r;
1230 bool wrong = false;
1231 Node use_s;
1232 Node eq_exp;
1233 if( options::dtRefIntro() ){
1234 eq_exp = d_true;
1235 use_s = getTermSkolemFor( c );
1236 }else{
1237 eq_exp = c.eqNode( s[0] );
1238 use_s = s;
1239 }
1240 if( s.getKind()==kind::APPLY_SELECTOR_TOTAL ){
1241 //Trace("dt-collapse-sel") << "Indices : " << Datatype::indexOf(c.getOperator().toExpr()) << " " << Datatype::cindexOf(s.getOperator().toExpr()) << std::endl;
1242 wrong = Datatype::indexOf(c.getOperator().toExpr())!=Datatype::cindexOf(s.getOperator().toExpr());
1243 //if( wrong ){
1244 // return;
1245 //}
1246 //if( Datatype::indexOf(c.getOperator().toExpr())!=Datatype::cindexOf(s.getOperator().toExpr()) ){
1247 // mkExpDefSkolem( s.getOperator(), s[0].getType(), s.getType() );
1248 // r = NodeManager::currentNM()->mkNode( kind::APPLY_UF, d_exp_def_skolem[s.getOperator().toExpr()], s[0] );
1249 //}else{
1250 r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), c );
1251 if( options::dtRefIntro() ){
1252 use_s = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), use_s );
1253 }
1254 }else{
1255 if( s.getKind()==DT_SIZE ){
1256 r = NodeManager::currentNM()->mkNode( DT_SIZE, c );
1257 if( options::dtRefIntro() ){
1258 use_s = NodeManager::currentNM()->mkNode( DT_SIZE, use_s );
1259 }
1260 }else if( s.getKind()==DT_HEIGHT_BOUND ){
1261 r = NodeManager::currentNM()->mkNode( DT_HEIGHT_BOUND, c, s[1] );
1262 if( options::dtRefIntro() ){
1263 use_s = NodeManager::currentNM()->mkNode( DT_HEIGHT_BOUND, use_s, s[1] );
1264 }
1265 if( r==d_true ){
1266 return;
1267 }
1268 }
1269 }
1270 if( !r.isNull() ){
1271 Node rr = Rewriter::rewrite( r );
1272 if( use_s!=rr ){
1273 Node eq = rr.getType().isBoolean() ? use_s.iffNode( rr ) : use_s.eqNode( rr );
1274 Node eq_exp;
1275 if( options::dtRefIntro() ){
1276 eq_exp = d_true;
1277 }else{
1278 eq_exp = c.eqNode( s[0] );
1279 }
1280 Trace("datatypes-infer") << "DtInfer : collapse sel";
1281 Trace("datatypes-infer") << ( wrong ? " wrong" : "");
1282 Trace("datatypes-infer") << " : " << eq << " by " << eq_exp << std::endl;
1283 d_pending.push_back( eq );
1284 d_pending_exp[ eq ] = eq_exp;
1285 d_infer.push_back( eq );
1286 d_infer_exp.push_back( eq_exp );
1287 }
1288 }
1289 }
1290
1291 EqualityStatus TheoryDatatypes::getEqualityStatus(TNode a, TNode b){
1292 Assert(d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b));
1293 if (d_equalityEngine.areEqual(a, b)) {
1294 // The terms are implied to be equal
1295 return EQUALITY_TRUE;
1296 }
1297 if (d_equalityEngine.areDisequal(a, b, false)) {
1298 // The terms are implied to be dis-equal
1299 return EQUALITY_FALSE;
1300 }
1301 return EQUALITY_FALSE_IN_MODEL;
1302 }
1303
1304 void TheoryDatatypes::computeCareGraph(){
1305 Trace("dt-cg") << "Compute graph for dt..." << std::endl;
1306 vector< pair<TNode, TNode> > currentPairs;
1307 for( unsigned r=0; r<2; r++ ){
1308 unsigned functionTerms = r==0 ? d_consTerms.size() : d_selTerms.size();
1309 for( unsigned i=0; i<functionTerms; i++ ){
1310 TNode f1 = r==0 ? d_consTerms[i] : d_selTerms[i];
1311 Assert(d_equalityEngine.hasTerm(f1));
1312 for( unsigned j=i+1; j<functionTerms; j++ ){
1313 TNode f2 = r==0 ? d_consTerms[j] : d_selTerms[j];
1314 Trace("dt-cg-debug") << "dt-cg(" << r << "): " << f1 << " and " << f2 << " " << (f1.getOperator()==f2.getOperator()) << " " << areEqual( f1, f2 ) << std::endl;
1315 Assert(d_equalityEngine.hasTerm(f2));
1316 if( f1.getOperator()==f2.getOperator() &&
1317 ( ( f1.getKind()!=DT_SIZE && f1.getKind()!=DT_HEIGHT_BOUND ) || f1[0].getType()==f2[0].getType() ) &&
1318 !areEqual( f1, f2 ) ){
1319 Trace("dt-cg") << "Check " << f1 << " and " << f2 << std::endl;
1320 bool somePairIsDisequal = false;
1321 currentPairs.clear();
1322 for (unsigned k = 0; k < f1.getNumChildren(); ++ k) {
1323 TNode x = f1[k];
1324 TNode y = f2[k];
1325 Assert(d_equalityEngine.hasTerm(x));
1326 Assert(d_equalityEngine.hasTerm(y));
1327 if( areDisequal(x, y) ){
1328 somePairIsDisequal = true;
1329 break;
1330 }else if( !d_equalityEngine.areEqual( x, y ) ){
1331 Trace("dt-cg") << "Arg #" << k << " is " << x << " " << y << std::endl;
1332 if( d_equalityEngine.isTriggerTerm(x, THEORY_DATATYPES) && d_equalityEngine.isTriggerTerm(y, THEORY_DATATYPES) ){
1333 TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_DATATYPES);
1334 TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_DATATYPES);
1335 Trace("dt-cg") << "Arg #" << k << " shared term is " << x_shared << " " << y_shared << std::endl;
1336 EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared);
1337 Trace("dt-cg") << "...eq status is " << eqStatus << std::endl;
1338 if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){
1339 somePairIsDisequal = true;
1340 break;
1341 }else{
1342 currentPairs.push_back(make_pair(x_shared, y_shared));
1343 }
1344 }
1345 }
1346 }
1347 if (!somePairIsDisequal) {
1348 for (unsigned c = 0; c < currentPairs.size(); ++ c) {
1349 Trace("dt-cg-pair") << "Pair : " << currentPairs[c].first << " " << currentPairs[c].second << std::endl;
1350 addCarePair(currentPairs[c].first, currentPairs[c].second);
1351 }
1352 }
1353 }
1354 }
1355 }
1356 }
1357 Trace("dt-cg") << "Done Compute graph for dt." << std::endl;
1358 }
1359
1360 void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
1361 Trace("dt-cmi") << "Datatypes : Collect model info " << d_equalityEngine.consistent() << std::endl;
1362 Trace("dt-model") << std::endl;
1363 printModelDebug( "dt-model" );
1364 Trace("dt-model") << std::endl;
1365
1366 //combine the equality engine
1367 m->assertEqualityEngine( &d_equalityEngine );
1368
1369 //get all constructors
1370 eq::EqClassesIterator eqccs_i = eq::EqClassesIterator( &d_equalityEngine );
1371 std::vector< Node > cons;
1372 std::vector< Node > nodes;
1373 std::map< Node, Node > eqc_cons;
1374 while( !eqccs_i.isFinished() ){
1375 Node eqc = (*eqccs_i);
1376 //for all equivalence classes that are datatypes
1377 if( DatatypesRewriter::isTermDatatype( eqc ) ){
1378 EqcInfo* ei = getOrMakeEqcInfo( eqc );
1379 if( ei && !ei->d_constructor.get().isNull() ){
1380 Node c = ei->d_constructor.get();
1381 cons.push_back( c );
1382 eqc_cons[ eqc ] = c;
1383 }else{
1384 //if eqc contains a symbol known to datatypes (a selector), then we must assign
1385 //should assign constructors to EQC if they have a selector or a tester
1386 bool shouldConsider = ( ei && ei->d_selectors ) || hasTester( eqc );
1387 if( shouldConsider ){
1388 nodes.push_back( eqc );
1389 }
1390 }
1391 }
1392 ++eqccs_i;
1393 }
1394
1395 //unsigned orig_size = nodes.size();
1396 std::map< TypeNode, int > typ_enum_map;
1397 std::vector< TypeEnumerator > typ_enum;
1398 unsigned index = 0;
1399 while( index<nodes.size() ){
1400 Node eqc = nodes[index];
1401 Node neqc;
1402 bool addCons = false;
1403 const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype();
1404 if( !d_equalityEngine.hasTerm( eqc ) ){
1405 Assert( false );
1406 /*
1407 if( !dt.isCodatatype() ){
1408 Trace("dt-cmi") << "NOTICE : Datatypes: need to assign constructor for " << eqc << std::endl;
1409 Trace("dt-cmi") << " Type : " << eqc.getType() << std::endl;
1410 TypeNode tn = eqc.getType();
1411 //if it is infinite, make sure it is fresh
1412 // this ensures that the term that this is an argument of is distinct.
1413 if( eqc.getType().getCardinality().isInfinite() ){
1414 std::map< TypeNode, int >::iterator it = typ_enum_map.find( tn );
1415 int teIndex;
1416 if( it==typ_enum_map.end() ){
1417 teIndex = (int)typ_enum.size();
1418 typ_enum_map[tn] = teIndex;
1419 typ_enum.push_back( TypeEnumerator(tn) );
1420 }else{
1421 teIndex = it->second;
1422 }
1423 bool success;
1424 do{
1425 success = true;
1426 Assert( !typ_enum[teIndex].isFinished() );
1427 neqc = *typ_enum[teIndex];
1428 Trace("dt-cmi-debug") << "Try " << neqc << " ... " << std::endl;
1429 ++typ_enum[teIndex];
1430 for( unsigned i=0; i<cons.size(); i++ ){
1431 //check if it is modulo equality the same
1432 if( cons[i].getOperator()==neqc.getOperator() ){
1433 bool diff = false;
1434 for( unsigned j=0; j<cons[i].getNumChildren(); j++ ){
1435 if( !m->areEqual( cons[i][j], neqc[j] ) ){
1436 diff = true;
1437 break;
1438 }
1439 }
1440 if( !diff ){
1441 Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons[i] << std::endl;
1442 success = false;
1443 break;
1444 }
1445 }
1446 }
1447 }while( !success );
1448 }else{
1449 TypeEnumerator te(tn);
1450 neqc = *te;
1451 }
1452 }
1453 */
1454 }else{
1455 Trace("dt-cmi") << "NOTICE : Datatypes: no constructor in equivalence class " << eqc << std::endl;
1456 Trace("dt-cmi") << " Type : " << eqc.getType() << std::endl;
1457 EqcInfo* ei = getOrMakeEqcInfo( eqc );
1458 std::vector< bool > pcons;
1459 getPossibleCons( ei, eqc, pcons );
1460 Trace("dt-cmi") << "Possible constructors : ";
1461 for( unsigned i=0; i<pcons.size(); i++ ){
1462 Trace("dt-cmi") << pcons[i] << " ";
1463 }
1464 Trace("dt-cmi") << std::endl;
1465 for( unsigned r=0; r<2; r++ ){
1466 if( neqc.isNull() ){
1467 for( unsigned i=0; i<pcons.size(); i++ ){
1468 //must try the infinite ones first
1469 bool cfinite = options::finiteModelFind() ? dt[ i ].isUFinite() : dt[ i ].isFinite();
1470 if( pcons[i] && (r==1)==cfinite ){
1471 neqc = DatatypesRewriter::getInstCons( eqc, dt, i );
1472 //for( unsigned j=0; j<neqc.getNumChildren(); j++ ){
1473 // //if( sels[i].find( j )==sels[i].end() && DatatypesRewriter::isTermDatatype( neqc[j] ) ){
1474 // if( !d_equalityEngine.hasTerm( neqc[j] ) && DatatypesRewriter::isTermDatatype( neqc[j] ) ){
1475 // nodes.push_back( neqc[j] );
1476 // }
1477 //}
1478 break;
1479 }
1480 }
1481 }
1482 }
1483 addCons = true;
1484 }
1485 if( !neqc.isNull() ){
1486 Trace("dt-cmi") << "Assign : " << neqc << std::endl;
1487 m->assertEquality( eqc, neqc, true );
1488 eqc_cons[ eqc ] = neqc;
1489 }
1490 if( addCons ){
1491 cons.push_back( neqc );
1492 }
1493 ++index;
1494 }
1495
1496 for( std::map< Node, Node >::iterator it = eqc_cons.begin(); it != eqc_cons.end(); ++it ){
1497 Node eqc = it->first;
1498 if( eqc.getType().isCodatatype() ){
1499 //until models are implemented for codatatypes
1500 //throw Exception("Models for codatatypes are not supported in this version.");
1501 //must proactive expand to avoid looping behavior in model builder
1502 if( !it->second.isNull() ){
1503 std::map< Node, int > vmap;
1504 Node v = getCodatatypesValue( it->first, eqc_cons, vmap, 0 );
1505 Trace("dt-cmi") << " EQC(" << it->first << "), constructor is " << it->second << ", value is " << v << ", const = " << v.isConst() << std::endl;
1506 m->assertEquality( eqc, v, true );
1507 m->assertRepresentative( v );
1508 }
1509 }else{
1510 Trace("dt-cmi") << "Datatypes : assert representative " << it->second << " for " << it->first << std::endl;
1511 m->assertRepresentative( it->second );
1512 }
1513 }
1514 }
1515
1516
1517 Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_cons, std::map< Node, int >& vmap, int depth ){
1518 std::map< Node, int >::iterator itv = vmap.find( n );
1519 if( itv!=vmap.end() ){
1520 int debruijn = depth - 1 - itv->second;
1521 return NodeManager::currentNM()->mkConst(UninterpretedConstant(n.getType().toType(), debruijn));
1522 }else if( DatatypesRewriter::isTermDatatype( n ) ){
1523 Node nc = eqc_cons[n];
1524 if( !nc.isNull() ){
1525 vmap[n] = depth;
1526 Trace("dt-cmi-cdt-debug") << " map " << n << " -> " << depth << std::endl;
1527 Assert( nc.getKind()==APPLY_CONSTRUCTOR );
1528 std::vector< Node > children;
1529 children.push_back( nc.getOperator() );
1530 for( unsigned i=0; i<nc.getNumChildren(); i++ ){
1531 Node r = getRepresentative( nc[i] );
1532 Node rv = getCodatatypesValue( r, eqc_cons, vmap, depth+1 );
1533 children.push_back( rv );
1534 }
1535 vmap.erase( n );
1536 return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
1537 }
1538 }
1539 return n;
1540 }
1541
1542 Node TheoryDatatypes::getSingletonLemma( TypeNode tn, bool pol ) {
1543 int index = pol ? 0 : 1;
1544 std::map< TypeNode, Node >::iterator it = d_singleton_lemma[index].find( tn );
1545 if( it==d_singleton_lemma[index].end() ){
1546 Node a;
1547 if( pol ){
1548 Node v1 = NodeManager::currentNM()->mkBoundVar( tn );
1549 Node v2 = NodeManager::currentNM()->mkBoundVar( tn );
1550 a = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, v1, v2 ), v1.eqNode( v2 ) );
1551 }else{
1552 Node v1 = NodeManager::currentNM()->mkSkolem( "k1", tn );
1553 Node v2 = NodeManager::currentNM()->mkSkolem( "k2", tn );
1554 a = v1.eqNode( v2 ).negate();
1555 //send out immediately as lemma
1556 doSendLemma( a );
1557 Trace("dt-singleton") << "******** assert " << a << " to avoid singleton cardinality for type " << tn << std::endl;
1558 }
1559 d_singleton_lemma[index][tn] = a;
1560 return a;
1561 }else{
1562 return it->second;
1563 }
1564 }
1565
1566 void TheoryDatatypes::collectTerms( Node n ) {
1567 if( d_collectTermsCache.find( n )==d_collectTermsCache.end() ){
1568 d_collectTermsCache[n] = true;
1569 for( int i=0; i<(int)n.getNumChildren(); i++ ) {
1570 collectTerms( n[i] );
1571 }
1572 if( n.getKind() == APPLY_CONSTRUCTOR ){
1573 Debug("datatypes") << " Found constructor " << n << endl;
1574 d_consTerms.push_back( n );
1575 }else{
1576
1577 if( n.getKind() == APPLY_SELECTOR_TOTAL || n.getKind() == DT_SIZE || n.getKind() == DT_HEIGHT_BOUND ){
1578 d_selTerms.push_back( n );
1579 //we must also record which selectors exist
1580 Trace("dt-collapse-sel") << " Found selector " << n << endl;
1581 Node rep = getRepresentative( n[0] );
1582 //record it in the selectors
1583 EqcInfo* eqc = getOrMakeEqcInfo( rep, true );
1584 //add it to the eqc info
1585 addSelector( n, eqc, rep );
1586
1587 if( n.getKind() == DT_SIZE ){
1588 Node conc = NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkConst( Rational(0) ), n );
1589 //must be non-negative
1590 Trace("datatypes-infer") << "DtInfer : non-negative size : " << conc << std::endl;
1591 //d_pending.push_back( conc );
1592 //d_pending_exp[ conc ] = d_true;
1593 //d_infer.push_back( conc );
1594 d_pending_lem.push_back( conc );
1595 /*
1596 //add size = 0 lemma
1597 Node nn = n.eqNode( NodeManager::currentNM()->mkConst( Rational(0) ) );
1598 std::vector< Node > children;
1599 children.push_back( nn.negate() );
1600 const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype();
1601 for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
1602 if( DatatypesRewriter::isNullaryConstructor( dt[i] ) ){
1603 Node test = DatatypesRewriter::mkTester( n[0], i, dt );
1604 children.push_back( test );
1605 }
1606 }
1607 conc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children );
1608 Trace("datatypes-infer") << "DtInfer : zero size : " << conc << std::endl;
1609 d_pending.push_back( conc );
1610 d_pending_exp[ conc ] = d_true;
1611 d_infer.push_back( conc );
1612 */
1613 }
1614
1615 if( n.getKind() == DT_HEIGHT_BOUND ){
1616 if( n[1].getConst<Rational>().isZero() ){
1617 std::vector< Node > children;
1618 const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype();
1619 for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
1620 if( DatatypesRewriter::isNullaryConstructor( dt[i] ) ){
1621 Node test = DatatypesRewriter::mkTester( n[0], i, dt );
1622 children.push_back( test );
1623 }
1624 }
1625 Node lem;
1626 if( children.empty() ){
1627 lem = n.negate();
1628 }else{
1629 lem = NodeManager::currentNM()->mkNode( IFF, n, children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ) );
1630 }
1631 Trace("datatypes-infer") << "DtInfer : zero height : " << lem << std::endl;
1632 //d_pending.push_back( lem );
1633 //d_pending_exp[ lem ] = d_true;
1634 //d_infer.push_back( lem );
1635 d_pending_lem.push_back( lem );
1636 }
1637 }
1638 }
1639 }
1640 }
1641 }
1642
1643 void TheoryDatatypes::processNewTerm( Node n ){
1644 Trace("dt-terms") << "Created term : " << n << std::endl;
1645 //see if it is rewritten to be something different
1646 Node rn = Rewriter::rewrite( n );
1647 if( rn!=n && !areEqual( rn, n ) ){
1648 Node eq = n.getType().isBoolean() ? rn.iffNode( n ) : rn.eqNode( n );
1649 d_pending.push_back( eq );
1650 d_pending_exp[ eq ] = d_true;
1651 Trace("datatypes-infer") << "DtInfer : rewrite : " << eq << std::endl;
1652 d_infer.push_back( eq );
1653 }
1654 }
1655
1656 Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index ){
1657 std::map< int, Node >::iterator it = d_inst_map[n].find( index );
1658 if( it!=d_inst_map[n].end() ){
1659 return it->second;
1660 }else{
1661 //add constructor to equivalence class
1662 Node k = getTermSkolemFor( n );
1663 Node n_ic = DatatypesRewriter::getInstCons( k, dt, index );
1664 //Assert( n_ic==Rewriter::rewrite( n_ic ) );
1665 n_ic = Rewriter::rewrite( n_ic );
1666 collectTerms( n_ic );
1667 d_equalityEngine.addTerm(n_ic);
1668 Debug("dt-enum") << "Made instantiate cons " << n_ic << std::endl;
1669 d_inst_map[n][index] = n_ic;
1670 return n_ic;
1671 }
1672 }
1673
1674 void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
1675 //add constructor to equivalence class if not done so already
1676 int index = getLabelIndex( eqc, n );
1677 if( index!=-1 && !eqc->d_inst ){
1678 if( options::dtUseTesters() ){
1679 Node exp;
1680 Node tt;
1681 if( !eqc->d_constructor.get().isNull() ){
1682 exp = d_true;
1683 tt = eqc->d_constructor;
1684 }else{
1685 exp = getLabel( n );
1686 tt = exp[0];
1687 }
1688 const Datatype& dt = ((DatatypeType)(tt.getType()).toType()).getDatatype();
1689 //must be finite or have a selector
1690 //if( eqc->d_selectors || dt[ index ].isFinite() ){
1691 //instantiate this equivalence class
1692 eqc->d_inst = true;
1693 Node tt_cons = getInstantiateCons( tt, dt, index );
1694 Node eq;
1695 if( tt!=tt_cons ){
1696 eq = tt.eqNode( tt_cons );
1697 Debug("datatypes-inst") << "DtInstantiate : " << eqc << " " << eq << std::endl;
1698 d_pending.push_back( eq );
1699 d_pending_exp[ eq ] = exp;
1700 Trace("datatypes-infer-debug") << "inst : " << eqc << " " << n << std::endl;
1701 Trace("datatypes-infer") << "DtInfer : instantiate : " << eq << " by " << exp << std::endl;
1702 //eqc->d_inst.set( eq );
1703 d_infer.push_back( eq );
1704 d_infer_exp.push_back( exp );
1705 }
1706 }else{
1707 eqc->d_inst = true;
1708 }
1709 //}
1710 //else{
1711 // Debug("datatypes-inst") << "Do not instantiate" << std::endl;
1712 //}
1713 }
1714 }
1715
1716 void TheoryDatatypes::checkCycles() {
1717 Debug("datatypes-cycle-check") << "Check cycles" << std::endl;
1718 std::vector< Node > cdt_eqc;
1719 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
1720 while( !eqcs_i.isFinished() ){
1721 Node eqc = (*eqcs_i);
1722 TypeNode tn = eqc.getType();
1723 if( DatatypesRewriter::isTypeDatatype( tn ) ) {
1724 if( !tn.isCodatatype() ){
1725 if( options::dtCyclic() ){
1726 //do cycle checks
1727 std::map< TNode, bool > visited;
1728 std::vector< TNode > expl;
1729 Node cn = searchForCycle( eqc, eqc, visited, expl );
1730 //if we discovered a different cycle while searching this one
1731 if( !cn.isNull() && cn!=eqc ){
1732 visited.clear();
1733 expl.clear();
1734 Node prev = cn;
1735 cn = searchForCycle( cn, cn, visited, expl );
1736 Assert( prev==cn );
1737 }
1738
1739 if( !cn.isNull() ) {
1740 Assert( expl.size()>0 );
1741 d_conflictNode = mkAnd( expl );
1742 Trace("dt-conflict") << "CONFLICT: Cycle conflict : " << d_conflictNode << std::endl;
1743 d_out->conflict( d_conflictNode );
1744 d_conflict = true;
1745 return;
1746 }
1747 }
1748 }else{
1749 //indexing
1750 cdt_eqc.push_back( eqc );
1751 }
1752 }
1753 ++eqcs_i;
1754 }
1755 //process codatatypes
1756 if( cdt_eqc.size()>1 && options::cdtBisimilar() ){
1757 printModelDebug("dt-cdt-debug");
1758 Trace("dt-cdt-debug") << "Process " << cdt_eqc.size() << " co-datatypes" << std::endl;
1759 std::vector< std::vector< Node > > part_out;
1760 std::vector< TNode > exp;
1761 std::map< Node, Node > cn;
1762 std::map< Node, std::map< Node, int > > dni;
1763 for( unsigned i=0; i<cdt_eqc.size(); i++ ){
1764 cn[cdt_eqc[i]] = cdt_eqc[i];
1765 }
1766 separateBisimilar( cdt_eqc, part_out, exp, cn, dni, 0, false );
1767 Trace("dt-cdt-debug") << "Done separate bisimilar." << std::endl;
1768 if( !part_out.empty() ){
1769 Trace("dt-cdt-debug") << "Process partition size " << part_out.size() << std::endl;
1770 for( unsigned i=0; i<part_out.size(); i++ ){
1771 std::vector< Node > part;
1772 part.push_back( part_out[i][0] );
1773 for( unsigned j=1; j<part_out[i].size(); j++ ){
1774 Trace("dt-cdt") << "Codatatypes : " << part_out[i][0] << " and " << part_out[i][j] << " must be equal!!" << std::endl;
1775 part.push_back( part_out[i][j] );
1776 std::vector< std::vector< Node > > tpart_out;
1777 exp.clear();
1778 cn.clear();
1779 cn[part_out[i][0]] = part_out[i][0];
1780 cn[part_out[i][j]] = part_out[i][j];
1781 dni.clear();
1782 separateBisimilar( part, tpart_out, exp, cn, dni, 0, true );
1783 Assert( tpart_out.size()==1 && tpart_out[0].size()==2 );
1784 part.pop_back();
1785 //merge based on explanation
1786 Trace("dt-cdt") << " exp is : ";
1787 for( unsigned k=0; k<exp.size(); k++ ){
1788 Trace("dt-cdt") << exp[k] << " ";
1789 }
1790 Trace("dt-cdt") << std::endl;
1791 Node eq = part_out[i][0].eqNode( part_out[i][j] );
1792 Node eqExp = mkAnd( exp );
1793 d_pending.push_back( eq );
1794 d_pending_exp[ eq ] = eqExp;
1795 Trace("datatypes-infer") << "DtInfer : cdt-bisimilar : " << eq << " by " << eqExp << std::endl;
1796 d_infer.push_back( eq );
1797 d_infer_exp.push_back( eqExp );
1798 }
1799 }
1800 }
1801 }
1802 }
1803
1804 //everything is in terms of representatives
1805 void TheoryDatatypes::separateBisimilar( std::vector< Node >& part, std::vector< std::vector< Node > >& part_out,
1806 std::vector< TNode >& exp,
1807 std::map< Node, Node >& cn,
1808 std::map< Node, std::map< Node, int > >& dni, int dniLvl, bool mkExp ){
1809 if( !mkExp ){
1810 Trace("dt-cdt-debug") << "Separate bisimilar : " << std::endl;
1811 for( unsigned i=0; i<part.size(); i++ ){
1812 Trace("dt-cdt-debug") << " " << part[i] << ", current = " << cn[part[i]] << std::endl;
1813 }
1814 }
1815 Assert( part.size()>1 );
1816 std::map< Node, std::vector< Node > > new_part;
1817 std::map< Node, std::vector< Node > > new_part_c;
1818 std::map< int, std::vector< Node > > new_part_rec;
1819
1820 std::map< Node, Node > cn_cons;
1821 for( unsigned j=0; j<part.size(); j++ ){
1822 Node c = cn[part[j]];
1823 std::map< Node, int >::iterator it_rec = dni[part[j]].find( c );
1824 if( it_rec!=dni[part[j]].end() ){
1825 //looped
1826 if( !mkExp ){ Trace("dt-cdt-debug") << " - " << part[j] << " is looping at index " << it_rec->second << std::endl; }
1827 new_part_rec[ it_rec->second ].push_back( part[j] );
1828 }else{
1829 if( DatatypesRewriter::isTermDatatype( c ) ){
1830 Node ncons = getEqcConstructor( c );
1831 if( ncons.getKind()==APPLY_CONSTRUCTOR ) {
1832 Node cc = ncons.getOperator();
1833 cn_cons[part[j]] = ncons;
1834 if( mkExp ){
1835 explainEquality( c, ncons, true, exp );
1836 }
1837 new_part[cc].push_back( part[j] );
1838 if( !mkExp ){ Trace("dt-cdt-debug") << " - " << part[j] << " is datatype " << ncons << "." << std::endl; }
1839 }else{
1840 new_part_c[c].push_back( part[j] );
1841 if( !mkExp ){ Trace("dt-cdt-debug") << " - " << part[j] << " is unspecified datatype." << std::endl; }
1842 }
1843 }else{
1844 //add equivalences
1845 if( !mkExp ){ Trace("dt-cdt-debug") << " - " << part[j] << " is term " << c << "." << std::endl; }
1846 new_part_c[c].push_back( part[j] );
1847 }
1848 }
1849 }
1850 //direct add for constants
1851 for( std::map< Node, std::vector< Node > >::iterator it = new_part_c.begin(); it != new_part_c.end(); ++it ){
1852 if( it->second.size()>1 ){
1853 std::vector< Node > vec;
1854 vec.insert( vec.begin(), it->second.begin(), it->second.end() );
1855 part_out.push_back( vec );
1856 }
1857 }
1858 //direct add for recursive
1859 for( std::map< int, std::vector< Node > >::iterator it = new_part_rec.begin(); it != new_part_rec.end(); ++it ){
1860 if( it->second.size()>1 ){
1861 std::vector< Node > vec;
1862 vec.insert( vec.begin(), it->second.begin(), it->second.end() );
1863 part_out.push_back( vec );
1864 }else{
1865 //add back : could match a datatype?
1866 }
1867 }
1868 //recurse for the datatypes
1869 for( std::map< Node, std::vector< Node > >::iterator it = new_part.begin(); it != new_part.end(); ++it ){
1870 if( it->second.size()>1 ){
1871 //set dni to check for loops
1872 std::map< Node, Node > dni_rem;
1873 for( unsigned i=0; i<it->second.size(); i++ ){
1874 Node n = it->second[i];
1875 dni[n][cn[n]] = dniLvl;
1876 dni_rem[n] = cn[n];
1877 }
1878
1879 //we will split based on the arguments of the datatype
1880 std::vector< std::vector< Node > > split_new_part;
1881 split_new_part.push_back( it->second );
1882
1883 unsigned nChildren = cn_cons[it->second[0]].getNumChildren();
1884 //for each child of constructor
1885 unsigned cindex = 0;
1886 while( cindex<nChildren && !split_new_part.empty() ){
1887 if( !mkExp ){ Trace("dt-cdt-debug") << "Split argument #" << cindex << " of " << it->first << "..." << std::endl; }
1888 std::vector< std::vector< Node > > next_split_new_part;
1889 for( unsigned j=0; j<split_new_part.size(); j++ ){
1890 //set current node
1891 for( unsigned k=0; k<split_new_part[j].size(); k++ ){
1892 Node n = split_new_part[j][k];
1893 cn[n] = getRepresentative( cn_cons[n][cindex] );
1894 if( mkExp ){
1895 explainEquality( cn[n], cn_cons[n][cindex], true, exp );
1896 }
1897 }
1898 std::vector< std::vector< Node > > c_part_out;
1899 separateBisimilar( split_new_part[j], c_part_out, exp, cn, dni, dniLvl+1, mkExp );
1900 next_split_new_part.insert( next_split_new_part.end(), c_part_out.begin(), c_part_out.end() );
1901 }
1902 split_new_part.clear();
1903 split_new_part.insert( split_new_part.end(), next_split_new_part.begin(), next_split_new_part.end() );
1904 cindex++;
1905 }
1906 part_out.insert( part_out.end(), split_new_part.begin(), split_new_part.end() );
1907
1908 for( std::map< Node, Node >::iterator it2 = dni_rem.begin(); it2 != dni_rem.end(); ++it2 ){
1909 dni[it2->first].erase( it2->second );
1910 }
1911 }
1912 }
1913 }
1914
1915 //postcondition: if cycle detected, explanation is why n is a subterm of on
1916 Node TheoryDatatypes::searchForCycle( TNode n, TNode on,
1917 std::map< TNode, bool >& visited,
1918 std::vector< TNode >& explanation, bool firstTime ) {
1919 Debug("datatypes-cycle-check") << "Search for cycle " << n << " " << on << endl;
1920 TNode ncons;
1921 TNode nn;
1922 if( !firstTime ){
1923 nn = getRepresentative( n );
1924 if( nn==on ){
1925 explainEquality( n, nn, true, explanation );
1926 return on;
1927 }
1928 }else{
1929 nn = n;
1930 }
1931 if( visited.find( nn ) == visited.end() ) {
1932 visited[nn] = true;
1933 TNode ncons = getEqcConstructor( nn );
1934 if( ncons.getKind()==APPLY_CONSTRUCTOR ) {
1935 for( int i=0; i<(int)ncons.getNumChildren(); i++ ) {
1936 TNode cn = searchForCycle( ncons[i], on, visited, explanation, false );
1937 if( cn==on ) {
1938 //if( Debug.isOn("datatypes-cycles") && !d_cycle_check.isConnectedNode( n, ncons[i] ) ){
1939 // Debug("datatypes-cycles") << "Cycle subterm: " << n << " is not -> " << ncons[i] << "!!!!" << std::endl;
1940 //}
1941 //add explanation for why the constructor is connected
1942 if( n != ncons ) {
1943 explainEquality( n, ncons, true, explanation );
1944 }
1945 return on;
1946 }else if( !cn.isNull() ){
1947 return cn;
1948 }
1949 }
1950 }
1951 visited.erase( nn );
1952 return Node::null();
1953 }else{
1954 TypeNode tn = nn.getType();
1955 if( DatatypesRewriter::isTypeDatatype( tn ) ) {
1956 if( !tn.isCodatatype() ){
1957 return nn;
1958 }
1959 }
1960 return Node::null();
1961 }
1962 }
1963
1964 bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){
1965 //the datatypes decision procedure makes "internal" inferences apart from the equality engine :
1966 // (1) Unification : C( t1...tn ) = C( s1...sn ) => ti = si
1967 // (2) Label : ~is_C1( t ) ... ~is_C{i-1}( t ) ~is_C{i+1}( t ) ... ~is_Cn( t ) => is_Ci( t )
1968 // (3) Instantiate : is_C( t ) => t = C( sel_1( t ) ... sel_n( t ) )
1969 // (4) collapse selector : S( C( t1...tn ) ) = t'
1970 // (5) collapse term size : size( C( t1...tn ) ) = 1 + size( t1 ) + ... + size( tn )
1971 // (6) non-negative size : 0 <= size( t )
1972 //We may need to communicate outwards if the conclusions involve other theories. Also communicate (6) and OR conclusions.
1973 Trace("dt-lemma-debug") << "Compute for " << exp << " => " << n << std::endl;
1974 bool addLemma = false;
1975 if( n.getKind()==EQUAL || n.getKind()==IFF ){
1976 /*
1977 for( unsigned i=0; i<2; i++ ){
1978 if( !n[i].isVar() && n[i].getKind()!=APPLY_SELECTOR_TOTAL && n[i].getKind()!=APPLY_CONSTRUCTOR ){
1979 addLemma = true;
1980 }
1981 }
1982 */
1983 TypeNode tn = n[0].getType();
1984 if( !DatatypesRewriter::isTypeDatatype( tn ) ){
1985 addLemma = true;
1986 }else{
1987 const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
1988 addLemma = dt.involvesExternalType();
1989 }
1990 //for( int j=0; j<(int)n[1].getNumChildren(); j++ ){
1991 // if( !DatatypesRewriter::isTermDatatype( n[1][j] ) ){
1992 // addLemma = true;
1993 // break;
1994 // }
1995 //}
1996 }else if( n.getKind()==LEQ ){
1997 addLemma = true;
1998 }else if( n.getKind()==OR ){
1999 addLemma = true;
2000 }
2001 if( addLemma ){
2002 //check if we have already added this lemma
2003 //if( std::find( d_inst_lemmas[ n[0] ].begin(), d_inst_lemmas[ n[0] ].end(), n[1] )==d_inst_lemmas[ n[0] ].end() ){
2004 // d_inst_lemmas[ n[0] ].push_back( n[1] );
2005 Trace("dt-lemma-debug") << "Communicate " << n << std::endl;
2006 return true;
2007 //}else{
2008 // Trace("dt-lemma-debug") << "Already communicated " << n << std::endl;
2009 // return false;
2010 //}
2011 }
2012 //else if( exp.getKind()==APPLY_TESTER ){
2013 //if( n.getKind()==EQUAL && !DatatypesRewriter::isTermDatatype( n[0] ) ){
2014 // return true;
2015 //}
2016 //}
2017 Trace("dt-lemma-debug") << "Do not need to communicate " << n << std::endl;
2018 return false;
2019 }
2020
2021 bool TheoryDatatypes::hasTerm( TNode a ){
2022 return d_equalityEngine.hasTerm( a );
2023 }
2024
2025 bool TheoryDatatypes::areEqual( TNode a, TNode b ){
2026 if( a==b ){
2027 return true;
2028 }else if( hasTerm( a ) && hasTerm( b ) ){
2029 return d_equalityEngine.areEqual( a, b );
2030 }else{
2031 return false;
2032 }
2033 }
2034
2035 bool TheoryDatatypes::areDisequal( TNode a, TNode b ){
2036 if( a==b ){
2037 return false;
2038 }else if( hasTerm( a ) && hasTerm( b ) ){
2039 return d_equalityEngine.areDisequal( a, b, false );
2040 }else{
2041 return false;
2042 }
2043 }
2044
2045 TNode TheoryDatatypes::getRepresentative( TNode a ){
2046 if( hasTerm( a ) ){
2047 return d_equalityEngine.getRepresentative( a );
2048 }else{
2049 return a;
2050 }
2051 }
2052
2053
2054 void TheoryDatatypes::printModelDebug( const char* c ){
2055 if(! (Trace.isOn(c))) {
2056 return;
2057 }
2058
2059 Trace( c ) << "Datatypes model : " << std::endl;
2060 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
2061 while( !eqcs_i.isFinished() ){
2062 Node eqc = (*eqcs_i);
2063 if( !eqc.getType().isBoolean() ){
2064 if( DatatypesRewriter::isTermDatatype( eqc ) ){
2065 Trace( c ) << "DATATYPE : ";
2066 }
2067 Trace( c ) << eqc << " : " << eqc.getType() << " : " << std::endl;
2068 Trace( c ) << " { ";
2069 //add terms to model
2070 eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
2071 while( !eqc_i.isFinished() ){
2072 if( (*eqc_i)!=eqc ){
2073 Trace( c ) << (*eqc_i) << " ";
2074 }
2075 ++eqc_i;
2076 }
2077 Trace( c ) << "}" << std::endl;
2078 if( DatatypesRewriter::isTermDatatype( eqc ) ){
2079 EqcInfo* ei = getOrMakeEqcInfo( eqc );
2080 if( ei ){
2081 Trace( c ) << " Instantiated : " << ei->d_inst.get() << std::endl;
2082 Trace( c ) << " Constructor : ";
2083 if( !ei->d_constructor.get().isNull() ){
2084 Trace( c )<< ei->d_constructor.get();
2085 }
2086 Trace( c ) << std::endl << " Labels : ";
2087 if( hasLabel( ei, eqc ) ){
2088 Trace( c ) << getLabel( eqc );
2089 }else{
2090 NodeListMap::iterator lbl_i = d_labels.find( eqc );
2091 if( lbl_i != d_labels.end() ){
2092 NodeList* lbl = (*lbl_i).second;
2093 for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ){
2094 Trace( c ) << *j << " ";
2095 }
2096 }
2097 }
2098 Trace( c ) << std::endl;
2099 Trace( c ) << " Selectors : " << ( ei->d_selectors ? "yes, " : "no " );
2100 NodeListMap::iterator sel_i = d_selector_apps.find( eqc );
2101 if( sel_i != d_selector_apps.end() ){
2102 NodeList* sel = (*sel_i).second;
2103 for( NodeList::const_iterator j = sel->begin(); j != sel->end(); j++ ){
2104 Trace( c ) << *j << " ";
2105 }
2106 }
2107 Trace( c ) << std::endl;
2108 }
2109 }
2110 }
2111 ++eqcs_i;
2112 }
2113 }
2114
2115 Node TheoryDatatypes::mkAnd( std::vector< TNode >& assumptions ) {
2116 if( assumptions.empty() ){
2117 return d_true;
2118 }else if( assumptions.size()==1 ){
2119 return assumptions[0];
2120 }else{
2121 return NodeManager::currentNM()->mkNode( AND, assumptions );
2122 }
2123 }
2124
2125 bool TheoryDatatypes::checkClashModEq( TNode n1, TNode n2, std::vector< Node >& exp, std::vector< std::pair< TNode, TNode > >& deq_cand ) {
2126 if( (n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR) ||
2127 (n1.getKind() == kind::TUPLE && n2.getKind() == kind::TUPLE) ||
2128 (n1.getKind() == kind::RECORD && n2.getKind() == kind::RECORD) ) {
2129 if( n1.getOperator() != n2.getOperator() ) {
2130 return true;
2131 } else {
2132 Assert( n1.getNumChildren() == n2.getNumChildren() );
2133 for( int i=0; i<(int)n1.getNumChildren(); i++ ) {
2134 TNode nc1 = getEqcConstructor( n1[i] );
2135 TNode nc2 = getEqcConstructor( n2[i] );
2136 if( checkClashModEq( nc1, nc2, exp, deq_cand ) ) {
2137 if( nc1!=n1[i] ){
2138 exp.push_back( nc1.eqNode( n1[i] ) );
2139 }
2140 if( nc2!=n2[i] ){
2141 exp.push_back( nc2.eqNode( n2[i] ) );
2142 }
2143 return true;
2144 }
2145 }
2146 }
2147 }else if( n1!=n2 ){
2148 if( n1.isConst() && n2.isConst() ){
2149 return true;
2150 }else{
2151 if( !areEqual( n1, n2 ) ){
2152 deq_cand.push_back( std::pair< TNode, TNode >( n1, n2 ) );
2153 }
2154 }
2155 }
2156 return false;
2157 }
2158
2159 } /* namepsace CVC4::theory::datatypes */
2160 } /* namepsace CVC4::theory */
2161 } /* namepsace CVC4 */