From 645aaaa186269c26d96a60c8df3350a2de9b6acb Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 2 Oct 2015 23:15:35 +0200 Subject: [PATCH] Fixes related to explanations for cycles, sym inferences. Minor fixes and improvements. --- src/theory/strings/theory_strings.cpp | 42 ++++++++++--------- src/theory/strings/theory_strings.h | 1 + .../strings/theory_strings_preprocess.cpp | 2 +- .../strings/theory_strings_rewriter.cpp | 6 +-- 4 files changed, 28 insertions(+), 23 deletions(-) diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 5cf7d8ee6..87cb220db 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -69,6 +69,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_registered_terms_cache(u), d_preproc_cache(u), d_proxy_var(u), + d_proxy_var_to_length(u), d_neg_ctn_eqlen(u), d_neg_ctn_ulen(u), d_pos_ctn_cached(u), @@ -1968,12 +1969,6 @@ bool TheoryStrings::registerTerm( Node n ) { ++(d_statistics.d_splits); } } else { - if( n.getKind()==kind::STRING_CONCAT ){ - //normalize wrt proxy variables - - } - - Node sk = mkSkolemS("lsym", 2); StringsProxyVarAttribute spva; sk.setAttribute(spva,true); @@ -1987,13 +1982,20 @@ bool TheoryStrings::registerTerm( Node n ) { if( n.getKind() == kind::STRING_CONCAT ) { std::vector node_vec; for( unsigned i=0; imkNode( kind::STRING_LENGTH, n[i] ); - node_vec.push_back(lni); + if( n[i].getAttribute(StringsProxyVarAttribute()) ){ + Assert( d_proxy_var_to_length.find( n[i] )!=d_proxy_var_to_length.end() ); + node_vec.push_back( d_proxy_var_to_length[n[i]] ); + }else{ + Node lni = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[i] ); + node_vec.push_back(lni); + } } lsum = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec ); } else if( n.getKind() == kind::CONST_STRING ) { lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst().size() ) ); } + lsum = Rewriter::rewrite( lsum ); + d_proxy_var_to_length[sk] = lsum; Node ceq = Rewriter::rewrite( skl.eqNode( lsum ) ); Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq << std::endl; Trace("strings-lemma-debug") << " prerewrite : " << skl.eqNode( lsum ) << std::endl; @@ -2034,6 +2036,7 @@ void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) { } void TheoryStrings::sendInfer( Node eq_exp, Node eq, const char * c ) { + Trace("strings-infer-debug") << "infer : " << eq << " from " << eq_exp << std::endl; eq = Rewriter::rewrite( eq ); if( eq==d_false || eq.getKind()==kind::OR ) { sendLemma( eq_exp, eq, c ); @@ -2118,7 +2121,7 @@ void TheoryStrings::inferSubstitutionProxyVars( Node n, std::vector< Node >& var Node ss; if( ns[i].getAttribute(StringsProxyVarAttribute()) ){ ss = ns[i]; - }else{ + }else if( ns[i].isConst() ){ NodeNodeMap::const_iterator it = d_proxy_var.find( ns[i] ); if( it!=d_proxy_var.end() ){ ss = (*it).second; @@ -2482,7 +2485,7 @@ Node TheoryStrings::checkCycles( Node eqc, std::vector< Node >& curr, std::vecto while( !eqc_i.isFinished() ) { Node n = (*eqc_i); if( std::find( d_congruent.begin(), d_congruent.end(), n )==d_congruent.end() ){ - Trace("strings-cycle") << "Check term : " << n << std::endl; + Trace("strings-cycle") << eqc << " check term : " << n << " in " << eqc << std::endl; if( n.getKind() == kind::STRING_CONCAT ) { if( eqc!=d_emptyString_r ){ d_eqc[eqc].push_back( n ); @@ -2503,6 +2506,13 @@ Node TheoryStrings::checkCycles( Node eqc, std::vector< Node >& curr, std::vecto //for non-empty eqc, recurse and see if we find a loop Node ncy = checkCycles( nr, curr, exp ); if( !ncy.isNull() ){ + Trace("strings-cycle") << eqc << " cycle: " << ncy << " at " << n << "[" << i << "] : " << n[i] << std::endl; + if( n!=eqc ){ + exp.push_back( n.eqNode( eqc ) ); + } + if( nr!=n[i] ){ + exp.push_back( nr.eqNode( n[i] ) ); + } if( ncy==eqc ){ //can infer all other components must be empty for( unsigned j=0; j& curr, std::vecto //should find a non-empty component, otherwise would have been singular congruent (I_Norm_S) Assert( false ); }else{ - if( n!=eqc ){ - exp.push_back( n.eqNode( eqc ) ); - } - if( nr!=n[i] ){ - exp.push_back( nr.eqNode( n[i] ) ); - } return ncy; } }else{ @@ -2754,9 +2758,9 @@ void TheoryStrings::separateByLength(std::vector< Node >& n, lt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt ); Node r = d_equalityEngine.getRepresentative( lt ); if( eqc_to_leqc.find( r )==eqc_to_leqc.end() ){ - eqc_to_leqc[r] = leqc_counter; - leqc_to_eqc[leqc_counter] = r; - leqc_counter++; + eqc_to_leqc[r] = leqc_counter; + leqc_to_eqc[leqc_counter] = r; + leqc_counter++; } eqc_to_strings[ eqc_to_leqc[r] ].push_back( eqc ); }else{ diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index dee958aee..98f8d0eea 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -251,6 +251,7 @@ private: EqcInfo * getOrMakeEqcInfo( Node eqc, bool doMake = true ); //maintain which concat terms have the length lemma instantiated NodeNodeMap d_proxy_var; + NodeNodeMap d_proxy_var_to_length; private: void mergeCstVec(std::vector< Node > &vec_strings); bool getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf, diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index bcea61937..e9b144a23 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -222,7 +222,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool d Node sk3 = NodeManager::currentNM()->mkSkolem( "io3", NodeManager::currentNM()->stringType(), "created for indexof" ); Node sk4 = NodeManager::currentNM()->mkSkolem( "io4", NodeManager::currentNM()->stringType(), "created for indexof" ); Node skk = NodeManager::currentNM()->mkSkolem( "iok", NodeManager::currentNM()->integerType(), "created for indexof" ); - Node st = NodeManager::currentNM()->mkNode( kind::STRING_SUBSTR_TOTAL, t[0], t[2], NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ) ); + Node st = NodeManager::currentNM()->mkNode( kind::STRING_SUBSTR_TOTAL, t[0], t[2], NodeManager::currentNM()->mkNode( kind::MINUS, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), t[2] ) ); Node eq = st.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk2, sk3, sk4 ) ); new_nodes.push_back( eq ); Node negone = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) ); diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index e326b9b93..ae0a7aeda 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -91,7 +91,7 @@ Node TheoryStringsRewriter::simpleRegexpConsume( std::vector< Node >& mchildren, return NodeManager::currentNM()->mkConst( false ); } }else if( rc.getKind()==kind::REGEXP_INTER || rc.getKind()==kind::REGEXP_UNION ){ - //TODO + //TODO? note this is only propagation : cannot make choices }else if( rc.getKind()==kind::REGEXP_STAR ){ //TODO } @@ -848,7 +848,7 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { }else if(x != node[0] || r != node[1]) { retNode = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, x, r ); } - + //do simple consumes if( retNode==node ){ if( r.getKind()==kind::REGEXP_STAR ){ @@ -957,7 +957,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { retNode = NodeManager::currentNM()->mkNode(kind::PLUS, node_vec); } } - } else if(node.getKind() == kind::STRING_SUBSTR_TOTAL) { + } else if( node.getKind() == kind::STRING_SUBSTR_TOTAL ){ Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ); if(node[2] == zero) { retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); -- 2.30.2