fixed bug in datatypes decision procedure enforcing rewriting of incorrectly applied...

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 224a939fc77672c1617224807a97f7b3f97daef4..34e7c6f112cc701e20ccb67237a09f11ea4695f8 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -782,8 +782,9 @@ void TheoryDatatypes::collapseSelectors(){
   //must check incorrect applications of selectors
   for( BoolMap::iterator it = d_selector_apps.begin(); it != d_selector_apps.end(); ++it ){
     if( !(*it).second ){
-      Node n = (*it).first[0];
-      EqcInfo* ei = getOrMakeEqcInfo( n );
+      Node n = getRepresentative( (*it).first[0] );
+      Trace("datatypes-collapse") << "Datatypes collapse selector? : " << n << std::endl;
+      EqcInfo* ei = getOrMakeEqcInfo( n, true );
       if( ei ){
         if( !ei->d_constructor.get().isNull() ){
           Node op = (*it).first.getOperator();
@@ -798,7 +799,11 @@ void TheoryDatatypes::collapseSelectors(){
             d_infer.push_back( eq );
           }
           d_selector_apps[ (*it).first ] = true;
+        }else{
+          Trace("datatypes-collapse") << "No constructor." << std::endl;
         }
+      }else{
+        Trace("datatypes-collapse") << "No e info." << std::endl;
       }
     }
   }

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