From 25cb880b2e3cd3f3624f9c2ba399a2a50b4b2da7 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 26 Oct 2012 17:18:14 +0000 Subject: [PATCH] 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 --- src/theory/datatypes/theory_datatypes.cpp | 9 +++++++-- test/regress/regress0/datatypes/datatype1.cvc | 4 ++-- test/regress/regress0/datatypes/datatype3.cvc | 4 ++-- 3 files changed, 11 insertions(+), 6 deletions(-) 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 -- 2.30.2