diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-01 14:44:42 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-01 14:44:42 +0100 |
| commit | ad213ae499e01fc06e5b24f0ba7a0a7f8fb52abc (patch) | |
| tree | a3d6d69fbbce97d0bc9bc915b176b07e1e722efc /src | |
| parent | 6b652f7239aaf7ef1793eb115a6e7371a3ec54eb (diff) | |
Simplify which lemmas to communicate in dt.
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 2b5e52415..c03040868 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -1760,20 +1760,23 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){ // (4) collapse selector : S( C( t1...tn ) ) = t' // (5) collapse term size : size( C( t1...tn ) ) = 1 + size( t1 ) + ... + size( tn ) // (6) non-negative size : 0 <= size( t ) - //We may need to communicate (3) outwards if the conclusions involve other theories. Also communicate (5), (6), and OR conclusions. + //We may need to communicate outwards if the conclusions involve other theories. Also communicate (6) and OR conclusions. Trace("dt-lemma-debug") << "Compute for " << exp << " => " << n << std::endl; bool addLemma = false; - if( ( n.getKind()==EQUAL || n.getKind()==IFF) && n[1].getKind()==APPLY_CONSTRUCTOR && exp.getKind()!=EQUAL ){ - const Datatype& dt = ((DatatypeType)(n[1].getType()).toType()).getDatatype(); - addLemma = dt.involvesExternalType(); + if( n.getKind()==EQUAL || n.getKind()==IFF ){ + TypeNode tn = n[0].getType(); + if( !tn.isDatatype() ){ + addLemma = true; + }else{ + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + addLemma = dt.involvesExternalType(); + } //for( int j=0; j<(int)n[1].getNumChildren(); j++ ){ // if( !DatatypesRewriter::isTermDatatype( n[1][j] ) ){ // addLemma = true; // break; // } //} - }else if( n.getKind()==EQUAL && !n[0].getType().isDatatype() ){ - addLemma = true; }else if( n.getKind()==LEQ ){ addLemma = true; }else if( n.getKind()==OR ){ |