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