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-2013 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/model.h"
26 #include "smt/options.h"
27 #include "smt/boolean_terms.h"
28 #include "theory/quantifiers/options.h"
34 using namespace CVC4::kind
;
35 using namespace CVC4::context
;
36 using namespace CVC4::theory
;
37 using namespace CVC4::theory::datatypes
;
40 TheoryDatatypes::TheoryDatatypes(Context
* c
, UserContext
* u
, OutputChannel
& out
, Valuation valuation
, const LogicInfo
& logicInfo
, QuantifiersEngine
* qe
) :
41 Theory(THEORY_DATATYPES
, c
, u
, out
, valuation
, logicInfo
, qe
),
43 d_hasSeenCycle(c
, false),
47 d_equalityEngine(d_notify
, c
, "theory::datatypes::TheoryDatatypes"),
50 d_conflict( c
, false ),
51 d_collectTermsCache( c
){
53 // The kinds we are treating as function application in congruence
54 d_equalityEngine
.addFunctionKind(kind::APPLY_CONSTRUCTOR
);
55 d_equalityEngine
.addFunctionKind(kind::APPLY_SELECTOR
);
56 d_equalityEngine
.addFunctionKind(kind::APPLY_TESTER
);
59 TheoryDatatypes::~TheoryDatatypes() {
62 void TheoryDatatypes::setMasterEqualityEngine(eq::EqualityEngine
* eq
) {
63 d_equalityEngine
.setMasterEqualityEngine(eq
);
66 TheoryDatatypes::EqcInfo
* TheoryDatatypes::getOrMakeEqcInfo( Node n
, bool doMake
){
67 std::map
< Node
, EqcInfo
* >::iterator eqc_i
= d_eqc_info
.find( n
);
68 if( !hasEqcInfo( n
) ){
71 NodeList
* lbl
= new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
72 ContextMemoryAllocator
<TNode
>(getSatContext()->getCMM()) );
73 d_labels
.insertDataFromContextMemory( n
, lbl
);
75 if( eqc_i
!=d_eqc_info
.end() ){
78 ei
= new EqcInfo( getSatContext() );
81 if( n
.getKind()==APPLY_CONSTRUCTOR
){
82 ei
->d_constructor
= n
;
89 return (*eqc_i
).second
;
93 void TheoryDatatypes::check(Effort e
) {
95 while(!done() && !d_conflict
) {
96 // Get all the assertions
97 Assertion assertion
= get();
98 TNode fact
= assertion
.assertion
;
99 Trace("datatypes-assert") << "Assert " << fact
<< std::endl
;
101 TNode atom CVC4_UNUSED
= fact
.getKind() == kind::NOT
? fact
[0] : fact
;
103 // extra debug check to make sure that the rewriter did its job correctly
104 Assert( atom
.getKind() != kind::EQUAL
||
105 ( atom
[0].getKind() != kind::TUPLE
&& atom
[1].getKind() != kind::TUPLE
&&
106 atom
[0].getKind() != kind::RECORD
&& atom
[1].getKind() != kind::RECORD
&&
107 atom
[0].getKind() != kind::TUPLE_UPDATE
&& atom
[1].getKind() != kind::TUPLE_UPDATE
&&
108 atom
[0].getKind() != kind::RECORD_UPDATE
&& atom
[1].getKind() != kind::RECORD_UPDATE
&&
109 atom
[0].getKind() != kind::TUPLE_SELECT
&& atom
[1].getKind() != kind::TUPLE_SELECT
&&
110 atom
[0].getKind() != kind::RECORD_SELECT
&& atom
[1].getKind() != kind::RECORD_SELECT
),
111 "tuple/record escaped into datatypes decision procedure; should have been rewritten away" );
114 assertFact( fact
, fact
);
118 if( e
== EFFORT_FULL
) {
119 Debug("datatypes-split") << "Check for splits " << e
<< endl
;
120 bool addedFact
= false;
122 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( &d_equalityEngine
);
123 while( !eqcs_i
.isFinished() ){
125 if( DatatypesRewriter::isTermDatatype( n
) ){
126 Trace("datatypes-debug") << "Process equivalence class " << n
<< std::endl
;
127 EqcInfo
* eqc
= getOrMakeEqcInfo( n
, true );
128 //if there are more than 1 possible constructors for eqc
129 if( eqc
->d_constructor
.get().isNull() && !hasLabel( eqc
, n
) ) {
130 Trace("datatypes-debug") << "No constructor..." << std::endl
;
131 const Datatype
& dt
= ((DatatypeType
)(n
.getType()).toType()).getDatatype();
132 //if only one constructor, then this term must be this constructor
133 if( dt
.getNumConstructors()==1 ){
134 Node t
= NodeManager::currentNM()->mkNode( APPLY_TESTER
, Node::fromExpr( dt
[0].getTester() ), n
);
135 d_pending
.push_back( t
);
136 d_pending_exp
[ t
] = NodeManager::currentNM()->mkConst( true );
137 Trace("datatypes-infer") << "DtInfer : " << t
<< ", trivial" << std::endl
;
138 d_infer
.push_back( t
);
140 std::vector
< bool > pcons
;
141 getPossibleCons( eqc
, n
, pcons
);
142 //std::cout << "pcons " << n << " = ";
143 //for( int i=0; i<(int)pcons.size(); i++ ){ //std::cout << pcons[i] << " "; }
144 //std::cout << std::endl;
145 //check if we do not need to resolve the constructor type for this equivalence class.
146 // this is if there are no selectors for this equivalence class, its possible values are infinite,
147 // and we are not producing a model, then do not split.
149 bool needSplit
= true;
150 for( unsigned int j
=0; j
<pcons
.size(); j
++ ) {
155 if( !dt
[ j
].isFinite() && !eqc
->d_selectors
) {
160 if( !needSplit
&& mustSpecifyAssignment() ){
161 //for the sake of termination, we must choose the constructor of a ground term
162 //NEED GUARENTEE: groundTerm should not contain any subterms of the same type
163 //** TODO: this is probably not good enough, actually need fair enumeration strategy
164 Node groundTerm
= n
.getType().mkGroundTerm();
165 int index
= Datatype::indexOf( groundTerm
.getOperator().toExpr() );
171 if( needSplit
&& consIndex
!=-1 ) {
172 Node test
= NodeManager::currentNM()->mkNode( APPLY_TESTER
, Node::fromExpr( dt
[consIndex
].getTester() ), n
);
173 Trace("dt-split") << "*************Split for possible constructor " << dt
[consIndex
] << " for " << n
<< endl
;
174 test
= Rewriter::rewrite( test
);
175 NodeBuilder
<> nb(kind::OR
);
176 nb
<< test
<< test
.notNode();
178 d_out
->lemma( lemma
);
179 d_out
->requirePhase( test
, true );
182 Trace("dt-split") << "Do not split constructor for " << n
<< std::endl
;
186 Trace("datatypes-debug") << "Has constructor " << eqc
->d_constructor
.get() << std::endl
;
191 Trace("datatypes-debug") << "Flush pending facts..." << std::endl
;
192 addedFact
= !d_pending
.empty();
195 if( options::dtRewriteErrorSel() ){
206 Trace("datatypes-debug") << "Finished. " << d_conflict
<< std::endl
;
208 Trace("dt-model-test") << std::endl
;
209 printModelDebug("dt-model-test");
213 if( Debug
.isOn("datatypes") || Debug
.isOn("datatypes-split") ) {
214 Notice() << "TheoryDatatypes::check(): done" << endl
;
218 void TheoryDatatypes::flushPendingFacts(){
220 if( !d_pending
.empty() ){
222 while( !d_conflict
&& i
<(int)d_pending
.size() ){
223 Node fact
= d_pending
[i
];
224 Node exp
= d_pending_exp
[ fact
];
225 //check to see if we have to communicate it to the rest of the system
226 if( mustCommunicateFact( fact
, exp
) ){
227 Trace("dt-lemma-debug") << "Assert fact " << fact
<< " " << exp
<< std::endl
;
229 if( exp
.isNull() || exp
==NodeManager::currentNM()->mkConst( true ) ){
232 Trace("dt-lemma-debug") << "Get explanation..." << std::endl
;
233 Node ee_exp
= explain( exp
);
234 Trace("dt-lemma-debug") << "Explanation : " << ee_exp
<< std::endl
;
235 lem
= NodeManager::currentNM()->mkNode( IMPLIES
, ee_exp
, fact
);
236 lem
= Rewriter::rewrite( lem
);
238 Trace("dt-lemma") << "Datatypes lemma : " << lem
<< std::endl
;
241 assertFact( fact
, exp
);
246 d_pending_exp
.clear();
250 void TheoryDatatypes::doPendingMerges(){
251 //do all pending merges
253 while( i
<(int)d_pending_merge
.size() ){
254 Assert( d_pending_merge
[i
].getKind()==EQUAL
|| d_pending_merge
[i
].getKind()==IFF
);
255 merge( d_pending_merge
[i
][0], d_pending_merge
[i
][1] );
258 d_pending_merge
.clear();
261 void TheoryDatatypes::assertFact( Node fact
, Node exp
){
262 Assert( d_pending_merge
.empty() );
263 bool polarity
= fact
.getKind() != kind::NOT
;
264 TNode atom
= polarity
? fact
: fact
[0];
265 if (atom
.getKind() == kind::EQUAL
) {
266 d_equalityEngine
.assertEquality( atom
, polarity
, exp
);
268 d_equalityEngine
.assertPredicate( atom
, polarity
, exp
);
271 //add to tester if applicable
272 if( atom
.getKind()==kind::APPLY_TESTER
){
273 Node rep
= getRepresentative( atom
[0] );
274 EqcInfo
* eqc
= getOrMakeEqcInfo( rep
, true );
275 addTester( fact
, eqc
, rep
);
280 void TheoryDatatypes::preRegisterTerm(TNode n
) {
281 Debug("datatypes-prereg") << "TheoryDatatypes::preRegisterTerm() " << n
<< endl
;
283 switch (n
.getKind()) {
285 // Add the trigger for equality
286 d_equalityEngine
.addTriggerEquality(n
);
288 case kind::APPLY_TESTER
:
289 // Get triggered for both equal and dis-equal
290 d_equalityEngine
.addTriggerPredicate(n
);
293 // Maybe it's a predicate
294 if (n
.getType().isBoolean()) {
295 // Get triggered for both equal and dis-equal
296 d_equalityEngine
.addTriggerPredicate(n
);
298 // Function applications/predicates
299 d_equalityEngine
.addTerm(n
);
306 void TheoryDatatypes::presolve() {
307 Debug("datatypes") << "TheoryDatatypes::presolve()" << endl
;
310 Node
TheoryDatatypes::ppRewrite(TNode in
) {
311 Debug("tuprec") << "TheoryDatatypes::ppRewrite(" << in
<< ")" << endl
;
313 if(in
.getKind() == kind::TUPLE_SELECT
) {
314 TypeNode t
= in
[0].getType();
315 if(t
.hasAttribute(expr::DatatypeTupleAttr())) {
316 t
= t
.getAttribute(expr::DatatypeTupleAttr());
318 TypeNode dtt
= NodeManager::currentNM()->getDatatypeForTupleRecord(t
);
319 const Datatype
& dt
= DatatypeType(dtt
.toType()).getDatatype();
320 return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR
, Node::fromExpr(dt
[0][in
.getOperator().getConst
<TupleSelect
>().getIndex()].getSelector()), in
[0]);
321 } else if(in
.getKind() == kind::RECORD_SELECT
) {
322 TypeNode t
= in
[0].getType();
323 if(t
.hasAttribute(expr::DatatypeRecordAttr())) {
324 t
= t
.getAttribute(expr::DatatypeRecordAttr());
326 TypeNode dtt
= NodeManager::currentNM()->getDatatypeForTupleRecord(t
);
327 const Datatype
& dt
= DatatypeType(dtt
.toType()).getDatatype();
328 return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR
, Node::fromExpr(dt
[0][in
.getOperator().getConst
<RecordSelect
>().getField()].getSelector()), in
[0]);
331 TypeNode t
= in
.getType();
333 // we only care about tuples and records here
334 if(in
.getKind() != kind::TUPLE
&& in
.getKind() != kind::TUPLE_UPDATE
&&
335 in
.getKind() != kind::RECORD
&& in
.getKind() != kind::RECORD_UPDATE
) {
336 if((t
.isTuple() || t
.isRecord()) && in
.hasAttribute(smt::BooleanTermAttr())) {
337 Debug("tuprec") << "should map " << in
<< " of type " << t
<< " back to " << in
.getAttribute(smt::BooleanTermAttr()).getType() << endl
;
338 Debug("tuprec") << "so " << NodeManager::currentNM()->getDatatypeForTupleRecord(t
).getDatatype() << " goes to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in
.getAttribute(smt::BooleanTermAttr()).getType()).getDatatype() << endl
;
340 Debug("tuprec") << "current datatype-tuple-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t
).getAttribute(expr::DatatypeTupleAttr()) << endl
;
341 Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in
.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr()) << endl
;
342 NodeManager::currentNM()->getDatatypeForTupleRecord(t
).setAttribute(expr::DatatypeTupleAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in
.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr()));
344 Debug("tuprec") << "current datatype-record-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t
).getAttribute(expr::DatatypeRecordAttr()) << endl
;
345 Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in
.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()) << endl
;
346 NodeManager::currentNM()->getDatatypeForTupleRecord(t
).setAttribute(expr::DatatypeRecordAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in
.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()));
353 if(t
.hasAttribute(expr::DatatypeTupleAttr())) {
354 t
= t
.getAttribute(expr::DatatypeTupleAttr());
355 } else if(t
.hasAttribute(expr::DatatypeRecordAttr())) {
356 t
= t
.getAttribute(expr::DatatypeRecordAttr());
359 // if the type doesn't have an associated datatype, then make one for it
360 TypeNode dtt
= (t
.isTuple() || t
.isRecord()) ? NodeManager::currentNM()->getDatatypeForTupleRecord(t
) : t
;
362 const Datatype
& dt
= DatatypeType(dtt
.toType()).getDatatype();
364 // now rewrite the expression
366 if(in
.getKind() == kind::TUPLE
|| in
.getKind() == kind::RECORD
) {
367 NodeBuilder
<> b(kind::APPLY_CONSTRUCTOR
);
368 b
<< Node::fromExpr(dt
[0].getConstructor());
369 b
.append(in
.begin(), in
.end());
371 } else if(in
.getKind() == kind::TUPLE_UPDATE
|| in
.getKind() == kind::RECORD_UPDATE
) {
372 NodeBuilder
<> b(kind::APPLY_CONSTRUCTOR
);
373 b
<< Node::fromExpr(dt
[0].getConstructor());
374 size_t size
, updateIndex
;
375 if(in
.getKind() == kind::TUPLE_UPDATE
) {
376 size
= t
.getNumChildren();
377 updateIndex
= in
.getOperator().getConst
<TupleUpdate
>().getIndex();
378 } else { // kind::RECORD_UPDATE
379 const Record
& record
= t
.getConst
<Record
>();
380 size
= record
.getNumFields();
381 updateIndex
= record
.getIndex(in
.getOperator().getConst
<RecordUpdate
>().getField());
383 Debug("tuprec") << "expr is " << in
<< std::endl
;
384 Debug("tuprec") << "updateIndex is " << updateIndex
<< std::endl
;
385 Debug("tuprec") << "t is " << t
<< std::endl
;
386 Debug("tuprec") << "t has arity " << size
<< std::endl
;
387 for(size_t i
= 0; i
< size
; ++i
) {
388 if(i
== updateIndex
) {
390 Debug("tuprec") << "arg " << i
<< " gets updated to " << in
[1] << std::endl
;
392 b
<< NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR
, Node::fromExpr(dt
[0][i
].getSelector()), in
[0]);
393 Debug("tuprec") << "arg " << i
<< " copies " << b
[b
.getNumChildren() - 1] << std::endl
;
396 Debug("tuprec") << "builder says " << b
<< std::endl
;
402 Debug("tuprec") << "REWROTE " << in
<< " to " << n
<< std::endl
;
407 void TheoryDatatypes::addSharedTerm(TNode t
) {
408 Debug("datatypes") << "TheoryDatatypes::addSharedTerm(): "
409 << t
<< " " << t
.getType().isBoolean() << endl
;
410 if( t
.getType().isBoolean() ){
411 //d_equalityEngine.addTriggerPredicate(t, THEORY_DATATYPES);
413 d_equalityEngine
.addTriggerTerm(t
, THEORY_DATATYPES
);
415 Debug("datatypes") << "TheoryDatatypes::addSharedTerm() finished" << std::endl
;
419 void TheoryDatatypes::propagate(Effort effort
){
424 bool TheoryDatatypes::propagate(TNode literal
){
425 Debug("dt::propagate") << "TheoryDatatypes::propagate(" << literal
<< ")" << std::endl
;
426 // If already in conflict, no more propagation
428 Debug("dt::propagate") << "TheoryDatatypes::propagate(" << literal
<< "): already in conflict" << std::endl
;
431 Trace("dt-prop") << "dtPropagate " << literal
<< std::endl
;
433 bool ok
= d_out
->propagate(literal
);
441 void TheoryDatatypes::explain(TNode literal
, std::vector
<TNode
>& assumptions
){
442 Debug("datatypes-explain") << "Explain " << literal
<< std::endl
;
443 bool polarity
= literal
.getKind() != kind::NOT
;
444 TNode atom
= polarity
? literal
: literal
[0];
445 if (atom
.getKind() == kind::EQUAL
|| atom
.getKind() == kind::IFF
) {
446 d_equalityEngine
.explainEquality(atom
[0], atom
[1], polarity
, assumptions
);
448 d_equalityEngine
.explainPredicate(atom
, polarity
, assumptions
);
452 Node
TheoryDatatypes::explain( TNode literal
){
453 std::vector
< TNode
> assumptions
;
454 explain( literal
, assumptions
);
455 if( assumptions
.empty() ){
456 return NodeManager::currentNM()->mkConst( true );
457 }else if( assumptions
.size()==1 ){
458 return assumptions
[0];
460 return NodeManager::currentNM()->mkNode( kind::AND
, assumptions
);
464 /** Conflict when merging two constants */
465 void TheoryDatatypes::conflict(TNode a
, TNode b
){
466 if (a
.getKind() == kind::CONST_BOOLEAN
) {
467 d_conflictNode
= explain( a
.iffNode(b
) );
469 d_conflictNode
= explain( a
.eqNode(b
) );
471 Debug("datatypes-conflict") << "CONFLICT: Eq engine conflict : " << d_conflictNode
<< std::endl
;
472 d_out
->conflict( d_conflictNode
);
476 /** called when a new equivalance class is created */
477 void TheoryDatatypes::eqNotifyNewClass(TNode t
){
478 if( t
.getKind()==APPLY_CONSTRUCTOR
){
479 getOrMakeEqcInfo( t
, true );
483 /** called when two equivalance classes will merge */
484 void TheoryDatatypes::eqNotifyPreMerge(TNode t1
, TNode t2
){
488 /** called when two equivalance classes have merged */
489 void TheoryDatatypes::eqNotifyPostMerge(TNode t1
, TNode t2
){
490 if( DatatypesRewriter::isTermDatatype( t1
) ){
491 d_pending_merge
.push_back( t1
.eqNode( t2
) );
495 void TheoryDatatypes::merge( Node t1
, Node t2
){
499 Debug("datatypes-debug") << "Merge " << t1
<< " " << t2
<< std::endl
;
500 EqcInfo
* eqc2
= getOrMakeEqcInfo( t2
);
502 bool checkInst
= false;
503 if( !eqc2
->d_constructor
.get().isNull() ){
504 trep2
= eqc2
->d_constructor
.get();
506 EqcInfo
* eqc1
= getOrMakeEqcInfo( t1
);
508 if( !eqc1
->d_constructor
.get().isNull() ){
509 trep1
= eqc1
->d_constructor
.get();
512 Node cons1
= eqc1
->d_constructor
;
513 Node cons2
= eqc2
->d_constructor
;
514 if( !cons1
.isNull() && !cons2
.isNull() ){
515 Debug("datatypes-debug") << "Constructors : " << cons1
<< " " << cons2
<< std::endl
;
516 if( cons1
.getOperator()!=cons2
.getOperator() ){
518 d_conflictNode
= explain( cons1
.eqNode( cons2
) );
519 Debug("datatypes-conflict") << "CONFLICT: Clash conflict : " << d_conflictNode
<< std::endl
;
520 d_out
->conflict( d_conflictNode
);
525 Node unifEq
= cons1
.eqNode( cons2
);
526 for( int i
=0; i
<(int)cons1
.getNumChildren(); i
++ ) {
527 if( cons1
[i
]!=cons2
[i
] ){
528 Node eq
= cons1
[i
].getType().isBoolean() ? cons1
[i
].iffNode( cons2
[i
] ) : cons1
[i
].eqNode( cons2
[i
] );
529 d_pending
.push_back( eq
);
530 d_pending_exp
[ eq
] = unifEq
;
531 Trace("datatypes-infer") << "DtInfer : " << eq
<< " by " << unifEq
<< std::endl
;
532 d_infer
.push_back( eq
);
533 d_infer_exp
.push_back( unifEq
);
538 if( !eqc1
->d_inst
&& eqc2
->d_inst
){
541 if( cons1
.isNull() && !cons2
.isNull() ){
543 eqc1
->d_constructor
.set( eqc2
->d_constructor
);
546 Debug("datatypes-debug") << "No eqc info for " << t1
<< ", must create" << std::endl
;
547 //just copy the equivalence class information
548 eqc1
= getOrMakeEqcInfo( t1
, true );
549 eqc1
->d_inst
.set( eqc2
->d_inst
);
550 eqc1
->d_constructor
.set( eqc2
->d_constructor
);
553 Debug("datatypes-debug") << "Merge labels from " << eqc2
<< " " << t2
<< std::endl
;
554 NodeListMap::iterator lbl_i
= d_labels
.find( t2
);
555 if( lbl_i
!= d_labels
.end() ){
556 NodeList
* lbl
= (*lbl_i
).second
;
557 for( NodeList::const_iterator j
= lbl
->begin(); j
!= lbl
->end(); ++j
){
558 addTester( *j
, eqc1
, t1
);
565 if( !eqc1
->d_selectors
&& eqc2
->d_selectors
){
566 eqc1
->d_selectors
= true;
570 instantiate( eqc1
, t1
);
576 //add this to the transitive closure module
579 if( trep1
.getKind()!=APPLY_CONSTRUCTOR
&& trep2
.getKind()==APPLY_CONSTRUCTOR
){
583 bool result
= d_cycle_check
.addEdgeNode( oldRep
, newRep
);
584 d_hasSeenCycle
.set( d_hasSeenCycle
.get() || result
);
585 Debug("datatypes-cycles") << "DtCyc: Equal " << oldRep
<< " -> " << newRep
<< " " << d_hasSeenCycle
.get() << endl
;
586 if( d_hasSeenCycle
.get() ){
595 /** called when two equivalence classes are made disequal */
596 void TheoryDatatypes::eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
){
600 TheoryDatatypes::EqcInfo::EqcInfo( context::Context
* c
) :
601 d_inst( c
, false ), d_constructor( c
, Node::null() ), d_selectors( c
, false ){
605 bool TheoryDatatypes::hasLabel( EqcInfo
* eqc
, Node n
){
606 return !eqc
->d_constructor
.get().isNull() || !getLabel( n
).isNull();
609 Node
TheoryDatatypes::getLabel( Node n
) {
610 NodeListMap::iterator lbl_i
= d_labels
.find( n
);
611 if( lbl_i
!= d_labels
.end() ){
612 NodeList
* lbl
= (*lbl_i
).second
;
613 if( !(*lbl
).empty() && (*lbl
)[ (*lbl
).size() - 1 ].getKind()==kind::APPLY_TESTER
){
614 return (*lbl
)[ (*lbl
).size() - 1 ];
620 int TheoryDatatypes::getLabelIndex( EqcInfo
* eqc
, Node n
){
621 if( !eqc
->d_constructor
.get().isNull() ){
622 return Datatype::indexOf( eqc
->d_constructor
.get().getOperator().toExpr() );
624 return Datatype::indexOf( getLabel( n
).getOperator().toExpr() );
628 void TheoryDatatypes::getPossibleCons( EqcInfo
* eqc
, Node n
, std::vector
< bool >& pcons
){
629 const Datatype
& dt
= ((DatatypeType
)(n
.getType()).toType()).getDatatype();
630 pcons
.resize( dt
.getNumConstructors(), !hasLabel( eqc
, n
) );
631 if( hasLabel( eqc
, n
) ){
632 pcons
[ getLabelIndex( eqc
, n
) ] = true;
634 NodeListMap::iterator lbl_i
= d_labels
.find( n
);
635 if( lbl_i
!= d_labels
.end() ){
636 NodeList
* lbl
= (*lbl_i
).second
;
637 for( NodeList::const_iterator i
= lbl
->begin(); i
!= lbl
->end(); i
++ ) {
638 Assert( (*i
).getKind()==NOT
);
639 pcons
[ Datatype::indexOf( (*i
)[0].getOperator().toExpr() ) ] = false;
645 void TheoryDatatypes::addTester( Node t
, EqcInfo
* eqc
, Node n
){
647 Debug("datatypes-labels") << "Add tester " << t
<< " " << eqc
<< std::endl
;
648 bool tpolarity
= t
.getKind()!=NOT
;
649 Node tt
= ( t
.getKind() == NOT
) ? t
[0] : t
;
650 int ttindex
= Datatype::indexOf( tt
.getOperator().toExpr() );
652 if( hasLabel( eqc
, n
) ){
653 //if we already know the constructor type, check whether it is in conflict or redundant
654 int jtindex
= getLabelIndex( eqc
, n
);
655 if( (jtindex
==ttindex
)!=tpolarity
){
657 if( !eqc
->d_constructor
.get().isNull() ){
658 //conflict because equivalence class contains a constructor
659 std::vector
< TNode
> assumptions
;
660 explain( t
, assumptions
);
661 explain( eqc
->d_constructor
.get().eqNode( tt
[0] ), assumptions
);
662 d_conflictNode
= NodeManager::currentNM()->mkNode( AND
, assumptions
);
663 Debug("datatypes-conflict") << "CONFLICT: Tester eq conflict : " << d_conflictNode
<< std::endl
;
664 d_out
->conflict( d_conflictNode
);
667 //conflict because the existing label is contradictory
675 //otherwise, scan list of labels
676 NodeListMap::iterator lbl_i
= d_labels
.find( n
);
677 Assert( lbl_i
!= d_labels
.end() );
678 NodeList
* lbl
= (*lbl_i
).second
;
679 for( NodeList::const_iterator i
= lbl
->begin(); i
!= lbl
->end(); i
++ ) {
680 Assert( (*i
).getKind()==NOT
);
683 int jtindex
= Datatype::indexOf( jt
.getOperator().toExpr() );
684 if( jtindex
==ttindex
){
685 if( tpolarity
){ //we are in conflict
688 }else{ //it is redundant
694 Debug("datatypes-labels") << "Add to labels " << t
<< std::endl
;
696 const Datatype
& dt
= ((DatatypeType
)(tt
[0].getType()).toType()).getDatatype();
697 Debug("datatypes-labels") << "Labels at " << lbl
->size() << " / " << dt
.getNumConstructors() << std::endl
;
699 instantiate( eqc
, n
);
701 //check if we have reached the maximum number of testers
702 // in this case, add the positive tester
703 if( lbl
->size()==dt
.getNumConstructors()-1 ){
704 std::vector
< bool > pcons
;
705 getPossibleCons( eqc
, n
, pcons
);
706 int testerIndex
= -1;
707 for( int i
=0; i
<(int)pcons
.size(); i
++ ) {
713 Assert( testerIndex
!=-1 );
714 //we must explain why each term in the set of testers for this equivalence class is equal
715 std::vector
< Node
> eq_terms
;
716 NodeBuilder
<> nb(kind::AND
);
717 for( NodeList::const_iterator i
= lbl
->begin(); i
!= lbl
->end(); i
++ ) {
719 if( std::find( eq_terms
.begin(), eq_terms
.end(), (*i
)[0][0] )==eq_terms
.end() ){
720 eq_terms
.push_back( (*i
)[0][0] );
721 if( (*i
)[0][0]!=tt
[0] ){
722 nb
<< (*i
)[0][0].eqNode( tt
[0] );
726 Node t_concl
= NodeManager::currentNM()->mkNode( APPLY_TESTER
, Node::fromExpr( dt
[unsigned(testerIndex
)].getTester() ), tt
[0] );
727 Node t_concl_exp
= ( nb
.getNumChildren() == 1 ) ? nb
.getChild( 0 ) : nb
;
728 d_pending
.push_back( t_concl
);
729 d_pending_exp
[ t_concl
] = t_concl_exp
;
730 Trace("datatypes-infer") << "DtInfer : " << t_concl
<< " by " << t_concl_exp
<< std::endl
;
731 d_infer
.push_back( t_concl
);
732 d_infer_exp
.push_back( t_concl_exp
);
739 std::vector
< TNode
> assumptions
;
740 explain( j
, assumptions
);
741 explain( t
, assumptions
);
742 explain( jt
[0].eqNode( tt
[0] ), assumptions
);
743 d_conflictNode
= NodeManager::currentNM()->mkNode( AND
, assumptions
);
744 Debug("datatypes-conflict") << "CONFLICT: Tester conflict : " << d_conflictNode
<< std::endl
;
745 d_out
->conflict( d_conflictNode
);
750 EqualityStatus
TheoryDatatypes::getEqualityStatus(TNode a
, TNode b
){
751 if( d_equalityEngine
.hasTerm(a
) && d_equalityEngine
.hasTerm(b
) ){
752 if (d_equalityEngine
.areEqual(a
, b
)) {
753 // The terms are implied to be equal
754 return EQUALITY_TRUE
;
756 if (d_equalityEngine
.areDisequal(a
, b
, false)) {
757 // The terms are implied to be dis-equal
758 return EQUALITY_FALSE
;
761 return EQUALITY_UNKNOWN
;
764 void TheoryDatatypes::computeCareGraph(){
765 Theory::computeCareGraph();
768 void TheoryDatatypes::collectModelInfo( TheoryModel
* m
, bool fullModel
){
769 Trace("dt-model") << std::endl
;
770 printModelDebug( "dt-model" );
771 m
->assertEqualityEngine( &d_equalityEngine
);
772 //must choose proper representatives
773 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( &d_equalityEngine
);
774 while( !eqcs_i
.isFinished() ){
775 Node eqc
= (*eqcs_i
);
776 //for all equivalence classes that are datatypes
777 if( DatatypesRewriter::isTermDatatype( eqc
) ){
778 EqcInfo
* ei
= getOrMakeEqcInfo( eqc
);
780 if( !ei
->d_constructor
.get().isNull() ){
781 //specify that we should use the constructor as the representative
782 m
->assertRepresentative( ei
->d_constructor
.get() );
784 Trace("model-warn") << "WARNING: Datatypes: no constructor in equivalence class " << eqc
<< std::endl
;
785 Trace("model-warn") << " Type : " << eqc
.getType() << std::endl
;
788 Trace("model-warn") << "WARNING: Datatypes: no equivalence class info for " << eqc
<< std::endl
;
789 Trace("model-warn") << " Type : " << eqc
.getType() << std::endl
;
797 void TheoryDatatypes::collectTerms( Node n
) {
798 if( d_collectTermsCache
.find( n
)==d_collectTermsCache
.end() ){
799 d_collectTermsCache
[n
] = true;
800 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ) {
801 collectTerms( n
[i
] );
803 if( n
.getKind() == APPLY_CONSTRUCTOR
){
804 //we must take into account subterm relation when checking for cycles
805 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ) {
806 Debug("datatypes-cycles") << "DtCyc: Subterm " << n
<< " -> " << n
[i
] << endl
;
807 bool result
= d_cycle_check
.addEdgeNode( n
, n
[i
] );
808 d_hasSeenCycle
.set( d_hasSeenCycle
.get() || result
);
810 }else if( n
.getKind() == APPLY_SELECTOR
){
811 if( d_selector_apps
.find( n
)==d_selector_apps
.end() ){
812 d_selector_apps
[n
] = false;
813 //we must also record which selectors exist
814 Debug("datatypes") << " Found selector " << n
<< endl
;
815 if (n
.getType().isBoolean()) {
816 d_equalityEngine
.addTriggerPredicate( n
);
818 d_equalityEngine
.addTerm( n
);
820 Node rep
= getRepresentative( n
[0] );
821 EqcInfo
* eqc
= getOrMakeEqcInfo( rep
, true );
822 if( !eqc
->d_selectors
){
823 eqc
->d_selectors
= true;
824 instantiate( eqc
, rep
);
831 void TheoryDatatypes::processNewTerm( Node n
){
832 Trace("dt-terms") << "Created term : " << n
<< std::endl
;
833 //see if it is rewritten to be something different
834 Node rn
= Rewriter::rewrite( n
);
836 Node eq
= n
.getType().isBoolean() ? rn
.iffNode( n
) : rn
.eqNode( n
);
837 d_pending
.push_back( eq
);
838 d_pending_exp
[ eq
] = NodeManager::currentNM()->mkConst( true );
839 Trace("datatypes-infer") << "DtInfer : " << eq
<< ", trivial" << std::endl
;
840 d_infer
.push_back( eq
);
844 Node
TheoryDatatypes::getInstantiateCons( Node n
, const Datatype
& dt
, int index
){
845 //if( !d_inst_map[n][index].isNull() ){
846 // return d_inst_map[n][index];
848 //add constructor to equivalence class
849 std::vector
< Node
> children
;
850 children
.push_back( Node::fromExpr( dt
[index
].getConstructor() ) );
851 for( int i
=0; i
<(int)dt
[index
].getNumArgs(); i
++ ){
852 Node nc
= NodeManager::currentNM()->mkNode( APPLY_SELECTOR
, Node::fromExpr( dt
[index
][i
].getSelector() ), n
);
853 children
.push_back( nc
);
854 processNewTerm( nc
);
856 Node n_ic
= NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR
, children
);
857 collectTerms( n_ic
);
858 //add type ascription for ambiguous constructor types
859 if(!n_ic
.getType().isComparableTo(n
.getType())) {
860 Assert( dt
.isParametric() );
861 Debug("datatypes-parametric") << "DtInstantiate: ambiguous type for " << n_ic
<< ", ascribe to " << n
.getType() << std::endl
;
862 Debug("datatypes-parametric") << "Constructor is " << dt
[index
] << std::endl
;
863 Type tspec
= dt
[index
].getSpecializedConstructorType(n
.getType().toType());
864 Debug("datatypes-parametric") << "Type specification is " << tspec
<< std::endl
;
865 children
[0] = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION
,
866 NodeManager::currentNM()->mkConst(AscriptionType(tspec
)), children
[0] );
867 n_ic
= NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR
, children
);
868 Assert( n_ic
.getType()==n
.getType() );
870 n_ic
= Rewriter::rewrite( n_ic
);
871 //d_inst_map[n][index] = n_ic;
876 void TheoryDatatypes::collapseSelectors(){
877 //must check incorrect applications of selectors
878 for( BoolMap::iterator it
= d_selector_apps
.begin(); it
!= d_selector_apps
.end(); ++it
){
880 Node n
= getRepresentative( (*it
).first
[0] );
881 Trace("datatypes-collapse") << "Datatypes collapse selector? : " << n
<< std::endl
;
882 EqcInfo
* ei
= getOrMakeEqcInfo( n
, true );
884 if( !ei
->d_constructor
.get().isNull() ){
885 Node op
= (*it
).first
.getOperator();
886 Node cons
= ei
->d_constructor
;
887 Node sn
= NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR
, op
, cons
);
888 Node s
= Rewriter::rewrite( sn
);
890 Node eq
= s
.getType().isBoolean() ? s
.iffNode( sn
) : s
.eqNode( sn
);
891 d_pending
.push_back( eq
);
892 d_pending_exp
[ eq
] = NodeManager::currentNM()->mkConst( true );
893 Trace("datatypes-infer") << "DtInfer : " << eq
<< ", by rewrite" << std::endl
;
894 d_infer
.push_back( eq
);
896 d_selector_apps
[ (*it
).first
] = true;
898 Trace("datatypes-collapse") << "No constructor." << std::endl
;
901 Trace("datatypes-collapse") << "No e info." << std::endl
;
907 void TheoryDatatypes::instantiate( EqcInfo
* eqc
, Node n
){
908 //add constructor to equivalence class if not done so already
909 if( hasLabel( eqc
, n
) && !eqc
->d_inst
){
912 if( !eqc
->d_constructor
.get().isNull() ){
913 exp
= NodeManager::currentNM()->mkConst( true );
914 tt
= eqc
->d_constructor
;
919 int index
= getLabelIndex( eqc
, n
);
920 const Datatype
& dt
= ((DatatypeType
)(tt
.getType()).toType()).getDatatype();
921 //must be finite or have a selector
922 if( eqc
->d_selectors
|| dt
[ index
].isFinite() || mustSpecifyAssignment() ){
923 //instantiate this equivalence class
925 Node tt_cons
= getInstantiateCons( tt
, dt
, index
);
928 eq
= tt
.eqNode( tt_cons
);
929 Debug("datatypes-inst") << "DtInstantiate : " << eqc
<< " " << eq
<< std::endl
;
930 d_pending
.push_back( eq
);
931 d_pending_exp
[ eq
] = exp
;
932 Trace("datatypes-infer") << "DtInfer : " << eq
<< " by " << exp
<< std::endl
;
933 //eqc->d_inst.set( eq );
934 d_infer
.push_back( eq
);
935 d_infer_exp
.push_back( exp
);
941 void TheoryDatatypes::checkCycles() {
942 Debug("datatypes-cycle-check") << "Check cycles" << std::endl
;
943 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( &d_equalityEngine
);
944 while( !eqcs_i
.isFinished() ){
945 Node eqc
= (*eqcs_i
);
946 map
< Node
, bool > visited
;
947 std::vector
< TNode
> expl
;
948 if( searchForCycle( eqc
, eqc
, visited
, expl
) ) {
949 Assert( expl
.size()>0 );
950 if( expl
.size() == 1 ){
951 d_conflictNode
= expl
[ 0 ];
953 d_conflictNode
= NodeManager::currentNM()->mkNode( AND
, expl
);
955 Debug("datatypes-conflict") << "CONFLICT: Cycle conflict : " << d_conflictNode
<< std::endl
;
956 d_out
->conflict( d_conflictNode
);
964 //postcondition: if cycle detected, explanation is why n is a subterm of on
965 bool TheoryDatatypes::searchForCycle( Node n
, Node on
,
966 map
< Node
, bool >& visited
,
967 std::vector
< TNode
>& explanation
, bool firstTime
) {
968 Debug("datatypes-cycle-check") << "Search for cycle " << n
<< " " << on
<< endl
;
972 nn
= getRepresentative( n
);
974 Node lit
= NodeManager::currentNM()->mkNode( EQUAL
, n
, nn
);
975 explain( lit
, explanation
);
981 if( visited
.find( nn
) == visited
.end() ) {
983 EqcInfo
* eqc
= getOrMakeEqcInfo( nn
);
985 Node ncons
= eqc
->d_constructor
.get();
986 if( !ncons
.isNull() ) {
987 for( int i
=0; i
<(int)ncons
.getNumChildren(); i
++ ) {
988 if( searchForCycle( ncons
[i
], on
, visited
, explanation
, false ) ) {
989 if( Debug
.isOn("datatypes-cycles") && !d_cycle_check
.isConnectedNode( n
, ncons
[i
] ) ){
990 Debug("datatypes-cycles") << "Cycle subterm: " << n
<< " is not -> " << ncons
[i
] << "!!!!" << std::endl
;
992 //add explanation for why the constructor is connected
994 Node lit
= NodeManager::currentNM()->mkNode( EQUAL
, n
, ncons
);
995 explain( lit
, explanation
);
1006 bool TheoryDatatypes::mustSpecifyAssignment(){
1007 //FIXME: the condition finiteModelFind is an over-approximation in this function
1008 // we still may not want to specify assignments for datatypes that are truly infinite
1009 // the fix for this is to correctly compute the cardinality for datatypes containing uninterpered sorts in fmf (i.e. by assuming they are finite)
1010 return options::finiteModelFind() || options::produceModels() || options::dtForceAssignment();
1011 //return options::produceModels();
1015 bool TheoryDatatypes::mustCommunicateFact( Node n
, Node exp
){
1016 //the datatypes decision procedure makes 3 "internal" inferences apart from the equality engine :
1017 // (1) Unification : C( t1...tn ) = C( s1...sn ) => ti = si
1018 // (2) Label : ~is_C1( t ) ... ~is_C{i-1}( t ) ~is_C{i+1}( t ) ... ~is_Cn( t ) => is_Ci( t )
1019 // (3) Instantiate : is_C( t ) => t = C( sel_1( t ) ... sel_n( t ) )
1020 //We may need to communicate (3) outwards if the conclusions involve other theories
1021 Trace("dt-lemma-debug") << "Compute for " << exp
<< " => " << n
<< std::endl
;
1022 if( ( n
.getKind()==EQUAL
|| n
.getKind()==IFF
) && n
[1].getKind()==APPLY_CONSTRUCTOR
&& exp
.getKind()!=EQUAL
){
1023 bool addLemma
= false;
1025 const Datatype
& dt
= ((DatatypeType
)(n
[1].getType()).toType()).getDatatype();
1026 addLemma
= dt
.involvesExternalType();
1028 for( int j
=0; j
<(int)n
[1].getNumChildren(); j
++ ){
1029 if( !DatatypesRewriter::isTermDatatype( n
[1][j
] ) ){
1036 //check if we have already added this lemma
1037 if( std::find( d_inst_lemmas
[ n
[0] ].begin(), d_inst_lemmas
[ n
[0] ].end(), n
[1] )==d_inst_lemmas
[ n
[0] ].end() ){
1038 d_inst_lemmas
[ n
[0] ].push_back( n
[1] );
1039 Trace("dt-lemma-debug") << "Communicate " << n
<< std::endl
;
1042 Trace("dt-lemma-debug") << "Already communicated " << n
<< std::endl
;
1047 Trace("dt-lemma-debug") << "Do not need to communicate " << n
<< std::endl
;
1051 bool TheoryDatatypes::hasTerm( Node a
){
1052 return d_equalityEngine
.hasTerm( a
);
1055 bool TheoryDatatypes::areEqual( Node a
, Node b
){
1058 }else if( hasTerm( a
) && hasTerm( b
) ){
1059 return d_equalityEngine
.areEqual( a
, b
);
1065 bool TheoryDatatypes::areDisequal( Node a
, Node b
){
1068 }else if( hasTerm( a
) && hasTerm( b
) ){
1069 return d_equalityEngine
.areDisequal( a
, b
, false );
1075 Node
TheoryDatatypes::getRepresentative( Node a
){
1077 return d_equalityEngine
.getRepresentative( a
);
1084 void TheoryDatatypes::printModelDebug( const char* c
){
1085 if(! (Trace
.isOn(c
))) {
1089 Trace( c
) << "Datatypes model : " << std::endl
;
1090 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( &d_equalityEngine
);
1091 while( !eqcs_i
.isFinished() ){
1092 Node eqc
= (*eqcs_i
);
1093 if( DatatypesRewriter::isTermDatatype( eqc
) ){
1094 Trace( c
) << "DATATYPE : ";
1096 Trace( c
) << eqc
<< " : " << eqc
.getType() << " : " << std::endl
;
1097 Trace( c
) << " { ";
1098 //add terms to model
1099 eq::EqClassIterator eqc_i
= eq::EqClassIterator( eqc
, &d_equalityEngine
);
1100 while( !eqc_i
.isFinished() ){
1101 Trace( c
) << (*eqc_i
) << " ";
1104 Trace( c
) << "}" << std::endl
;
1105 if( DatatypesRewriter::isTermDatatype( eqc
) ){
1106 EqcInfo
* ei
= getOrMakeEqcInfo( eqc
);
1108 Trace( c
) << " Instantiated : " << ei
->d_inst
.get() << std::endl
;
1109 if( ei
->d_constructor
.get().isNull() ){
1110 Trace("model-warn") << eqc
<< " has no constructor in equivalence class!" << std::endl
;
1111 Trace("model-warn") << " Type : " << eqc
.getType() << std::endl
;
1112 Trace( c
) << " Constructor : " << std::endl
;
1113 Trace( c
) << " Labels : ";
1114 if( hasLabel( ei
, eqc
) ){
1115 Trace( c
) << getLabel( eqc
);
1117 NodeListMap::iterator lbl_i
= d_labels
.find( eqc
);
1118 if( lbl_i
!= d_labels
.end() ){
1119 NodeList
* lbl
= (*lbl_i
).second
;
1120 for( NodeList::const_iterator j
= lbl
->begin(); j
!= lbl
->end(); j
++ ){
1121 Trace( c
) << *j
<< " ";
1125 Trace( c
) << std::endl
;
1127 Trace( c
) << " Constructor : " << ei
->d_constructor
.get() << std::endl
;
1129 Trace( c
) << " Selectors : " << ( ei
->d_selectors
? "yes" : "no" ) << std::endl
;