summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/smt_engine.cpp2
-rw-r--r--src/theory/strings/theory_strings.cpp206
-rw-r--r--src/theory/strings/theory_strings.h1
-rw-r--r--test/regress/regress0/strings/Makefile.am9
-rw-r--r--test/regress/regress0/strings/loop001.smt22
-rw-r--r--test/regress/regress0/strings/loop002.smt22
-rw-r--r--test/regress/regress0/strings/loop003.smt22
-rw-r--r--test/regress/regress0/strings/loop005.smt24
-rw-r--r--test/regress/regress0/strings/loop007.smt22
-rw-r--r--test/regress/regress0/strings/model001.smt22
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<d_normal_forms[ni].size() ){
- Node i = d_normal_forms[ni][index];
- Node j = d_normal_forms[nj][index];
+ while( index<nfi.size() ){
+ Node i = nfi[index];
+ Node j = nfj[index];
Trace("strings-solve-debug") << "...Processing " << i << " " << j << std::endl;
if( !areEqual( i, j ) ) {
- 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;
+ }
}
}
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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback