From 36cfaab5caa86773e47a8cca8f4d8c0d5edec99f Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 16 Aug 2016 12:24:58 -0500 Subject: [PATCH] Initial infrastructure for ExtTheory, generalize extended term handling in TheoryStrings to use this. --- src/theory/bv/bv_subtheory_core.h | 1 + src/theory/bv/theory_bv.cpp | 29 ++ src/theory/bv/theory_bv.h | 4 + src/theory/datatypes/theory_datatypes.cpp | 3 + src/theory/datatypes/theory_datatypes.h | 6 +- src/theory/strings/theory_strings.cpp | 425 ++++++++++------------ src/theory/strings/theory_strings.h | 13 +- src/theory/theory.cpp | 141 +++++++ src/theory/theory.h | 57 +++ 9 files changed, 437 insertions(+), 242 deletions(-) diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h index 643093327..93a938cc0 100644 --- a/src/theory/bv/bv_subtheory_core.h +++ b/src/theory/bv/bv_subtheory_core.h @@ -117,6 +117,7 @@ public: bool hasTerm(TNode node) const { return d_equalityEngine.hasTerm(node); } void addTermToEqualityEngine(TNode node) { d_equalityEngine.addTerm(node); } void enableSlicer(); + eq::EqualityEngine * getEqualityEngine() { return &d_equalityEngine; } }; diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index fec93e033..f0981044b 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -495,7 +495,36 @@ void TheoryBV::propagate(Effort e) { } } +eq::EqualityEngine * TheoryBV::getEqualityEngine() { + return NULL; +} +bool TheoryBV::getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) { +#if 0 + CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE]; + if( core ){ + //get the constant equivalence classes + bool retVal = false; + for( unsigned i=0; igetEqualityEngine()->hasTerm( n ) ){ + Node nr = core->getEqualityEngine()->getRepresenative( n ); + if( nr.isConst() ){ + subs.push_back( nr ); + exp[n].push_back( n.eqNode( nr ) ); + retVal = true; + }else{ + subs.push_back( n ); + } + } + } + //return true if the substitution is non-trivial + return retVal; + } +#endif + return false; +} + Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { switch(in.getKind()) { case kind::EQUAL: diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index ba2a4fc2a..0709ca427 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -79,6 +79,10 @@ public: std::string identify() const { return std::string("TheoryBV"); } + /** equality engine */ + eq::EqualityEngine * getEqualityEngine(); + bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ); + PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); void enableCoreTheorySlicer(); diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index dc39183b5..59b9f1d96 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -2095,6 +2095,9 @@ TNode TheoryDatatypes::getRepresentative( TNode a ){ } } +bool TheoryDatatypes::getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) { + return false; +} void TheoryDatatypes::printModelDebug( const char* c ){ if(! (Trace.isOn(c))) { diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 5722e7822..49c45590c 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -266,6 +266,9 @@ public: void collectModelInfo( TheoryModel* m, bool fullModel ); void shutdown() { } std::string identify() const { return std::string("TheoryDatatypes"); } + /** equality engine */ + eq::EqualityEngine * getEqualityEngine() { return &d_equalityEngine; } + bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ); /** debug print */ void printModelDebug( const char* c ); /** entailment check */ @@ -313,9 +316,6 @@ private: bool areEqual( TNode a, TNode b ); bool areDisequal( TNode a, TNode b ); TNode getRepresentative( TNode a ); -public: - /** get equality engine */ - eq::EqualityEngine* getEqualityEngine() { return &d_equalityEngine; } };/* class TheoryDatatypes */ }/* CVC4::theory::datatypes namespace */ diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 09b5d00eb..7caa1cbb1 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -82,7 +82,6 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, d_proxy_var(u), d_proxy_var_to_length(u), d_functionsTerms(c), - d_ext_func_terms(c), d_has_extf(c, false ), d_regexp_memberships(c), d_regexp_ucached(u), @@ -98,6 +97,19 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, d_cardinality_lits(u), d_curr_cardinality(c, 0) { + d_extt = new ExtTheory( this ); + d_extt->addFunctionKind( kind::STRING_SUBSTR ); + d_extt->addFunctionKind( kind::STRING_STRIDOF ); + d_extt->addFunctionKind( kind::STRING_ITOS ); + d_extt->addFunctionKind( kind::STRING_U16TOS ); + d_extt->addFunctionKind( kind::STRING_U32TOS ); + d_extt->addFunctionKind( kind::STRING_STOI ); + d_extt->addFunctionKind( kind::STRING_STOU16 ); + d_extt->addFunctionKind( kind::STRING_STOU32 ); + d_extt->addFunctionKind( kind::STRING_STRREPL ); + d_extt->addFunctionKind( kind::STRING_STRCTN ); + d_extt->addFunctionKind( kind::STRING_IN_REGEXP ); + // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP); d_equalityEngine.addFunctionKind(kind::STRING_LENGTH); @@ -130,6 +142,7 @@ TheoryStrings::~TheoryStrings() { for( std::map< Node, EqcInfo* >::iterator it = d_eqc_info.begin(); it != d_eqc_info.end(); ++it ){ delete it->second; } + delete d_extt; } Node TheoryStrings::getRepresentative( Node t ) { @@ -158,23 +171,6 @@ bool TheoryStrings::areDisequal( Node a, Node b ){ if( a==b ){ return false; }else{ - /* - if( a.getType().isString() ) { - for( unsigned i=0; i<2; i++ ) { - Node ac = a.getKind()==kind::STRING_CONCAT ? a[i==0 ? 0 : a.getNumChildren()-1] : a; - Node bc = b.getKind()==kind::STRING_CONCAT ? b[i==0 ? 0 : b.getNumChildren()-1] : b; - if( ac.isConst() && bc.isConst() ){ - CVC4::String as = ac.getConst(); - CVC4::String bs = bc.getConst(); - int slen = as.size() > bs.size() ? bs.size() : as.size(); - bool flag = i == 1 ? as.rstrncmp(bs, slen): as.strncmp(bs, slen); - if(!flag) { - return true; - } - } - } - } - */ if( hasTerm( a ) && hasTerm( b ) ) { Node ar = d_equalityEngine.getRepresentative( a ); Node br = d_equalityEngine.getRepresentative( b ); @@ -291,6 +287,50 @@ Node TheoryStrings::explain( TNode literal ){ } } +bool TheoryStrings::getCurrentSubstitution( int effort, std::vector< Node >& vars, + std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) { + Trace("strings-subs") << "getCurrentSubstitution, effort = " << effort << std::endl; + for( unsigned i=0; i=3 ){ + //model values + Node mv = d_valuation.getModel()->getRepresentative( n ); + Trace("strings-subs") << " model val : " << mv << std::endl; + subs.push_back( mv ); + }else{ + Node nr = getRepresentative( n ); + std::map< Node, Node >::iterator itc = d_eqc_to_const.find( nr ); + if( itc!=d_eqc_to_const.end() ){ + //constant equivalence classes + Trace("strings-subs") << " constant eqc : " << d_eqc_to_const_exp[nr] << " " << d_eqc_to_const_base[nr] << " " << nr << std::endl; + subs.push_back( itc->second ); + if( !d_eqc_to_const_exp[nr].isNull() ){ + exp[n].push_back( d_eqc_to_const_exp[nr] ); + } + if( !d_eqc_to_const_base[nr].isNull() ){ + addToExplanation( n, d_eqc_to_const_base[nr], exp[n] ); + } + }else if( effort>=1 && effort<3 && n.getType().isString() ){ + //normal forms + Node ns = getNormalString( d_normal_forms_base[nr], exp[n] ); + subs.push_back( ns ); + Trace("strings-subs") << " normal eqc : " << ns << " " << d_normal_forms_base[nr] << " " << nr << std::endl; + if( !d_normal_forms_base[nr].isNull() ) { + addToExplanation( n, d_normal_forms_base[nr], exp[n] ); + } + }else{ + //representative? + //Trace("strings-subs") << " representative : " << nr << std::endl; + //addToExplanation( n, nr, exp[n] ); + //subs.push_back( nr ); + subs.push_back( n ); + } + } + } + return true; +} + ///////////////////////////////////////////////////////////////////////////// // NOTIFICATIONS ///////////////////////////////////////////////////////////////////////////// @@ -652,13 +692,15 @@ bool TheoryStrings::needsCheckLastEffort() { } void TheoryStrings::checkExtfReductions( int effort ) { - Trace("strings-process-debug") << "Checking preprocess at effort " << effort << ", #to process=" << d_ext_func_terms.size() << "..." << std::endl; - for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){ - Node n = (*it).first; - Trace("strings-process-debug2") << n << ", active=" << (*it).second << ", model active=" << d_extf_info_tmp[n].d_model_active << std::endl; - if( (*it).second && d_extf_info_tmp[n].d_model_active ){ + std::vector< Node > extf; + d_extt->getActive( extf ); + for( unsigned i=0; imarkReduced( n ); + } if( hasProcessed() ){ return; } @@ -666,7 +708,7 @@ void TheoryStrings::checkExtfReductions( int effort ) { } } -void TheoryStrings::checkExtfReduction( Node atom, int pol, int effort ) { +bool TheoryStrings::checkExtfReduction( Node atom, int pol, int effort ) { //determine the effort level to process the extf at // 0 - at assertion time, 1+ - after no other reduction is applicable int r_effort = -1; @@ -683,7 +725,6 @@ void TheoryStrings::checkExtfReduction( Node atom, int pol, int effort ) { Node lens = getLength( s, lexp ); if( areEqual( lenx, lens ) ){ Trace("strings-extf-debug") << " resolve extf : " << atom << " based on equal lengths disequality." << std::endl; - d_ext_func_terms[atom] = false; //we can reduce to disequality when lengths are equal if( !areDisequal( x, s ) ){ lexp.push_back( lenx.eqNode(lens) ); @@ -691,6 +732,7 @@ void TheoryStrings::checkExtfReduction( Node atom, int pol, int effort ) { Node xneqs = x.eqNode(s).negate(); sendInference( lexp, xneqs, "NEG-CTN-EQL", true ); } + return true; }else if( !areDisequal( lenx, lens ) ){ //split on their lenths sendSplit( lenx, lens, "NEG-CTN-SP" ); @@ -724,8 +766,8 @@ void TheoryStrings::checkExtfReduction( Node atom, int pol, int effort ) { exp_vec.push_back( atom ); sendInference( d_empty_vec, exp_vec, eq, "POS-CTN", true ); //we've reduced this atom - d_ext_func_terms[ atom ] = false; Trace("strings-extf-debug") << " resolve extf : " << atom << " based on positive contain reduction." << std::endl; + return true; }else{ // for STRING_SUBSTR, STRING_STRCTN with pol=-1, // STRING_STRIDOF, STRING_ITOS, STRING_U16TOS, STRING_U32TOS, STRING_STOI, STRING_STOU16, STRING_STOU32, STRING_STRREPL @@ -739,11 +781,12 @@ void TheoryStrings::checkExtfReduction( Node atom, int pol, int effort ) { Trace("strings-red-lemma") << "...from " << atom << std::endl; sendInference( d_empty_vec, nnlem, "Reduction", true ); //we've reduced this atom - d_ext_func_terms[ atom ] = false; Trace("strings-extf-debug") << " resolve extf : " << atom << " based on reduction." << std::endl; + return true; } } } + return false; } TheoryStrings::EqcInfo::EqcInfo( context::Context* c ) : d_const_term(c), d_length_term(c), d_cardinality_lem_k(c), d_normalized_length(c) { @@ -945,7 +988,7 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) { d_equalityEngine.assertPredicate( atom, polarity, exp ); //process extf if( atom.getKind()==kind::STRING_IN_REGEXP ){ - addExtendedFuncTerm( atom ); + d_extt->registerTerm( atom ); if( polarity && atom[1].getKind()==kind::REGEXP_RANGE ){ if( d_extf_infer_cache_u.find( atom )==d_extf_infer_cache_u.end() ){ d_extf_infer_cache_u.insert( atom ); @@ -1044,15 +1087,15 @@ void TheoryStrings::checkInit() { eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); while( !eqc_i.isFinished() ) { Node n = *eqc_i; - if( tn.isInteger() ){ + if( n.isConst() ){ + d_eqc_to_const[eqc] = n; + d_eqc_to_const_base[eqc] = n; + d_eqc_to_const_exp[eqc] = Node::null(); + }else if( tn.isInteger() ){ if( n.getKind()==kind::STRING_LENGTH ){ Node nr = getRepresentative( n[0] ); d_eqc_to_len_term[nr] = n[0]; } - }else if( n.isConst() ){ - d_eqc_to_const[eqc] = n; - d_eqc_to_const_base[eqc] = n; - d_eqc_to_const_exp[eqc] = Node::null(); }else if( n.getNumChildren()>0 ){ Kind k = n.getKind(); if( k!=kind::EQUAL ){ @@ -1089,16 +1132,8 @@ void TheoryStrings::checkInit() { //infer the equality sendInference( exp, n.eqNode( nc ), "I_Norm" ); }else{ - //update the extf map : only process if neither has been reduced - NodeBoolMap::const_iterator it = d_ext_func_terms.find( n ); - if( it!=d_ext_func_terms.end() ){ - if( d_ext_func_terms.find( nc )==d_ext_func_terms.end() ){ - d_ext_func_terms[nc] = (*it).second; - }else{ - d_ext_func_terms[nc] = d_ext_func_terms[nc] && (*it).second; - } - d_ext_func_terms[n] = false; - } + //mark as congruent : only process if neither has been reduced + d_extt->markCongruent( nc, n ); } //this node is congruent to another one, we can ignore it Trace("strings-process-debug") << " congruent term : " << n << std::endl; @@ -1255,179 +1290,126 @@ void TheoryStrings::checkExtfEval( int effort ) { Trace("strings-extf-list") << "Active extended functions, effort=" << effort << " : " << std::endl; d_extf_info_tmp.clear(); bool has_nreduce = false; - Trace("strings-extf-debug") << "Checking " << d_ext_func_terms.size() << " extended functions." << std::endl; - for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){ - //if not already reduced - if( (*it).second ){ - Node n = (*it).first; - - //setup information about extf - std::map< Node, ExtfInfo >::iterator iti = d_extf_info.find( n ); - Assert( iti!=d_extf_info.end() ); - d_extf_info_tmp[n].init(); - std::map< Node, ExtfInfoTmp >::iterator itit = d_extf_info_tmp.find( n ); - //get polarity - if( n.getType().isBoolean() ){ - if( areEqual( n, d_true ) ){ - itit->second.d_pol = 1; - }else if( areEqual( n, d_false ) ){ - itit->second.d_pol = -1; - } + std::vector< Node > terms; + std::vector< Node > sterms; + std::vector< std::vector< Node > > exp; + d_extt->getInferences( effort, terms, sterms, exp ); + for( unsigned i=0; i::iterator itit = d_extf_info_tmp.find( n ); + if( n.getType().isBoolean() ){ + if( areEqual( n, d_true ) ){ + itit->second.d_pol = 1; + }else if( areEqual( n, d_false ) ){ + itit->second.d_pol = -1; } - //compute rep vars map - for( unsigned j=0; jsecond.d_vars.size(); j++ ){ - Node nr = getRepresentative( iti->second.d_vars[j] ); - itit->second.d_rep_vars[nr].push_back( iti->second.d_vars[j] ); - } - - Trace("strings-extf-debug") << "Check extf " << n << ", pol = " << itit->second.d_pol << ", effort=" << effort << "..." << std::endl; - //build up a best current substitution for the variables in the term, exp is explanation for substitution - std::vector< Node > var; - std::vector< Node > sub; - for( std::map< Node, std::vector< Node > >::iterator itv = itit->second.d_rep_vars.begin(); itv != itit->second.d_rep_vars.end(); ++itv ){ - Node nr = itv->first; - Node s; - Node b; - Node e; - if( effort>=3 ){ - //model values - s = d_valuation.getModel()->getRepresentative( nr ); - }else{ - std::map< Node, Node >::iterator itc = d_eqc_to_const.find( nr ); - if( itc!=d_eqc_to_const.end() ){ - //constant equivalence classes - b = d_eqc_to_const_base[nr]; - s = itc->second; - e = d_eqc_to_const_exp[nr]; - }else if( effort>=1 && effort<3 ){ - //normal forms - b = d_normal_forms_base[nr]; - std::vector< Node > expt; - s = getNormalString( b, expt ); - e = mkAnd( expt ); - } - } - if( !s.isNull() ){ - bool added = false; - for( unsigned i=0; isecond.size(); i++ ){ - if( itv->second[i]!=s ){ - var.push_back( itv->second[i] ); - sub.push_back( s ); - if( !b.isNull() ){ - addToExplanation( itv->second[i], b, itit->second.d_exp ); - } - Trace("strings-extf-debug") << " " << itv->second[i] << " --> " << s << std::endl; - added = true; + } + Trace("strings-extf-debug") << "Check extf " << n << " == " << sn << ", pol = " << itit->second.d_pol << ", effort=" << effort << "..." << std::endl; + //do the inference + Node to_reduce; + if( n!=sn ){ + itit->second.d_exp.insert( itit->second.d_exp.end(), exp[i].begin(), exp[i].end() ); + // inference is rewriting the substituted node + Node nrc = Rewriter::rewrite( sn ); + //if rewrites to a constant, then do the inference and mark as reduced + if( nrc.isConst() ){ + if( effort<3 ){ + d_extt->markReduced( n ); + Trace("strings-extf-debug") << " resolvable by evaluation..." << std::endl; + std::vector< Node > exps; + Trace("strings-extf-debug") << " get symbolic definition..." << std::endl; + Node nrs = getSymbolicDefinition( sn, exps ); + if( !nrs.isNull() ){ + Trace("strings-extf-debug") << " rewrite " << nrs << "..." << std::endl; + nrs = Rewriter::rewrite( nrs ); + //ensure the symbolic form is non-trivial + if( nrs.isConst() ){ + Trace("strings-extf-debug") << " symbolic definition is trivial..." << std::endl; + nrs = Node::null(); } + }else{ + Trace("strings-extf-debug") << " could not infer symbolic definition." << std::endl; } - if( added && !e.isNull() ){ - addToExplanation( e, itit->second.d_exp ); - } - } - } - Node to_reduce; - if( !var.empty() ){ - //do substitution, evaluate - Node nr = n.substitute( var.begin(), var.end(), sub.begin(), sub.end() ); - Node nrc = Rewriter::rewrite( nr ); - //if rewrites to a constant, then do the inference and mark as reduced - if( nrc.isConst() ){ - if( effort<3 ){ - d_ext_func_terms[n] = false; - Trace("strings-extf-debug") << " resolvable by evaluation..." << std::endl; - std::vector< Node > exps; - Trace("strings-extf-debug") << " get symbolic definition..." << std::endl; - Node nrs = getSymbolicDefinition( nr, exps ); - if( !nrs.isNull() ){ - Trace("strings-extf-debug") << " rewrite " << nrs << "..." << std::endl; - nrs = Rewriter::rewrite( nrs ); - //ensure the symbolic form is non-trivial - if( nrs.isConst() ){ - Trace("strings-extf-debug") << " symbolic definition is trivial..." << std::endl; - nrs = Node::null(); + Node conc; + if( !nrs.isNull() ){ + Trace("strings-extf-debug") << " symbolic def : " << nrs << std::endl; + if( !areEqual( nrs, nrc ) ){ + //infer symbolic unit + if( n.getType().isBoolean() ){ + conc = nrc==d_true ? nrs : nrs.negate(); + }else{ + conc = nrs.eqNode( nrc ); } - }else{ - Trace("strings-extf-debug") << " could not infer symbolic definition." << std::endl; + itit->second.d_exp.clear(); } - Node conc; - if( !nrs.isNull() ){ - Trace("strings-extf-debug") << " symbolic def : " << nrs << std::endl; - if( !areEqual( nrs, nrc ) ){ - //infer symbolic unit - if( n.getType().isBoolean() ){ - conc = nrc==d_true ? nrs : nrs.negate(); - }else{ - conc = nrs.eqNode( nrc ); - } - itit->second.d_exp.clear(); - } - }else{ - if( !areEqual( n, nrc ) ){ - if( n.getType().isBoolean() ){ - if( areEqual( n, nrc==d_true ? d_false : d_true ) ){ - itit->second.d_exp.push_back( nrc==d_true ? n.negate() : n ); - conc = d_false; - }else{ - conc = nrc==d_true ? n : n.negate(); - } + }else{ + if( !areEqual( n, nrc ) ){ + if( n.getType().isBoolean() ){ + if( areEqual( n, nrc==d_true ? d_false : d_true ) ){ + itit->second.d_exp.push_back( nrc==d_true ? n.negate() : n ); + conc = d_false; }else{ - conc = n.eqNode( nrc ); + conc = nrc==d_true ? n : n.negate(); } + }else{ + conc = n.eqNode( nrc ); } } - if( !conc.isNull() ){ - Trace("strings-extf") << " resolve extf : " << nr << " -> " << nrc << std::endl; - sendInference( itit->second.d_exp, conc, effort==0 ? "EXTF" : "EXTF-N", true ); - if( d_conflict ){ - Trace("strings-extf-debug") << " conflict, return." << std::endl; - return; - } - } - }else{ - //check if it is already equal, if so, mark as reduced. Otherwise, do nothing. - if( areEqual( n, nrc ) ){ - Trace("strings-extf") << " resolved extf, since satisfied by model: " << n << std::endl; - itit->second.d_model_active = false; - } } - //if it reduces to a conjunction, infer each and reduce - }else if( ( nrc.getKind()==kind::OR && itit->second.d_pol==-1 ) || ( nrc.getKind()==kind::AND && itit->second.d_pol==1 ) ){ - Assert( effort<3 ); - d_ext_func_terms[n] = false; - itit->second.d_exp.push_back( itit->second.d_pol==-1 ? n.negate() : n ); - Trace("strings-extf-debug") << " decomposable..." << std::endl; - Trace("strings-extf") << " resolve extf : " << nr << " -> " << nrc << ", pol = " << itit->second.d_pol << std::endl; - for( unsigned i=0; isecond.d_exp, itit->second.d_pol==-1 ? nrc[i].negate() : nrc[i], effort==0 ? "EXTF_d" : "EXTF_d-N" ); + if( !conc.isNull() ){ + Trace("strings-extf") << " resolve extf : " << sn << " -> " << nrc << std::endl; + sendInference( itit->second.d_exp, conc, effort==0 ? "EXTF" : "EXTF-N", true ); + if( d_conflict ){ + Trace("strings-extf-debug") << " conflict, return." << std::endl; + return; + } } }else{ - to_reduce = nrc; + //check if it is already equal, if so, mark as reduced. Otherwise, do nothing. + if( areEqual( n, nrc ) ){ + Trace("strings-extf") << " resolved extf, since satisfied by model: " << n << std::endl; + itit->second.d_model_active = false; + } + } + //if it reduces to a conjunction, infer each and reduce + }else if( ( nrc.getKind()==kind::OR && itit->second.d_pol==-1 ) || ( nrc.getKind()==kind::AND && itit->second.d_pol==1 ) ){ + Assert( effort<3 ); + d_extt->markReduced( n ); + itit->second.d_exp.push_back( itit->second.d_pol==-1 ? n.negate() : n ); + Trace("strings-extf-debug") << " decomposable..." << std::endl; + Trace("strings-extf") << " resolve extf : " << sn << " -> " << nrc << ", pol = " << itit->second.d_pol << std::endl; + for( unsigned i=0; isecond.d_exp, itit->second.d_pol==-1 ? nrc[i].negate() : nrc[i], effort==0 ? "EXTF_d" : "EXTF_d-N" ); } }else{ - to_reduce = n; + to_reduce = nrc; } - if( !to_reduce.isNull() ){ - Assert( effort<3 ); - if( effort==1 ){ - Trace("strings-extf") << " cannot rewrite extf : " << to_reduce << std::endl; + }else{ + to_reduce = sterms[i]; + } + //if not reduced + if( !to_reduce.isNull() ){ + Assert( effort<3 ); + if( effort==1 ){ + Trace("strings-extf") << " cannot rewrite extf : " << to_reduce << std::endl; + } + checkExtfInference( n, to_reduce, itit->second, effort ); + if( Trace.isOn("strings-extf-list") ){ + Trace("strings-extf-list") << " * " << to_reduce; + if( itit->second.d_pol!=0 ){ + Trace("strings-extf-list") << ", pol = " << itit->second.d_pol; } - checkExtfInference( n, to_reduce, itit->second, effort ); - if( Trace.isOn("strings-extf-list") ){ - Trace("strings-extf-list") << " * " << to_reduce; - if( itit->second.d_pol!=0 ){ - Trace("strings-extf-list") << ", pol = " << itit->second.d_pol; - } - if( n!=to_reduce ){ - Trace("strings-extf-list") << ", from " << n; - } - Trace("strings-extf-list") << std::endl; + if( n!=to_reduce ){ + Trace("strings-extf-list") << ", from " << n; } - } - if( d_ext_func_terms[n] && itit->second.d_model_active ){ + Trace("strings-extf-list") << std::endl; + } + if( d_extt->isActive( n ) && itit->second.d_model_active ){ has_nreduce = true; } - }else{ - Trace("strings-extf-debug") << " already reduced " << (*it).first << std::endl; } } d_has_extf = has_nreduce; @@ -1457,7 +1439,7 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef children[index] = nr[index][i]; Node conc = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, children ); //can mark as reduced, since model for n => model for conc - d_ext_func_terms[conc] = false; + d_extt->markReduced( conc ); sendInference( in.d_exp, in.d_pol==1 ? conc : conc.negate(), "CTN_Decompose" ); } @@ -1494,7 +1476,7 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef } }else{ Trace("strings-extf-debug") << " redundant." << std::endl; - d_ext_func_terms[n] = false; + d_extt->markReduced( n ); } } } @@ -3897,29 +3879,13 @@ Node TheoryStrings::ppRewrite(TNode atom) { void TheoryStrings::collectExtendedFuncTerms( Node n, std::map< Node, bool >& visited ) { if( visited.find( n )==visited.end() ){ visited[n] = true; - if( n.getKind()==kind::STRING_SUBSTR || n.getKind()==kind::STRING_STRIDOF || - n.getKind() == kind::STRING_ITOS || n.getKind() == kind::STRING_U16TOS || n.getKind() == kind::STRING_U32TOS || - n.getKind() == kind::STRING_STOI || n.getKind() == kind::STRING_STOU16 || n.getKind() == kind::STRING_STOU32 || - n.getKind() == kind::STRING_STRREPL || n.getKind() == kind::STRING_STRCTN ){ - addExtendedFuncTerm( n ); - } + d_extt->registerTerm( n ); for( unsigned i=0; i visited; - collectVars( n, d_extf_info[n].d_vars, visited ); - } -} - // Stats TheoryStrings::Statistics::Statistics(): d_splits("TheoryStrings::NumOfSplitOnDemands", 0), @@ -4291,7 +4257,7 @@ bool TheoryStrings::checkMemberships2() { } else { //TODO: split } - */ + */ } Assert(false); //TODO:tmp } @@ -4302,20 +4268,17 @@ bool TheoryStrings::checkMemberships2() { void TheoryStrings::checkMemberships() { //add the memberships - for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){ - if( (*it).second ){ - Node n = (*it).first; - if( n.getKind()==kind::STRING_IN_REGEXP ) { - Assert( d_extf_info_tmp.find( n )!=d_extf_info_tmp.end() ); - Assert( d_extf_info_tmp[n].d_pol==1 || d_extf_info_tmp[n].d_pol==-1 ); - bool pol = d_extf_info_tmp[n].d_pol==1; - Trace("strings-process-debug") << " add membership : " << n << ", pol = " << pol << std::endl; - addMembership( pol ? n : n.negate() ); - } - } + std::vector< Node > mems; + d_extt->getActive( mems, kind::STRING_IN_REGEXP ); + for( unsigned i=0; igetSatContext() ), d_has_extf( p->getSatContext() ){ + +} + +void ExtTheory::collectVars( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited ) { + if( !n.isConst() ){ + if( visited.find( n )==visited.end() ){ + visited[n] = true; + if( n.getNumChildren()>0 ){ + for( unsigned i=0; i& terms, std::vector< Node >& sterms, std::vector< std::vector< Node > >& exp ) { + //all variables we need to find a substitution for + std::vector< Node > vars; + std::vector< Node > sub; + std::map< Node, std::vector< Node > > expc; + Trace("extt-debug") << "Checking " << d_ext_func_terms.size() << " extended functions." << std::endl; + for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){ + //if not already reduced + if( (*it).second ){ + Node n = (*it).first; + terms.push_back( n ); + std::map< Node, ExtfInfo >::iterator iti = d_extf_info.find( n ); + Assert( iti!=d_extf_info.end() ); + for( unsigned i=0; isecond.d_vars.size(); i++ ){ + if( std::find( vars.begin(), vars.end(), iti->second.d_vars[i] )==vars.end() ){ + vars.push_back( iti->second.d_vars[i] ); + } + } + } + } + Trace("extt-debug") << "..." << terms.size() << " unreduced." << std::endl; + if( !terms.empty() ){ + //get the current substitution + if( d_parent->getCurrentSubstitution( effort, vars, sub, expc ) ){ + for( unsigned i=0; i expn; + if( ns!=n ){ + //build explanation: explanation vars = sub for each vars in FV( n ) + std::map< Node, ExtfInfo >::iterator iti = d_extf_info.find( n ); + Assert( iti!=d_extf_info.end() ); + for( unsigned j=0; jsecond.d_vars.size(); j++ ){ + Node v = iti->second.d_vars[j]; + std::map< Node, std::vector< Node > >::iterator itx = expc.find( v ); + if( itx!=expc.end() ){ + for( unsigned k=0; ksecond.size(); k++ ){ + if( std::find( expn.begin(), expn.end(), itx->second[k] )==expn.end() ){ + expn.push_back( itx->second[k] ); + } + } + } + } + } + Trace("extt-debug") << " have " << n << " == " << ns << ", exp size=" << expn.size() << "." << std::endl; + //add to vector + sterms.push_back( ns ); + exp.push_back( expn ); + } + }else{ + for( unsigned i=0; igetId() << std::endl; + d_ext_func_terms[n] = true; + d_has_extf = true; + std::map< Node, bool > visited; + collectVars( n, d_extf_info[n].d_vars, visited ); + } + } +} + +//mark reduced +void ExtTheory::markReduced( Node n ) { + d_ext_func_terms[n] = false; + //TODO update has_extf +} + +//mark congruent +void ExtTheory::markCongruent( Node a, Node b ) { + NodeBoolMap::const_iterator it = d_ext_func_terms.find( b ); + if( it!=d_ext_func_terms.end() ){ + if( d_ext_func_terms.find( a )==d_ext_func_terms.end() ){ + d_ext_func_terms[a] = (*it).second; + }else{ + d_ext_func_terms[a] = d_ext_func_terms[a] && (*it).second; + } + d_ext_func_terms[b] = false; + } +} + +//is active +bool ExtTheory::isActive( Node n ) { + NodeBoolMap::const_iterator it = d_ext_func_terms.find( n ); + if( it!=d_ext_func_terms.end() ){ + return (*it).second; + }else{ + return false; + } +} +//get active +void ExtTheory::getActive( std::vector< Node >& active ) { + for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){ + //if not already reduced + if( (*it).second ){ + active.push_back( (*it).first ); + } + } +} + +void ExtTheory::getActive( std::vector< Node >& active, Kind k ) { + for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){ + //if not already reduced + if( (*it).second && (*it).first.getKind()==k ){ + active.push_back( (*it).first ); + } + } +} + }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/theory.h b/src/theory/theory.h index b5a5d4e6d..ede06fd2d 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -48,6 +48,7 @@ namespace theory { class QuantifiersEngine; class TheoryModel; class SubstitutionMap; +class ExtTheory; class EntailmentCheckParameters; class EntailmentCheckSideEffects; @@ -201,6 +202,9 @@ private: protected: + /** extended theory */ + ExtTheory * d_extt; + // === STATISTICS === /** time spent in check calls */ TimerStat d_checkTime; @@ -881,6 +885,16 @@ public: */ virtual std::pair entailmentCheck(TNode lit, const EntailmentCheckParameters* params = NULL, EntailmentCheckSideEffects* out = NULL); + /* equality engine */ + virtual eq::EqualityEngine * getEqualityEngine() { return NULL; } + + /* get current substitution at an effort + * input : vars + * output : subs, exp + * where ( exp[vars[i]] => vars[i] = subs[i] ) holds for all i + */ + virtual bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) { return false; } + /** * Turn on proof-production mode. */ @@ -950,6 +964,49 @@ public: virtual ~EntailmentCheckSideEffects(); };/* class EntailmentCheckSideEffects */ + +class ExtTheory { + friend class Theory; + typedef context::CDHashMap NodeBoolMap; +protected: + Theory * d_parent; + //extended string terms, map to whether they are active + NodeBoolMap d_ext_func_terms; + //any non-reduced extended functions exist + context::CDO< bool > d_has_extf; + //extf kind + std::map< Kind, bool > d_extf_kind; + //information for extf + class ExtfInfo { + public: + //all variables in this term + std::vector< Node > d_vars; + }; + std::map< Node, ExtfInfo > d_extf_info; + //collect variables + void collectVars( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited ); +public: + ExtTheory( Theory * p ); + virtual ~ExtTheory(){} + //add extf kind + void addFunctionKind( Kind k ) { d_extf_kind[k] = true; } + //do inferences + // input : effort + // output : terms, sterms, exp, where ( exp[i] => terms[i] = sterms[i] ) for all i + void getInferences( int effort, std::vector< Node >& terms, std::vector< Node >& sterms, std::vector< std::vector< Node > >& exp ); + //register term + void registerTerm( Node n ); + //mark reduced + void markReduced( Node n ); + //mark congruent + void markCongruent( Node a, Node b ); + //is active + bool isActive( Node n ); + //get active + void getActive( std::vector< Node >& active ); + void getActive( std::vector< Node >& active, Kind k ); +}; + }/* CVC4::theory namespace */ }/* CVC4 namespace */ -- 2.30.2