From: ajreynol Date: Sat, 1 Oct 2016 12:08:45 +0000 (-0500) Subject: Incorporate non-bv parts of ajr/bvExt branch X-Git-Tag: cvc5-1.0.0~6028^2~12 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4adb2ef78320743ff4b56eac15bfdbe4b9591b51;p=cvc5.git Incorporate non-bv parts of ajr/bvExt branch --- diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 2f6f7e9e7..3ef6df3fc 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -331,6 +331,92 @@ bool TheoryStrings::getCurrentSubstitution( int effort, std::vector< Node >& var return true; } +int TheoryStrings::getReduction( int effort, Node n, Node& nr ) { + //determine the effort level to process the extf at + // 0 - at assertion time, 1+ - after no other reduction is applicable + Assert( d_extf_info_tmp.find( n )!=d_extf_info_tmp.end() ); + if( d_extf_info_tmp[n].d_model_active ){ + int r_effort = -1; + int pol = d_extf_info_tmp[n].d_pol; + if( n.getKind()==kind::STRING_STRCTN ){ + if( pol==1 ){ + r_effort = 1; + }else if( pol==-1 ){ + if( effort==2 ){ + Node x = n[0]; + Node s = n[1]; + std::vector< Node > lexp; + Node lenx = getLength( x, lexp ); + Node lens = getLength( s, lexp ); + if( areEqual( lenx, lens ) ){ + Trace("strings-extf-debug") << " resolve extf : " << n << " based on equal lengths disequality." << std::endl; + //we can reduce to disequality when lengths are equal + if( !areDisequal( x, s ) ){ + lexp.push_back( lenx.eqNode(lens) ); + lexp.push_back( n.negate() ); + Node xneqs = x.eqNode(s).negate(); + sendInference( lexp, xneqs, "NEG-CTN-EQL", true ); + } + return 1; + }else if( !areDisequal( lenx, lens ) ){ + //split on their lenths + sendSplit( lenx, lens, "NEG-CTN-SP" ); + }else{ + r_effort = 2; + } + } + } + }else{ + if( options::stringLazyPreproc() ){ + if( n.getKind()==kind::STRING_SUBSTR ){ + r_effort = 1; + }else if( n.getKind()!=kind::STRING_IN_REGEXP ){ + r_effort = 2; + } + } + } + if( effort==r_effort ){ + Node c_n = pol==-1 ? n.negate() : n; + if( d_preproc_cache.find( c_n )==d_preproc_cache.end() ){ + d_preproc_cache[ c_n ] = true; + Trace("strings-process-debug") << "Process reduction for " << n << ", pol = " << pol << std::endl; + if( n.getKind()==kind::STRING_STRCTN && pol==1 ){ + Node x = n[0]; + Node s = n[1]; + //positive contains reduces to a equality + Node sk1 = mkSkolemCached( x, s, sk_id_ctn_pre, "sc1" ); + Node sk2 = mkSkolemCached( x, s, sk_id_ctn_post, "sc2" ); + Node eq = Rewriter::rewrite( x.eqNode( mkConcat( sk1, s, sk2 ) ) ); + std::vector< Node > exp_vec; + exp_vec.push_back( n ); + sendInference( d_empty_vec, exp_vec, eq, "POS-CTN", true ); + //we've reduced this n + Trace("strings-extf-debug") << " resolve extf : " << n << " based on positive contain reduction." << std::endl; + return 1; + }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 + std::vector< Node > new_nodes; + Node res = d_preproc.simplify( n, new_nodes ); + Assert( res!=n ); + new_nodes.push_back( NodeManager::currentNM()->mkNode( res.getType().isBoolean() ? kind::IFF : kind::EQUAL, res, n ) ); + Node nnlem = new_nodes.size()==1 ? new_nodes[0] : NodeManager::currentNM()->mkNode( kind::AND, new_nodes ); + nnlem = Rewriter::rewrite( nnlem ); + Trace("strings-red-lemma") << "Reduction_" << effort << " lemma : " << nnlem << std::endl; + Trace("strings-red-lemma") << "...from " << n << std::endl; + sendInference( d_empty_vec, nnlem, "Reduction", true ); + //we've reduced this n + Trace("strings-extf-debug") << " resolve extf : " << n << " based on reduction." << std::endl; + return 1; + } + }else{ + return 1; + } + } + } + return 0; +} + ///////////////////////////////////////////////////////////////////////////// // NOTIFICATIONS ///////////////////////////////////////////////////////////////////////////// @@ -404,15 +490,13 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) { for( unsigned j=0; jd_const_term : Node::null(); - if( cst.isNull() ){ + if( !col[i][j].isConst() ){ Assert( d_normal_forms.find( col[i][j] )!=d_normal_forms.end() ); if( d_normal_forms[col[i][j]].size()==1 ){//&& d_normal_forms[col[i][j]][0]==col[i][j] ){ pure_eq.push_back( col[i][j] ); } }else{ - processed[col[i][j]] = cst; + processed[col[i][j]] = col[i][j]; } } Trace("strings-model") << "have length " << lts_values[i] << std::endl; @@ -692,104 +776,29 @@ bool TheoryStrings::needsCheckLastEffort() { } void TheoryStrings::checkExtfReductions( int effort ) { + //standardize this? + //std::vector< Node > nred; + //d_extt->doReductions( effort, nred, false ); + std::vector< Node > extf; d_extt->getActive( extf ); + Trace("strings-process") << "checking " << extf.size() << " active extf" << std::endl; for( unsigned i=0; imarkReduced( n ); - } - if( hasProcessed() ){ + Trace("strings-process") << "Check " << n << ", active in model=" << d_extf_info_tmp[n].d_model_active << std::endl; + Node nr; + int ret = getReduction( effort, n, nr ); + Assert( nr.isNull() ); + if( ret!=0 ){ + d_extt->markReduced( extf[i] ); + if( options::stringOpt1() && hasProcessed() ){ return; } } } } -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; - if( atom.getKind()==kind::STRING_STRCTN ){ - if( pol==1 ){ - r_effort = 1; - }else{ - Assert( pol==-1 ); - if( effort==2 ){ - Node x = atom[0]; - Node s = atom[1]; - std::vector< Node > lexp; - Node lenx = getLength( x, lexp ); - Node lens = getLength( s, lexp ); - if( areEqual( lenx, lens ) ){ - Trace("strings-extf-debug") << " resolve extf : " << atom << " based on equal lengths disequality." << std::endl; - //we can reduce to disequality when lengths are equal - if( !areDisequal( x, s ) ){ - lexp.push_back( lenx.eqNode(lens) ); - lexp.push_back( atom.negate() ); - 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" ); - }else{ - r_effort = 2; - } - } - } - }else{ - if( options::stringLazyPreproc() ){ - if( atom.getKind()==kind::STRING_SUBSTR ){ - r_effort = 1; - }else if( atom.getKind()!=kind::STRING_IN_REGEXP ){ - r_effort = 2; - } - } - } - if( effort==r_effort ){ - Node c_atom = pol==-1 ? atom.negate() : atom; - if( d_preproc_cache.find( c_atom )==d_preproc_cache.end() ){ - d_preproc_cache[ c_atom ] = true; - Trace("strings-process-debug") << "Process reduction for " << atom << ", pol = " << pol << std::endl; - if( atom.getKind()==kind::STRING_STRCTN && pol==1 ){ - Node x = atom[0]; - Node s = atom[1]; - //positive contains reduces to a equality - Node sk1 = mkSkolemCached( x, s, sk_id_ctn_pre, "sc1" ); - Node sk2 = mkSkolemCached( x, s, sk_id_ctn_post, "sc2" ); - Node eq = Rewriter::rewrite( x.eqNode( mkConcat( sk1, s, sk2 ) ) ); - std::vector< Node > exp_vec; - exp_vec.push_back( atom ); - sendInference( d_empty_vec, exp_vec, eq, "POS-CTN", true ); - //we've reduced this atom - 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 - std::vector< Node > new_nodes; - Node res = d_preproc.simplify( atom, new_nodes ); - Assert( res!=atom ); - new_nodes.push_back( NodeManager::currentNM()->mkNode( res.getType().isBoolean() ? kind::IFF : kind::EQUAL, res, atom ) ); - Node nnlem = new_nodes.size()==1 ? new_nodes[0] : NodeManager::currentNM()->mkNode( kind::AND, new_nodes ); - nnlem = Rewriter::rewrite( nnlem ); - Trace("strings-red-lemma") << "Reduction_" << effort << " lemma : " << nnlem << std::endl; - Trace("strings-red-lemma") << "...from " << atom << std::endl; - sendInference( d_empty_vec, nnlem, "Reduction", true ); - //we've reduced this atom - 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) { +TheoryStrings::EqcInfo::EqcInfo( context::Context* c ) : d_length_term(c), d_cardinality_lem_k(c), d_normalized_length(c) { } @@ -827,10 +836,6 @@ void TheoryStrings::conflict(TNode a, TNode b){ /** called when a new equivalance class is created */ void TheoryStrings::eqNotifyNewClass(TNode t){ - if( t.getKind() == kind::CONST_STRING ){ - EqcInfo * ei =getOrMakeEqcInfo( t, true ); - ei->d_const_term = t; - } if( t.getKind() == kind::STRING_LENGTH ){ Trace("strings-debug") << "New length eqc : " << t << std::endl; Node r = d_equalityEngine.getRepresentative(t[0]); @@ -838,6 +843,8 @@ void TheoryStrings::eqNotifyNewClass(TNode t){ ei->d_length_term = t[0]; //we care about the length of this string registerTerm( t[0], 1 ); + }else{ + //d_extt->registerTerm( t ); } } @@ -847,9 +854,6 @@ void TheoryStrings::eqNotifyPreMerge(TNode t1, TNode t2){ if( e2 ){ EqcInfo * e1 = getOrMakeEqcInfo( t1 ); //add information from e2 to e1 - if( !e2->d_const_term.get().isNull() ){ - e1->d_const_term.set( e2->d_const_term ); - } if( !e2->d_length_term.get().isNull() ){ e1->d_length_term.set( e2->d_length_term ); } @@ -987,7 +991,6 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) { d_equalityEngine.assertPredicate( atom, polarity, exp ); //process extf if( atom.getKind()==kind::STRING_IN_REGEXP ){ - 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 ); @@ -999,6 +1002,8 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) { } } } + //register the atom here, since it may not create a new equivalence class + //d_extt->registerTerm( atom ); } Trace("strings-pending-debug") << " Now collect terms" << std::endl; //collect extended function terms in the atom @@ -1292,7 +1297,8 @@ void TheoryStrings::checkExtfEval( int effort ) { std::vector< Node > terms; std::vector< Node > sterms; std::vector< std::vector< Node > > exp; - d_extt->getInferences( effort, terms, sterms, exp ); + d_extt->getActive( terms ); + d_extt->getSubstitutedTerms( effort, terms, sterms, exp ); for( unsigned i=0; i& visited ) { - if( visited.find( n )==visited.end() ){ - visited[n] = true; - d_extt->registerTerm( n ); - for( unsigned i=0; i& nf_r0 = d_normal_forms[r[0]]; - nf_r = mkConcat(nf_r0); - Debug("regexp-nf") << "Term: " << r[0] << " has a normal form " - << nf_r << std::endl; - std::vector::iterator nf_end_exp = nf_exp.end(); - std::vector::const_iterator nf_r0_begin = nf_r0.begin(); - std::vector::const_iterator nf_r0_end = nf_r0.end(); - nf_exp.insert(nf_end_exp, nf_r0_begin, nf_r0_end); - nf_r = Rewriter::rewrite(NodeManager::currentNM()->mkNode( - kind::STRING_TO_REGEXP, nf_r)); + if(d_normal_forms.find( r[0] ) != d_normal_forms.end()) { + nf_r = mkConcat( d_normal_forms[r[0]] ); + Debug("regexp-nf") << "Term: " << r[0] << " has a normal form " << nf_r << std::endl; + nf_exp.insert(nf_exp.end(), d_normal_forms_exp[r[0]].begin(), d_normal_forms_exp[r[0]].end()); + nf_r = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, nf_r) ); } } } @@ -4873,6 +4863,16 @@ Node TheoryStrings::getNormalSymRegExp(Node r, std::vector &nf_exp) { return ret; } +void TheoryStrings::collectExtendedFuncTerms( Node n, std::map< Node, bool >& visited ) { + if( visited.find( n )==visited.end() ){ + visited[n] = true; + d_extt->registerTerm( n ); + for( unsigned i=0; i& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ); + int getReduction( int effort, Node n, Node& nr ); // NotifyClass for equality engine class NotifyClass : public eq::EqualityEngineNotify { @@ -237,7 +238,6 @@ private: EqcInfo( context::Context* c ); ~EqcInfo(){} //constant in this eqc - context::CDO< Node > d_const_term; context::CDO< Node > d_length_term; context::CDO< unsigned > d_cardinality_lem_k; // 1 = added length lemma @@ -274,8 +274,6 @@ private: int d_pol; //explanation std::vector< Node > d_exp; - //reps -> list of variables - //std::map< Node, std::vector< Node > > d_rep_vars; //false if it is reduced in the model bool d_model_active; }; @@ -321,7 +319,6 @@ private: Node getSymbolicDefinition( Node n, std::vector< Node >& exp ); //check extf reduction void checkExtfReductions( int effort ); - bool checkExtfReduction( Node atom, int pol, int effort ); //flat forms check void checkFlatForms(); Node checkCycles( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp ); @@ -523,6 +520,7 @@ public: ~Statistics(); };/* class TheoryStrings::Statistics */ Statistics d_statistics; + };/* class TheoryStrings */ }/* CVC4::theory::strings namespace */ diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 7fa74df6a..9e71a1ddf 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -314,15 +314,18 @@ EntailmentCheckSideEffects::~EntailmentCheckSideEffects() { ExtTheory::ExtTheory( Theory * p ) : d_parent( p ), -d_ext_func_terms( p->getSatContext() ), d_has_extf( p->getSatContext() ){ - +d_ext_func_terms( p->getSatContext() ), d_ci_inactive( p->getUserContext() ), +d_lemmas( p->getUserContext() ), d_pp_lemmas( p->getUserContext() ), d_has_extf( p->getSatContext() ){ + d_true = NodeManager::currentNM()->mkConst( true ); } +//gets all leaf terms in n 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 ){ + //treat terms not belonging to this theory as leaf + if( n.getNumChildren()>0 ){//&& Theory::theoryOf(n)==d_parent->getId() ){ for( unsigned i=0; i& vars, std::map< Node, } //do inferences -void ExtTheory::getInferences( int effort, std::vector< Node >& 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 ); +void ExtTheory::getSubstitutedTerms( int effort, std::vector< Node >& terms, std::vector< Node >& sterms, std::vector< std::vector< Node > >& exp ) { + Trace("extt-debug") << "Currently " << d_ext_func_terms.size() << " extended functions." << std::endl; + Trace("extt-debug") << "..." << terms.size() << " to reduce." << std::endl; + if( !terms.empty() ){ + //all variables we need to find a substitution for + std::vector< Node > vars; + std::vector< Node > sub; + std::map< Node, std::vector< Node > > expc; + for( unsigned i=0; i::iterator iti = d_extf_info.find( n ); Assert( iti!=d_extf_info.end() ); for( unsigned i=0; isecond.d_vars.size(); i++ ){ @@ -353,13 +356,11 @@ void ExtTheory::getInferences( int effort, std::vector< Node >& terms, std::vect } } } - } - Trace("extt-debug") << "..." << terms.size() << " unreduced." << std::endl; - if( !terms.empty() ){ - //get the current substitution + //get the current substitution for all variables if( d_parent->getCurrentSubstitution( effort, vars, sub, expc ) ){ + Assert( vars.size()==sub.size() ); for( unsigned i=0; i expn; @@ -392,13 +393,134 @@ void ExtTheory::getInferences( int effort, std::vector< Node >& terms, std::vect } } +bool ExtTheory::doInferencesInternal( int effort, std::vector< Node >& terms, std::vector< Node >& nred, bool batch, bool isRed ) { + if( batch ){ + bool addedLemma = false; + if( isRed ){ + for( unsigned i=0; igetReduction( effort, n, nr ); + if( ret==0 ){ + nred.push_back( n ); + }else{ + if( !nr.isNull() && n!=nr ){ + Node lem = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? kind::IFF : kind::EQUAL, n, nr ); + if( sendLemma( lem, true ) ){ + Trace("extt-lemma") << "ExtTheory : Reduction lemma : " << lem << std::endl; + addedLemma = true; + } + } + markReduced( terms[i], ret<0 ); + } + } + }else{ + std::vector< Node > sterms; + std::vector< std::vector< Node > > exp; + getSubstitutedTerms( effort, terms, sterms, exp ); + for( unsigned i=0; i1 ? NodeManager::currentNM()->mkNode( kind::AND, exp[i] ) : ( exp[i].size()==1 ? exp[i][0] : d_true ); + Trace("extt-debug") << "ExtTheory::doInferences : infer : " << eq << " by " << expn << std::endl; + Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, expn, eq ); + Trace("extt-debug") << "...send lemma " << lem << std::endl; + if( sendLemma( lem ) ){ + Trace("extt-lemma") << "ExtTheory : Constant rewrite lemma : " << lem << std::endl; + addedLemma = true; + } + } + } + if( !processed ){ + nred.push_back( terms[i] ); + } + } + } + return addedLemma; + }else{ + std::vector< Node > nnred; + if( terms.empty() ){ + for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){ + if( (*it).second && !isContextIndependentInactive( (*it).first ) ){ + std::vector< Node > nterms; + nterms.push_back( (*it).first ); + if( doInferencesInternal( effort, nterms, nnred, true, isRed ) ){ + return true; + } + } + } + }else{ + for( unsigned i=0; i nterms; + nterms.push_back( terms[i] ); + if( doInferencesInternal( effort, nterms, nnred, true, isRed ) ){ + return true; + } + } + } + return false; + } +} + +bool ExtTheory::sendLemma( Node lem, bool preprocess ) { + if( preprocess ){ + if( d_pp_lemmas.find( lem )==d_pp_lemmas.end() ){ + d_pp_lemmas.insert( lem ); + d_parent->getOutputChannel().lemma( lem, false, true ); + return true; + } + }else{ + if( d_lemmas.find( lem )==d_lemmas.end() ){ + d_lemmas.insert( lem ); + d_parent->getOutputChannel().lemma( lem ); + return true; + } + } + return false; +} + +bool ExtTheory::doInferences( int effort, std::vector< Node >& terms, std::vector< Node >& nred, bool batch ) { + if( !terms.empty() ){ + return doInferencesInternal( effort, terms, nred, batch, false ); + }else{ + return false; + } +} + +bool ExtTheory::doInferences( int effort, std::vector< Node >& nred, bool batch ) { + std::vector< Node > terms; + getActive( terms ); + return doInferencesInternal( effort, terms, nred, batch, false ); +} + +bool ExtTheory::doReductions( int effort, std::vector< Node >& terms, std::vector< Node >& nred, bool batch ) { + if( !terms.empty() ){ + return doInferencesInternal( effort, terms, nred, batch, true ); + }else{ + return false; + } +} + +bool ExtTheory::doReductions( int effort, std::vector< Node >& nred, bool batch ) { + std::vector< Node > terms; + getActive( terms ); + return doInferencesInternal( effort, terms, nred, batch, true ); +} + + //register term void ExtTheory::registerTerm( Node n ) { if( d_extf_kind.find( n.getKind() )!=d_extf_kind.end() ){ if( d_ext_func_terms.find( n )==d_ext_func_terms.end() ){ Trace("extt-debug") << "Found extended function : " << n << " in " << d_parent->getId() << std::endl; d_ext_func_terms[n] = true; - d_has_extf = true; + d_has_extf = n; std::map< Node, bool > visited; collectVars( n, d_extf_info[n].d_vars, visited ); } @@ -406,9 +528,22 @@ void ExtTheory::registerTerm( Node n ) { } //mark reduced -void ExtTheory::markReduced( Node n ) { +void ExtTheory::markReduced( Node n, bool contextDepend ) { d_ext_func_terms[n] = false; - //TODO update has_extf + if( !contextDepend ){ + d_ci_inactive.insert( n ); + } + + //update has_extf + if( d_has_extf.get()==n ){ + for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){ + //if not already reduced + if( (*it).second && !isContextIndependentInactive( (*it).first ) ){ + d_has_extf = (*it).first; + } + } + + } } //mark congruent @@ -424,11 +559,19 @@ void ExtTheory::markCongruent( Node a, Node b ) { } } +bool ExtTheory::isContextIndependentInactive( Node n ) { + return d_ci_inactive.find( n )!=d_ci_inactive.end(); +} + +bool ExtTheory::hasActiveTerm() { + return !d_has_extf.get().isNull(); +} + //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; + return (*it).second && !isContextIndependentInactive( n ); }else{ return false; } @@ -437,7 +580,7 @@ bool ExtTheory::isActive( Node n ) { 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 ){ + if( (*it).second && !isContextIndependentInactive( (*it).first ) ){ active.push_back( (*it).first ); } } @@ -446,7 +589,7 @@ void ExtTheory::getActive( std::vector< Node >& active ) { 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 ){ + if( (*it).first.getKind()==k && (*it).second && !isContextIndependentInactive( (*it).first ) ){ active.push_back( (*it).first ); } } diff --git a/src/theory/theory.h b/src/theory/theory.h index 08505be66..5d64c6446 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -24,6 +24,7 @@ #include #include "context/cdlist.h" +#include "context/cdhashset.h" #include "context/cdo.h" #include "context/context.h" #include "expr/node.h" @@ -891,8 +892,11 @@ public: */ virtual std::pair entailmentCheck(TNode lit, const EntailmentCheckParameters* params = NULL, EntailmentCheckSideEffects* out = NULL); - /* equality engine */ + /* equality engine TODO: use? */ virtual eq::EqualityEngine * getEqualityEngine() { return NULL; } + + /* get extended theory */ + virtual ExtTheory * getExtTheory() { return d_extt; } /* get current substitution at an effort * input : vars @@ -900,6 +904,13 @@ public: * 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; } + + /* get reduction for node + if return value is not 0, then n is reduced. + if return value <0 then n is reduced SAT-context-independently (e.g. by a lemma that persists at this user-context level). + if nr is non-null, then ( n = nr ) should be added as a lemma by caller, and return value should be <0. + */ + virtual int getReduction( int effort, Node n, Node& nr ) { return 0; } /** * Turn on proof-production mode. @@ -974,15 +985,23 @@ public: class ExtTheory { friend class Theory; typedef context::CDHashMap NodeBoolMap; + typedef context::CDHashSet NodeSet; protected: Theory * d_parent; + Node d_true; //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; + //set of terms from d_ext_func_terms that are SAT-context-independently inactive + // (e.g. term t when a reduction lemma of the form t = t' was added) + NodeSet d_ci_inactive; + //cache of all lemmas sent + NodeSet d_lemmas; + NodeSet d_pp_lemmas; + //watched term for checking if any non-reduced extended functions exist + context::CDO< Node > d_has_extf; //extf kind std::map< Kind, bool > d_extf_kind; - //information for extf + //information for each term in d_ext_func_terms class ExtfInfo { public: //all variables in this term @@ -991,25 +1010,49 @@ protected: std::map< Node, ExtfInfo > d_extf_info; //collect variables void collectVars( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited ); + // is context dependent inactive + bool isContextIndependentInactive( Node n ); + //do inferences internal + bool doInferencesInternal( int effort, std::vector< Node >& terms, std::vector< Node >& nred, bool batch, bool isRed ); + //send lemma + bool sendLemma( Node lem, bool preprocess = false ); 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 + // adds n to d_ext_func_terms if addFunctionKind( n.getKind() ) was called void registerTerm( Node n ); - //mark reduced - void markReduced( Node n ); - //mark congruent + // set n as reduced/inactive + // if contextDepend = false, then n remains inactive in the duration of this user-context level + void markReduced( Node n, bool contextDepend = true ); + // mark that a and b are congruent terms: set b inactive, set a to inactive if b was inactive void markCongruent( Node a, Node b ); - //is active + + //getSubstitutedTerms + // input : effort, terms + // output : sterms, exp, where ( exp[i] => terms[i] = sterms[i] ) for all i + void getSubstitutedTerms( int effort, std::vector< Node >& terms, std::vector< Node >& sterms, std::vector< std::vector< Node > >& exp ); + //doInferences + // * input : effort, terms, batch (whether to send one lemma or lemmas for all terms) + // * sends rewriting lemmas of the form ( exp => t = c ) where t is in terms and c is a constant, c = rewrite( t*sigma ) where exp |= sigma + // * output : nred (the terms that are still active) + // * return : true iff lemma is sent + bool doInferences( int effort, std::vector< Node >& terms, std::vector< Node >& nred, bool batch=true ); + bool doInferences( int effort, std::vector< Node >& nred, bool batch=true ); + //doReductions + // same as doInferences, but will send reduction lemmas of the form ( t = t' ) where t is in terms, t' is equivalent, reduced term + bool doReductions( int effort, std::vector< Node >& terms, std::vector< Node >& nred, bool batch=true ); + bool doReductions( int effort, std::vector< Node >& nred, bool batch=true ); + + //has active term + bool hasActiveTerm(); + //is n active bool isActive( Node n ); - //get active + //get the set of active terms from d_ext_func_terms void getActive( std::vector< Node >& active ); + //get the set of active terms from d_ext_func_terms of kind k void getActive( std::vector< Node >& active, Kind k ); };