fixed problem with datatypes giving incorrect explanations, now corrected and improve...

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 5da054c3ac9e3ce0ae2d8d06fb412bb1c724039e..224a939fc77672c1617224807a97f7b3f97daef4 100644 (file)
--- 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 26a8d83a92363e76a209af7ae42ef795c77717bf..16e403e95e99c4bf1eb77a7a5fbfdccb813281bb 100644 (file)
--- 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 */

diff --git a/test/regress/regress0/datatypes/datatype1.cvc b/test/regress/regress0/datatypes/datatype1.cvc
index 4c5984cb9bfa4ab7350283df71de72c30e201834..71d857400b55211583a43e2d36d594c97d10c474 100644 (file)
--- a/test/regress/regress0/datatypes/datatype1.cvc
+++ b/test/regress/regress0/datatypes/datatype1.cvc
@@ -1,5 +1,5 @@
-% EXPECT: valid
-% EXIT: 20
+% EXPECT: invalid
+% EXIT: 10
 
 DATATYPE
   tree = node(left : tree, right : tree) | leaf

diff --git a/test/regress/regress0/datatypes/datatype3.cvc b/test/regress/regress0/datatypes/datatype3.cvc
index 53c9e2ffc5a7756efa36686786d60569a1733cf7..1e2b19055dd829954a05818d6660b011e2f688a4 100644 (file)
--- a/test/regress/regress0/datatypes/datatype3.cvc
+++ b/test/regress/regress0/datatypes/datatype3.cvc
@@ -1,5 +1,5 @@
-% EXPECT: valid
-% EXIT: 20
+% EXPECT: invalid
+% EXIT: 10
 
 DATATYPE
   tree = node(left : tree, right : tree) | leaf