From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Fri, 7 Mar 2014 18:35:15 +0000 (-0600)
Subject: bring back D-Norm
X-Git-Tag: cvc5-1.0.0~7039^2~1
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6c2616980ddb8d0c6c92a6a790cba16ac94d7d21;p=cvc5.git

bring back D-Norm
---

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;
 						}
-					//}
+					}
 				}
 			}
 		}