From a747f01c1ee737bb8c4c1cc8ce355b79078d03d7 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Mon, 30 Sep 2013 23:29:57 -0500 Subject: [PATCH] replace with a new method for disequality, move to QF_S --- src/smt/smt_engine.cpp | 2 +- src/theory/strings/theory_strings.cpp | 206 +++++++++++++------- src/theory/strings/theory_strings.h | 1 + test/regress/regress0/strings/Makefile.am | 9 +- test/regress/regress0/strings/loop001.smt2 | 2 +- test/regress/regress0/strings/loop002.smt2 | 2 +- test/regress/regress0/strings/loop003.smt2 | 2 +- test/regress/regress0/strings/loop005.smt2 | 4 - test/regress/regress0/strings/loop007.smt2 | 2 +- test/regress/regress0/strings/model001.smt2 | 2 +- 10 files changed, 146 insertions(+), 86 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 39ccc70c4..1d080ea6a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -835,7 +835,7 @@ void SmtEngine::setLogicInternal() throw() { // Set the options for the theoryOf if(!options::theoryOfMode.wasSetByUser()) { - if(d_logic.isSharingEnabled() && !d_logic.isTheoryEnabled(THEORY_BV)) { + if(d_logic.isSharingEnabled() && !d_logic.isTheoryEnabled(THEORY_BV) && !d_logic.isTheoryEnabled(THEORY_STRINGS)) { Trace("smt") << "setting theoryof-mode to term-based" << endl; options::theoryOfMode.set(THEORY_OF_TERM_BASED); } diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 1a3fe62b4..bf61d3852 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -752,24 +752,36 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v }else{ Node length_term_i = getLength( normal_forms[i][index_i] ); Node length_term_j = getLength( normal_forms[j][index_j] ); - //check if length(normal_forms[i][index]) == length(normal_forms[j][index]) - if( areEqual(length_term_i, length_term_j) ){ - Trace("strings-solve-debug") << "Case 2 : string lengths are equal" << std::endl; - //length terms are equal, merge equivalence classes if not already done so - Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], normal_forms[j][index_j] ); - std::vector< Node > temp_exp; - temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() ); - temp_exp.push_back(NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j )); - Node eq_exp = temp_exp.empty() ? d_true : - temp_exp.size() == 1 ? temp_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, temp_exp ); - Trace("strings-lemma") << "Strings : Infer " << eq << " from " << eq_exp << std::endl; - //d_equalityEngine.assertEquality( eq, true, eq_exp ); - d_pending.push_back( eq ); - d_pending_exp[eq] = eq_exp; - d_infer.push_back(eq); - d_infer_exp.push_back(eq_exp); - return; - + //check length(normal_forms[i][index]) == length(normal_forms[j][index]) + if( !areDisequal(length_term_i, length_term_j) && + normal_forms[i][index_i].getKind()!=kind::CONST_STRING && + normal_forms[j][index_j].getKind()!=kind::CONST_STRING ) { + + //length terms are equal, merge equivalence classes if not already done so + Node length_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ); + if( !areEqual(length_term_i, length_term_j) ) { + Trace("strings-solve-debug") << "Case 2.1 : string lengths neither equal nor disequal" << std::endl; + //try to make the lengths equal via splitting on demand + sendSplit( length_term_i, length_term_j, "Length" ); + length_eq = Rewriter::rewrite( length_eq ); + d_pending_req_phase[ length_eq ] = true; + return; + }else{ + Trace("strings-solve-debug") << "Case 2.2 : string lengths are explicitly equal" << std::endl; + //lengths are already equal, do unification + Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], normal_forms[j][index_j] ); + std::vector< Node > temp_exp; + temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() ); + temp_exp.push_back(length_eq); + Node eq_exp = temp_exp.empty() ? d_true : + temp_exp.size() == 1 ? temp_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, temp_exp ); + Trace("strings-lemma") << "Strings : Infer " << eq << " from " << eq_exp << std::endl; + d_pending.push_back( eq ); + d_pending_exp[eq] = eq_exp; + d_infer.push_back(eq); + d_infer_exp.push_back(eq_exp); + return; + } }else if( ( normal_forms[i][index_i].getKind()!=kind::CONST_STRING && index_i==normal_forms[i].size()-1 ) || ( normal_forms[j][index_j].getKind()!=kind::CONST_STRING && index_j==normal_forms[j].size()-1 ) ){ Trace("strings-solve-debug") << "Case 3 : at endpoint" << std::endl; @@ -974,16 +986,6 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v }else{ antec_new_lits.push_back(ldeq); } - // first, M |=/= |x|=|y|, then x=y - Node len_x = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, normal_forms[i][index_i] ); - Node len_y = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, normal_forms[j][index_j] ); - if( !areDisequal( len_x, len_y ) ) { - Node x_eq_y = Rewriter::rewrite( normal_forms[i][index_i].eqNode( normal_forms[j][index_j] ) ); - antec_new_lits.push_back( x_eq_y.negate() ); - d_pending_req_phase[ x_eq_y ] = true; - } - - // second, split Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for v/v split" ); Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[j][index_j], sk ) ); @@ -1042,52 +1044,107 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v bool TheoryStrings::normalizeDisequality( Node ni, Node nj ) { //Assert( areDisequal( ni, nj ) ); if( d_normal_forms[ni].size()>1 || d_normal_forms[nj].size()>1 ){ + std::vector< Node > nfi; + nfi.insert( nfi.end(), d_normal_forms[ni].begin(), d_normal_forms[ni].end() ); + std::vector< Node > nfj; + nfj.insert( nfj.end(), d_normal_forms[nj].begin(), d_normal_forms[nj].end() ); + unsigned index = 0; - while( index 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().size() < j.getConst().size() ? i.getConst().size() : j.getConst().size(); + String si = i.getConst().substr(0, len_short); + String sj = j.getConst().substr(0, len_short); + if(si == sj) { + if( i.getConst().size() < j.getConst().size() ) { + Node remainderStr = NodeManager::currentNM()->mkConst( j.getConst().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().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; + } } } index++; @@ -1238,6 +1295,13 @@ void TheoryStrings::sendSplit( Node a, Node b, const char * c ) { d_pending_req_phase[eq] = true; } +Node TheoryStrings::mkConcat( Node n1, Node n2 ) { + std::vector< Node > c; + c.push_back( n1 ); + c.push_back( n2 ); + return mkConcat( c ); +} + Node TheoryStrings::mkConcat( std::vector< Node >& c ) { Node cc = c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c ) : ( c.size()==1 ? c[0] : d_emptyString ); return Rewriter::rewrite( cc ); diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 6b8144d6e..52c7288a8 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -222,6 +222,7 @@ protected: void sendLemma( Node ant, Node conc, const char * c ); void sendSplit( Node a, Node b, const char * c ); /** mkConcat **/ + Node mkConcat( Node n1, Node n2 ); Node mkConcat( std::vector< Node >& c ); /** mkExplain **/ Node mkExplain( std::vector< Node >& a, std::vector< Node >& an ); diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index a1ae66a5f..90872cf4d 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -27,14 +27,13 @@ TESTS = \ str005.smt2 \ model001.smt2 \ loop001.smt2 \ + loop002.smt2 \ loop003.smt2 \ + loop004.smt2 \ + loop005.smt2 \ + loop006.smt2 \ loop007.smt2 -# loop002.smt2 -# loop004.smt2 -# loop005.smt2 -# loop006.smt2 - FAILING_TESTS = EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/strings/loop001.smt2 b/test/regress/regress0/strings/loop001.smt2 index 11460b335..815acce5c 100644 --- a/test/regress/regress0/strings/loop001.smt2 +++ b/test/regress/regress0/strings/loop001.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_S) (set-info :status unsat) (declare-fun x () String) diff --git a/test/regress/regress0/strings/loop002.smt2 b/test/regress/regress0/strings/loop002.smt2 index 2f96241dc..90492189f 100644 --- a/test/regress/regress0/strings/loop002.smt2 +++ b/test/regress/regress0/strings/loop002.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_S) (set-info :status sat) (declare-fun x () String) diff --git a/test/regress/regress0/strings/loop003.smt2 b/test/regress/regress0/strings/loop003.smt2 index b4fbcf7d5..1247170c9 100644 --- a/test/regress/regress0/strings/loop003.smt2 +++ b/test/regress/regress0/strings/loop003.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_S) (set-info :status sat) (declare-fun x () String) diff --git a/test/regress/regress0/strings/loop005.smt2 b/test/regress/regress0/strings/loop005.smt2 index 6e5fc96d4..4401ef794 100644 --- a/test/regress/regress0/strings/loop005.smt2 +++ b/test/regress/regress0/strings/loop005.smt2 @@ -1,7 +1,3 @@ -; COMMAND-LINE: --no-check-models -; EXPECT: sat -; EXIT: 10 -; (set-logic QF_S) (set-info :status sat) diff --git a/test/regress/regress0/strings/loop007.smt2 b/test/regress/regress0/strings/loop007.smt2 index 0534d8b53..bea4037d1 100644 --- a/test/regress/regress0/strings/loop007.smt2 +++ b/test/regress/regress0/strings/loop007.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_S) (set-info :status sat) (declare-fun x () String) diff --git a/test/regress/regress0/strings/model001.smt2 b/test/regress/regress0/strings/model001.smt2 index 2832b5c96..ac43afee1 100644 --- a/test/regress/regress0/strings/model001.smt2 +++ b/test/regress/regress0/strings/model001.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_S) (set-info :status sat) (set-option :produce-models true) -- 2.30.2