From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 26 Oct 2012 17:18:14 +0000 (+0000)
Subject: fixed bug in datatypes decision procedure enforcing rewriting of incorrectly applied... 
X-Git-Tag: cvc5-1.0.0~7668
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=25cb880b2e3cd3f3624f9c2ba399a2a50b4b2da7;p=cvc5.git

fixed bug in datatypes decision procedure enforcing rewriting of incorrectly applied selector terms, this effects two regression test where TCC fails, using --disable-dt-rewrite-error-sel changes answer of both regression tests
---

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 224a939fc..34e7c6f11 100644
--- 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 71d857400..4c5984cb9 100644
--- 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 1e2b19055..53c9e2ffc 100644
--- 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