- Node li = getLength( i );
- Node lj = getLength( j );
- if( !areEqual(li, lj) ){
- Trace("strings-solve") << "Case 2 : 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() );
- antec.push_back( ni.eqNode( nj ).negate() );
- antec_new_lits.push_back( li.eqNode( lj ).negate() );
- std::vector< Node > conc;
- Node sk1 = NodeManager::currentNM()->mkSkolem( "w1sym_$$", ni.getType(), "created for disequality normalization" );
- Node sk2 = NodeManager::currentNM()->mkSkolem( "w2sym_$$", ni.getType(), "created for disequality normalization" );
- Node sk3 = NodeManager::currentNM()->mkSkolem( "w3sym_$$", ni.getType(), "created for disequality normalization" );
- Node sk4 = NodeManager::currentNM()->mkSkolem( "w4sym_$$", ni.getType(), "created for disequality normalization" );
- Node sk5 = NodeManager::currentNM()->mkSkolem( "w5sym_$$", ni.getType(), "created for disequality normalization" );
- Node w1w2w3 = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 );
- Node w1w4w5 = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk4, sk5 );
- Node s_eq_w1w2w3 = NodeManager::currentNM()->mkNode( kind::EQUAL, ni, w1w2w3 );
- conc.push_back( s_eq_w1w2w3 );
- Node t_eq_w1w4w5 = NodeManager::currentNM()->mkNode( kind::EQUAL, nj, w1w4w5 );
- conc.push_back( t_eq_w1w4w5 );
- Node w2_neq_w4 = sk2.eqNode( sk4 ).negate();
- conc.push_back( w2_neq_w4 );
- Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) );
- Node w2_len_one = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2), one);
- conc.push_back( w2_len_one );
- Node w4_len_one = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk4), one);
- conc.push_back( w4_len_one );
-
- //Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2),
- // NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk4) );
- //conc.push_back( eq );
- sendLemma( mkExplain( antec, antec_new_lits ), NodeManager::currentNM()->mkNode( kind::AND, conc ), "Disequality Normalize" );
- return true;
- }else if( areDisequal( i, j ) ){
- Trace("strings-solve") << "Case 1 : found equal length disequal sub strings " << i << " " << j << std::endl;
- //we are done
- return false;
+ if( i.getKind()==kind::CONST_STRING && j.getKind()==kind::CONST_STRING ){
+ unsigned int len_short = i.getConst<String>().size() < j.getConst<String>().size() ? i.getConst<String>().size() : j.getConst<String>().size();
+ String si = i.getConst<String>().substr(0, len_short);
+ String sj = j.getConst<String>().substr(0, len_short);
+ if(si == sj) {
+ if( i.getConst<String>().size() < j.getConst<String>().size() ) {
+ Node remainderStr = NodeManager::currentNM()->mkConst( j.getConst<String>().substr(len_short) );
+ Trace("strings-solve-debug-test") << "Break normal form of " << nfj[index] << " into " << nfi[index] << ", " << remainderStr << std::endl;
+ nfj.insert( nfj.begin() + index + 1, remainderStr );
+ nfj[index] = nfi[index];
+ } else {
+ Node remainderStr = NodeManager::currentNM()->mkConst( i.getConst<String>().substr(len_short) );
+ Trace("strings-solve-debug-test") << "Break normal form of " << nfi[index] << " into " << nfj[index] << ", " << remainderStr << std::endl;
+ nfi.insert( nfi.begin() + index + 1, remainderStr );
+ nfi[index] = nfj[index];
+ }
+ } else {
+ //conflict
+ return false;
+ }
+ }else{
+ Node li = getLength( i );
+ Node lj = getLength( j );
+ if( areDisequal(li, lj) ){
+ Trace("strings-solve") << "Case 2 : 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() );
+ antec.push_back( ni.eqNode( nj ).negate() );
+ antec_new_lits.push_back( li.eqNode( lj ).negate() );
+ std::vector< Node > conc;
+ Node sk1 = NodeManager::currentNM()->mkSkolem( "xpdsym_$$", ni.getType(), "created for disequality normalization" );
+ Node sk2 = NodeManager::currentNM()->mkSkolem( "ypdsym_$$", ni.getType(), "created for disequality normalization" );
+ Node sk3 = NodeManager::currentNM()->mkSkolem( "zpdsym_$$", ni.getType(), "created for disequality normalization" );
+ Node lsk1 = getLength( sk1 );
+ conc.push_back( lsk1.eqNode( li ) );
+ Node lsk2 = getLength( sk2 );
+ conc.push_back( lsk2.eqNode( lj ) );
+ conc.push_back( NodeManager::currentNM()->mkNode( kind::OR,
+ j.eqNode( mkConcat( sk1, sk3 ) ), i.eqNode( mkConcat( sk2, sk3 ) ) ) );
+
+ /*
+ Node sk1 = NodeManager::currentNM()->mkSkolem( "w1sym_$$", ni.getType(), "created for disequality normalization" );
+ Node sk2 = NodeManager::currentNM()->mkSkolem( "w2sym_$$", ni.getType(), "created for disequality normalization" );
+ Node sk3 = NodeManager::currentNM()->mkSkolem( "w3sym_$$", ni.getType(), "created for disequality normalization" );
+ Node sk4 = NodeManager::currentNM()->mkSkolem( "w4sym_$$", ni.getType(), "created for disequality normalization" );
+ Node sk5 = NodeManager::currentNM()->mkSkolem( "w5sym_$$", ni.getType(), "created for disequality normalization" );
+ Node w1w2w3 = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 );
+ Node w1w4w5 = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk4, sk5 );
+ Node s_eq_w1w2w3 = NodeManager::currentNM()->mkNode( kind::EQUAL, ni, w1w2w3 );
+ conc.push_back( s_eq_w1w2w3 );
+ Node t_eq_w1w4w5 = NodeManager::currentNM()->mkNode( kind::EQUAL, nj, w1w4w5 );
+ conc.push_back( t_eq_w1w4w5 );
+ Node w2_neq_w4 = sk2.eqNode( sk4 ).negate();
+ conc.push_back( w2_neq_w4 );
+ Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) );
+ Node w2_len_one = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2), one);
+ conc.push_back( w2_len_one );
+ Node w4_len_one = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk4), one);
+ conc.push_back( w4_len_one );
+ Node c = NodeManager::currentNM()->mkNode( kind::AND, conc );
+ */
+ //Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2),
+ // NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk4) );
+ //conc.push_back( eq );
+ sendLemma( mkExplain( antec, antec_new_lits ), NodeManager::currentNM()->mkNode( kind::AND, conc ), "Disequality Normalize" );
+ return true;
+ }else if( areEqual( li, lj ) ){
+ if( areDisequal( i, j ) ){
+ Trace("strings-solve") << "Case 1 : found equal length disequal sub strings " << i << " " << j << std::endl;
+ //we are done
+ return false;
+ } else {
+ //splitting on demand : try to make them disequal
+ Node eq = i.eqNode( j );
+ sendSplit( i, j, "Disequality : disequal terms" );
+ eq = Rewriter::rewrite( eq );
+ d_pending_req_phase[ eq ] = false;
+ return true;
+ }
+ }else{
+ //splitting on demand : try to make lengths equal
+ Node eq = li.eqNode( lj );
+ sendSplit( li, lj, "Disequality : equal length" );
+ eq = Rewriter::rewrite( eq );
+ d_pending_req_phase[ eq ] = true;
+ return true;
+ }