adds LB strategy

diff --git a/src/theory/strings/options b/src/theory/strings/options
index 68d1f7bde93729ca405be9de7f237690d98e69dd..8bede6cae5bb41b6f964d36f5cceeb32f9712cfa 100644 (file)
--- a/src/theory/strings/options
+++ b/src/theory/strings/options
@@ -5,13 +5,16 @@
 
 module STRINGS "theory/strings/options.h" Strings theory
 
-option stringCharCardinality str-alphabet-card --str-alphabet-card=N int16_t :default 256 :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h"
+option stringCharCardinality strings-alphabet-card --strings-alphabet-card=N int16_t :default 256 :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h"
  the cardinality of the characters used by the theory of strings, default 256
 
-option stringRegExpUnrollDepth str-regexp-depth --str-regexp-depth=N int16_t :default 10 :read-write
+option stringRegExpUnrollDepth strings-regexp-depth --strings-regexp-depth=N int16_t :default 10 :read-write
  the depth of unrolloing regular expression used by the theory of strings, default 10
 
-option stringFMF fmf-strings --fmf-strings bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h"
+option stringFMF strings-fmf --strings-fmf bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h"
  the finite model finding used by the theory of strings
 
+option stringLB strings-lb --strings-lb=N unsigned :default 0 :predicate less_equal(2) :predicate-include "smt/smt_engine.h"
+ the strategy of LB rule application: 0-lazy, 1-eager, 2-no
+
 endmodule

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 91647802434929ce01b35c2cdd9c48c21a1378a3..9a88883fc71762dff1d4558d206f4948fc93275b 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -737,7 +737,7 @@ bool TheoryStrings::detectLoop( std::vector< std::vector< Node > > &normal_forms
                                                                int i, int j, int index_i, int index_j, 
                                                                int &loop_in_i, int &loop_in_j) {
        int has_loop[2] = { -1, -1 };
-       //if( !options::stringFMF() ) {
+       if( options::stringLB() != 2 ) {
                for( unsigned r=0; r<2; r++ ) {
                        int index = (r==0 ? index_i : index_j);
                        int other_index = (r==0 ? index_j : index_i );
@@ -752,7 +752,7 @@ bool TheoryStrings::detectLoop( std::vector< std::vector< Node > > &normal_forms
                                }
                        }
                }
-       //}
+       }
        if( has_loop[0]!=-1 || has_loop[1]!=-1 ) {
                loop_in_i = has_loop[0];
                loop_in_j = has_loop[1];
@@ -762,14 +762,12 @@ bool TheoryStrings::detectLoop( std::vector< std::vector< Node > > &normal_forms
        }
 }
 //xs(zy)=t(yz)xr
-bool TheoryStrings::processLoop(std::vector< Node > &curr_exp, 
+bool TheoryStrings::processLoop(std::vector< Node > &antec, 
                                                                std::vector< std::vector< Node > > &normal_forms,
                                                                std::vector< Node > &normal_form_src,
                                                                int i, int j, int loop_n_index, int other_n_index,
                                                                int loop_index, int index, int other_index) {
        Node conc;
-       std::vector< Node > antec;
-       std::vector< Node > antec_new_lits;
        Trace("strings-loop") << "Detected possible loop for " << normal_forms[loop_n_index][loop_index] << std::endl;
        Trace("strings-loop") << " ... (X)= " << normal_forms[other_n_index][other_index] << std::endl;
        
@@ -817,14 +815,12 @@ bool TheoryStrings::processLoop(std::vector< Node > &curr_exp,
                }
                if(flag) {
                        Trace("strings-loop") << "Strings::Loop: tails are different." << std::endl;
-                       antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
-                       Node ant = mkExplain( antec, antec_new_lits );
+                       Node ant = mkExplain( antec );
                        sendLemma( ant, conc, "Conflict" );
                        return true;
                }
        }
 
-       antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
        //require that x is non-empty
        if( !areDisequal( normal_forms[loop_n_index][loop_index], d_emptyString ) ){
                //try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop
@@ -838,7 +834,7 @@ bool TheoryStrings::processLoop(std::vector< Node > &curr_exp,
                if( t_yz.getKind()!=kind::CONST_STRING ) {
                        antec.push_back( t_yz.eqNode( d_emptyString ).negate() );
                }
-               Node ant = mkExplain( antec, antec_new_lits );
+               Node ant = mkExplain( antec );
                if(d_loop_antec.find(ant) == d_loop_antec.end()) {
                        d_loop_antec[ant] = true;
 
@@ -903,6 +899,8 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
                                                                std::vector< std::vector< Node > > &normal_forms_exp,
                                                                std::vector< Node > &normal_form_src) {
        bool flag_lb = false;
+       std::vector< Node > c_lb_exp;
+       int c_i, c_j, c_loop_n_index, c_other_n_index, c_loop_index, c_index, c_other_index;
        for(unsigned i=0; i<normal_forms.size()-1; i++) {
                //unify each normalform[j] with normal_forms[i]
                for( unsigned j=i+1; j<normal_forms.size(); j++ ) {
@@ -1001,7 +999,6 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
                                                                Node conc;
                                                                std::vector< Node > antec;
                                                                antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
-                                                               std::vector< Node > antec_new_lits;
                                                                std::vector< Node > eqn;
                                                                for( unsigned r=0; r<2; r++ ) {
                                                                        int index_k = r==0 ? index_i : index_j;
@@ -1016,7 +1013,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
                                                                        addNormalFormPair( normal_form_src[i], normal_form_src[j] );
                                                                } else {
                                                                        conc = eqn[0].eqNode( eqn[1] );
-                                                                       Node ant = mkExplain( antec, antec_new_lits );
+                                                                       Node ant = mkExplain( antec );
                                                                        sendLemma( ant, conc, "ENDPOINT" );
                                                                        return true;
                                                                }
@@ -1024,22 +1021,30 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
                                                                Trace("strings-solve-debug") << "Case 4 : must compare strings" << std::endl;
                                                                int loop_in_i = -1;
                                                                int loop_in_j = -1;
-                                                               if(!flag_lb && detectLoop(normal_forms, i, j, index_i, index_j, loop_in_i, loop_in_j)) {
-                                                                       //flag_lb = true;
-                                                                       int loop_n_index = loop_in_i!=-1 ? i : j;
-                                                                       int other_n_index = loop_in_i!=-1 ? j : i;
-                                                                       int loop_index = loop_in_i!=-1 ? loop_in_i : loop_in_j;
-                                                                       int index = loop_in_i!=-1 ? index_i : index_j;
-                                                                       int other_index = loop_in_i!=-1 ? index_j : index_i;
-
-                                                                       if(processLoop(curr_exp, normal_forms, normal_form_src, 
-                                                                               i, j, loop_n_index, other_n_index, loop_index, index, other_index)) {
-                                                                               return true;
+                                                               if(detectLoop(normal_forms, i, j, index_i, index_j, loop_in_i, loop_in_j)) {
+                                                                       if(!flag_lb) {
+                                                                               c_i = i;
+                                                                               c_j = j;
+                                                                               c_loop_n_index = loop_in_i!=-1 ? i : j;
+                                                                               c_other_n_index = loop_in_i!=-1 ? j : i;
+                                                                               c_loop_index = loop_in_i!=-1 ? loop_in_i : loop_in_j;
+                                                                               c_index = loop_in_i!=-1 ? index_i : index_j;
+                                                                               c_other_index = loop_in_i!=-1 ? index_j : index_i;
+
+                                                                               c_lb_exp = curr_exp;
+
+                                                                               if(options::stringLB() == 0) {
+                                                                                       flag_lb = true;
+                                                                               } else {
+                                                                                       if(processLoop(c_lb_exp, normal_forms, normal_form_src, 
+                                                                                               c_i, c_j, c_loop_n_index, c_other_n_index, c_loop_index, c_index, c_other_index)) {
+                                                                                               return true;
+                                                                                       }
+                                                                               }
                                                                        }
                                                                } else {
                                                                        Node conc;
                                                                        std::vector< Node > antec;
-                                                                       std::vector< Node > antec_new_lits;
                                                                        Trace("strings-solve-debug") << "No loops detected." << std::endl;
                                                                        if( normal_forms[i][index_i].getKind() == kind::CONST_STRING ||
                                                                                normal_forms[j][index_j].getKind() == kind::CONST_STRING) {
@@ -1066,7 +1071,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
                                                                                        } else {
                                                                                                //curr_exp is conflict
                                                                                                antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
-                                                                                               Node ant = mkExplain( antec, antec_new_lits );
+                                                                                               Node ant = mkExplain( antec );
                                                                                                sendLemma( ant, conc, "Conflict" );
                                                                                                return true;
                                                                                        }
@@ -1076,21 +1081,18 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
                                                                                        Node firstChar = const_str.getConst<String>().size() == 1 ? const_str :
                                                                                                NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) );
                                                                                        //split the string
-                                                                                       //Node sk = NodeManager::currentNM()->mkSkolem( "c_spt_$$", normal_forms[i][index_i].getType(), "created for v/c split" );
-
-                                                                                       Node eq1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, d_emptyString ) );
+                                                                                       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 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL, other_str,
-                                                                                       //                      NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, sk ) ) );
                                                                                        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, antec_new_lits );
+                                                                                       Node ant = mkExplain( antec );
                                                                                        sendLemma( ant, conc, "CST-SPLIT" );
                                                                                        return true;
                                                                                }
                                                                        } else {
+                                                                               std::vector< Node > antec_new_lits;
                                                                                antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
 
                                                                                Node ldeq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ).negate();
@@ -1119,13 +1121,6 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
                                                                                Node eq1 = mkSplitEq( "v_spt_l_$$", "created for v/v split", normal_forms[i][index_i], normal_forms[j][index_j], true );
                                                                                Node eq2 = mkSplitEq( "v_spt_r_$$", "created for v/v split", normal_forms[j][index_j], normal_forms[i][index_i], true );
                                                                                conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
-                                                                               // |sk| > 0
-                                                                               ////Node sk_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
-                                                                               ////Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::GT, sk_len, d_zero);
-                                                                               //Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, d_emptyString).negate();
-                                                                               //Trace("strings-lemma") << "Strings lemma : " << sk_gt_zero << std::endl;
-                                                                               ////d_out->lemma(sk_gt_zero);
-                                                                               //d_lemma_cache.push_back( sk_gt_zero );
 
                                                                                Node ant = mkExplain( antec, antec_new_lits );
                                                                                sendLemma( ant, conc, "VAR-SPLIT" );
@@ -1143,11 +1138,13 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
                }
        }
        if(flag_lb) {
-               //TODO
-               return true;
-       } else {
-               return false;
+               if(processLoop(c_lb_exp, normal_forms, normal_form_src, 
+                       c_i, c_j, c_loop_n_index, c_other_n_index, c_loop_index, c_index, c_other_index)) {
+                       return true;
+               }
        }
+
+       return false;
 }
 
 //nf_exp is conjunction

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index c7ea830b67258a17b207d887d45a5a630d4cc4b1..9fae67a9f95f8122923102806348898b6147b2c1 100644 (file)
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -198,7 +198,7 @@ private:
        bool detectLoop(std::vector< std::vector< Node > > &normal_forms,
                                        int i, int j, int index_i, int index_j, 
                                        int &loop_in_i, int &loop_in_j);
-       bool processLoop(std::vector< Node > &curr_exp,
+       bool processLoop(std::vector< Node > &antec,
                                         std::vector< std::vector< Node > > &normal_forms,
                                         std::vector< Node > &normal_form_src,
                                         int i, int j, int loop_n_index, int other_n_index,

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index c98f37958219d611ddc64cdc98a0560328399051..e24cbc565076a16d7bbc36ee064002823069c35d 100644 (file)
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -26,6 +26,7 @@ TESTS =       \
   str004.smt2 \
   str005.smt2 \
   str006.smt2 \
+  str007.smt2 \
   fmf001.smt2 \
   fmf002.smt2 \
   model001.smt2 \

diff --git a/test/regress/regress0/strings/cardinality.smt2 b/test/regress/regress0/strings/cardinality.smt2
index 465ea0b5e0e31e0e9dd80d103a645e1e0236341c..d64bc240e8fc33f1a3040d19fd9409e77c583c38 100644 (file)
--- a/test/regress/regress0/strings/cardinality.smt2
+++ b/test/regress/regress0/strings/cardinality.smt2
@@ -1,7 +1,7 @@
 (set-logic QF_S)
 (set-info :status unsat)
 
-(set-option :str-alphabet-card 2)
+(set-option :strings-alphabet-card 2)
 
 (declare-fun x () String)
 (declare-fun y () String)

diff --git a/test/regress/regress0/strings/fmf001.smt2 b/test/regress/regress0/strings/fmf001.smt2
index a8874b59f92cbd14f3447df43d6a3a46a0be4d0e..f5ed1c3fb4ed323602c8a6a8726ad17b7a4d03be 100644 (file)
--- a/test/regress/regress0/strings/fmf001.smt2
+++ b/test/regress/regress0/strings/fmf001.smt2
@@ -1,5 +1,5 @@
 (set-logic QF_S)\r
-(set-option :fmf-strings true)\r
+(set-option :strings-fmf true)\r
 (set-info :status sat)\r
 \r
 (declare-fun x () String)\r

diff --git a/test/regress/regress0/strings/fmf002.smt2 b/test/regress/regress0/strings/fmf002.smt2
index 14f50c710f0c2b9dc35d30bf7b8daa5c2d3f9b44..525fc152c4fd600ba8e81c90603f00e29a44773e 100644 (file)
--- a/test/regress/regress0/strings/fmf002.smt2
+++ b/test/regress/regress0/strings/fmf002.smt2
@@ -1,5 +1,5 @@
 (set-logic QF_S)\r
-(set-option :fmf-strings true)\r
+(set-option :strings-fmf true)\r
 (set-info :status sat)\r
 \r
 (declare-fun x () String)\r

diff --git a/test/regress/regress0/strings/str007.smt2 b/test/regress/regress0/strings/str007.smt2
new file mode 100644 (file)
index 0000000..0ca2ec4
--- /dev/null
+++ b/test/regress/regress0/strings/str007.smt2
@@ -0,0 +1,13 @@
+(set-logic QF_S)\r
+(set-info :status unsat)\r
+\r
+(declare-fun x () String)\r
+(declare-fun y () String)\r
+\r
+\r
+(assert (or (= x y) (= x y)))\r
+\r
+(assert (= (str.++ x "ba") (str.++ "ab" x)))\r
+(assert (= (str.++ y "ab") (str.++ "ab" y)))\r
+\r
+(check-sat)\r