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

diff --cc src/theory/builtin/theory_builtin_type_rules.h
Simple merge

diff --cc src/theory/quantifiers/first_order_model.cpp
Simple merge

diff --cc src/theory/quantifiers/full_model_check.cpp
Simple merge

diff --cc src/theory/quantifiers/term_database.cpp
Simple merge

diff --cc src/theory/strings/regexp_operation.cpp
Simple merge

diff --cc src/theory/strings/theory_strings.cpp
index ac5a97167cf9efa310c0f30cc3dde13348b1b46d,d03faa72a11ff537f947d582e04c58a96d5120db..d44f38bc3f9eaeca6ab37ec1d68f04d6e9f922d3
--- 1/src/theory/strings/theory_strings.cpp
--- 2/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;