1 /********************* */
2 /*! \file theory_datatypes.cpp
4 ** Original author: Morgan Deters
5 ** Major contributors: Andrew Reynolds
6 ** Minor contributors (to current version): Dejan Jovanovic
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Implementation of the theory of datatypes
14 ** Implementation of the theory of datatypes.
18 #include "theory/datatypes/theory_datatypes.h"
19 #include "theory/valuation.h"
20 #include "expr/kind.h"
21 #include "util/datatype.h"
22 #include "util/cvc4_assert.h"
23 #include "theory/datatypes/datatypes_rewriter.h"
24 #include "theory/datatypes/theory_datatypes_type_rules.h"
25 #include "theory/theory_model.h"
26 #include "smt/options.h"
27 #include "smt/boolean_terms.h"
28 #include "theory/quantifiers/options.h"
29 #include "theory/datatypes/options.h"
30 #include "theory/type_enumerator.h"
36 using namespace CVC4::kind
;
37 using namespace CVC4::context
;
38 using namespace CVC4::theory
;
39 using namespace CVC4::theory::datatypes
;
42 TheoryDatatypes::TheoryDatatypes(Context
* c
, UserContext
* u
, OutputChannel
& out
, Valuation valuation
, const LogicInfo
& logicInfo
) :
43 Theory(THEORY_DATATYPES
, c
, u
, out
, valuation
, logicInfo
),
45 d_hasSeenCycle(c
, false),
49 d_equalityEngine(d_notify
, c
, "theory::datatypes::TheoryDatatypes"),
53 d_conflict( c
, false ),
54 d_collectTermsCache( c
),
58 // The kinds we are treating as function application in congruence
59 d_equalityEngine
.addFunctionKind(kind::APPLY_CONSTRUCTOR
);
60 d_equalityEngine
.addFunctionKind(kind::APPLY_SELECTOR_TOTAL
);
61 d_equalityEngine
.addFunctionKind(kind::APPLY_TESTER
);
62 d_equalityEngine
.addFunctionKind(kind::APPLY_UF
);
64 d_true
= NodeManager::currentNM()->mkConst( true );
68 TheoryDatatypes::~TheoryDatatypes() {
71 void TheoryDatatypes::setMasterEqualityEngine(eq::EqualityEngine
* eq
) {
72 d_equalityEngine
.setMasterEqualityEngine(eq
);
75 TheoryDatatypes::EqcInfo
* TheoryDatatypes::getOrMakeEqcInfo( TNode n
, bool doMake
){
76 if( !hasEqcInfo( n
) ){
79 NodeList
* lbl
= new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
80 ContextMemoryAllocator
<TNode
>(getSatContext()->getCMM()) );
81 d_labels
.insertDataFromContextMemory( n
, lbl
);
83 std::map
< Node
, EqcInfo
* >::iterator eqc_i
= d_eqc_info
.find( n
);
85 if( eqc_i
!=d_eqc_info
.end() ){
88 ei
= new EqcInfo( getSatContext() );
91 if( n
.getKind()==APPLY_CONSTRUCTOR
){
92 ei
->d_constructor
= n
;
95 NodeList
* sel
= new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
96 ContextMemoryAllocator
<TNode
>(getSatContext()->getCMM()) );
97 d_selector_apps
.insertDataFromContextMemory( n
, sel
);
103 std::map
< Node
, EqcInfo
* >::iterator eqc_i
= d_eqc_info
.find( n
);
104 return (*eqc_i
).second
;
108 TNode
TheoryDatatypes::getEqcConstructor( TNode r
) {
109 if( r
.getKind()==APPLY_CONSTRUCTOR
){
112 EqcInfo
* ei
= getOrMakeEqcInfo( r
, false );
113 if( ei
&& !ei
->d_constructor
.get().isNull() ){
114 return ei
->d_constructor
.get();
121 void TheoryDatatypes::check(Effort e
) {
122 Trace("datatypes-debug") << "Check effort " << e
<< std::endl
;
123 while(!done() && !d_conflict
) {
124 // Get all the assertions
125 Assertion assertion
= get();
126 TNode fact
= assertion
.assertion
;
127 Trace("datatypes-assert") << "Assert " << fact
<< std::endl
;
129 TNode atom CVC4_UNUSED
= fact
.getKind() == kind::NOT
? fact
[0] : fact
;
131 // extra debug check to make sure that the rewriter did its job correctly
132 Assert( atom
.getKind() != kind::EQUAL
||
133 ( atom
[0].getKind() != kind::TUPLE
&& atom
[1].getKind() != kind::TUPLE
&&
134 atom
[0].getKind() != kind::RECORD
&& atom
[1].getKind() != kind::RECORD
&&
135 atom
[0].getKind() != kind::TUPLE_UPDATE
&& atom
[1].getKind() != kind::TUPLE_UPDATE
&&
136 atom
[0].getKind() != kind::RECORD_UPDATE
&& atom
[1].getKind() != kind::RECORD_UPDATE
&&
137 atom
[0].getKind() != kind::TUPLE_SELECT
&& atom
[1].getKind() != kind::TUPLE_SELECT
&&
138 atom
[0].getKind() != kind::RECORD_SELECT
&& atom
[1].getKind() != kind::RECORD_SELECT
),
139 "tuple/record escaped into datatypes decision procedure; should have been rewritten away" );
142 assertFact( fact
, fact
);
146 if( e
== EFFORT_FULL
&& !d_conflict
) {
151 addedFact
= !d_pending
.empty() || !d_pending_merge
.empty();
159 Debug("datatypes-split") << "Check for splits " << e
<< endl
;
162 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( &d_equalityEngine
);
163 while( !eqcs_i
.isFinished() ){
165 TypeNode tn
= n
.getType();
166 if( DatatypesRewriter::isTypeDatatype( tn
) ){
167 Trace("datatypes-debug") << "Process equivalence class " << n
<< std::endl
;
168 EqcInfo
* eqc
= getOrMakeEqcInfo( n
, true );
169 //if there are more than 1 possible constructors for eqc
170 if( eqc
->d_constructor
.get().isNull() && !hasLabel( eqc
, n
) ) {
171 Trace("datatypes-debug") << "No constructor..." << std::endl
;
172 const Datatype
& dt
= ((DatatypeType
)(tn
).toType()).getDatatype();
174 std::vector
< bool > pcons
;
175 getPossibleCons( eqc
, n
, pcons
);
176 //std::cout << "pcons " << n << " = ";
177 //for( int i=0; i<(int)pcons.size(); i++ ){ //std::cout << pcons[i] << " "; }
178 //std::cout << std::endl;
179 //check if we do not need to resolve the constructor type for this equivalence class.
180 // this is if there are no selectors for this equivalence class, its possible values are infinite,
181 // and we are not producing a model, then do not split.
183 bool needSplit
= true;
184 for( unsigned int j
=0; j
<pcons
.size(); j
++ ) {
189 if( !dt
[ j
].isFinite() && !eqc
->d_selectors
) {
195 if( !needSplit
&& options::dtForceAssignment() && d_dtfCounter
%2==0 ){
196 //for the sake of termination, we must choose the constructor of a ground term
197 //NEED GUARENTEE: groundTerm should not contain any subterms of the same type
198 // TODO: this is probably not good enough, actually need fair enumeration strategy
199 if( !n
.getType().isRecord() ){ //FIXME
200 Node groundTerm
= n
.getType().mkGroundTerm();
201 if( groundTerm
.getOperator().getType().isConstructor() ){ //FIXME
202 int index
= Datatype::indexOf( groundTerm
.getOperator().toExpr() );
211 if( needSplit
&& consIndex
!=-1 ) {
212 //if only one constructor, then this term must be this constructor
213 if( dt
.getNumConstructors()==1 ){
214 Node t
= NodeManager::currentNM()->mkNode( APPLY_TESTER
, Node::fromExpr( dt
[0].getTester() ), n
);
215 d_pending
.push_back( t
);
216 d_pending_exp
[ t
] = d_true
;
217 Trace("datatypes-infer") << "DtInfer : 1-cons : " << t
<< std::endl
;
218 d_infer
.push_back( t
);
220 Node test
= NodeManager::currentNM()->mkNode( APPLY_TESTER
, Node::fromExpr( dt
[consIndex
].getTester() ), n
);
221 Trace("dt-split") << "*************Split for possible constructor " << dt
[consIndex
] << " for " << n
<< endl
;
222 test
= Rewriter::rewrite( test
);
223 NodeBuilder
<> nb(kind::OR
);
224 nb
<< test
<< test
.notNode();
226 d_out
->lemma( lemma
);
227 d_out
->requirePhase( test
, true );
231 Trace("dt-split-debug") << "Do not split constructor for " << n
<< " : " << n
.getType() << " " << dt
.getNumConstructors() << std::endl
;
235 Trace("datatypes-debug") << "Has constructor " << eqc
->d_constructor
.get() << std::endl
;
240 Trace("datatypes-debug") << "Flush pending facts..." << std::endl
;
241 addedFact
= !d_pending
.empty() || !d_pending_merge
.empty();
245 if( options::dtRewriteErrorSel() ){
246 bool innerAddedFact = false;
249 innerAddedFact = !d_pending.empty() || !d_pending_merge.empty();
251 }while( !d_conflict && innerAddedFact );
255 }while( !d_conflict
&& addedFact
);
256 Trace("datatypes-debug") << "Finished. " << d_conflict
<< std::endl
;
258 Trace("dt-model-test") << std::endl
;
259 printModelDebug("dt-model-test");
263 if( Debug
.isOn("datatypes") || Debug
.isOn("datatypes-split") ) {
264 Notice() << "TheoryDatatypes::check(): done" << endl
;
268 void TheoryDatatypes::flushPendingFacts(){
270 if( !d_pending
.empty() ){
272 while( !d_conflict
&& i
<(int)d_pending
.size() ){
273 Node fact
= d_pending
[i
];
274 Node exp
= d_pending_exp
[ fact
];
275 //check to see if we have to communicate it to the rest of the system
276 if( mustCommunicateFact( fact
, exp
) ){
277 Trace("dt-lemma-debug") << "Assert fact " << fact
<< " " << exp
<< std::endl
;
279 if( exp
.isNull() || exp
==d_true
){
282 Trace("dt-lemma-debug") << "Get explanation..." << std::endl
;
283 Node ee_exp
= explain( exp
);
284 Trace("dt-lemma-debug") << "Explanation : " << ee_exp
<< std::endl
;
285 lem
= NodeManager::currentNM()->mkNode( IMPLIES
, ee_exp
, fact
);
286 lem
= Rewriter::rewrite( lem
);
288 Trace("dt-lemma") << "Datatypes lemma : " << lem
<< std::endl
;
291 assertFact( fact
, exp
);
296 d_pending_exp
.clear();
300 void TheoryDatatypes::doPendingMerges(){
301 //do all pending merges
303 while( i
<(int)d_pending_merge
.size() ){
304 Assert( d_pending_merge
[i
].getKind()==EQUAL
|| d_pending_merge
[i
].getKind()==IFF
);
305 merge( d_pending_merge
[i
][0], d_pending_merge
[i
][1] );
308 d_pending_merge
.clear();
311 void TheoryDatatypes::assertFact( Node fact
, Node exp
){
312 Assert( d_pending_merge
.empty() );
313 bool polarity
= fact
.getKind() != kind::NOT
;
314 TNode atom
= polarity
? fact
: fact
[0];
315 if (atom
.getKind() == kind::EQUAL
) {
316 d_equalityEngine
.assertEquality( atom
, polarity
, exp
);
318 d_equalityEngine
.assertPredicate( atom
, polarity
, exp
);
321 //add to tester if applicable
322 if( atom
.getKind()==kind::APPLY_TESTER
){
323 Node rep
= getRepresentative( atom
[0] );
324 EqcInfo
* eqc
= getOrMakeEqcInfo( rep
, true );
325 addTester( fact
, eqc
, rep
);
330 void TheoryDatatypes::preRegisterTerm(TNode n
) {
331 Debug("datatypes-prereg") << "TheoryDatatypes::preRegisterTerm() " << n
<< endl
;
333 switch (n
.getKind()) {
335 // Add the trigger for equality
336 d_equalityEngine
.addTriggerEquality(n
);
338 case kind::APPLY_TESTER
:
339 // Get triggered for both equal and dis-equal
340 d_equalityEngine
.addTriggerPredicate(n
);
343 // Maybe it's a predicate
344 if (n
.getType().isBoolean()) {
345 // Get triggered for both equal and dis-equal
346 d_equalityEngine
.addTriggerPredicate(n
);
348 // Function applications/predicates
349 d_equalityEngine
.addTerm(n
);
356 Node
TheoryDatatypes::expandDefinition(LogicRequest
&logicRequest
, Node n
) {
357 switch( n
.getKind() ){
358 case kind::APPLY_SELECTOR
: {
359 Node selector
= n
.getOperator();
360 Expr selectorExpr
= selector
.toExpr();
361 Node sel
= NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL
, Node::fromExpr( selectorExpr
), n
[0] );
362 if( options::dtRewriteErrorSel() ){
365 size_t selectorIndex
= Datatype::cindexOf(selectorExpr
);
366 const Datatype
& dt
= Datatype::datatypeOf(selectorExpr
);
367 const DatatypeConstructor
& c
= dt
[selectorIndex
];
368 Expr tester
= c
.getTester();
369 Node tst
= NodeManager::currentNM()->mkNode( kind::APPLY_TESTER
, Node::fromExpr( tester
), n
[0] );
370 tst
= Rewriter::rewrite( tst
);
375 if( d_exp_def_skolem
.find( selector
)==d_exp_def_skolem
.end() ){
376 std::stringstream ss
;
377 ss
<< selector
<< "_uf";
378 d_exp_def_skolem
[ selector
] = NodeManager::currentNM()->mkSkolem( ss
.str().c_str(),
379 NodeManager::currentNM()->mkFunctionType( n
[0].getType(), n
.getType() ) );
381 Node sk
= NodeManager::currentNM()->mkNode( kind::APPLY_UF
, d_exp_def_skolem
[ selector
], n
[0] );
382 if( tst
==NodeManager::currentNM()->mkConst( false ) ){
385 n_ret
= NodeManager::currentNM()->mkNode( kind::ITE
, tst
, sel
, sk
);
388 //n_ret = Rewriter::rewrite( n_ret );
389 Trace("dt-expand") << "Expand def : " << n
<< " to " << n_ret
<< std::endl
;
401 void TheoryDatatypes::presolve() {
402 Debug("datatypes") << "TheoryDatatypes::presolve()" << endl
;
405 Node
TheoryDatatypes::ppRewrite(TNode in
) {
406 Debug("tuprec") << "TheoryDatatypes::ppRewrite(" << in
<< ")" << endl
;
408 if(in
.getKind() == kind::TUPLE_SELECT
) {
409 TypeNode t
= in
[0].getType();
410 if(t
.hasAttribute(expr::DatatypeTupleAttr())) {
411 t
= t
.getAttribute(expr::DatatypeTupleAttr());
413 TypeNode dtt
= NodeManager::currentNM()->getDatatypeForTupleRecord(t
);
414 const Datatype
& dt
= DatatypeType(dtt
.toType()).getDatatype();
415 return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL
, Node::fromExpr(dt
[0][in
.getOperator().getConst
<TupleSelect
>().getIndex()].getSelector()), in
[0]);
416 } else if(in
.getKind() == kind::RECORD_SELECT
) {
417 TypeNode t
= in
[0].getType();
418 if(t
.hasAttribute(expr::DatatypeRecordAttr())) {
419 t
= t
.getAttribute(expr::DatatypeRecordAttr());
421 TypeNode dtt
= NodeManager::currentNM()->getDatatypeForTupleRecord(t
);
422 const Datatype
& dt
= DatatypeType(dtt
.toType()).getDatatype();
423 return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL
, Node::fromExpr(dt
[0][in
.getOperator().getConst
<RecordSelect
>().getField()].getSelector()), in
[0]);
426 TypeNode t
= in
.getType();
428 // we only care about tuples and records here
429 if(in
.getKind() != kind::TUPLE
&& in
.getKind() != kind::TUPLE_UPDATE
&&
430 in
.getKind() != kind::RECORD
&& in
.getKind() != kind::RECORD_UPDATE
) {
431 if((t
.isTuple() || t
.isRecord()) && in
.hasAttribute(smt::BooleanTermAttr())) {
432 Debug("tuprec") << "should map " << in
<< " of type " << t
<< " back to " << in
.getAttribute(smt::BooleanTermAttr()).getType() << endl
;
433 Debug("tuprec") << "so " << NodeManager::currentNM()->getDatatypeForTupleRecord(t
).getDatatype() << " goes to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in
.getAttribute(smt::BooleanTermAttr()).getType()).getDatatype() << endl
;
435 Debug("tuprec") << "current datatype-tuple-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t
).getAttribute(expr::DatatypeTupleAttr()) << endl
;
436 Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in
.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr()) << endl
;
437 NodeManager::currentNM()->getDatatypeForTupleRecord(t
).setAttribute(expr::DatatypeTupleAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in
.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr()));
439 Debug("tuprec") << "current datatype-record-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t
).getAttribute(expr::DatatypeRecordAttr()) << endl
;
440 Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in
.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()) << endl
;
441 NodeManager::currentNM()->getDatatypeForTupleRecord(t
).setAttribute(expr::DatatypeRecordAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in
.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()));
445 if( in
.getKind()==EQUAL
){
447 std::vector
< Node
> rew
;
448 if( DatatypesRewriter::checkClash(in
[0], in
[1], rew
) ){
449 nn
= NodeManager::currentNM()->mkConst(false);
451 nn
= rew
.size()==0 ? d_true
:
452 ( rew
.size()==1 ? rew
[0] : NodeManager::currentNM()->mkNode( kind::AND
, rew
) );
461 if(t
.hasAttribute(expr::DatatypeTupleAttr())) {
462 t
= t
.getAttribute(expr::DatatypeTupleAttr());
463 } else if(t
.hasAttribute(expr::DatatypeRecordAttr())) {
464 t
= t
.getAttribute(expr::DatatypeRecordAttr());
467 // if the type doesn't have an associated datatype, then make one for it
468 TypeNode dtt
= (t
.isTuple() || t
.isRecord()) ? NodeManager::currentNM()->getDatatypeForTupleRecord(t
) : t
;
470 const Datatype
& dt
= DatatypeType(dtt
.toType()).getDatatype();
472 // now rewrite the expression
474 if(in
.getKind() == kind::TUPLE
|| in
.getKind() == kind::RECORD
) {
475 NodeBuilder
<> b(kind::APPLY_CONSTRUCTOR
);
476 b
<< Node::fromExpr(dt
[0].getConstructor());
477 b
.append(in
.begin(), in
.end());
479 } else if(in
.getKind() == kind::TUPLE_UPDATE
|| in
.getKind() == kind::RECORD_UPDATE
) {
480 NodeBuilder
<> b(kind::APPLY_CONSTRUCTOR
);
481 b
<< Node::fromExpr(dt
[0].getConstructor());
482 size_t size
, updateIndex
;
483 if(in
.getKind() == kind::TUPLE_UPDATE
) {
484 size
= t
.getNumChildren();
485 updateIndex
= in
.getOperator().getConst
<TupleUpdate
>().getIndex();
486 } else { // kind::RECORD_UPDATE
487 const Record
& record
= t
.getConst
<Record
>();
488 size
= record
.getNumFields();
489 updateIndex
= record
.getIndex(in
.getOperator().getConst
<RecordUpdate
>().getField());
491 Debug("tuprec") << "expr is " << in
<< std::endl
;
492 Debug("tuprec") << "updateIndex is " << updateIndex
<< std::endl
;
493 Debug("tuprec") << "t is " << t
<< std::endl
;
494 Debug("tuprec") << "t has arity " << size
<< std::endl
;
495 for(size_t i
= 0; i
< size
; ++i
) {
496 if(i
== updateIndex
) {
498 Debug("tuprec") << "arg " << i
<< " gets updated to " << in
[1] << std::endl
;
500 b
<< NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL
, Node::fromExpr(dt
[0][i
].getSelector()), in
[0]);
501 Debug("tuprec") << "arg " << i
<< " copies " << b
[b
.getNumChildren() - 1] << std::endl
;
504 Debug("tuprec") << "builder says " << b
<< std::endl
;
511 Debug("tuprec") << "REWROTE " << in
<< " to " << n
<< std::endl
;
516 void TheoryDatatypes::addSharedTerm(TNode t
) {
517 Debug("datatypes") << "TheoryDatatypes::addSharedTerm(): "
518 << t
<< " " << t
.getType().isBoolean() << endl
;
519 if( t
.getType().isBoolean() ){
520 //d_equalityEngine.addTriggerPredicate(t, THEORY_DATATYPES);
522 d_equalityEngine
.addTriggerTerm(t
, THEORY_DATATYPES
);
524 Debug("datatypes") << "TheoryDatatypes::addSharedTerm() finished" << std::endl
;
528 void TheoryDatatypes::propagate(Effort effort
){
533 bool TheoryDatatypes::propagate(TNode literal
){
534 Debug("dt::propagate") << "TheoryDatatypes::propagate(" << literal
<< ")" << std::endl
;
535 // If already in conflict, no more propagation
537 Debug("dt::propagate") << "TheoryDatatypes::propagate(" << literal
<< "): already in conflict" << std::endl
;
540 Trace("dt-prop") << "dtPropagate " << literal
<< std::endl
;
542 bool ok
= d_out
->propagate(literal
);
549 void TheoryDatatypes::addAssumptions( std::vector
<TNode
>& assumptions
, std::vector
<TNode
>& tassumptions
) {
550 for( unsigned i
=0; i
<tassumptions
.size(); i
++ ){
551 if( std::find( assumptions
.begin(), assumptions
.end(), tassumptions
[i
] )==assumptions
.end() ){
552 assumptions
.push_back( tassumptions
[i
] );
557 void TheoryDatatypes::explainEquality( TNode a
, TNode b
, bool polarity
, std::vector
<TNode
>& assumptions
) {
559 std::vector
<TNode
> tassumptions
;
560 d_equalityEngine
.explainEquality(a
, b
, polarity
, tassumptions
);
561 addAssumptions( assumptions
, tassumptions
);
565 void TheoryDatatypes::explainPredicate( TNode p
, bool polarity
, std::vector
<TNode
>& assumptions
) {
566 std::vector
<TNode
> tassumptions
;
567 d_equalityEngine
.explainPredicate(p
, polarity
, tassumptions
);
568 addAssumptions( assumptions
, tassumptions
);
572 void TheoryDatatypes::explain(TNode literal
, std::vector
<TNode
>& assumptions
){
573 Debug("datatypes-explain") << "Explain " << literal
<< std::endl
;
574 bool polarity
= literal
.getKind() != kind::NOT
;
575 TNode atom
= polarity
? literal
: literal
[0];
576 if (atom
.getKind() == kind::EQUAL
|| atom
.getKind() == kind::IFF
) {
577 explainEquality( atom
[0], atom
[1], polarity
, assumptions
);
578 } else if( atom
.getKind() == kind::AND
&& polarity
){
579 for( unsigned i
=0; i
<atom
.getNumChildren(); i
++ ){
580 explain( atom
[i
], assumptions
);
583 Assert( atom
.getKind()!=kind::AND
);
584 explainPredicate( atom
, polarity
, assumptions
);
588 Node
TheoryDatatypes::explain( TNode literal
){
589 std::vector
< TNode
> assumptions
;
590 explain( literal
, assumptions
);
591 return mkAnd( assumptions
);
594 Node
TheoryDatatypes::explain( std::vector
< Node
>& lits
) {
595 std::vector
< TNode
> assumptions
;
596 for( unsigned i
=0; i
<lits
.size(); i
++ ){
597 explain( lits
[i
], assumptions
);
599 return mkAnd( assumptions
);
602 /** Conflict when merging two constants */
603 void TheoryDatatypes::conflict(TNode a
, TNode b
){
604 if (a
.getKind() == kind::CONST_BOOLEAN
) {
605 d_conflictNode
= explain( a
.iffNode(b
) );
607 d_conflictNode
= explain( a
.eqNode(b
) );
609 Trace("dt-conflict") << "CONFLICT: Eq engine conflict : " << d_conflictNode
<< std::endl
;
610 d_out
->conflict( d_conflictNode
);
614 /** called when a new equivalance class is created */
615 void TheoryDatatypes::eqNotifyNewClass(TNode t
){
616 if( t
.getKind()==APPLY_CONSTRUCTOR
){
617 getOrMakeEqcInfo( t
, true );
618 //look at all equivalence classes with constructor terms
620 for( BoolMap::const_iterator it = d_consEqc.begin(); it != d_consEqc.end(); ++it ){
622 TNode r = (*it).first;
623 if( r.getType()==t.getType() ){
624 EqcInfo * ei = getOrMakeEqcInfo( r, false );
625 if( ei && !ei->d_constructor.get().isNull() && ei->d_constructor.get().getOperator()!=t.getOperator() ){
626 Node deq = ei->d_constructor.get().eqNode( t ).negate();
627 d_pending.push_back( deq );
628 d_pending_exp[ deq ] = d_true;
629 Trace("datatypes-infer") << "DtInfer : diff constructor : " << deq << std::endl;
630 d_infer.push_back( deq );
640 /** called when two equivalance classes will merge */
641 void TheoryDatatypes::eqNotifyPreMerge(TNode t1
, TNode t2
){
645 /** called when two equivalance classes have merged */
646 void TheoryDatatypes::eqNotifyPostMerge(TNode t1
, TNode t2
){
647 if( DatatypesRewriter::isTermDatatype( t1
) ){
648 d_pending_merge
.push_back( t1
.eqNode( t2
) );
652 void TheoryDatatypes::merge( Node t1
, Node t2
){
656 Debug("datatypes-debug") << "Merge " << t1
<< " " << t2
<< std::endl
;
657 EqcInfo
* eqc2
= getOrMakeEqcInfo( t2
);
659 bool checkInst
= false;
660 if( !eqc2
->d_constructor
.get().isNull() ){
661 trep2
= eqc2
->d_constructor
.get();
663 EqcInfo
* eqc1
= getOrMakeEqcInfo( t1
);
665 if( !eqc1
->d_constructor
.get().isNull() ){
666 trep1
= eqc1
->d_constructor
.get();
669 TNode cons1
= eqc1
->d_constructor
.get();
670 TNode cons2
= eqc2
->d_constructor
.get();
671 //if both have constructor, then either clash or unification
672 if( !cons1
.isNull() && !cons2
.isNull() ){
673 Debug("datatypes-debug") << "Constructors : " << cons1
<< " " << cons2
<< std::endl
;
674 Node unifEq
= cons1
.eqNode( cons2
);
676 std::vector
< Node
> exp
;
677 std::vector
< std::pair
< TNode
, TNode
> > deq_cand
;
678 bool conf
= checkClashModEq( cons1
, cons2
, exp
, deq_cand
);
680 for( unsigned i
=0; i
<deq_cand
.size(); i
++ ){
681 if( d_equalityEngine
.areDisequal( deq_cand
[i
].first
, deq_cand
[i
].second
, true ) ){
683 Node eq
= NodeManager::currentNM()->mkNode( deq_cand
[i
].first
.getType().isBoolean() ? kind::IFF
: kind::EQUAL
,
684 deq_cand
[i
].first
, deq_cand
[i
].second
);
685 exp
.push_back( eq
.negate() );
690 exp
.push_back( unifEq
);
691 d_conflictNode
= explain( exp
);
693 std::vector
< Node
> rew
;
694 if( DatatypesRewriter::checkClash( cons1
, cons2
, rew
) ){
695 d_conflictNode
= explain( unifEq
);
697 Trace("dt-conflict") << "CONFLICT: Clash conflict : " << d_conflictNode
<< std::endl
;
698 d_out
->conflict( d_conflictNode
);
704 for( int i
=0; i
<(int)cons1
.getNumChildren(); i
++ ) {
705 if( !areEqual( cons1
[i
], cons2
[i
] ) ){
706 Node eq
= cons1
[i
].getType().isBoolean() ? cons1
[i
].iffNode( cons2
[i
] ) : cons1
[i
].eqNode( cons2
[i
] );
707 d_pending
.push_back( eq
);
708 d_pending_exp
[ eq
] = unifEq
;
709 Trace("datatypes-infer") << "DtInfer : cons-inj : " << eq
<< " by " << unifEq
<< std::endl
;
710 d_infer
.push_back( eq
);
711 d_infer_exp
.push_back( unifEq
);
715 for( unsigned i=0; i<rew.size(); i++ ){
716 d_pending.push_back( rew[i] );
717 d_pending_exp[ rew[i] ] = unifEq;
718 Trace("datatypes-infer") << "DtInfer : cons-inj : " << rew[i] << " by " << unifEq << std::endl;
719 d_infer.push_back( rew[i] );
720 d_infer_exp.push_back( unifEq );
725 if( !eqc1
->d_inst
&& eqc2
->d_inst
){
728 if( !cons2
.isNull() ){
729 if( cons1
.isNull() ){
730 Debug("datatypes-debug") << "Must check if it is okay to set the constructor." << std::endl
;
732 addConstructor( eqc2
->d_constructor
.get(), eqc1
, t1
);
736 d_consEqc
[t1
] = true;
738 d_consEqc
[t2
] = false;
741 Debug("datatypes-debug") << "No eqc info for " << t1
<< ", must create" << std::endl
;
742 //just copy the equivalence class information
743 eqc1
= getOrMakeEqcInfo( t1
, true );
744 eqc1
->d_inst
.set( eqc2
->d_inst
);
745 eqc1
->d_constructor
.set( eqc2
->d_constructor
);
746 eqc1
->d_selectors
.set( eqc2
->d_selectors
);
751 NodeListMap::iterator lbl_i
= d_labels
.find( t2
);
752 if( lbl_i
!= d_labels
.end() ){
753 Debug("datatypes-debug") << "Merge labels from " << eqc2
<< " " << t2
<< std::endl
;
754 NodeList
* lbl
= (*lbl_i
).second
;
755 for( NodeList::const_iterator j
= lbl
->begin(); j
!= lbl
->end(); ++j
){
756 addTester( *j
, eqc1
, t1
);
758 Debug("datatypes-debug") << "Conflict!" << std::endl
;
764 if( !eqc1
->d_selectors
&& eqc2
->d_selectors
){
765 eqc1
->d_selectors
= true;
768 NodeListMap::iterator sel_i
= d_selector_apps
.find( t2
);
769 if( sel_i
!= d_selector_apps
.end() ){
770 Debug("datatypes-debug") << "Merge selectors from " << eqc2
<< " " << t2
<< std::endl
;
771 NodeList
* sel
= (*sel_i
).second
;
772 for( NodeList::const_iterator j
= sel
->begin(); j
!= sel
->end(); ++j
){
773 addSelector( *j
, eqc1
, t1
, eqc2
->d_constructor
.get().isNull() );
777 instantiate( eqc1
, t1
);
783 //add this to the transitive closure module
786 if( trep1
.getKind()!=APPLY_CONSTRUCTOR
&& trep2
.getKind()==APPLY_CONSTRUCTOR
){
791 bool result = d_cycle_check.addEdgeNode( oldRep, newRep );
792 //d_hasSeenCycle.set( d_hasSeenCycle.get() || result );
793 Debug("datatypes-cycles") << "DtCyc: Equal " << oldRep << " -> " << newRep << " " << result << " " << d_hasSeenCycle.get() << endl;
797 Debug("datatypes-cycles-find") << "Cycle found." << std::endl;
800 Debug("datatypes-cycles-find") << "WARNING : no cycle found." << std::endl;
801 d_cycle_check.debugPrint();
808 /** called when two equivalence classes are made disequal */
809 void TheoryDatatypes::eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
){
813 TheoryDatatypes::EqcInfo::EqcInfo( context::Context
* c
) :
814 d_inst( c
, false ), d_constructor( c
, Node::null() ), d_selectors( c
, false ){
818 bool TheoryDatatypes::hasLabel( EqcInfo
* eqc
, Node n
){
819 return !eqc
->d_constructor
.get().isNull() || !getLabel( n
).isNull();
822 Node
TheoryDatatypes::getLabel( Node n
) {
823 NodeListMap::iterator lbl_i
= d_labels
.find( n
);
824 if( lbl_i
!= d_labels
.end() ){
825 NodeList
* lbl
= (*lbl_i
).second
;
826 if( !(*lbl
).empty() && (*lbl
)[ (*lbl
).size() - 1 ].getKind()==kind::APPLY_TESTER
){
827 return (*lbl
)[ (*lbl
).size() - 1 ];
833 int TheoryDatatypes::getLabelIndex( EqcInfo
* eqc
, Node n
){
834 if( !eqc
->d_constructor
.get().isNull() ){
835 return Datatype::indexOf( eqc
->d_constructor
.get().getOperator().toExpr() );
837 return Datatype::indexOf( getLabel( n
).getOperator().toExpr() );
841 void TheoryDatatypes::getPossibleCons( EqcInfo
* eqc
, Node n
, std::vector
< bool >& pcons
){
842 const Datatype
& dt
= ((DatatypeType
)(n
.getType()).toType()).getDatatype();
843 pcons
.resize( dt
.getNumConstructors(), !hasLabel( eqc
, n
) );
844 if( hasLabel( eqc
, n
) ){
845 pcons
[ getLabelIndex( eqc
, n
) ] = true;
847 NodeListMap::iterator lbl_i
= d_labels
.find( n
);
848 if( lbl_i
!= d_labels
.end() ){
849 NodeList
* lbl
= (*lbl_i
).second
;
850 for( NodeList::const_iterator i
= lbl
->begin(); i
!= lbl
->end(); i
++ ) {
851 Assert( (*i
).getKind()==NOT
);
852 pcons
[ Datatype::indexOf( (*i
)[0].getOperator().toExpr() ) ] = false;
858 void TheoryDatatypes::addTester( Node t
, EqcInfo
* eqc
, Node n
){
859 Debug("datatypes-debug") << "Add tester : " << t
<< " to eqc(" << n
<< ")" << std::endl
;
860 Debug("datatypes-labels") << "Add tester " << t
<< " " << n
<< " " << eqc
<< std::endl
;
861 bool tpolarity
= t
.getKind()!=NOT
;
862 Node tt
= ( t
.getKind() == NOT
) ? t
[0] : t
;
863 int ttindex
= Datatype::indexOf( tt
.getOperator().toExpr() );
865 bool makeConflict
= false;
866 if( hasLabel( eqc
, n
) ){
867 //if we already know the constructor type, check whether it is in conflict or redundant
868 int jtindex
= getLabelIndex( eqc
, n
);
869 if( (jtindex
==ttindex
)!=tpolarity
){
870 if( !eqc
->d_constructor
.get().isNull() ){
871 //conflict because equivalence class contains a constructor
872 std::vector
< TNode
> assumptions
;
873 explain( t
, assumptions
);
874 explainEquality( eqc
->d_constructor
.get(), tt
[0], true, assumptions
);
875 d_conflictNode
= mkAnd( assumptions
);
876 Trace("dt-conflict") << "CONFLICT: Tester eq conflict : " << d_conflictNode
<< std::endl
;
877 d_out
->conflict( d_conflictNode
);
882 //conflict because the existing label is contradictory
890 //otherwise, scan list of labels
891 NodeListMap::iterator lbl_i
= d_labels
.find( n
);
892 Assert( lbl_i
!= d_labels
.end() );
893 NodeList
* lbl
= (*lbl_i
).second
;
894 for( NodeList::const_iterator i
= lbl
->begin(); i
!= lbl
->end(); i
++ ) {
895 Assert( (*i
).getKind()==NOT
);
898 int jtindex
= Datatype::indexOf( jt
.getOperator().toExpr() );
899 if( jtindex
==ttindex
){
900 if( tpolarity
){ //we are in conflict
903 }else{ //it is redundant
909 Debug("datatypes-labels") << "Add to labels " << t
<< std::endl
;
911 const Datatype
& dt
= ((DatatypeType
)(tt
[0].getType()).toType()).getDatatype();
912 Debug("datatypes-labels") << "Labels at " << lbl
->size() << " / " << dt
.getNumConstructors() << std::endl
;
914 instantiate( eqc
, n
);
916 //check if we have reached the maximum number of testers
917 // in this case, add the positive tester
918 if( lbl
->size()==dt
.getNumConstructors()-1 ){
919 std::vector
< bool > pcons
;
920 getPossibleCons( eqc
, n
, pcons
);
921 int testerIndex
= -1;
922 for( int i
=0; i
<(int)pcons
.size(); i
++ ) {
928 Assert( testerIndex
!=-1 );
929 //we must explain why each term in the set of testers for this equivalence class is equal
930 std::vector
< Node
> eq_terms
;
931 NodeBuilder
<> nb(kind::AND
);
932 for( NodeList::const_iterator i
= lbl
->begin(); i
!= lbl
->end(); i
++ ) {
934 if( std::find( eq_terms
.begin(), eq_terms
.end(), (*i
)[0][0] )==eq_terms
.end() ){
935 eq_terms
.push_back( (*i
)[0][0] );
936 if( (*i
)[0][0]!=tt
[0] ){
937 nb
<< (*i
)[0][0].eqNode( tt
[0] );
941 Node t_concl
= NodeManager::currentNM()->mkNode( APPLY_TESTER
, Node::fromExpr( dt
[unsigned(testerIndex
)].getTester() ), tt
[0] );
942 Node t_concl_exp
= ( nb
.getNumChildren() == 1 ) ? nb
.getChild( 0 ) : nb
;
943 d_pending
.push_back( t_concl
);
944 d_pending_exp
[ t_concl
] = t_concl_exp
;
945 Trace("datatypes-infer") << "DtInfer : label : " << t_concl
<< " by " << t_concl_exp
<< std::endl
;
946 d_infer
.push_back( t_concl
);
947 d_infer_exp
.push_back( t_concl_exp
);
955 Debug("datatypes-labels") << "Explain " << j
<< " " << t
<< std::endl
;
956 std::vector
< TNode
> assumptions
;
957 explain( j
, assumptions
);
958 explain( t
, assumptions
);
959 explainEquality( jt
[0], tt
[0], true, assumptions
);
960 d_conflictNode
= mkAnd( assumptions
);
961 Trace("dt-conflict") << "CONFLICT: Tester conflict : " << d_conflictNode
<< std::endl
;
962 d_out
->conflict( d_conflictNode
);
966 void TheoryDatatypes::addSelector( Node s
, EqcInfo
* eqc
, Node n
, bool assertFacts
) {
967 Debug("datatypes-debug") << "Add selector : " << s
<< " to eqc(" << n
<< ")" << std::endl
;
968 //check to see if it is redundant
969 NodeListMap::iterator sel_i
= d_selector_apps
.find( n
);
970 Assert( sel_i
!= d_selector_apps
.end() );
971 if( sel_i
!= d_selector_apps
.end() ){
972 NodeList
* sel
= (*sel_i
).second
;
973 for( NodeList::const_iterator j
= sel
->begin(); j
!= sel
->end(); ++j
){
975 if( s
.getOperator()==ss
.getOperator() ){
979 //add it to the vector
981 eqc
->d_selectors
= true;
983 if( assertFacts
&& !eqc
->d_constructor
.get().isNull() ){
984 //conclude the collapsed merge
985 collapseSelector( s
, eqc
->d_constructor
.get() );
989 void TheoryDatatypes::addConstructor( Node c
, EqcInfo
* eqc
, Node n
){
990 Debug("datatypes-debug") << "Add constructor : " << c
<< " to eqc(" << n
<< ")" << std::endl
;
991 Assert( eqc
->d_constructor
.get().isNull() );
993 NodeListMap::iterator lbl_i
= d_labels
.find( n
);
994 if( lbl_i
!= d_labels
.end() ){
995 size_t constructorIndex
= Datatype::indexOf(c
.getOperator().toExpr());
996 NodeList
* lbl
= (*lbl_i
).second
;
997 for( NodeList::const_iterator i
= lbl
->begin(); i
!= lbl
->end(); i
++ ) {
998 if( (*i
).getKind()==NOT
){
999 if( Datatype::indexOf( (*i
)[0].getOperator().toExpr() )==constructorIndex
){
1001 std::vector
< TNode
> assumptions
;
1002 explain( *i
, assumptions
);
1003 explainEquality( c
, (*i
)[0][0], true, assumptions
);
1004 d_conflictNode
= mkAnd( assumptions
);
1005 Trace("dt-conflict") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode
<< std::endl
;
1006 d_out
->conflict( d_conflictNode
);
1014 NodeListMap::iterator sel_i
= d_selector_apps
.find( n
);
1015 if( sel_i
!= d_selector_apps
.end() ){
1016 NodeList
* sel
= (*sel_i
).second
;
1017 for( NodeList::const_iterator j
= sel
->begin(); j
!= sel
->end(); ++j
){
1018 //collapse the selector
1019 collapseSelector( *j
, c
);
1022 eqc
->d_constructor
.set( c
);
1025 void TheoryDatatypes::collapseSelector( Node s
, Node c
) {
1026 Node r
= NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL
, s
.getOperator(), c
);
1027 Node rr
= Rewriter::rewrite( r
);
1029 //Node eq_exp = NodeManager::currentNM()->mkConst(true);
1030 //Node eq = r.getType().isBoolean() ? r.iffNode( rr ) : r.eqNode( rr );
1032 Node eq_exp
= c
.eqNode( s
[0] );
1033 Node eq
= rr
.getType().isBoolean() ? s
.iffNode( rr
) : s
.eqNode( rr
);
1036 d_pending
.push_back( eq
);
1037 d_pending_exp
[ eq
] = eq_exp
;
1038 Trace("datatypes-infer") << "DtInfer : collapse sel : " << eq
<< " by " << eq_exp
<< std::endl
;
1039 d_infer
.push_back( eq
);
1040 d_infer_exp
.push_back( eq_exp
);
1044 EqualityStatus
TheoryDatatypes::getEqualityStatus(TNode a
, TNode b
){
1045 if( d_equalityEngine
.hasTerm(a
) && d_equalityEngine
.hasTerm(b
) ){
1046 if (d_equalityEngine
.areEqual(a
, b
)) {
1047 // The terms are implied to be equal
1048 return EQUALITY_TRUE
;
1050 if (d_equalityEngine
.areDisequal(a
, b
, false)) {
1051 // The terms are implied to be dis-equal
1052 return EQUALITY_FALSE
;
1055 return EQUALITY_UNKNOWN
;
1058 void TheoryDatatypes::computeCareGraph(){
1059 Trace("dt-cg") << "Compute graph for dt..." << std::endl
;
1060 vector
< pair
<TNode
, TNode
> > currentPairs
;
1061 for( unsigned r
=0; r
<2; r
++ ){
1062 unsigned functionTerms
= r
==0 ? d_consTerms
.size() : d_selTerms
.size();
1063 for( unsigned i
=0; i
<functionTerms
; i
++ ){
1064 TNode f1
= r
==0 ? d_consTerms
[i
] : d_selTerms
[i
];
1065 for( unsigned j
=i
+1; j
<functionTerms
; j
++ ){
1066 TNode f2
= r
==0 ? d_consTerms
[j
] : d_selTerms
[j
];
1067 if( f1
.getOperator()==f2
.getOperator() && !areEqual( f1
, f2
) ){
1068 Trace("dt-cg") << "Check " << f1
<< " and " << f2
<< std::endl
;
1069 bool somePairIsDisequal
= false;
1070 currentPairs
.clear();
1071 for (unsigned k
= 0; k
< f1
.getNumChildren(); ++ k
) {
1074 if( areDisequal(x
, y
) ){
1075 somePairIsDisequal
= true;
1077 }else if( !areEqual( x
, y
) ){
1078 Trace("dt-cg") << "Arg #" << k
<< " is " << x
<< " " << y
<< std::endl
;
1079 //check if they are definately disequal
1080 bool defDiseq
= false;
1082 TNode rx = getRepresentative( x );
1083 EqcInfo* eix = getOrMakeEqcInfo( rx, false );
1085 TNode ry = getRepresentative( y );
1086 EqcInfo* eiy = getOrMakeEqcInfo( ry, false );
1088 if( !eix->d_constructor.get().isNull() && !eiy->d_constructor.get().isNull() ){
1089 defDiseq = eix->d_constructor.get().getOperator()!=eiy->d_constructor.get().getOperator();
1095 if( !defDiseq
&& d_equalityEngine
.isTriggerTerm(x
, THEORY_UF
) && d_equalityEngine
.isTriggerTerm(y
, THEORY_UF
) ){
1096 EqualityStatus eqStatus
= d_valuation
.getEqualityStatus(x
, y
);
1097 if( eqStatus
!=EQUALITY_UNKNOWN
){
1098 TNode x_shared
= d_equalityEngine
.getTriggerTermRepresentative(x
, THEORY_DATATYPES
);
1099 TNode y_shared
= d_equalityEngine
.getTriggerTermRepresentative(y
, THEORY_DATATYPES
);
1100 Trace("dt-cg") << "Arg #" << k
<< " shared term is " << x_shared
<< " " << y_shared
<< std::endl
;
1101 currentPairs
.push_back(make_pair(x_shared
, y_shared
));
1106 if (!somePairIsDisequal
) {
1107 for (unsigned c
= 0; c
< currentPairs
.size(); ++ c
) {
1108 Trace("dt-cg-pair") << "Pair : " << currentPairs
[c
].first
<< " " << currentPairs
[c
].second
<< std::endl
;
1109 addCarePair(currentPairs
[c
].first
, currentPairs
[c
].second
);
1116 Trace("dt-cg") << "Done Compute graph for dt." << std::endl
;
1119 void TheoryDatatypes::collectModelInfo( TheoryModel
* m
, bool fullModel
){
1120 Trace("dt-cmi") << "Datatypes : Collect model info " << d_equalityEngine
.consistent() << std::endl
;
1121 Trace("dt-model") << std::endl
;
1122 printModelDebug( "dt-model" );
1123 Trace("dt-model") << std::endl
;
1126 bool eq_merged = false;
1127 std::vector< Node > all_eqc;
1128 eq::EqClassesIterator eqcs1_i = eq::EqClassesIterator( &d_equalityEngine );
1129 while( !eqcs1_i.isFinished() ){
1130 Node eqc = (*eqcs1_i);
1131 all_eqc.push_back( eqc );
1134 //check if equivalence classes have merged
1135 for( unsigned i=0; i<all_eqc.size(); i++ ){
1136 for( unsigned j=(i+1); j<all_eqc.size(); j++ ){
1137 if( m->areEqual( all_eqc[i], all_eqc[j] ) ){
1138 Trace("dt-cmi") << "Pre-already forced equal : " << all_eqc[i] << " = " << all_eqc[j] << std::endl;
1143 Assert( !eq_merged );
1146 //combine the equality engine
1147 m
->assertEqualityEngine( &d_equalityEngine
);
1150 //check again if equivalence classes have merged
1151 for( unsigned i=0; i<all_eqc.size(); i++ ){
1152 for( unsigned j=(i+1); j<all_eqc.size(); j++ ){
1153 if( m->areEqual( all_eqc[i], all_eqc[j] ) ){
1154 Trace("dt-cmi") << "Already forced equal : " << all_eqc[i] << " = " << all_eqc[j] << std::endl;
1159 Assert( !eq_merged );
1162 //get all constructors
1163 eq::EqClassesIterator eqccs_i
= eq::EqClassesIterator( &d_equalityEngine
);
1164 std::vector
< Node
> cons
;
1165 std::vector
< Node
> nodes
;
1166 std::map
< Node
, Node
> eqc_cons
;
1167 while( !eqccs_i
.isFinished() ){
1168 Node eqc
= (*eqccs_i
);
1169 //for all equivalence classes that are datatypes
1170 if( DatatypesRewriter::isTermDatatype( eqc
) ){
1171 EqcInfo
* ei
= getOrMakeEqcInfo( eqc
);
1172 if( !ei
->d_constructor
.get().isNull() ){
1173 cons
.push_back( ei
->d_constructor
.get() );
1174 eqc_cons
[ eqc
] = ei
->d_constructor
.get();
1176 nodes
.push_back( eqc
);
1182 //unsigned orig_size = nodes.size();
1183 std::map
< TypeNode
, int > typ_enum_map
;
1184 std::vector
< TypeEnumerator
> typ_enum
;
1186 while( index
<nodes
.size() ){
1187 Node eqc
= nodes
[index
];
1189 bool addCons
= false;
1190 const Datatype
& dt
= ((DatatypeType
)(eqc
.getType()).toType()).getDatatype();
1191 if( !d_equalityEngine
.hasTerm( eqc
) ){
1192 if( !dt
.isCodatatype() ){
1193 Trace("dt-cmi") << "NOTICE : Datatypes: need to assign constructor for " << eqc
<< std::endl
;
1194 Trace("dt-cmi") << " Type : " << eqc
.getType() << std::endl
;
1195 TypeNode tn
= eqc
.getType();
1196 //if it is infinite, make sure it is fresh
1197 if( eqc
.getType().getCardinality().isInfinite() ){
1198 std::map
< TypeNode
, int >::iterator it
= typ_enum_map
.find( tn
);
1200 if( it
==typ_enum_map
.end() ){
1201 teIndex
= (int)typ_enum
.size();
1202 typ_enum_map
[tn
] = teIndex
;
1203 typ_enum
.push_back( TypeEnumerator(tn
) );
1205 teIndex
= it
->second
;
1210 Assert( !typ_enum
[teIndex
].isFinished() );
1211 neqc
= *typ_enum
[teIndex
];
1212 Trace("dt-cmi-debug") << "Try " << neqc
<< " ... " << std::endl
;
1213 ++typ_enum
[teIndex
];
1214 for( unsigned i
=0; i
<cons
.size(); i
++ ){
1215 //check if it is modulo equality the same
1216 if( cons
[i
].getOperator()==neqc
.getOperator() ){
1218 for( unsigned j
=0; j
<cons
[i
].getNumChildren(); j
++ ){
1219 if( !m
->areEqual( cons
[i
][j
], neqc
[j
] ) ){
1225 Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons
[i
] << std::endl
;
1233 TypeEnumerator
te(tn
);
1238 Trace("dt-cmi") << "NOTICE : Datatypes: no constructor in equivalence class " << eqc
<< std::endl
;
1239 Trace("dt-cmi") << " Type : " << eqc
.getType() << std::endl
;
1240 EqcInfo
* ei
= getOrMakeEqcInfo( eqc
);
1241 std::vector
< bool > pcons
;
1242 getPossibleCons( ei
, eqc
, pcons
);
1243 Trace("dt-cmi") << "Possible constructors : ";
1244 for( unsigned i
=0; i
<pcons
.size(); i
++ ){
1245 Trace("dt-cmi") << pcons
[i
] << " ";
1247 Trace("dt-cmi") << std::endl
;
1249 std::map< int, std::map< int, bool > > sels;
1250 Trace("dt-cmi") << "Existing selectors : ";
1251 NodeListMap::iterator sel_i = d_selector_apps.find( eqc );
1252 if( sel_i != d_selector_apps.end() ){
1253 NodeList* sel = (*sel_i).second;
1254 for( NodeList::const_iterator j = sel->begin(); j != sel->end(); j++ ){
1255 Expr selectorExpr = (*j).getOperator().toExpr();
1256 unsigned cindex = Datatype::cindexOf( selectorExpr );
1257 unsigned index = Datatype::indexOf( selectorExpr );
1258 sels[cindex][index] = true;
1259 Trace("dt-cmi") << (*j) << " (" << cindex << ", " << index << ") ";
1262 Trace("dt-cmi") << std::endl;
1264 for( unsigned r
=0; r
<2; r
++ ){
1265 if( neqc
.isNull() ){
1266 for( unsigned i
=0; i
<pcons
.size(); i
++ ){
1267 //must try the infinite ones first
1268 if( pcons
[i
] && (r
==1)==dt
[ i
].isFinite() ){
1269 neqc
= getInstantiateCons( eqc
, dt
, i
, false, false );
1270 for( unsigned j
=0; j
<neqc
.getNumChildren(); j
++ ){
1271 //if( sels[i].find( j )==sels[i].end() && DatatypesRewriter::isTermDatatype( neqc[j] ) ){
1272 if( !d_equalityEngine
.hasTerm( neqc
[j
] ) && DatatypesRewriter::isTermDatatype( neqc
[j
] ) ){
1273 nodes
.push_back( neqc
[j
] );
1283 if( !neqc
.isNull() ){
1284 Trace("dt-cmi") << "Assign : " << neqc
<< std::endl
;
1285 m
->assertEquality( eqc
, neqc
, true );
1286 eqc_cons
[ eqc
] = neqc
;
1289 for( unsigned kk=0; kk<all_eqc.size(); kk++ ){
1290 for( unsigned ll=(kk+1); ll<all_eqc.size(); ll++ ){
1291 if( m->areEqual( all_eqc[kk], all_eqc[ll] ) ){
1292 Trace("dt-cmi") << "Forced equal : " << kk << " " << ll << " : " << all_eqc[kk] << " = " << all_eqc[ll] << std::endl;
1293 Node r = m->getRepresentative( all_eqc[kk] );
1294 Trace("dt-cmi") << " { ";
1295 eq::EqClassIterator eqc_i = eq::EqClassIterator( r, m->d_equalityEngine );
1296 while( !eqc_i.isFinished() ){
1297 Trace("dt-cmi") << (*eqc_i) << " ";
1300 Trace("dt-cmi") << "} " << std::endl;
1302 Assert( !m->areEqual( all_eqc[kk], all_eqc[ll] ) );
1306 //m->assertRepresentative( neqc );
1308 cons
.push_back( neqc
);
1313 //assign MU for each codatatype eqc
1314 std::map
< Node
, Node
> eqc_mu
;
1315 for( std::map
< Node
, Node
>::iterator it
= eqc_cons
.begin(); it
!= eqc_cons
.end(); ++it
){
1316 Node eqc
= it
->first
;
1317 const Datatype
& dt
= ((DatatypeType
)(eqc
.getType()).toType()).getDatatype();
1318 if( dt
.isCodatatype() ){
1319 std::map
< Node
, Node
> vmap
;
1320 Node v
= getCodatatypesValue( it
->first
, eqc_cons
, eqc_mu
, vmap
);
1321 Trace("dt-cmi-cod") << " EQC(" << it
->first
<< "), constructor is " << it
->second
<< ", value is " << v
<< std::endl
;
1327 Node
TheoryDatatypes::getCodatatypesValue( Node n
, std::map
< Node
, Node
>& eqc_cons
, std::map
< Node
, Node
>& eqc_mu
, std::map
< Node
, Node
>& vmap
){
1328 std::map
< Node
, Node
>::iterator itv
= vmap
.find( n
);
1329 if( itv
!=vmap
.end() ){
1331 }else if( DatatypesRewriter::isTermDatatype( n
) ){
1332 Node nv
= NodeManager::currentNM()->mkBoundVar( n
.getType() );
1334 Trace("dt-cmi-cod-debug") << " map " << n
<< " -> " << nv
<< std::endl
;
1335 Node nc
= eqc_cons
[n
];
1336 Assert( nc
.getKind()==APPLY_CONSTRUCTOR
);
1337 std::vector
< Node
> children
;
1338 children
.push_back( nc
.getOperator() );
1339 for( unsigned i
=0; i
<nc
.getNumChildren(); i
++ ){
1340 Node r
= getRepresentative( nc
[i
] );
1341 Node rv
= getCodatatypesValue( r
, eqc_cons
, eqc_mu
, vmap
);
1342 children
.push_back( rv
);
1345 return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR
, children
);
1351 void TheoryDatatypes::collectTerms( Node n
) {
1352 if( d_collectTermsCache
.find( n
)==d_collectTermsCache
.end() ){
1353 d_collectTermsCache
[n
] = true;
1354 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ) {
1355 collectTerms( n
[i
] );
1357 if( n
.getKind() == APPLY_CONSTRUCTOR
){
1358 d_consTerms
.push_back( n
);
1360 //we must take into account subterm relation when checking for cycles
1361 for( int i=0; i<(int)n.getNumChildren(); i++ ) {
1362 bool result = d_cycle_check.addEdgeNode( n, n[i] );
1363 Debug("datatypes-cycles") << "DtCyc: Subterm " << n << " -> " << n[i] << " " << result << endl;
1364 if( result && !d_hasSeenCycle.get() ){
1365 Debug("datatypes-cycles") << "FOUND CYCLE" << std::endl;
1367 d_hasSeenCycle.set( d_hasSeenCycle.get() || result );
1368 //Node r = getRepresentative( n[i] );
1369 //EqcInfo* eqc = getOrMakeEqcInfo( r, true );
1370 //eqc->d_selectors = true;
1373 }else if( n
.getKind() == APPLY_SELECTOR_TOTAL
){
1374 d_selTerms
.push_back( n
);
1375 //we must also record which selectors exist
1376 Debug("datatypes") << " Found selector " << n
<< endl
;
1377 if (n
.getType().isBoolean()) {
1378 d_equalityEngine
.addTriggerPredicate( n
);
1380 d_equalityEngine
.addTerm( n
);
1382 Node rep
= getRepresentative( n
[0] );
1383 //record it in the selectors
1384 EqcInfo
* eqc
= getOrMakeEqcInfo( rep
, true );
1385 //add it to the eqc info
1386 addSelector( n
, eqc
, rep
);
1391 void TheoryDatatypes::processNewTerm( Node n
){
1392 Trace("dt-terms") << "Created term : " << n
<< std::endl
;
1393 //see if it is rewritten to be something different
1394 Node rn
= Rewriter::rewrite( n
);
1395 if( rn
!=n
&& !areEqual( rn
, n
) ){
1396 Node eq
= n
.getType().isBoolean() ? rn
.iffNode( n
) : rn
.eqNode( n
);
1397 d_pending
.push_back( eq
);
1398 d_pending_exp
[ eq
] = d_true
;
1399 Trace("datatypes-infer") << "DtInfer : rewrite : " << eq
<< std::endl
;
1400 d_infer
.push_back( eq
);
1404 Node
TheoryDatatypes::getInstantiateCons( Node n
, const Datatype
& dt
, int index
, bool mkVar
, bool isActive
){
1405 std::map
< int, Node
>::iterator it
= d_inst_map
[n
].find( index
);
1406 if( it
!=d_inst_map
[n
].end() ){
1409 //add constructor to equivalence class
1410 Node n_ic
= DatatypesRewriter::getInstCons( n
, dt
, index
, mkVar
);
1412 for( unsigned i
= 0; i
<n_ic
.getNumChildren(); i
++ ){
1413 processNewTerm( n_ic
[i
] );
1415 collectTerms( n_ic
);
1417 n_ic
= Rewriter::rewrite( n_ic
);
1418 Debug("dt-enum") << "Made instantiate cons " << n_ic
<< std::endl
;
1419 d_inst_map
[n
][index
] = n_ic
;
1424 void TheoryDatatypes::instantiate( EqcInfo
* eqc
, Node n
){
1425 //add constructor to equivalence class if not done so already
1426 if( hasLabel( eqc
, n
) && !eqc
->d_inst
){
1429 if( !eqc
->d_constructor
.get().isNull() ){
1431 tt
= eqc
->d_constructor
;
1433 exp
= getLabel( n
);
1436 int index
= getLabelIndex( eqc
, n
);
1437 const Datatype
& dt
= ((DatatypeType
)(tt
.getType()).toType()).getDatatype();
1438 //must be finite or have a selector
1439 //if( eqc->d_selectors || dt[ index ].isFinite() ){ // || mustSpecifyAssignment()
1440 //instantiate this equivalence class
1442 Node tt_cons
= getInstantiateCons( tt
, dt
, index
, false, true );
1445 eq
= tt
.eqNode( tt_cons
);
1446 Debug("datatypes-inst") << "DtInstantiate : " << eqc
<< " " << eq
<< std::endl
;
1447 d_pending
.push_back( eq
);
1448 d_pending_exp
[ eq
] = exp
;
1449 Trace("datatypes-infer") << "DtInfer : instantiate : " << eq
<< " by " << exp
<< std::endl
;
1450 //eqc->d_inst.set( eq );
1451 d_infer
.push_back( eq
);
1452 d_infer_exp
.push_back( exp
);
1456 // Debug("datatypes-inst") << "Do not instantiate" << std::endl;
1461 void TheoryDatatypes::checkCycles() {
1462 Debug("datatypes-cycle-check") << "Check cycles" << std::endl
;
1463 std::vector
< Node
> cod_eqc
;
1464 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( &d_equalityEngine
);
1465 while( !eqcs_i
.isFinished() ){
1466 Node eqc
= (*eqcs_i
);
1467 TypeNode tn
= eqc
.getType();
1468 if( DatatypesRewriter::isTypeDatatype( tn
) ) {
1469 const Datatype
& dt
= ((DatatypeType
)(tn
).toType()).getDatatype();
1470 if( !dt
.isCodatatype() ){
1472 std::map
< TNode
, bool > visited
;
1473 std::vector
< TNode
> expl
;
1474 Node cn
= searchForCycle( eqc
, eqc
, visited
, expl
);
1475 //if we discovered a different cycle while searching this one
1476 if( !cn
.isNull() && cn
!=eqc
){
1480 cn
= searchForCycle( cn
, cn
, visited
, expl
);
1484 if( !cn
.isNull() ) {
1485 Assert( expl
.size()>0 );
1486 d_conflictNode
= mkAnd( expl
);
1487 Trace("dt-conflict") << "CONFLICT: Cycle conflict : " << d_conflictNode
<< std::endl
;
1488 d_out
->conflict( d_conflictNode
);
1494 cod_eqc
.push_back( eqc
);
1499 //process codatatypes
1500 if( cod_eqc
.size()>1 ){
1501 Trace("dt-cod-debug") << "Process " << cod_eqc
.size() << " co-datatypes" << std::endl
;
1502 std::vector
< std::vector
< Node
> > part_out
;
1503 std::vector
< TNode
> exp
;
1504 std::map
< Node
, Node
> cn
;
1505 std::map
< Node
, std::map
< Node
, int > > dni
;
1506 for( unsigned i
=0; i
<cod_eqc
.size(); i
++ ){
1507 cn
[cod_eqc
[i
]] = cod_eqc
[i
];
1509 separateBisimilar( cod_eqc
, part_out
, exp
, cn
, dni
, 0, false );
1510 Trace("dt-cod-debug") << "Done separate bisimilar." << std::endl
;
1511 if( !part_out
.empty() ){
1512 Trace("dt-cod-debug") << "Process partition size " << part_out
.size() << std::endl
;
1513 for( unsigned i
=0; i
<part_out
.size(); i
++ ){
1514 std::vector
< Node
> part
;
1515 part
.push_back( part_out
[i
][0] );
1516 for( unsigned j
=1; j
<part_out
[i
].size(); j
++ ){
1517 Trace("dt-cod") << "Codatatypes : " << part_out
[i
][0] << " and " << part_out
[i
][j
] << " must be equal!!" << std::endl
;
1518 part
.push_back( part_out
[i
][j
] );
1519 std::vector
< std::vector
< Node
> > tpart_out
;
1522 cn
[part_out
[i
][0]] = part_out
[i
][0];
1523 cn
[part_out
[i
][j
]] = part_out
[i
][j
];
1525 separateBisimilar( part
, tpart_out
, exp
, cn
, dni
, 0, true );
1526 Assert( tpart_out
.size()==1 && tpart_out
[0].size()==2 );
1528 //merge based on explanation
1529 Trace("dt-cod") << " exp is : ";
1530 for( unsigned k
=0; k
<exp
.size(); k
++ ){
1531 Trace("dt-cod") << exp
[k
] << " ";
1533 Trace("dt-cod") << std::endl
;
1534 Node eq
= part_out
[i
][0].eqNode( part_out
[i
][j
] );
1535 Node eqExp
= mkAnd( exp
);
1536 d_pending
.push_back( eq
);
1537 d_pending_exp
[ eq
] = eqExp
;
1538 Trace("datatypes-infer") << "DtInfer : cod-bisimilar : " << eq
<< " by " << eqExp
<< std::endl
;
1539 d_infer
.push_back( eq
);
1540 d_infer_exp
.push_back( eqExp
);
1547 //everything is in terms of representatives
1548 void TheoryDatatypes::separateBisimilar( std::vector
< Node
>& part
, std::vector
< std::vector
< Node
> >& part_out
,
1549 std::vector
< TNode
>& exp
,
1550 std::map
< Node
, Node
>& cn
,
1551 std::map
< Node
, std::map
< Node
, int > >& dni
, int dniLvl
, bool mkExp
){
1553 Trace("dt-cod-debug") << "Separate bisimilar : " << std::endl
;
1554 for( unsigned i
=0; i
<part
.size(); i
++ ){
1555 Trace("dt-cod-debug") << " " << part
[i
] << ", current = " << cn
[part
[i
]] << std::endl
;
1558 Assert( part
.size()>1 );
1559 std::map
< Node
, std::vector
< Node
> > new_part
;
1560 std::map
< Node
, std::vector
< Node
> > new_part_c
;
1561 std::map
< int, std::vector
< Node
> > new_part_rec
;
1563 std::map
< Node
, Node
> cn_cons
;
1564 for( unsigned j
=0; j
<part
.size(); j
++ ){
1565 Node c
= cn
[part
[j
]];
1566 std::map
< Node
, int >::iterator it_rec
= dni
[part
[j
]].find( c
);
1567 if( it_rec
!=dni
[part
[j
]].end() ){
1569 if( !mkExp
){ Trace("dt-cod-debug") << " - " << part
[j
] << " is looping at index " << it_rec
->second
<< std::endl
; }
1570 new_part_rec
[ it_rec
->second
].push_back( part
[j
] );
1572 if( DatatypesRewriter::isTermDatatype( c
) ){
1573 Node ncons
= getEqcConstructor( c
);
1574 if( ncons
.getKind()==APPLY_CONSTRUCTOR
) {
1575 Node cc
= ncons
.getOperator();
1576 cn_cons
[part
[j
]] = ncons
;
1578 explainEquality( c
, ncons
, true, exp
);
1580 new_part
[cc
].push_back( part
[j
] );
1581 if( !mkExp
){ Trace("dt-cod-debug") << " - " << part
[j
] << " is datatype " << ncons
<< "." << std::endl
; }
1583 new_part_c
[c
].push_back( part
[j
] );
1584 if( !mkExp
){ Trace("dt-cod-debug") << " - " << part
[j
] << " is unspecified datatype." << std::endl
; }
1588 if( !mkExp
){ Trace("dt-cod-debug") << " - " << part
[j
] << " is term " << c
<< "." << std::endl
; }
1589 new_part_c
[c
].push_back( part
[j
] );
1593 //direct add for constants
1594 for( std::map
< Node
, std::vector
< Node
> >::iterator it
= new_part_c
.begin(); it
!= new_part_c
.end(); ++it
){
1595 if( it
->second
.size()>1 ){
1596 std::vector
< Node
> vec
;
1597 vec
.insert( vec
.begin(), it
->second
.begin(), it
->second
.end() );
1598 part_out
.push_back( vec
);
1601 //direct add for recursive
1602 for( std::map
< int, std::vector
< Node
> >::iterator it
= new_part_rec
.begin(); it
!= new_part_rec
.end(); ++it
){
1603 if( it
->second
.size()>1 ){
1604 std::vector
< Node
> vec
;
1605 vec
.insert( vec
.begin(), it
->second
.begin(), it
->second
.end() );
1606 part_out
.push_back( vec
);
1608 //add back : could match a datatype?
1611 //recurse for the datatypes
1612 for( std::map
< Node
, std::vector
< Node
> >::iterator it
= new_part
.begin(); it
!= new_part
.end(); ++it
){
1613 if( it
->second
.size()>1 ){
1614 //set dni to check for loops
1615 std::map
< Node
, Node
> dni_rem
;
1616 for( unsigned i
=0; i
<it
->second
.size(); i
++ ){
1617 Node n
= it
->second
[i
];
1618 dni
[n
][cn
[n
]] = dniLvl
;
1622 //we will split based on the arguments of the datatype
1623 std::vector
< std::vector
< Node
> > split_new_part
;
1624 split_new_part
.push_back( it
->second
);
1626 unsigned nChildren
= cn_cons
[it
->second
[0]].getNumChildren();
1627 //for each child of constructor
1628 unsigned cindex
= 0;
1629 while( cindex
<nChildren
&& !split_new_part
.empty() ){
1630 if( !mkExp
){ Trace("dt-cod-debug") << "Split argument #" << cindex
<< " of " << it
->first
<< "..." << std::endl
; }
1631 std::vector
< std::vector
< Node
> > next_split_new_part
;
1632 for( unsigned j
=0; j
<split_new_part
.size(); j
++ ){
1634 for( unsigned k
=0; k
<split_new_part
[j
].size(); k
++ ){
1635 Node n
= split_new_part
[j
][k
];
1636 cn
[n
] = getRepresentative( cn_cons
[n
][cindex
] );
1638 explainEquality( cn
[n
], cn_cons
[n
][cindex
], true, exp
);
1641 std::vector
< std::vector
< Node
> > c_part_out
;
1642 separateBisimilar( split_new_part
[j
], c_part_out
, exp
, cn
, dni
, dniLvl
+1, mkExp
);
1643 next_split_new_part
.insert( next_split_new_part
.end(), c_part_out
.begin(), c_part_out
.end() );
1645 split_new_part
.clear();
1646 split_new_part
.insert( split_new_part
.end(), next_split_new_part
.begin(), next_split_new_part
.end() );
1649 part_out
.insert( part_out
.end(), split_new_part
.begin(), split_new_part
.end() );
1651 for( std::map
< Node
, Node
>::iterator it2
= dni_rem
.begin(); it2
!= dni_rem
.end(); ++it2
){
1652 dni
[it2
->first
].erase( it2
->second
);
1658 //postcondition: if cycle detected, explanation is why n is a subterm of on
1659 Node
TheoryDatatypes::searchForCycle( TNode n
, TNode on
,
1660 std::map
< TNode
, bool >& visited
,
1661 std::vector
< TNode
>& explanation
, bool firstTime
) {
1662 Debug("datatypes-cycle-check") << "Search for cycle " << n
<< " " << on
<< endl
;
1666 nn
= getRepresentative( n
);
1668 explainEquality( n
, nn
, true, explanation
);
1674 if( visited
.find( nn
) == visited
.end() ) {
1676 TNode ncons
= getEqcConstructor( nn
);
1677 if( ncons
.getKind()==APPLY_CONSTRUCTOR
) {
1678 for( int i
=0; i
<(int)ncons
.getNumChildren(); i
++ ) {
1679 TNode cn
= searchForCycle( ncons
[i
], on
, visited
, explanation
, false );
1681 //if( Debug.isOn("datatypes-cycles") && !d_cycle_check.isConnectedNode( n, ncons[i] ) ){
1682 // Debug("datatypes-cycles") << "Cycle subterm: " << n << " is not -> " << ncons[i] << "!!!!" << std::endl;
1684 //add explanation for why the constructor is connected
1686 explainEquality( n
, ncons
, true, explanation
);
1689 }else if( !cn
.isNull() ){
1694 visited
.erase( nn
);
1695 return Node::null();
1697 TypeNode tn
= nn
.getType();
1698 if( DatatypesRewriter::isTypeDatatype( tn
) ) {
1699 const Datatype
& dt
= ((DatatypeType
)(tn
).toType()).getDatatype();
1700 if( !dt
.isCodatatype() ){
1704 return Node::null();
1708 bool TheoryDatatypes::mustSpecifyAssignment(){
1709 //FIXME: the condition finiteModelFind is an over-approximation in this function
1710 // we still may not want to specify assignments for datatypes that are truly infinite
1711 // the fix for this is to correctly compute the cardinality for datatypes containing uninterpered sorts in fmf (i.e. by assuming they are finite)
1712 return options::finiteModelFind() || options::produceModels() || options::dtForceAssignment();
1713 //return options::produceModels();
1717 bool TheoryDatatypes::mustCommunicateFact( Node n
, Node exp
){
1718 //the datatypes decision procedure makes 3 "internal" inferences apart from the equality engine :
1719 // (1) Unification : C( t1...tn ) = C( s1...sn ) => ti = si
1720 // (2) Label : ~is_C1( t ) ... ~is_C{i-1}( t ) ~is_C{i+1}( t ) ... ~is_Cn( t ) => is_Ci( t )
1721 // (3) Instantiate : is_C( t ) => t = C( sel_1( t ) ... sel_n( t ) )
1722 //We may need to communicate (3) outwards if the conclusions involve other theories
1723 Trace("dt-lemma-debug") << "Compute for " << exp
<< " => " << n
<< std::endl
;
1724 bool addLemma
= false;
1725 if( ( n
.getKind()==EQUAL
|| n
.getKind()==IFF
) && n
[1].getKind()==APPLY_CONSTRUCTOR
&& exp
.getKind()!=EQUAL
){
1727 const Datatype
& dt
= ((DatatypeType
)(n
[1].getType()).toType()).getDatatype();
1728 addLemma
= dt
.involvesExternalType();
1730 for( int j
=0; j
<(int)n
[1].getNumChildren(); j
++ ){
1731 if( !DatatypesRewriter::isTermDatatype( n
[1][j
] ) ){
1738 //check if we have already added this lemma
1739 if( std::find( d_inst_lemmas
[ n
[0] ].begin(), d_inst_lemmas
[ n
[0] ].end(), n
[1] )==d_inst_lemmas
[ n
[0] ].end() ){
1740 d_inst_lemmas
[ n
[0] ].push_back( n
[1] );
1741 Trace("dt-lemma-debug") << "Communicate " << n
<< std::endl
;
1744 Trace("dt-lemma-debug") << "Already communicated " << n
<< std::endl
;
1749 //else if( exp.getKind()==APPLY_TESTER ){
1750 //if( n.getKind()==EQUAL && !DatatypesRewriter::isTermDatatype( n[0] ) ){
1754 Trace("dt-lemma-debug") << "Do not need to communicate " << n
<< std::endl
;
1758 bool TheoryDatatypes::hasTerm( TNode a
){
1759 return d_equalityEngine
.hasTerm( a
);
1762 bool TheoryDatatypes::areEqual( TNode a
, TNode b
){
1765 }else if( hasTerm( a
) && hasTerm( b
) ){
1766 return d_equalityEngine
.areEqual( a
, b
);
1772 bool TheoryDatatypes::areDisequal( TNode a
, TNode b
){
1775 }else if( hasTerm( a
) && hasTerm( b
) ){
1776 return d_equalityEngine
.areDisequal( a
, b
, false );
1782 TNode
TheoryDatatypes::getRepresentative( TNode a
){
1784 return d_equalityEngine
.getRepresentative( a
);
1791 void TheoryDatatypes::printModelDebug( const char* c
){
1792 if(! (Trace
.isOn(c
))) {
1796 Trace( c
) << "Datatypes model : " << std::endl
;
1797 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( &d_equalityEngine
);
1798 while( !eqcs_i
.isFinished() ){
1799 Node eqc
= (*eqcs_i
);
1800 if( !eqc
.getType().isBoolean() ){
1801 if( DatatypesRewriter::isTermDatatype( eqc
) ){
1802 Trace( c
) << "DATATYPE : ";
1804 Trace( c
) << eqc
<< " : " << eqc
.getType() << " : " << std::endl
;
1805 Trace( c
) << " { ";
1806 //add terms to model
1807 eq::EqClassIterator eqc_i
= eq::EqClassIterator( eqc
, &d_equalityEngine
);
1808 while( !eqc_i
.isFinished() ){
1809 Trace( c
) << (*eqc_i
) << " ";
1812 Trace( c
) << "}" << std::endl
;
1813 if( DatatypesRewriter::isTermDatatype( eqc
) ){
1814 EqcInfo
* ei
= getOrMakeEqcInfo( eqc
);
1816 Trace( c
) << " Instantiated : " << ei
->d_inst
.get() << std::endl
;
1817 Trace( c
) << " Constructor : ";
1818 if( !ei
->d_constructor
.get().isNull() ){
1819 Trace( c
)<< ei
->d_constructor
.get();
1821 Trace( c
) << std::endl
<< " Labels : ";
1822 if( hasLabel( ei
, eqc
) ){
1823 Trace( c
) << getLabel( eqc
);
1825 NodeListMap::iterator lbl_i
= d_labels
.find( eqc
);
1826 if( lbl_i
!= d_labels
.end() ){
1827 NodeList
* lbl
= (*lbl_i
).second
;
1828 for( NodeList::const_iterator j
= lbl
->begin(); j
!= lbl
->end(); j
++ ){
1829 Trace( c
) << *j
<< " ";
1833 Trace( c
) << std::endl
;
1834 Trace( c
) << " Selectors : " << ( ei
->d_selectors
? "yes, " : "no " );
1835 NodeListMap::iterator sel_i
= d_selector_apps
.find( eqc
);
1836 if( sel_i
!= d_selector_apps
.end() ){
1837 NodeList
* sel
= (*sel_i
).second
;
1838 for( NodeList::const_iterator j
= sel
->begin(); j
!= sel
->end(); j
++ ){
1839 Trace( c
) << *j
<< " ";
1842 Trace( c
) << std::endl
;
1850 Node
TheoryDatatypes::mkAnd( std::vector
< TNode
>& assumptions
) {
1851 if( assumptions
.empty() ){
1853 }else if( assumptions
.size()==1 ){
1854 return assumptions
[0];
1856 return NodeManager::currentNM()->mkNode( AND
, assumptions
);
1860 bool TheoryDatatypes::checkClashModEq( TNode n1
, TNode n2
, std::vector
< Node
>& exp
, std::vector
< std::pair
< TNode
, TNode
> >& deq_cand
) {
1861 if( (n1
.getKind() == kind::APPLY_CONSTRUCTOR
&& n2
.getKind() == kind::APPLY_CONSTRUCTOR
) ||
1862 (n1
.getKind() == kind::TUPLE
&& n2
.getKind() == kind::TUPLE
) ||
1863 (n1
.getKind() == kind::RECORD
&& n2
.getKind() == kind::RECORD
) ) {
1864 if( n1
.getOperator() != n2
.getOperator() ) {
1867 Assert( n1
.getNumChildren() == n2
.getNumChildren() );
1868 for( int i
=0; i
<(int)n1
.getNumChildren(); i
++ ) {
1869 TNode nc1
= getEqcConstructor( n1
[i
] );
1870 TNode nc2
= getEqcConstructor( n2
[i
] );
1871 if( checkClashModEq( nc1
, nc2
, exp
, deq_cand
) ) {
1873 exp
.push_back( nc1
.eqNode( n1
[i
] ) );
1876 exp
.push_back( nc2
.eqNode( n2
[i
] ) );
1883 if( n1
.isConst() && n2
.isConst() ){
1886 if( !areEqual( n1
, n2
) ){
1887 deq_cand
.push_back( std::pair
< TNode
, TNode
>( n1
, n2
) );