diff options
Diffstat (limited to 'src/theory/quantifiers/relevant_domain.cpp')
| -rw-r--r-- | src/theory/quantifiers/relevant_domain.cpp | 43 |
1 files changed, 28 insertions, 15 deletions
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 1563a3d1d..495e0f7a4 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -26,16 +26,18 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; -RelevantDomain::RelevantDomain( FirstOrderModel* m ) : d_model( m ){ +RelevantDomain::RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m ) : d_qe( qe ), d_model( m ){ } void RelevantDomain::compute(){ + Trace("rel-dom") << "compute relevant domain" << std::endl; d_quant_inst_domain.clear(); for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){ Node f = d_model->getAssertedQuantifier( i ); d_quant_inst_domain[f].resize( f[0].getNumChildren() ); } + Trace("rel-dom") << "account for ground terms" << std::endl; //add ground terms to domain (rule 1 of complete instantiation essentially uf fragment) for( std::map< Node, uf::UfModelTree >::iterator it = d_model->d_uf_model_tree.begin(); it != d_model->d_uf_model_tree.end(); ++it ){ @@ -47,6 +49,7 @@ void RelevantDomain::compute(){ if( d_model->d_rep_set.hasType( n[j].getType() ) ){ Node ra = d_model->getRepresentative( n[j] ); int raIndex = d_model->d_rep_set.getIndexFor( ra ); + if( raIndex==-1 ) Trace("rel-dom-warn") << "WARNING: Ground domain: rep set does not contain : " << ra << std::endl; Assert( raIndex!=-1 ); if( std::find( d_active_domain[op][j].begin(), d_active_domain[op][j].end(), raIndex )==d_active_domain[op][j].end() ){ d_active_domain[op][j].push_back( raIndex ); @@ -56,12 +59,14 @@ void RelevantDomain::compute(){ //add to range Node r = d_model->getRepresentative( n ); int raIndex = d_model->d_rep_set.getIndexFor( r ); + if( raIndex==-1 ) Trace("rel-dom-warn") << "WARNING: Ground range: rep set does not contain : " << r << std::endl; Assert( raIndex!=-1 ); if( std::find( d_active_range[op].begin(), d_active_range[op].end(), raIndex )==d_active_range[op].end() ){ d_active_range[op].push_back( raIndex ); } } } + Trace("rel-dom") << "do quantifiers" << std::endl; //find fixed point for relevant domain computation bool success; do{ @@ -69,19 +74,20 @@ void RelevantDomain::compute(){ for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){ Node f = d_model->getAssertedQuantifier( i ); //compute the domain of relevant instantiations (rule 3 of complete instantiation, essentially uf fragment) - if( computeRelevantInstantiationDomain( d_model->getTermDatabase()->getCounterexampleBody( f ), Node::null(), -1, d_quant_inst_domain[f] ) ){ + if( computeRelevantInstantiationDomain( d_qe->getTermDatabase()->getCounterexampleBody( f ), Node::null(), -1, f ) ){ success = false; } //extend the possible domain for functions (rule 2 of complete instantiation, essentially uf fragment) RepDomain range; - if( extendFunctionDomains( d_model->getTermDatabase()->getCounterexampleBody( f ), range ) ){ + if( extendFunctionDomains( d_qe->getTermDatabase()->getCounterexampleBody( f ), range ) ){ success = false; } } }while( !success ); + Trace("rel-dom") << "done compute relevant domain" << std::endl; } -bool RelevantDomain::computeRelevantInstantiationDomain( Node n, Node parent, int arg, std::vector< RepDomain >& rd ){ +bool RelevantDomain::computeRelevantInstantiationDomain( Node n, Node parent, int arg, Node f ){ bool domainChanged = false; if( n.getKind()==INST_CONSTANT ){ bool domainSet = false; @@ -93,8 +99,9 @@ bool RelevantDomain::computeRelevantInstantiationDomain( Node n, Node parent, in if( d_active_domain.find( op )!=d_active_domain.end() ){ for( size_t i=0; i<d_active_domain[op][arg].size(); i++ ){ int d = d_active_domain[op][arg][i]; - if( std::find( rd[vi].begin(), rd[vi].end(), d )==rd[vi].end() ){ - rd[vi].push_back( d ); + if( std::find( d_quant_inst_domain[f][vi].begin(), d_quant_inst_domain[f][vi].end(), d )== + d_quant_inst_domain[f][vi].end() ){ + d_quant_inst_domain[f][vi].push_back( d ); domainChanged = true; } } @@ -104,21 +111,21 @@ bool RelevantDomain::computeRelevantInstantiationDomain( Node n, Node parent, in if( !domainSet ){ //otherwise, we must consider the entire domain TypeNode tn = n.getType(); - if( d_model->d_rep_set.hasType( tn ) ){ - if( rd[vi].size()!=d_model->d_rep_set.d_type_reps[tn].size() ){ - rd[vi].clear(); + if( d_quant_inst_domain_complete[f].find( vi )==d_quant_inst_domain_complete[f].end() ){ + if( d_model->d_rep_set.hasType( tn ) ){ + //it is the complete domain + d_quant_inst_domain[f][vi].clear(); for( size_t i=0; i<d_model->d_rep_set.d_type_reps[tn].size(); i++ ){ - rd[vi].push_back( i ); - domainChanged = true; + d_quant_inst_domain[f][vi].push_back( i ); } + domainChanged = true; } - }else{ - //infinite domain? + d_quant_inst_domain_complete[f][vi] = true; } } }else{ for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( computeRelevantInstantiationDomain( n[i], n, i, rd ) ){ + if( computeRelevantInstantiationDomain( n[i], n, i, f ) ){ domainChanged = true; } } @@ -166,7 +173,13 @@ bool RelevantDomain::extendFunctionDomains( Node n, RepDomain& range ){ } }else{ Node r = d_model->getRepresentative( n ); - range.push_back( d_model->d_rep_set.getIndexFor( r ) ); + int index = d_model->d_rep_set.getIndexFor( r ); + if( index==-1 ){ + //we consider all ground terms in bodies of quantifiers to be the first ground representative + range.push_back( 0 ); + }else{ + range.push_back( index ); + } } return domainChanged; } |