From: Tianyi Liang Date: Wed, 4 Dec 2013 04:53:02 +0000 (-0600) Subject: adds LB strategy X-Git-Tag: cvc5-1.0.0~7211^2 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=452bc1078621569df513726fcc89ee8155d158ea;p=cvc5.git adds LB strategy --- diff --git a/src/theory/strings/options b/src/theory/strings/options index 68d1f7bde..8bede6cae 100644 --- 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 916478024..9a88883fc 100644 --- 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 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().size() == 1 ? const_str : NodeManager::currentNM()->mkConst( const_str.getConst().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 c7ea830b6..9fae67a9f 100644 --- 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 c98f37958..e24cbc565 100644 --- 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 465ea0b5e..d64bc240e 100644 --- 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 a8874b59f..f5ed1c3fb 100644 --- a/test/regress/regress0/strings/fmf001.smt2 +++ b/test/regress/regress0/strings/fmf001.smt2 @@ -1,5 +1,5 @@ (set-logic QF_S) -(set-option :fmf-strings true) +(set-option :strings-fmf true) (set-info :status sat) (declare-fun x () String) diff --git a/test/regress/regress0/strings/fmf002.smt2 b/test/regress/regress0/strings/fmf002.smt2 index 14f50c710..525fc152c 100644 --- a/test/regress/regress0/strings/fmf002.smt2 +++ b/test/regress/regress0/strings/fmf002.smt2 @@ -1,5 +1,5 @@ (set-logic QF_S) -(set-option :fmf-strings true) +(set-option :strings-fmf true) (set-info :status sat) (declare-fun x () String) diff --git a/test/regress/regress0/strings/str007.smt2 b/test/regress/regress0/strings/str007.smt2 new file mode 100644 index 000000000..0ca2ec4c3 --- /dev/null +++ b/test/regress/regress0/strings/str007.smt2 @@ -0,0 +1,13 @@ +(set-logic QF_S) +(set-info :status unsat) + +(declare-fun x () String) +(declare-fun y () String) + + +(assert (or (= x y) (= x y))) + +(assert (= (str.++ x "ba") (str.++ "ab" x))) +(assert (= (str.++ y "ab") (str.++ "ab" y))) + +(check-sat)