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