- if( areDisequal(li, lj) ){
- //if( i.getKind()==kind::CONST_STRING || j.getKind()==kind::CONST_STRING ){
-
- Trace("strings-solve") << "Non-Simple Case 1 : add lemma " << std::endl;
- //must add lemma
- std::vector< Node > antec;
- std::vector< Node > antec_new_lits;
- antec.insert( antec.end(), d_normal_forms_exp[ni].begin(), d_normal_forms_exp[ni].end() );
- antec.insert( antec.end(), d_normal_forms_exp[nj].begin(), d_normal_forms_exp[nj].end() );
- //check disequal
- if( areDisequal( ni, nj ) ){
- antec.push_back( ni.eqNode( nj ).negate() );
+ if( areDisequal( li, lj ) ){
+ if( i.getKind()==kind::CONST_STRING || j.getKind()==kind::CONST_STRING ){
+ //check if empty
+ Node const_k = i.getKind() == kind::CONST_STRING ? i : j;
+ Node nconst_k = i.getKind() == kind::CONST_STRING ? j : i;
+ Node lnck = i.getKind() == kind::CONST_STRING ? lj : li;
+ if( !d_equalityEngine.areDisequal( nconst_k, d_emptyString, true ) ){
+ Node eq = nconst_k.eqNode( d_emptyString );
+ Node conc = NodeManager::currentNM()->mkNode( kind::OR, eq, eq.negate() );
+ sendInference( d_empty_vec, conc, "D-DISL-Emp-Split" );
+ return true;
+ }else{
+ //split on first character
+ CVC4::String str = const_k.getConst<String>();
+ Node firstChar = str.size() == 1 ? const_k : NodeManager::currentNM()->mkConst( str.prefix( 1 ) );
+ if( areEqual( lnck, d_one ) ){
+ if( areDisequal( firstChar, nconst_k ) ){
+ return true;
+ }else if( !areEqual( firstChar, nconst_k ) ){
+ //splitting on demand : try to make them disequal
+ Node eq = firstChar.eqNode( nconst_k );
+ sendSplit( firstChar, nconst_k, "S-Split(DEQL-Const)" );
+ eq = Rewriter::rewrite( eq );
+ d_pending_req_phase[ eq ] = false;
+ return true;
+ }
+ }else{
+ Node sk = mkSkolemCached( nconst_k, firstChar, sk_id_dc_spt, "dc_spt", 2 );
+ Node skr = mkSkolemCached( nconst_k, firstChar, sk_id_dc_spt_rem, "dc_spt_rem", -1 );
+ Node eq1 = nconst_k.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk, skr ) );
+ eq1 = Rewriter::rewrite( eq1 );
+ Node eq2 = nconst_k.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, skr ) );
+ std::vector< Node > antec;
+ antec.insert( antec.end(), d_normal_forms_exp[ni].begin(), d_normal_forms_exp[ni].end() );
+ antec.insert( antec.end(), d_normal_forms_exp[nj].begin(), d_normal_forms_exp[nj].end() );
+ antec.push_back( nconst_k.eqNode( d_emptyString ).negate() );
+ sendInference( antec, NodeManager::currentNM()->mkNode( kind::OR,
+ NodeManager::currentNM()->mkNode( kind::AND, eq1, sk.eqNode( firstChar ).negate() ), eq2 ), "D-DISL-CSplit" );
+ d_pending_req_phase[ eq1 ] = true;
+ return true;
+ }
+ }