From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Mon, 28 Apr 2014 15:28:25 +0000 (-0400)
Subject: Merge remote-tracking branch 'upstream/master' into sets
X-Git-Tag: cvc5-1.0.0~6956^2~1
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b01a91bb5690b2648a5b8d91f940a6746cba34a3;p=cvc5.git

Merge remote-tracking branch 'upstream/master' into sets
---

b01a91bb5690b2648a5b8d91f940a6746cba34a3
diff --cc src/theory/strings/theory_strings.cpp
index ac5a97167,d03faa72a..d44f38bc3
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@@ -1232,18 -1232,37 +1232,37 @@@ bool TheoryStrings::processNEqc(std::ve
  									Assert( other_str.getKind()!=kind::CONST_STRING, "Other string is not constant." );
  									Assert( other_str.getKind()!=kind::STRING_CONCAT, "Other string is not CONCAT." );
  									antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
- 									Node firstChar = const_str.getConst<String>().size() == 1 ? const_str :
- 										NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) );
- 									//split the string
- 									Node eq1 = Rewriter::rewrite( other_str.eqNode( d_emptyString ) );
- 									Node eq2 = mkSplitEq( "c_spt", "created for v/c split", other_str, firstChar, false );
- 									d_pending_req_phase[ eq1 ] = true;
- 									conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
- 									Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl;
- 
- 									Node ant = mkExplain( antec );
- 									sendLemma( ant, conc, "CST-SPLIT" );
- 									++(d_statistics.d_eq_splits);
+ 									//Opt
+ 									bool optflag = false;
+ 									if( normal_forms[nconst_k].size() > nconst_index_k + 1 &&
+ 										normal_forms[nconst_k][nconst_index_k + 1].isConst() ) {
+ 										CVC4::String stra = const_str.getConst<String>();
+ 										CVC4::String strb = normal_forms[nconst_k][nconst_index_k + 1].getConst<String>();
+ 										CVC4::String fc = strb.substr(0, 1);
+ 										if( stra.find(fc) == std::string::npos ||
+ 											(stra.find(strb) == std::string::npos &&
+ 											 !stra.overlap(strb)) ) {
 -											Node sk = NodeManager::currentNM()->mkSkolem( "sopt_$$", NodeManager::currentNM()->stringType(), "created for string sp" );
++											Node sk = NodeManager::currentNM()->mkSkolem( "sopt", NodeManager::currentNM()->stringType(), "created for string sp" );
+ 											Node eq = other_str.eqNode( mkConcat(const_str, sk) );
+ 											Node ant = mkExplain( antec );
+ 											sendLemma(ant, eq, "CST-EPS");
+ 											optflag = true;
+ 										}
+ 									}
+ 									if(!optflag){
+ 										Node firstChar = const_str.getConst<String>().size() == 1 ? const_str :
+ 											NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) );
+ 										//split the string
+ 										Node eq1 = Rewriter::rewrite( other_str.eqNode( d_emptyString ) );
 -										Node eq2 = mkSplitEq( "c_spt_$$", "created for v/c split", other_str, firstChar, false );
++										Node eq2 = mkSplitEq( "c_spt", "created for v/c split", other_str, firstChar, false );
+ 										d_pending_req_phase[ eq1 ] = true;
+ 										conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
+ 										Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl;
+ 
+ 										Node ant = mkExplain( antec );
+ 										sendLemma( ant, conc, "CST-SPLIT" );
+ 										++(d_statistics.d_eq_splits);
+ 									}
  									return true;
  								} else {
  									std::vector< Node > antec_new_lits;