merge from fmf-devel branch. more updates to models: now with collectModelInfo with fullModel argument, most theory-specific implementation out of the model class, model printer relegated to printer classes. Also updates to finite mode finding, modifications to datatypes making them compatible with theory combination, support for theory-specific handling of user attributes, refactoring of uf models

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;
   }