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 12:35:15 -0600 |
commit | 6c2616980ddb8d0c6c92a6a790cba16ac94d7d21 (patch) | |
tree | 0d3544e05edd3c2344c472d3b1d542839686aefe | |
parent | 68fcb0947e58ba12ae8d07bd8a253fbbd9f8ec34 (diff) |
bring back D-Norm
-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; } - //} + } } } } |