From c388e89e5253aa6fbde7685fc53126872f578f0b Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Fri, 11 Oct 2013 16:54:22 -0500 Subject: [PATCH] Adds regular expression support, it is actually CFL because of variables. --- src/theory/strings/options | 3 + src/theory/strings/theory_strings.cpp | 368 +++++------------- src/theory/strings/theory_strings.h | 16 +- .../strings/theory_strings_rewriter.cpp | 33 +- src/theory/strings/theory_strings_rewriter.h | 1 + .../strings/theory_strings_type_rules.h | 6 +- test/regress/regress0/strings/Makefile.am | 4 +- test/regress/regress0/strings/loop005.smt2 | 10 +- test/regress/regress0/strings/loop007.smt2 | 5 +- test/regress/regress0/strings/loop008.smt2 | 9 + test/regress/regress0/strings/regexp001.smt2 | 12 + 11 files changed, 169 insertions(+), 298 deletions(-) create mode 100644 test/regress/regress0/strings/loop008.smt2 create mode 100644 test/regress/regress0/strings/regexp001.smt2 diff --git a/src/theory/strings/options b/src/theory/strings/options index 9226f9999..3fceb06d4 100644 --- a/src/theory/strings/options +++ b/src/theory/strings/options @@ -8,4 +8,7 @@ module STRINGS "theory/strings/options.h" Strings theory option stringCharCardinality str-alphabet-card --str-alphabet-card=N int16_t :default 256 :read-write the cardinality of the characters used by the theory of string, default 256 +option stringRegExpUnrollDepth str-regexp-depth --str-regexp-depth=N int16_t :default 10 :read-write + the depth of unrolloing regular expression used by the theory of string, default 10 + endmodule diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index f01da389b..9f33e9191 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -26,8 +26,6 @@ #include "theory/strings/type_enumerator.h" #include -#define STR_UNROLL_INDUCTION - using namespace std; using namespace CVC4::context; @@ -43,17 +41,16 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_infer(c), d_infer_exp(c), d_nf_pairs(c), - d_ind_map1(c), - d_ind_map2(c), - d_ind_map_exp(c), - d_ind_map_lemma(c), + //d_ind_map1(c), + //d_ind_map2(c), + //d_ind_map_exp(c), + //d_ind_map_lemma(c), //d_lit_to_decide_index( c, 0 ), //d_lit_to_decide( c ), - d_reg_exp_mem( c ), - d_lit_to_unroll( c ) + d_reg_exp_mem( c ) { // The kinds we are treating as function application in congruence - d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP); + //d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP); d_equalityEngine.addFunctionKind(kind::STRING_LENGTH); d_equalityEngine.addFunctionKind(kind::STRING_CONCAT); @@ -61,6 +58,9 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); + + //option + d_regexp_unroll_depth = options::stringRegExpUnrollDepth(); } TheoryStrings::~TheoryStrings() { @@ -328,7 +328,7 @@ void TheoryStrings::preRegisterTerm(TNode n) { d_equalityEngine.addTriggerEquality(n); break; case kind::STRING_IN_REGEXP: - d_equalityEngine.addTriggerPredicate(n); + //d_equalityEngine.addTriggerPredicate(n); break; default: if(n.getKind() == kind::VARIABLE || n.getKind()==kind::SKOLEM) { @@ -370,22 +370,16 @@ void TheoryStrings::check(Effort e) { polarity = fact.getKind() != kind::NOT; atom = polarity ? fact : fact[0]; - if (atom.getKind() == kind::EQUAL) { + //must record string in regular expressions + if ( atom.getKind() == kind::STRING_IN_REGEXP ) { + //if(fact[0].getKind() != kind::CONST_STRING) { + d_reg_exp_mem.push_back( assertion ); + //} + }else if (atom.getKind() == kind::EQUAL) { d_equalityEngine.assertEquality(atom, polarity, fact); } else { d_equalityEngine.assertPredicate(atom, polarity, fact); } - if ( atom.getKind() == kind::STRING_IN_REGEXP ) { - if(fact[0].getKind() != kind::CONST_STRING) { - d_reg_exp_mem.push_back( assertion ); - } - } -#ifdef STR_UNROLL_INDUCTION - //check if it is a literal to unroll? - if( d_lit_to_unroll.find( atom )!=d_lit_to_unroll.end() ){ - Trace("strings-ind") << "Strings-ind : Possibly unroll for : " << atom << ", polarity = " << polarity << std::endl; - } -#endif } doPendingFacts(); @@ -404,12 +398,8 @@ void TheoryStrings::check(Effort e) { addedLemma = checkCardinality(); Trace("strings-process") << "Done check cardinality, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; if( !d_conflict && !addedLemma ){ - addedLemma = checkInductiveEquations(); - Trace("strings-process") << "Done check inductive equations, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; - if( !d_conflict && !addedLemma ){ - addedLemma = checkMemberships(); - Trace("strings-process") << "Done check membership constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; - } + addedLemma = checkMemberships(); + Trace("strings-process") << "Done check membership constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; } } } @@ -447,7 +437,7 @@ void TheoryStrings::conflict(TNode a, TNode b){ } else { conflictNode = explain( a.eqNode(b) ); } - Debug("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode << std::endl; + Trace("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode << std::endl; d_out->conflict( conflictNode ); d_conflict = true; } @@ -883,7 +873,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v int loop_index = has_loop[0]!=-1 ? has_loop[0] : has_loop[1]; int index = has_loop[0]!=-1 ? index_i : index_j; int other_index = has_loop[0]!=-1 ? index_j : index_i; - Trace("strings-loop") << "Detected possible loop for " << normal_forms[loop_n_index][loop_index]; + 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; Trace("strings-loop") << " ... T(Y.Z)= "; @@ -914,8 +904,9 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v Trace("strings-loop") << "Must add lemma." << std::endl; //need to break - Node sk_y= NodeManager::currentNM()->mkSkolem( "ysym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); - Node sk_z= NodeManager::currentNM()->mkSkolem( "zsym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); + 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" ); + Node sk_w= NodeManager::currentNM()->mkSkolem( "w_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); //require that x is non-empty @@ -953,6 +944,11 @@ 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, + 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 ); @@ -966,7 +962,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v // NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, normal_forms[other_n_index][other_index]), // sk_y_len ); Node ant = mkExplain( antec, antec_new_lits ); - conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2 );//, x_eq_y_rest );// , z_neq_empty //, len_x_gt_len_y + conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2, conc3, conc4 );//, 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 ); @@ -974,7 +970,6 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v //we will be done addNormalFormPair( normal_form_src[i], normal_form_src[j] ); sendLemma( ant, conc, "Loop" ); - addInductiveEquation( normal_forms[other_n_index][other_index], sk_y, sk_z, ant, "Loop Induction" ); return true; }else{ Trace("strings-solve-debug") << "No loops detected." << std::endl; @@ -1013,7 +1008,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v 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( "ssym_$$", normal_forms[i][index_i].getType(), "created for v/c split" ); + Node sk = NodeManager::currentNM()->mkSkolem( "c_split_$$", normal_forms[i][index_i].getType(), "created for v/c split" ); Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, d_emptyString ); Node eq2 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, @@ -1034,7 +1029,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v }else{ antec_new_lits.push_back(ldeq); } - Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for v/v split" ); + Node sk = NodeManager::currentNM()->mkSkolem( "v_split_$$", 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 ) ); Node eq2 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[j][index_j], @@ -1158,9 +1153,9 @@ bool TheoryStrings::normalizeDisequality( Node ni, Node nj ) { 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 sk1 = NodeManager::currentNM()->mkSkolem( "x_dsplit_$$", ni.getType(), "created for disequality normalization" ); + Node sk2 = NodeManager::currentNM()->mkSkolem( "y_dsplit_$$", ni.getType(), "created for disequality normalization" ); + Node sk3 = NodeManager::currentNM()->mkSkolem( "z_dsplit_$$", ni.getType(), "created for disequality normalization" ); Node lsk1 = getLength( sk1 ); conc.push_back( lsk1.eqNode( li ) ); Node lsk2 = getLength( sk2 ); @@ -1168,30 +1163,6 @@ bool TheoryStrings::normalizeDisequality( Node ni, Node nj ) { 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 ) ){ @@ -1269,81 +1240,6 @@ bool TheoryStrings::isNormalFormPair2( Node n1, Node n2 ) { return false; } -bool TheoryStrings::addInductiveEquation( Node x, Node y, Node z, Node exp, const char * c ) { - Trace("strings-solve-debug") << "add inductive equation for " << x << " = (" << y << " " << z << ")* " << y << std::endl; -#ifdef STR_UNROLL_INDUCTION - Node w = NodeManager::currentNM()->mkSkolem( "wsym_$$", x.getType(), "created for induction" ); - Node x_eq_y_w = NodeManager::currentNM()->mkNode( kind::EQUAL, x, - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, y, w ) ); - Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, x_eq_y_w ); - Trace("strings-lemma") << "Strings " << c << " lemma : " << lem << std::endl; - d_lemma_cache.push_back( lem ); - - //add initial induction - Node lit1 = w.eqNode( d_emptyString ); - lit1 = Rewriter::rewrite( lit1 ); - Node wp = NodeManager::currentNM()->mkSkolem( "wpsym_$$", x.getType(), "created for induction" ); - Node lit2 = w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, z, y, wp ) ); - lit2 = Rewriter::rewrite( lit2 ); - Node split_lem = NodeManager::currentNM()->mkNode( kind::OR, lit1, lit2 ); - Trace("strings-ind") << "Strings : Lemma " << c << " for unrolling " << split_lem << std::endl; - Trace("strings-lemma") << "Strings : Lemma " << c << " for unrolling " << split_lem << std::endl; - d_lemma_cache.push_back( split_lem ); - - //d_lit_to_decide.push_back( lit1 ); - d_lit_to_unroll[lit2] = true; - d_pending_req_phase[lit1] = true; - d_pending_req_phase[lit2] = false; - - x = w; - std::vector< Node > skc; - skc.push_back( y ); - skc.push_back( z ); - y = d_emptyString; - z = mkConcat( skc ); -#endif - - NodeListMap::iterator itr_x_y = d_ind_map1.find(x); - NodeList* lst1; - NodeList* lst2; - NodeList* lste; - NodeList* lstl; - if( itr_x_y == d_ind_map1.end() ) { - // add x->y - lst1 = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, - ContextMemoryAllocator(getSatContext()->getCMM()) ); - d_ind_map1.insertDataFromContextMemory( x, lst1 ); - // add x->z - lst2 = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, - ContextMemoryAllocator(getSatContext()->getCMM()) ); - d_ind_map2.insertDataFromContextMemory( x, lst2 ); - // add x->exp - lste = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, - ContextMemoryAllocator(getSatContext()->getCMM()) ); - d_ind_map_exp.insertDataFromContextMemory( x, lste ); - // add x->hasLemma false - lstl = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, - ContextMemoryAllocator(getSatContext()->getCMM()) ); - d_ind_map_lemma.insertDataFromContextMemory( x, lstl ); - } else { - //TODO: x in (yz)*y (exp) vs x in (y1 z1)*y1 (exp1) - lst1 = (*itr_x_y).second; - lst2 = (*d_ind_map2.find(x)).second; - lste = (*d_ind_map_exp.find(x)).second; - lstl = (*d_ind_map_lemma.find(x)).second; - Trace("strings-solve-debug") << "Already in maps " << x << " = (" << lst1 << " " << lst2 << ")* " << lst1 << std::endl; - Trace("strings-solve-debug") << "... with exp = " << lste << std::endl; - } - lst1->push_back( y ); - lst2->push_back( z ); - lste->push_back( exp ); -#ifdef STR_UNROLL_INDUCTION - return true; -#else - return false; -#endif -} - void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) { if( conc.isNull() || conc==d_false ){ d_out->conflict(ant); @@ -1517,6 +1413,7 @@ bool TheoryStrings::checkNormalForms() { Trace("strings-nf") << std::endl; } Trace("strings-nf") << std::endl; + /* Trace("strings-nf") << "Current inductive equations : " << std::endl; for( NodeListMap::const_iterator it = d_ind_map1.begin(); it != d_ind_map1.end(); ++it ){ Node x = (*it).first; @@ -1532,6 +1429,7 @@ bool TheoryStrings::checkNormalForms() { ++i2; } } + */ bool addedFact; do { @@ -1757,125 +1655,6 @@ int TheoryStrings::gcd ( int a, int b ) { return b; } -bool TheoryStrings::checkInductiveEquations() { - bool hasEq = false; - if(d_ind_map1.size() != 0){ - Trace("strings-ind") << "We are sat, with these inductive equations : " << std::endl; - for( NodeListMap::const_iterator it = d_ind_map1.begin(); it != d_ind_map1.end(); ++it ){ - Node x = (*it).first; - Trace("strings-ind-debug") << "Check eq for " << x << std::endl; - NodeList* lst1 = (*it).second; - NodeList* lst2 = (*d_ind_map2.find(x)).second; - NodeList* lste = (*d_ind_map_exp.find(x)).second; - //NodeList* lstl = (*d_ind_map_lemma.find(x)).second; - NodeList::const_iterator i1 = lst1->begin(); - NodeList::const_iterator i2 = lst2->begin(); - NodeList::const_iterator ie = lste->begin(); - //NodeList::const_iterator il = lstl->begin(); - while( i1!=lst1->end() ){ - Node y = *i1; - Node z = *i2; - //Trace("strings-ind-debug") << "Check y=" << y << " , z=" << z << std::endl; - //if( il==lstl->end() ) { - std::vector< Node > nf_y, nf_z, exp_y, exp_z; - - //getFinalNormalForm( y, nf_y, exp_y); - //getFinalNormalForm( z, nf_z, exp_z); - //std::vector< Node > vec_empty; - //Node nexp_y = mkExplain( exp_y, vec_empty ); - //Trace("strings-ind-debug") << "Check nexp_y=" << nexp_y << std::endl; - //Node nexp_z = mkExplain( exp_z, vec_empty ); - - //Node exp = *ie; - //Trace("strings-ind-debug") << "Check exp=" << exp << std::endl; - - //exp = NodeManager::currentNM()->mkNode( kind::AND, exp, nexp_y, nexp_z ); - //exp = Rewriter::rewrite( exp ); - - Trace("strings-ind") << "Inductive equation : " << x << " = ( " << y << " ++ " << z << " )* " << y << std::endl; - /* - for( std::vector< Node >::const_iterator itr = nf_y.begin(); itr != nf_y.end(); ++itr) { - Trace("strings-ind") << (*itr) << " "; - } - Trace("strings-ind") << " ++ "; - for( std::vector< Node >::const_iterator itr = nf_z.begin(); itr != nf_z.end(); ++itr) { - Trace("strings-ind") << (*itr) << " "; - } - Trace("strings-ind") << " )* "; - for( std::vector< Node >::const_iterator itr = nf_y.begin(); itr != nf_y.end(); ++itr) { - Trace("strings-ind") << (*itr) << " "; - } - Trace("strings-ind") << std::endl; - */ - /* - Trace("strings-ind") << "Explanation is : " << exp << std::endl; - std::vector< Node > nf_yz; - nf_yz.insert( nf_yz.end(), nf_y.begin(), nf_y.end() ); - nf_yz.insert( nf_yz.end(), nf_z.begin(), nf_z.end() ); - std::vector< std::vector< Node > > cols; - std::vector< Node > lts; - seperateByLength( nf_yz, cols, lts ); - Trace("strings-ind") << "This can be grouped into collections : " << std::endl; - for( unsigned j=0; j co; - co.push_back(0); - for(unsigned int k=0; k().getNumerator().toUnsignedInt(); - co[0] += cols[k].size() * len; - } else { - co.push_back( cols[k].size() ); - } - } - int g_co = co[0]; - for(unsigned k=1; kmkNode( kind::STRING_LENGTH, x ); - Node sk = NodeManager::currentNM()->mkSkolem( "argsym_$$", NodeManager::currentNM()->integerType(), "created for length inductive lemma" ); - Node g_co_node = NodeManager::currentNM()->mkConst( CVC4::Rational(g_co) ); - Node sk_m_gcd = NodeManager::currentNM()->mkNode( kind::MULT, g_co_node, sk ); - Node len_y = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, y ); - Node sk_m_g_p_y = NodeManager::currentNM()->mkNode( kind::PLUS, sk_m_gcd, len_y ); - lemma_len = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_m_g_p_y, len_x ); - //Node sk_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, sk, d_zero ); - //lemma_len = NodeManager::currentNM()->mkNode( kind::AND, lemma_len, sk_geq_zero ); - lemma_len = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, lemma_len ); - Trace("strings-lemma") << "Strings: Add lemma " << lemma_len << std::endl; - d_out->lemma(lemma_len); - lstl->push_back( d_true ); - return true;*/ - //} - ++i1; - ++i2; - ++ie; - //++il; - if( !areEqual( y, d_emptyString ) || !areEqual( x, d_emptyString ) ){ - hasEq = true; - } - } - } - } - if( hasEq ){ - Trace("strings-ind") << "Induction is incomplete." << std::endl; - d_out->setIncomplete(); - }else{ - Trace("strings-ind") << "We can answer SAT." << std::endl; - } - return false; -} - void TheoryStrings::getEquivalenceClasses( std::vector< Node >& eqcs ) { eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); while( !eqcs_i.isFinished() ) { @@ -1966,34 +1745,79 @@ void TheoryStrings::printConcat( std::vector< Node >& n, const char * c ) { } } +bool TheoryStrings::unrollStar( Node atom ) { + Node x = atom[0]; + Node r = atom[1]; + int depth = d_reg_exp_unroll_depth.find( atom )==d_reg_exp_unroll_depth.end() ? 0 : d_reg_exp_unroll_depth[atom]; + if( depth <= d_regexp_unroll_depth ){ + Trace("strings-regex") << "...unroll " << atom << " now." << std::endl; + d_reg_exp_unroll[atom] = true; + //add lemma? + Node xeqe = x.eqNode( d_emptyString ); + xeqe = Rewriter::rewrite( xeqe ); + d_pending_req_phase[xeqe] = true; + Node sk_s= NodeManager::currentNM()->mkSkolem( "s_unroll_$$", x.getType(), "created for unrolling" ); + Node sk_xp= NodeManager::currentNM()->mkSkolem( "x_unroll_$$", x.getType(), "created for unrolling" ); + Node unr0 = sk_s.eqNode( d_emptyString ).negate(); + Node unr1 = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_s, r[0] ); + Node unr2 = x.eqNode( mkConcat( sk_s, sk_xp ) ); + Node unr3 = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_xp, r ); + unr3 = Rewriter::rewrite( unr3 ); + d_reg_exp_unroll_depth[unr3] = depth + 1; + Node unr = NodeManager::currentNM()->mkNode( kind::AND, unr0, unr1, unr2, unr3 ); + Node lem = NodeManager::currentNM()->mkNode( kind::OR, xeqe, unr ); + sendLemma( atom, lem, "Unroll" ); + return true; + }else{ + return false; + } +} bool TheoryStrings::checkMemberships() { + bool is_unk = false; + bool addedLemma = false; for( unsigned i=0; isetIncomplete(); + Trace("strings-regex") << "SET INCOMPLETE" << std::endl; + d_out->setIncomplete(); } + return false; } - return false; } /* diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index c906d7f91..48bc28b05 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -37,6 +37,7 @@ class TheoryStrings : public Theory { typedef context::CDChunkList NodeList; typedef context::CDHashMap NodeListMap; typedef context::CDHashMap NodeBoolMap; + typedef context::CDHashMap NodeIntMap; public: TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); @@ -124,6 +125,8 @@ class TheoryStrings : public Theory { Node d_true; Node d_false; Node d_zero; + // RegExp depth + int d_regexp_unroll_depth; //list of pairs of nodes to merge std::map< Node, Node > d_pending_exp; std::vector< Node > d_pending; @@ -142,18 +145,10 @@ class TheoryStrings : public Theory { bool isNormalFormPair( Node n1, Node n2 ); bool isNormalFormPair2( Node n1, Node n2 ); - //inductive equations - NodeListMap d_ind_map1; - NodeListMap d_ind_map2; - NodeListMap d_ind_map_exp; - NodeListMap d_ind_map_lemma; //regular expression memberships NodeList d_reg_exp_mem; - bool addInductiveEquation( Node x, Node y, Node z, Node exp, const char * c ); - - //for unrolling inductive equations - NodeBoolMap d_lit_to_unroll; - + std::map< Node, bool > d_reg_exp_unroll; + std::map< Node, int > d_reg_exp_unroll_depth; ///////////////////////////////////////////////////////////////////////////// // MODEL GENERATION @@ -200,6 +195,7 @@ class TheoryStrings : public Theory { std::vector< std::vector< Node > > &normal_forms, std::vector< std::vector< Node > > &normal_forms_exp, std::vector< Node > &normal_form_src); bool normalizeEquivalenceClass( Node n, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ); bool normalizeDisequality( Node n1, Node n2 ); + bool unrollStar( Node atom ); bool checkLengths(); bool checkNormalForms(); diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 29e35981d..31203b767 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -131,6 +131,21 @@ void TheoryStringsRewriter::simplifyRegExp( Node s, Node r, std::vector< Node > break; } } +bool TheoryStringsRewriter::checkConstRegExp( Node t ) { + if( t.getKind() != kind::STRING_TO_REGEXP ) { + for( unsigned i = 0; i(); - return s2 == r[0].getConst(); + if(r[0].getKind() == kind::CONST_STRING) { + return ( s2 == r[0].getConst() ); + } else { + Assert( false, "RegExp contains variable" ); + } } case kind::REGEXP_CONCAT: { @@ -199,7 +217,7 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i for(unsigned int k=s.size() - index_start; k>0; --k) { CVC4::String t = s.substr(index_start, k); if( testConstStringInRegExp( t, 0, r[0] ) ) { - if( index_start + k == s.size() || testConstStringInRegExp( s, index_start + k, r[0] ) ) { + if( index_start + k == s.size() || testConstStringInRegExp( s, index_start + k, r ) ) { return true; } } @@ -228,7 +246,8 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { x = node[0]; } - if( x.getKind() == kind::CONST_STRING ) { + if( x.getKind() == kind::CONST_STRING && checkConstRegExp(node[1]) ) { + //TODO x \in R[y] //test whether x in node[1] CVC4::String s = x.getConst(); retNode = NodeManager::currentNM()->mkConst( testConstStringInRegExp( s, 0, node[1] ) ); @@ -257,6 +276,7 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { Trace("strings-postrewrite") << "Strings::postRewrite start " << node << std::endl; Node retNode = node; + Node orig = retNode; if(node.getKind() == kind::STRING_CONCAT) { retNode = rewriteConcatString(node); @@ -317,11 +337,12 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { } Trace("strings-postrewrite") << "Strings::postRewrite returning " << retNode << std::endl; - return RewriteResponse(REWRITE_DONE, retNode); + return RewriteResponse(orig==retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, retNode); } RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) { Node retNode = node; + Node orig = retNode; Trace("strings-prerewrite") << "Strings::preRewrite start " << node << std::endl; if(node.getKind() == kind::STRING_CONCAT) { @@ -336,5 +357,5 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) { } Trace("strings-prerewrite") << "Strings::preRewrite returning " << retNode << std::endl; - return RewriteResponse(REWRITE_DONE, retNode); + return RewriteResponse(orig==retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, retNode); } diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index ecc863a75..9dcfb4ce5 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -30,6 +30,7 @@ namespace strings { class TheoryStringsRewriter { public: + static bool checkConstRegExp( Node t ); static bool testConstStringInRegExp( CVC4::String &s, unsigned int index_start, Node r ); static void simplifyRegExp( Node s, Node r, std::vector< Node > &ret ); diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index ef8f58f80..f63cd32fc 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -203,9 +203,9 @@ public: if (!t.isString()) { throw TypeCheckingExceptionPrivate(n, "expecting string terms"); } - if( (*it).getKind() != kind::CONST_STRING ) { - throw TypeCheckingExceptionPrivate(n, "expecting constant string terms"); - } + //if( (*it).getKind() != kind::CONST_STRING ) { + // throw TypeCheckingExceptionPrivate(n, "expecting constant string terms"); + //} if(++it != it_end) { throw TypeCheckingExceptionPrivate(n, "too many terms"); } diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index 9b9fdef7a..daa817c4f 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -27,13 +27,15 @@ TESTS = \ str005.smt2 \ model001.smt2 \ substr001.smt2 \ + regexp001.smt2 \ loop001.smt2 \ loop002.smt2 \ loop003.smt2 \ loop004.smt2 \ loop005.smt2 \ loop006.smt2 \ - loop007.smt2 + loop007.smt2 \ + loop008.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/strings/loop005.smt2 b/test/regress/regress0/strings/loop005.smt2 index 4401ef794..039409ea6 100644 --- a/test/regress/regress0/strings/loop005.smt2 +++ b/test/regress/regress0/strings/loop005.smt2 @@ -5,11 +5,13 @@ (declare-fun y () String) (declare-fun z () String) (declare-fun w () String) -(declare-fun w1 () String) -(declare-fun w2 () String) -(assert (= (str.++ x y z) (str.++ x z y))) -(assert (= (str.++ x w z) (str.++ x z w))) +;(assert (= (str.++ x y z) (str.++ x z y))) +;(assert (= (str.++ x w z) (str.++ x z w))) + +(assert (= (str.++ y z) (str.++ z y))) +(assert (= (str.++ w z) (str.++ z w))) + (assert (not (= y w))) (assert (> (str.len z) 0)) diff --git a/test/regress/regress0/strings/loop007.smt2 b/test/regress/regress0/strings/loop007.smt2 index bea4037d1..b292de512 100644 --- a/test/regress/regress0/strings/loop007.smt2 +++ b/test/regress/regress0/strings/loop007.smt2 @@ -5,6 +5,7 @@ (declare-fun y () String) (assert (= (str.++ x y "aa") (str.++ "aa" y x))) -(assert (= (str.len x) 1)) +(assert (= (str.len x) (* 2 (str.len y)))) +(assert (> (str.len x) 0)) -(check-sat) \ No newline at end of file +(check-sat) diff --git a/test/regress/regress0/strings/loop008.smt2 b/test/regress/regress0/strings/loop008.smt2 new file mode 100644 index 000000000..91ed8cdf0 --- /dev/null +++ b/test/regress/regress0/strings/loop008.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_S) +(set-info :status sat) + +(declare-fun x () String) + +(assert (= (str.++ x "ab") (str.++ "ba" x))) +(assert (> (str.len x) 5)) + +(check-sat) diff --git a/test/regress/regress0/strings/regexp001.smt2 b/test/regress/regress0/strings/regexp001.smt2 new file mode 100644 index 000000000..41aefbd41 --- /dev/null +++ b/test/regress/regress0/strings/regexp001.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_S) +(set-info :status sat) + +(declare-fun x () String) + +(assert (str.in.re x + (re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") )) + )) + +(assert (= (str.len x) 3)) + +(check-sat) -- 2.30.2