diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-26 17:18:14 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-26 17:18:14 +0000 |
| commit | 25cb880b2e3cd3f3624f9c2ba399a2a50b4b2da7 (patch) | |
| tree | ea6435737fb0a677816301b717ad44d8b75b3564 | |
| parent | ddd3797ee72443bd35f6cea146c3752ea0dd2286 (diff) | |
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
| -rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 9 | ||||
| -rw-r--r-- | test/regress/regress0/datatypes/datatype1.cvc | 4 | ||||
| -rw-r--r-- | 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 |