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
/////////////////////////////////////////////////////////////////////////////
for( unsigned j=0; j<col[i].size(); j++ ) {
Trace("strings-model") << col[i][j] << " ";
//check if col[i][j] has only variables
- EqcInfo* ei = getOrMakeEqcInfo( col[i][j], false );
- Node cst = ei ? ei->d_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;
}
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; i<extf.size(); i++ ){
Node n = extf[i];
- if( d_extf_info_tmp[n].d_model_active ){
- Assert( d_extf_info_tmp.find( n )!=d_extf_info_tmp.end() );
- if( checkExtfReduction( n, d_extf_info_tmp[n].d_pol, effort ) ){
- d_extt->markReduced( 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) {
}
/** 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]);
ei->d_length_term = t[0];
//we care about the length of this string
registerTerm( t[0], 1 );
+ }else{
+ //d_extt->registerTerm( t );
}
}
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 );
}
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 );
}
}
}
+ //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
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<terms.size(); i++ ){
Node n = terms[i];
Node sn = sterms[i];
return atom;
}
-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<n.getNumChildren(); i++ ){
- collectExtendedFuncTerms( n[i], visited );
- }
- }
-}
-
// Stats
TheoryStrings::Statistics::Statistics():
d_splits("TheoryStrings::NumOfSplitOnDemands", 0),
if(r[0].isConst()) {
break;
} else {
- if (d_normal_forms.find(r[0]) != d_normal_forms.end()) {
- const std::vector<Node>& 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<Node>::iterator nf_end_exp = nf_exp.end();
- std::vector<Node>::const_iterator nf_r0_begin = nf_r0.begin();
- std::vector<Node>::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) );
}
}
}
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<n.getNumChildren(); i++ ){
+ collectExtendedFuncTerms( n[i], visited );
+ }
+ }
+}
+
}/* CVC4::theory::strings namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
Node explain( TNode literal );
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 );
+ int getReduction( int effort, Node n, Node& nr );
// NotifyClass for equality engine
class NotifyClass : public eq::EqualityEngineNotify {
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
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;
};
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 );
~Statistics();
};/* class TheoryStrings::Statistics */
Statistics d_statistics;
+
};/* class TheoryStrings */
}/* CVC4::theory::strings namespace */
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<n.getNumChildren(); i++ ){
collectVars( n[i], vars, visited );
}
}
//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<terms.size(); i++ ){
+ //do substitution, rewrite
+ Node n = terms[i];
std::map< Node, ExtfInfo >::iterator iti = d_extf_info.find( n );
Assert( iti!=d_extf_info.end() );
for( unsigned i=0; i<iti->second.d_vars.size(); i++ ){
}
}
}
- }
- 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<terms.size(); i++ ){
- //do substitution, rewrite
+ //do substitution
Node n = terms[i];
Node ns = n.substitute( vars.begin(), vars.end(), sub.begin(), sub.end() );
std::vector< Node > expn;
}
}
+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; i<terms.size(); i++ ){
+ Node n = terms[i];
+ Node nr;
+ //TODO: reduction with substitution?
+ int ret = d_parent->getReduction( 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; i<terms.size(); i++ ){
+ bool processed = false;
+ if( sterms[i]!=terms[i] ){
+ Node sr = Rewriter::rewrite( sterms[i] );
+ if( sr.isConst() ){
+ processed = true;
+ markReduced( terms[i] );
+ Node eq = terms[i].eqNode( sr );
+ Node expn = exp[i].size()>1 ? 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<terms.size(); i++ ){
+ std::vector< Node > 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 );
}
}
//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
}
}
+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;
}
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 );
}
}
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 );
}
}
#include <string>
#include "context/cdlist.h"
+#include "context/cdhashset.h"
#include "context/cdo.h"
#include "context/context.h"
#include "expr/node.h"
*/
virtual std::pair<bool, Node> 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
* 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.
class ExtTheory {
friend class Theory;
typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
+ typedef context::CDHashSet<Node, NodeHashFunction> 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
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 );
};
projects / cvc5.git / commitdiff