diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-03-07 12:35:15 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-03-07 15:03:45 -0600 |
| commit | ed61fb35596949aaa59ba5481c823f2ba99b6b5c (patch) | |
| tree | 15ac63b2583d3c489f071006598ff654bfbee219 /src/theory | |
| parent | 2594dfe76830d3e03aedf6bc3310bce6d362e4eb (diff) | |
bring back D-Norm
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index f819d46fb..fd9605e59 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1979,10 +1979,10 @@ void TheoryStrings::checkDeqNF() { for( unsigned j=0; j<cols[i].size(); j++ ){ for( unsigned k=(j+1); k<cols[i].size(); k++ ){ Assert( !d_conflict ); - //if( !areDisequal( cols[i][j], cols[i][k] ) ){ - // sendSplit( cols[i][j], cols[i][k], "D-NORM", false ); - // return; - //}else{ + if( !areDisequal( cols[i][j], cols[i][k] ) ){ + sendSplit( cols[i][j], cols[i][k], "D-NORM", false ); + return; + }else{ Trace("strings-solve") << "- Compare "; printConcat( d_normal_forms[cols[i][j]], "strings-solve" ); Trace("strings-solve") << " against "; @@ -1991,7 +1991,7 @@ void TheoryStrings::checkDeqNF() { if( processDeq( cols[i][j], cols[i][k] ) ){ return; } - //} + } } } } |