more minor updates to inst gen and representative selection, clean up of equality query

1 files changed, 96 insertions, 56 deletions

diff --git a/src/theory/quantifiers/inst_gen.cpp b/src/theory/quantifiers/inst_gen.cpp
index 428a224ee..932a00185 100755
--- a/src/theory/quantifiers/inst_gen.cpp
+++ b/src/theory/quantifiers/inst_gen.cpp
@@ -19,7 +19,7 @@
 #include "theory/quantifiers/model_builder.h"

 #include "theory/quantifiers/first_order_model.h"

 

-#define RECONSIDER_FUNC_CONSTANT

+//#define CHILD_USE_CONSIDER

 

 using namespace std;

 using namespace CVC4;

@@ -55,6 +55,7 @@ void InstGenProcess::addMatchValue( QuantifiersEngine* qe, Node f, Node val, Ins
 }

 

 void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vector< Node >& considerVal, bool useConsider ){

+  Trace("inst-gen-cm") << "* Calculate matches " << d_node << std::endl;

   //whether we are doing a product or sum or matches

   bool doProduct = true;

   //get the model

@@ -64,32 +65,25 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vecto
   std::vector< Node > considerTerms;

   std::vector< std::vector< Node > > newConsiderVal;

   std::vector< bool > newUseConsider;

+  std::map< Node, InstMatch > considerTermsMatch[2];

+  std::map< Node, bool > considerTermsSuccess[2];

   newConsiderVal.resize( d_children.size() );

-  newUseConsider.resize( d_children.size(), false );

+  newUseConsider.resize( d_children.size(), useConsider );

   if( d_node.getKind()==APPLY_UF ){

     Node op = d_node.getOperator();

     if( useConsider ){

+#ifndef CHILD_USE_CONSIDER

+      for( size_t i=0; i<newUseConsider.size(); i++ ){

+        newUseConsider[i] = false;

+      }

+#endif

       for( size_t i=0; i<considerVal.size(); i++ ){

         eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( considerVal[i] ),

                                  qe->getEqualityQuery()->getEngine() );

         while( !eqc.isFinished() ){

           Node en = (*eqc);

           if( en.getKind()==APPLY_UF && en.getOperator()==op ){

-            bool isSelected = qe->getModelEngine()->getModelBuilder()->isTermSelected( en );

-            bool isActive = !en.getAttribute(NoMatchAttribute());

-            //check if we need to consider it

-            if( isSelected || isActive ){

               considerTerms.push_back( en );

-#if 0

-              for( int i=0; i<(int)d_children.size(); i++ ){

-                int childIndex = d_children_index[i];

-                Node n = qe->getModel()->getRepresentative( n );

-                if( std::find( newConsiderVal[i].begin(), newConsiderVal[i].end(), n )==newConsiderVal[i].end() ){

-                  newConsiderVal[i].push_back( n );

-                }

-              }

-#endif

-            }

           }

           ++eqc;

         }

@@ -97,23 +91,92 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vecto
     }else{

       considerTerms.insert( considerTerms.begin(), fm->d_uf_terms[op].begin(), fm->d_uf_terms[op].end() );

     }

-  }else if( d_node.getType().isBoolean() ){

-    if( useConsider ){

-      Assert( considerVal.size()==1 );

-      bool reqPol = considerVal[0]==fm->d_true;

-      if( d_node.getKind()==NOT ){

-        if( !newConsiderVal.empty() ){

-          newConsiderVal[0].push_back( reqPol ? fm->d_false : fm->d_true );

-          newUseConsider[0] = true;

+    //for each term we consider, calculate a current match

+    for( size_t i=0; i<considerTerms.size(); i++ ){

+      Node n = considerTerms[i];

+      bool isSelected = qe->getModelEngine()->getModelBuilder()->isTermSelected( n );

+      bool hadSuccess = false;

+      for( int t=(isSelected ? 0 : 1); t<2; t++ ){

+        if( t==0 || !n.getAttribute(NoMatchAttribute()) ){

+          considerTermsMatch[t][n] = InstMatch();

+          considerTermsSuccess[t][n] = true;

+          for( size_t j=0; j<d_node.getNumChildren(); j++ ){

+            if( d_children_map.find( j )==d_children_map.end() ){

+              if( t!=0 || !n[j].getAttribute(ModelBasisAttribute()) ){

+                if( d_node[j].getKind()==INST_CONSTANT ){

+                  if( !considerTermsMatch[t][n].setMatch( qe->getEqualityQuery(), d_node[j], n[j] ) ){

+                    Trace("inst-gen-cm") << "fail match: " << n[j] << " is not equal to ";

+                    Trace("inst-gen-cm") << considerTermsMatch[t][n].getValue( d_node[j] ) << std::endl;

+                    considerTermsSuccess[t][n] = false;

+                    break;

+                  }

+                }else if( !qe->getEqualityQuery()->areEqual( d_node[j], n[j] ) ){

+                  Trace("inst-gen-cm") << "fail arg: " << n[j] << " is not equal to " << d_node[j] << std::endl;

+                  considerTermsSuccess[t][n] = false;

+                  break;

+                }

+              }

+            }

+          }

+          //if successful, store it

+          if( considerTermsSuccess[t][n] ){

+#ifdef CHILD_USE_CONSIDER

+            if( !hadSuccess ){

+              hadSuccess = true;

+              for( size_t k=0; k<d_children.size(); k++ ){

+                if( newUseConsider[k] ){

+                  int childIndex = d_children_index[k];

+                  //determine if we are restricted or not

+                  if( t!=0 || !n[childIndex].getAttribute(ModelBasisAttribute()) ){

+                    Node r = qe->getModel()->getRepresentative( n[childIndex] );

+                    if( std::find( newConsiderVal[k].begin(), newConsiderVal[k].end(), r )==newConsiderVal[k].end() ){

+                      newConsiderVal[k].push_back( r );

+                      //check if we now need to consider the entire domain

+                      TypeNode tn = r.getType();

+                      if( qe->getModel()->d_rep_set.hasType( tn ) ){

+                        if( (int)newConsiderVal[k].size()>=qe->getModel()->d_rep_set.getNumRepresentatives( tn ) ){

+                          newConsiderVal[k].clear();

+                          newUseConsider[k] = false;

+                        }

+                      }

+                    }

+                  }else{

+                    //matching against selected term, will need to consider all values

+                    newConsiderVal[k].clear();

+                    newUseConsider[k] = false;

+                  }

+                }

+              }

+            }

+#endif

+          }

         }

-      }else if( d_node.getKind()==AND || d_node.getKind()==OR ){

-        for( size_t i=0; i<newConsiderVal.size(); i++ ){

-          newConsiderVal[i].push_back( considerVal[0] );

-          newUseConsider[i] = true;

+      }

+    }

+  }else{

+    //the interpretted case

+    if( d_node.getType().isBoolean() ){

+      if( useConsider ){

+        //if( considerVal.size()!=1 ) { std::cout << "consider val = " << considerVal.size() << std::endl; }

+        Assert( considerVal.size()==1 );

+        bool reqPol = considerVal[0]==fm->d_true;

+        Node ncv = considerVal[0];

+        if( d_node.getKind()==NOT ){

+          ncv = reqPol ? fm->d_false : fm->d_true;

         }

-        //instead we will do a sum

-        if( ( d_node.getKind()==AND && !reqPol ) || ( d_node.getKind()==OR && reqPol )  ){

-          doProduct = false;

+        if( d_node.getKind()==NOT || d_node.getKind()==AND || d_node.getKind()==OR ){

+          for( size_t i=0; i<newConsiderVal.size(); i++ ){

+            newConsiderVal[i].push_back( ncv );

+          }

+          //instead we will do a sum

+          if( ( d_node.getKind()==AND && !reqPol ) || ( d_node.getKind()==OR && reqPol )  ){

+            doProduct = false;

+          }

+        }else{

+          //do not use consider

+          for( size_t i=0; i<newUseConsider.size(); i++ ){

+            newUseConsider[i] = false;

+          }

         }

       }

     }

@@ -126,7 +189,6 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vecto
       return;

     }

   }

-  Trace("inst-gen-cm") << "* Calculate matches " << d_node << std::endl;

   if( d_node.getKind()==APPLY_UF ){

     //if this is an uninterpreted function

     Node op = d_node.getOperator();

@@ -138,35 +200,13 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vecto
         //do not consider ground case if it is already congruent to another ground term

         if( t==0 || !n.getAttribute(NoMatchAttribute()) ){

           Trace("inst-gen-cm") << "calculate for " << n << ", selected = " << (t==0) << std::endl;

-          bool success = true;

-          InstMatch curr;

-          for( size_t j=0; j<d_node.getNumChildren(); j++ ){

-            if( d_children_map.find( j )==d_children_map.end() ){

-              if( t!=0 || !n[j].getAttribute(ModelBasisAttribute()) ){

-                if( d_node[j].getKind()==INST_CONSTANT ){

-                  //FIXME: is this correct?

-                  if( !curr.setMatch( qe->getEqualityQuery(), d_node[j], n[j] ) ){

-                    Trace("inst-gen-cm") << "fail match: " << n[j] << " is not equal to " << curr.get( d_node[j] ) << std::endl;

-                    Trace("inst-gen-cm") << "  are equal : " << qe->getEqualityQuery()->areEqual( n[j], curr.get( d_node[j] ) ) << std::endl;

-                    success = false;

-                    break;

-                  }

-                }else if( !qe->getEqualityQuery()->areEqual( d_node[j], n[j] ) ){

-                  Trace("inst-gen-cm") << "fail arg: " << n[j] << " is not equal to " << d_node[j] << std::endl;

-                  success = false;

-                  break;

-                }

-              }

-            }

-          }

-          if( success ){

+          if( considerTermsSuccess[t][n] ){

             //try to find unifier for d_node = n

-            calculateMatchesUninterpreted( qe, f, curr, n, 0, t==0 );

+            calculateMatchesUninterpreted( qe, f, considerTermsMatch[t][n], n, 0, t==0 );

           }

         }

       }

     }

-

   }else{

     //if this is an interpreted function

     if( doProduct ){