diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 50 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.h | 2 |
2 files changed, 33 insertions, 19 deletions
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 5da054c3a..224a939fc 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -844,9 +844,14 @@ void TheoryDatatypes::checkCycles() { while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); map< Node, bool > visited; - NodeBuilder<> explanation(kind::AND); - if( searchForCycle( eqc, eqc, visited, explanation ) ) { - d_conflictNode = explanation.getNumChildren() == 1 ? explanation.getChild( 0 ) : explanation; + std::vector< TNode > expl; + if( searchForCycle( eqc, eqc, visited, expl ) ) { + Assert( expl.size()>0 ); + if( expl.size() == 1 ){ + d_conflictNode = expl[ 0 ]; + }else{ + d_conflictNode = NodeManager::currentNM()->mkNode( AND, expl ); + } Debug("datatypes-conflict") << "CONFLICT: Cycle conflict : " << d_conflictNode << std::endl; d_out->conflict( d_conflictNode ); d_conflict = true; @@ -859,26 +864,35 @@ void TheoryDatatypes::checkCycles() { //postcondition: if cycle detected, explanation is why n is a subterm of on bool TheoryDatatypes::searchForCycle( Node n, Node on, map< Node, bool >& visited, - NodeBuilder<>& explanation ) { + std::vector< TNode >& explanation, bool firstTime ) { Debug("datatypes-cycle-check") << "Search for cycle " << n << " " << on << endl; Node ncons; - EqcInfo* eqc = getOrMakeEqcInfo( n ); - if( eqc ){ - Node ncons = eqc->d_constructor.get(); - if( !ncons.isNull() ) { - for( int i=0; i<(int)ncons.getNumChildren(); i++ ) { - Node nn = getRepresentative( ncons[i] ); - if( visited.find( nn ) == visited.end() ) { - visited[nn] = true; - if( nn == on || searchForCycle( nn, on, visited, explanation ) ) { + Node nn; + if( !firstTime ){ + nn = getRepresentative( n ); + if( nn==on ){ + Node lit = NodeManager::currentNM()->mkNode( EQUAL, n, nn ); + explain( lit, explanation ); + return true; + } + }else{ + nn = n; + } + if( visited.find( nn ) == visited.end() ) { + visited[nn] = true; + EqcInfo* eqc = getOrMakeEqcInfo( nn ); + if( eqc ){ + Node ncons = eqc->d_constructor.get(); + if( !ncons.isNull() ) { + for( int i=0; i<(int)ncons.getNumChildren(); i++ ) { + if( searchForCycle( ncons[i], on, visited, explanation, false ) ) { if( Debug.isOn("datatypes-cycles") && !d_cycle_check.isConnectedNode( n, ncons[i] ) ){ Debug("datatypes-cycles") << "Cycle subterm: " << n << " is not -> " << ncons[i] << "!!!!" << std::endl; } - if( nn != ncons[i] ) { - if( Debug.isOn("datatypes-cycles") && !d_cycle_check.isConnectedNode( ncons[i], nn ) ){ - Debug("datatypes-cycles") << "Cycle equality: " << ncons[i] << " is not -> " << nn << "!!!!" << std::endl; - } - explanation << NodeManager::currentNM()->mkNode( EQUAL, nn, ncons[i] ); + //add explanation for why the constructor is connected + if( n != ncons ) { + Node lit = NodeManager::currentNM()->mkNode( EQUAL, n, ncons ); + explain( lit, explanation ); } return true; } diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 26a8d83a9..16e403e95 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -216,7 +216,7 @@ private: void checkCycles(); bool searchForCycle( Node n, Node on, std::map< Node, bool >& visited, - NodeBuilder<>& explanation ); + std::vector< TNode >& explanation, bool firstTime = true ); /** collect terms */ void collectTerms( Node n ); /** get instantiate cons */ |