From: ajreynol Date: Wed, 7 Oct 2015 10:54:55 +0000 (+0200) Subject: Minor improvements, add endpoint eq inference to strings. X-Git-Tag: cvc5-1.0.0~6216 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d3af3aab6827bd898cc7f62776febef79150e250;p=cvc5.git Minor improvements, add endpoint eq inference to strings. --- diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index a19bab836..ad878e0f3 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -675,25 +675,22 @@ bool TheoryStrings::doPreprocess( Node atom ) { subs_rhs.push_back( d_true ); Node sres = res.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() ); sres = Rewriter::rewrite( sres ); + Node plem; if( sres!=res ){ - Node plem = NodeManager::currentNM()->mkNode( kind::IMPLIES, atom, sres ); - plem = Rewriter::rewrite( plem ); - Trace("strings-assert") << "(assert " << plem << ")" << std::endl; - d_out->lemma( plem ); - Trace("strings-pp-lemma") << "Preprocess impl lemma : " << plem << std::endl; - Trace("strings-pp-lemma") << "...from " << atom << std::endl; + plem = NodeManager::currentNM()->mkNode( kind::IMPLIES, atom, sres ); }else{ Trace("strings-assertion-debug") << "...preprocessed to : " << res << std::endl; - Node plem = NodeManager::currentNM()->mkNode( kind::IFF, atom, res ); - plem = Rewriter::rewrite( plem ); - Trace("strings-assert") << "(assert " << plem << ")" << std::endl; - d_out->lemma( plem ); - Trace("strings-pp-lemma") << "Preprocess eq lemma : " << plem << std::endl; - Trace("strings-pp-lemma") << "...from " << atom << std::endl; + plem = NodeManager::currentNM()->mkNode( kind::IFF, atom, res ); //reduced by preprocess addFact = false; d_preproc_cache[ atom ] = false; } + plem = Rewriter::rewrite( plem ); + Trace("strings-assert") << "(assert " << plem << ")" << std::endl; + Trace("strings-lemma") << "Strings::Lemma " << plem << " by preprocess" << std::endl; + d_out->lemma( plem ); + Trace("strings-pp-lemma") << "Preprocess reduce lemma : " << plem << std::endl; + Trace("strings-pp-lemma") << "...from " << atom << std::endl; }else{ Trace("strings-assertion-debug") << "...preprocess ok." << std::endl; } @@ -2420,6 +2417,8 @@ void TheoryStrings::checkNormalForms() { }else{ Node cc = d_flat_form[b][count]; if( cc!=curr ){ + Node ac = a[d_flat_form_index[a][count]]; + Node bc = b[d_flat_form_index[b][count]]; inelig.push_back( b ); Assert( !areEqual( curr, cc ) ); Node cc_c = d_eqc_to_const[cc]; @@ -2428,20 +2427,22 @@ void TheoryStrings::checkNormalForms() { int index; Node s = TheoryStringsRewriter::splitConstant( cc_c, curr_c, index, r==1 ); if( s.isNull() ){ - addToExplanation( a[d_flat_form_index[a][count]], d_eqc_to_const_base[curr], exp ); + addToExplanation( ac, d_eqc_to_const_base[curr], exp ); addToExplanation( d_eqc_to_const_exp[curr], exp ); - addToExplanation( b[d_flat_form_index[b][count]], d_eqc_to_const_base[cc], exp ); + addToExplanation( bc, d_eqc_to_const_base[cc], exp ); addToExplanation( d_eqc_to_const_exp[cc], exp ); conc = d_false; inf_type = 0; break; } + }else if( (d_flat_form[a].size()-1)==count && (d_flat_form[b].size()-1)==count ){ + conc = ac.eqNode( bc ); + inf_type = 3; + break; }else{ //if lengths are the same, apply LengthEq Node lcc = getLength( cc ); if( areEqual( lcurr, lcc ) ){ - Node ac = a[d_flat_form_index[a][count]]; - Node bc = b[d_flat_form_index[b][count]]; //exp_n.push_back( getLength( curr, true ).eqNode( getLength( cc, true ) ) ); addToExplanation( lcurr, lcc, exp ); if( !lcc.isConst() ){ @@ -2487,7 +2488,7 @@ void TheoryStrings::checkNormalForms() { } } //if( exp_n.empty() ){ - sendInfer( mkAnd( exp ), conc, inf_type==0? "F_Const" : ( inf_type==1 ? "F_LengthEq" : "F_Endpoint" ) ); + sendInfer( mkAnd( exp ), conc, inf_type==0? "F_Const" : ( inf_type==1 ? "F_LengthEq" : ( inf_type==2 ? "F_Endpoint" : "F_EndpointEq" ) ) ); //}else{ //} if( d_conflict ){ @@ -3894,7 +3895,7 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) { if( !var.empty() ){ Node nr = n.substitute( var.begin(), var.end(), sub.begin(), sub.end() ); Node nrc = Rewriter::rewrite( nr ); - if( nrc.isConst() || hasTerm( nrc ) ){ + if( nrc.isConst() ){ //mark as reduced d_ext_func_terms[n] = false; Trace("strings-extf-debug") << " resolvable by evaluation..." << std::endl; @@ -3947,7 +3948,13 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) { } } }else{ - Trace("strings-extf-debug") << " cannot rewrite extf : " << nrc << std::endl; + if( effort==1 ){ + Trace("strings-extf") << " cannot rewrite extf : " << nrc << std::endl; + } + } + }else{ + if( effort==1 ){ + Trace("strings-extf") << " cannot rewrite extf : " << n << std::endl; } } } diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 6efa048ca..fc17198c2 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -35,6 +35,8 @@ Node TheoryStringsRewriter::simpleRegexpConsume( std::vector< Node >& mchildren, do_next = false; Node xc = mchildren[mchildren.size()-1]; Node rc = children[children.size()-1]; + Assert( rc.getKind()!=kind::REGEXP_CONCAT ); + Assert( xc.getKind()!=kind::STRING_CONCAT ); if( rc.getKind() == kind::STRING_TO_REGEXP ){ if( xc==rc[0] ){ children.pop_back(); @@ -88,7 +90,7 @@ Node TheoryStringsRewriter::simpleRegexpConsume( std::vector< Node >& mchildren, std::vector< Node > mchildren_s; std::vector< Node > children_s; mchildren_s.push_back( xc ); - children_s.push_back( rc[i] ); + getConcat( rc[i], children_s ); Node ret = simpleRegexpConsume( mchildren_s, children_s, t ); if( !ret.isNull() ){ // one conjunct cannot be satisfied, return false diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 92f834bff..cde3aef1c 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -119,11 +119,12 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const // no good. Instead, return the quantifier itself. If we're in // checkModel(), and the quantifier actually matters, we'll get an // assert-fail since the quantifier isn't a constant. - if(!d_equalityEngine->hasTerm(Rewriter::rewrite(n))) { + Node nr = Rewriter::rewrite(n); + if(!d_equalityEngine->hasTerm(nr)) { d_modelCache[n] = ret; return ret; } else { - ret = Rewriter::rewrite(n); + ret = nr; } } else { if(n.getKind() == kind::LAMBDA) { @@ -193,8 +194,7 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const ret = NodeManager::currentNM()->mkConst(getCardinality(ret[0].getType().toType()).getFiniteCardinality() <= ret[1].getConst().getNumerator()); } if(ret.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT ){ - //FIXME - ret = NodeManager::currentNM()->mkConst(false); + //do nothing } d_modelCache[n] = ret; return ret;