From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Tue, 3 Dec 2013 19:53:47 +0000 (-0600)
Subject: string fmf perfomance fix
X-Git-Tag: cvc5-1.0.0~7219
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d896d6c67c7fe262a18aefc770e85185fa8286ff;p=cvc5.git

string fmf perfomance fix
---

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index b8f3f496f..226411b8a 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -356,12 +356,12 @@ void TheoryStrings::preRegisterTerm(TNode n) {
     if(n.getKind() == kind::VARIABLE || n.getKind()==kind::SKOLEM) {
 	  if( std::find( d_length_intro_vars.begin(), d_length_intro_vars.end(), n )==d_length_intro_vars.end() ){
 		  Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n);
-		  //Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, n_len, d_zero);
-		  Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR,
-			n_len.eqNode( d_zero ),
-			NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) );
+		  Node n_len_eq_z = n_len.eqNode( d_zero );
+		  Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR, n_len_eq_z,
+									NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) );
 		  Trace("strings-lemma") << "Strings::Lemma LENGTH geq 0 : " << n_len_geq_zero << std::endl;
 		  d_out->lemma(n_len_geq_zero);
+		  d_out->requirePhase( n_len_eq_z, true );
 	  }
 	  // FMF
 	  if( n.getKind() == kind::VARIABLE ) {//options::stringFMF() &&