From fb5fcafe43c1c7fc65c852dad2b7541df0b352c8 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Tue, 15 Oct 2013 13:16:03 -0500 Subject: [PATCH] bug fix: string cache cleaning --- src/theory/strings/theory_strings.cpp | 112 +++++++++++++++------- src/theory/strings/theory_strings.h | 2 + test/regress/regress0/strings/Makefile.am | 1 + test/regress/regress0/strings/str006.smt2 | 14 +++ 4 files changed, 94 insertions(+), 35 deletions(-) create mode 100644 test/regress/regress0/strings/str006.smt2 diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index cfc9fa77e..4876b54e7 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -159,14 +159,19 @@ bool TheoryStrings::propagate(TNode literal) { /** explain */ void TheoryStrings::explain(TNode literal, std::vector& assumptions){ - Debug("strings-explain") << "Explain " << literal << std::endl; + Debug("strings-explain") << "Explain " << literal << " " << d_conflict << std::endl; bool polarity = literal.getKind() != kind::NOT; TNode atom = polarity ? literal : literal[0]; + unsigned ps = assumptions.size(); if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) { d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions); } else { d_equalityEngine.explainPredicate(atom, polarity, assumptions); } + Debug("strings-explain-debug") << "Explanation for " << literal << " was " << std::endl; + for( unsigned i=ps; iconflict( conflictNode ); } - Trace("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode << std::endl; - d_out->conflict( conflictNode ); - d_conflict = true; } /** called when a new equivalance class is created */ @@ -549,9 +561,9 @@ void TheoryStrings::doPendingLemmas() { Trace("strings-pending") << "Require phase : " << it->first << ", polarity = " << it->second << std::endl; d_out->requirePhase( it->first, it->second ); } - d_lemma_cache.clear(); - d_pending_req_phase.clear(); } + d_lemma_cache.clear(); + d_pending_req_phase.clear(); } bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf, @@ -702,6 +714,18 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v Trace("strings-process") << "Return process equivalence class " << eqc << " : already visited." << std::endl; return false; } else if( areEqual( eqc, d_emptyString ) ){ + eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); + while( !eqc_i.isFinished() ) { + Node n = (*eqc_i); + if( n.getKind()==kind::STRING_CONCAT ){ + for( unsigned i=0; i & v //need to break Node sk_w= NodeManager::currentNM()->mkSkolem( "w_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); Node ant = mkExplain( antec, antec_new_lits ); + Node str_in_re; if(index == loop_index - 1 && other_index + 2 == (int) normal_forms[other_n_index].size() && loop_index + 1 == (int) normal_forms[loop_n_index].size() && @@ -929,11 +954,10 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v Trace("strings-loop") << "... (C)=" << normal_forms[loop_n_index][index] << " " << std::endl; //special case Node conc3 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], mkConcat( normal_forms[loop_n_index][index], sk_w ) ); - Node conc4 = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w, - NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, - NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, normal_forms[loop_n_index][index] ) ) ); - unrollStar( conc4 ); - conc = conc4; + str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w, + NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, + NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, normal_forms[loop_n_index][index] ) ) ); + conc = str_in_re; } else { Node sk_y= NodeManager::currentNM()->mkSkolem( "y_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); Node sk_z= NodeManager::currentNM()->mkSkolem( "z_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); @@ -962,10 +986,9 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v Node conc2 = NodeManager::currentNM()->mkNode( kind::EQUAL, left2, mkConcat( c3c ) ); Node conc3 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], mkConcat( sk_y, sk_w ) ); - Node conc4 = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w, + str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w, NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, mkConcat( sk_z, sk_y ) ) ) ); - unrollStar( conc4 ); //Node sk_y_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_y ); //Node sk_z_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_z ); @@ -979,12 +1002,17 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v //Node len_x_gt_len_y = NodeManager::currentNM()->mkNode( kind::GT, // NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, normal_forms[other_n_index][other_index]), // sk_y_len ); - conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2, conc3, conc4 );//, x_eq_y_rest );// , z_neq_empty //, len_x_gt_len_y + conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2, conc3, str_in_re );//, x_eq_y_rest );// , z_neq_empty //, len_x_gt_len_y //Node x_eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], d_emptyString); //conc = NodeManager::currentNM()->mkNode( kind::OR, x_eq_empty, conc ); } // normal case + //set its antecedant to ant, to say when it is relevant + d_reg_exp_ant[str_in_re] = ant; + //unroll the str in re constraint once + unrollStar( str_in_re ); + //we will be done addNormalFormPair( normal_form_src[i], normal_form_src[j] ); //Assert( isNormalFormPair( normal_form_src[i], normal_form_src[j] ) ); @@ -1302,24 +1330,30 @@ Node TheoryStrings::mkExplain( std::vector< Node >& a ) { Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an ) { std::vector< TNode > antec_exp; for( unsigned i=0; i eqcs; @@ -1547,7 +1582,7 @@ bool TheoryStrings::checkNormalForms() { } //flush pending lemmas - if( !d_conflict && !d_lemma_cache.empty() ){ + if( !d_lemma_cache.empty() ){ doPendingLemmas(); return true; }else{ @@ -1796,6 +1831,9 @@ bool TheoryStrings::unrollStar( Node atom ) { Node unr3 = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_xp, r ); unr3 = Rewriter::rewrite( unr3 ); d_reg_exp_unroll_depth[unr3] = depth + 1; + if( d_reg_exp_ant.find( atom )!=d_reg_exp_ant.end() ){ + d_reg_exp_ant[unr3] = d_reg_exp_ant[atom]; + } //|x|>|xp| Node len_x_gt_len_xp = NodeManager::currentNM()->mkNode( kind::GT, @@ -1804,7 +1842,11 @@ bool TheoryStrings::unrollStar( Node atom ) { Node unr = NodeManager::currentNM()->mkNode( kind::AND, unr0, urc[0], unr2, unr3, len_x_gt_len_xp ); Node lem = NodeManager::currentNM()->mkNode( kind::OR, xeqe, unr ); - sendLemma( atom, lem, "Unroll" ); + Node ant = atom; + if( d_reg_exp_ant.find( atom )!=d_reg_exp_ant.end() ){ + ant = d_reg_exp_ant[atom]; + } + sendLemma( ant, lem, "Unroll" ); return true; }else{ return false; @@ -1819,9 +1861,9 @@ bool TheoryStrings::checkMemberships() { Node assertion = d_reg_exp_mem[i]; Trace("strings-regex") << "We have regular expression assertion : " << assertion << std::endl; Node atom = assertion.getKind()==kind::NOT ? assertion[0] : assertion; - if( d_reg_exp_unroll.find(atom)==d_reg_exp_unroll.end() ){ - bool polarity = assertion.getKind()!=kind::NOT; - if( polarity ){ + bool polarity = assertion.getKind()!=kind::NOT; + if( polarity ){ + if( d_reg_exp_unroll.find(atom)==d_reg_exp_unroll.end() ){ Assert( atom.getKind()==kind::STRING_IN_REGEXP ); Node x = atom[0]; Node r = atom[1]; @@ -1838,12 +1880,12 @@ bool TheoryStrings::checkMemberships() { Trace("strings-regex") << "...is satisfied." << std::endl; } }else{ - //TODO: negative membership - Trace("strings-regex") << "RegEx is incomplete due to " << assertion << "." << std::endl; - is_unk = true; + Trace("strings-regex") << "...Already unrolled." << std::endl; } }else{ - Trace("strings-regex") << "...Already unrolled." << std::endl; + //TODO: negative membership + Trace("strings-regex") << "RegEx is incomplete due to " << assertion << "." << std::endl; + is_unk = true; } } if( addedLemma ){ diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index d059d8bba..d043f06ec 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -150,6 +150,8 @@ class TheoryStrings : public Theory { NodeList d_reg_exp_mem; std::map< Node, bool > d_reg_exp_unroll; std::map< Node, int > d_reg_exp_unroll_depth; + //antecedant for why reg exp membership must be true + std::map< Node, Node > d_reg_exp_ant; ///////////////////////////////////////////////////////////////////////////// // MODEL GENERATION diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index 66827b578..49a431796 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -25,6 +25,7 @@ TESTS = \ str003.smt2 \ str004.smt2 \ str005.smt2 \ + str006.smt2 \ model001.smt2 \ substr001.smt2 \ regexp001.smt2 \ diff --git a/test/regress/regress0/strings/str006.smt2 b/test/regress/regress0/strings/str006.smt2 new file mode 100644 index 000000000..592ef6a7f --- /dev/null +++ b/test/regress/regress0/strings/str006.smt2 @@ -0,0 +1,14 @@ +(set-logic QF_S) +(set-info :status sat) + +(declare-fun x () String) +(declare-fun y () String) +(declare-fun z () String) + +;plandowski p469 1 +(assert (= (str.++ x "ab" y) (str.++ y "ba" z))) +(assert (= z (str.++ x y))) +(assert (not (= (str.++ x "a") (str.++ "a" x)))) + +(check-sat) + -- 2.30.2