From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 29 Sep 2014 19:39:34 +0000 (+0200)
Subject: Add option for aggressive model filtering in conjecture generator (enumerate ground... 
X-Git-Tag: cvc5-1.0.0~6613
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a4a943134f888a514f19adaffe2f6743a16a25a6;p=cvc5.git

Add option for aggressive model filtering in conjecture generator (enumerate ground terms).
---

diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index a2e3d4ce3..799cce9ed 100755
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -32,8 +32,8 @@ struct sortConjectureScore {
   std::vector< int > d_scores;
   bool operator() (unsigned i, unsigned j) { return d_scores[i]>d_scores[j]; }
 };
-  
-  
+
+
 void OpArgIndex::addTerm( ConjectureGenerator * s, TNode n, unsigned index ){
   if( index==n.getNumChildren() ){
     Assert( n.hasOperator() );
@@ -264,7 +264,7 @@ TNode ConjectureGenerator::getUniversalRepresentative( TNode n, bool add ) {
       }
     }
   }
-  
+
   if( d_uequalityEngine.hasTerm( n ) ){
     Node r = d_uequalityEngine.getRepresentative( n );
     EqcInfo * ei = getOrMakeEqcInfo( r );
@@ -381,6 +381,25 @@ bool ConjectureGenerator::needsCheck( Theory::Effort e ) {
   return e==Theory::EFFORT_FULL;
 }
 
+bool ConjectureGenerator::hasEnumeratedUf( Node n ) {
+  if( options::conjectureGenGtEnum()>0 ){
+    std::map< Node, bool >::iterator it = d_uf_enum.find( n.getOperator() );
+    if( it==d_uf_enum.end() ){
+      d_uf_enum[n.getOperator()] = true;
+      std::vector< Node > lem;
+      getEnumeratePredUfTerm( n, options::conjectureGenGtEnum(), lem );
+      if( !lem.empty() ){
+        for( unsigned j=0; j<lem.size(); j++ ){
+          d_quantEngine->addLemma( lem[j], false );
+          d_hasAddedLemma = true;
+        }
+        return false;
+      }
+    }
+  }
+  return true;
+}
+
 void ConjectureGenerator::reset_round( Theory::Effort e ) {
 
 }
@@ -389,11 +408,12 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
   if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
     d_fullEffortCount++;
     if( d_fullEffortCount%optFullCheckFrequency()==0 ){
+      d_hasAddedLemma = false;
       d_tge.d_cg = this;
       double clSet = 0;
       if( Trace.isOn("sg-engine") ){
         clSet = double(clock())/double(CLOCKS_PER_SEC);
-        Trace("sg-engine") << "---Instantiation Engine Round, effort = " << e << "---" << std::endl;
+        Trace("sg-engine") << "---Conjecture Engine Round, effort = " << e << "---" << std::endl;
       }
       eq::EqualityEngine * ee = getEqualityEngine();
 
@@ -529,8 +549,11 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
 
       Trace("sg-proc") << "Collect signature information..." << std::endl;
       d_tge.collectSignatureInformation();
+      if( d_hasAddedLemma ){
+        Trace("sg-proc") << "...added enumeration lemmas." << std::endl;
+      }
       Trace("sg-proc") << "...done collect signature information" << std::endl;
-      
+
 
 
       Trace("sg-proc") << "Build theorem index..." << std::endl;
@@ -631,7 +654,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
       d_thm_index.debugPrint( "thm-db" );
       Trace("thm-db") << std::endl;
       Trace("sg-proc") << "...done build theorem index" << std::endl;
-      
+
 
       //clear patterns
       d_patterns.clear();
@@ -759,12 +782,12 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
         Trace("sg-proc") << "...done generate terms at depth " << depth << std::endl;
         Trace("sg-stats") << "--------> Total LHS of depth " << depth << " : " << rel_term_count << std::endl;
         //Trace("conjecture-count") << "Total LHS of depth " << depth << " : " << conj_lhs[depth].size() << std::endl;
-        
+
         /* test...
         for( unsigned i=0; i<rt_types.size(); i++ ){
           Trace("sg-term-enum") << "Term enumeration for " << rt_types[i] << " : " << std::endl;
           Trace("sg-term-enum") << "Ground term : " << rt_types[i].mkGroundTerm() << std::endl;
-          for( unsigned j=0; j<10; j++ ){
+          for( unsigned j=0; j<150; j++ ){
             Trace("sg-term-enum") << "  " << getEnumerateTerm( rt_types[i], j ) << std::endl;
           }
         }
@@ -785,7 +808,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
 
             Trace("sg-proc") << "Generate relevant RHS terms of type " << rt_types[i] << " at depth " << rdepth << "..." << std::endl;
             d_tge.reset( rdepth, false, rt_types[i] );
-            
+
             while( d_tge.getNextTerm() ){
               Node rhs = d_tge.getTerm();
               if( considerTermCanon( rhs, false ) ){
@@ -882,7 +905,7 @@ unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, in
       }
       if( doSort && d_waiting_conjectures_score[indices[0]]<optFilterScoreThreshold() ){
         //do splitting on demand (TODO)
-        
+
       }else{
         for( unsigned i=0; i<indices.size(); i++ ){
           //if( d_waiting_conjectures_score[indices[i]]<optFilterScoreThreshold() ){
@@ -1094,8 +1117,105 @@ Node ConjectureGenerator::getEnumerateTerm( TypeNode tn, unsigned index ) {
   return d_enum_terms[tn][index];
 }
 
+
+Node ConjectureGenerator::getPredicateForType( TypeNode tn ) {
+  std::map< TypeNode, Node >::iterator it = d_typ_pred.find( tn );
+  if( it==d_typ_pred.end() ){
+    TypeNode op_tn = NodeManager::currentNM()->mkFunctionType( tn, NodeManager::currentNM()->booleanType() );
+    Node op = NodeManager::currentNM()->mkSkolem( "PE", op_tn, "was created by conjecture ground term enumerator." );
+    d_typ_pred[tn] = op;
+    return op;
+  }else{
+    return it->second;
+  }
+}
+
+void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< Node >& terms ) {
+  if( n.getNumChildren()>0 ){
+    std::vector< int > vec;
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      vec.push_back( 0 );
+    }
+    vec.pop_back();
+    int size_limit = 0;
+    int vec_sum = -1;
+    unsigned index = 0;
+    unsigned last_size = terms.size();
+    while( terms.size()<num ){
+      bool success = true;
+      if( vec_sum==-1 ){
+        vec_sum = 0;
+        vec.push_back( size_limit );
+      }else{
+        //see if we can iterate current
+        if( vec_sum<size_limit && !getEnumerateTerm( n[index].getType(), vec[index]+1 ).isNull() ){
+          vec[index]++;
+          vec_sum++;
+          vec.push_back( size_limit - vec_sum );
+        }else{
+          vec_sum -= vec[index];
+          vec[index] = 0;
+          index++;
+          if( index==n.getNumChildren() ){
+            success = false;
+          }
+        }
+      }
+      if( success ){
+        if( vec.size()==n.getNumChildren() ){
+          Node lc = getEnumerateTerm( n[vec.size()-1].getType(), vec[vec.size()-1] );
+          if( !lc.isNull() ){
+            for( unsigned i=0; i<vec.size(); i++ ){
+              Trace("sg-gt-enum-debug") << vec[i] << " ";
+            }
+            Trace("sg-gt-enum-debug") << " / " << size_limit << std::endl;
+            for( unsigned i=0; i<n.getNumChildren(); i++ ){
+              Trace("sg-gt-enum-debug") << n[i].getType() << " ";
+            }
+            Trace("sg-gt-enum-debug") << std::endl;
+            std::vector< Node > children;
+            children.push_back( n.getOperator() );
+            for( unsigned i=0; i<(vec.size()-1); i++ ){
+              Node nn = getEnumerateTerm( n[i].getType(), vec[i] );
+              Assert( !nn.isNull() );
+              Assert( nn.getType()==n[i].getType() );
+              children.push_back( nn );
+            }
+            children.push_back( lc );
+            Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );
+            Trace("sg-gt-enum") << "Ground term enumerate : " << n << std::endl;
+            terms.push_back( n );
+          }
+          vec.pop_back();
+          index = 0;
+        }
+      }else{
+        if( terms.size()>last_size ){
+          last_size = terms.size();
+          size_limit++;
+          for( unsigned i=0; i<vec.size(); i++ ){
+            vec[i] = 0;
+          }
+          vec_sum = -1;
+        }
+      }
+    }
+  }else{
+    terms.push_back( n );
+  }
+}
+
+void ConjectureGenerator::getEnumeratePredUfTerm( Node n, unsigned num, std::vector< Node >& terms ) {
+  std::vector< Node > uf_terms;
+  getEnumerateUfTerm( n, num, uf_terms );
+  Node p = getPredicateForType( n.getType() );
+  for( unsigned i=0; i<uf_terms.size(); i++ ){
+    terms.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, p, uf_terms[i] ) );
+  }
+}
+
 void ConjectureGenerator::processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth ) {
-  int score = considerCandidateConjecture( lhs, rhs ); 
+  int score = considerCandidateConjecture( lhs, rhs );
   if( score>0 ){
     Trace("sg-conjecture") << "* Candidate conjecture : " << lhs << " == " << rhs << std::endl;
     Trace("sg-conjecture-debug") << "     LHS, RHS generalization depth : " << lhs_depth << ", " << rhs_depth << std::endl;
@@ -1132,7 +1252,7 @@ void ConjectureGenerator::processCandidateConjecture( TNode lhs, TNode rhs, unsi
 
 int ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) {
   Assert( lhs.getType()==rhs.getType() );
-  
+
   Trace("sg-cconj-debug") << "Consider candidate conjecture : " << lhs << " == " << rhs << "?" << std::endl;
   if( lhs==rhs ){
     Trace("sg-cconj-debug") << "  -> trivial." << std::endl;
@@ -1179,7 +1299,7 @@ int ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) {
     //  Trace("sg-cconj") << "  -> after processing, not canonical." << std::endl;
     //  return -1;
     //}
-    
+
     int score;
     bool scoreSet = false;
 
@@ -1218,7 +1338,7 @@ int ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) {
 
     Trace("sg-cconj") << "  -> SUCCESS." << std::endl;
     Trace("sg-cconj") << "     score : " << score << std::endl;
-    
+
     return score;
   }
 }
@@ -1684,15 +1804,24 @@ void TermGenEnv::collectSignatureInformation() {
     if( !getTermDatabase()->d_op_map[it->first].empty() ){
       Node nn = getTermDatabase()->d_op_map[it->first][0];
       if( d_cg->isHandledTerm( nn ) && nn.getKind()!=APPLY_SELECTOR_TOTAL && !nn.getType().isBoolean() ){
-        d_funcs.push_back( it->first );
-        for( unsigned i=0; i<nn.getNumChildren(); i++ ){
-          d_func_args[it->first].push_back( nn[i].getType() );
+        bool do_enum = true;
+        //check if we have enumerated ground terms
+        if( nn.getKind()==APPLY_UF ){
+          if( !d_cg->hasEnumeratedUf( nn ) ){
+            do_enum = false;
+          }
+        }
+        if( do_enum ){
+          d_funcs.push_back( it->first );
+          for( unsigned i=0; i<nn.getNumChildren(); i++ ){
+            d_func_args[it->first].push_back( nn[i].getType() );
+          }
+          d_func_kind[it->first] = nn.getKind();
+          d_typ_tg_funcs[tnull].push_back( it->first );
+          d_typ_tg_funcs[nn.getType()].push_back( it->first );
+          Trace("sg-rel-sig") << "Will enumerate function applications of : " << it->first << ", #args = " << d_func_args[it->first].size() << ", kind = " << nn.getKind() << std::endl;
+          getTermDatabase()->computeUfEqcTerms( it->first );
         }
-        d_func_kind[it->first] = nn.getKind();
-        d_typ_tg_funcs[tnull].push_back( it->first );
-        d_typ_tg_funcs[nn.getType()].push_back( it->first );
-        Trace("sg-rel-sig") << "Will enumerate function applications of : " << it->first << ", #args = " << d_func_args[it->first].size() << ", kind = " << nn.getKind() << std::endl;
-        getTermDatabase()->computeUfEqcTerms( it->first );
       }
     }
   }
@@ -1712,18 +1841,18 @@ void TermGenEnv::collectSignatureInformation() {
 void TermGenEnv::reset( unsigned depth, bool genRelevant, TypeNode tn ) {
   Assert( d_tg_alloc.empty() );
   d_tg_alloc.clear();
-  
+
   if( genRelevant ){
     for( unsigned i=0; i<2; i++ ){
       d_ccand_eqc[i].clear();
       d_ccand_eqc[i].push_back( d_relevant_eqc[i] );
     }
   }
-  
+
   d_tg_id = 0;
   d_tg_gdepth = 0;
   d_tg_gdepth_limit = depth;
-  d_gen_relevant_terms = genRelevant;        
+  d_gen_relevant_terms = genRelevant;
   d_tg_alloc[0].reset( this, tn );
 }
 
@@ -1741,8 +1870,8 @@ bool TermGenEnv::getNextTerm() {
 }
 
 //reset matching
-void TermGenEnv::resetMatching( TNode eqc, unsigned mode ) { 
-  d_tg_alloc[0].resetMatching( this, eqc, mode ); 
+void TermGenEnv::resetMatching( TNode eqc, unsigned mode ) {
+  d_tg_alloc[0].resetMatching( this, eqc, mode );
 }
 
 //get next match
@@ -1751,8 +1880,8 @@ bool TermGenEnv::getNextMatch( TNode eqc, std::map< TypeNode, std::map< unsigned
 }
 
 //get term
-Node TermGenEnv::getTerm() { 
-  return d_tg_alloc[0].getTerm( this ); 
+Node TermGenEnv::getTerm() {
+  return d_tg_alloc[0].getTerm( this );
 }
 
 void TermGenEnv::debugPrint( const char * c, const char * cd ) {
@@ -1931,7 +2060,6 @@ bool TermGenEnv::isGroundTerm( TNode n ){
 }
 
 
-
 void SubstitutionIndex::addSubstitution( TNode eqc, std::vector< TNode >& vars, std::vector< TNode >& terms, unsigned i ) {
   if( i==vars.size() ){
     d_var = eqc;
@@ -2084,5 +2212,3 @@ unsigned ConjectureGenerator::optFullCheckFrequency() { return 1; }
 bool ConjectureGenerator::optStatsOnly() { return false; }
 
 }
-
-
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index eb7f4b2aa..23e2b88ba 100755
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -129,7 +129,7 @@ public:
   Node getTerm();
   //debug print
   void debugPrint( const char * c, const char * cd );
-  
+
   //conjecture generation
   ConjectureGenerator * d_cg;
   //the current number of enumerated variables per type
@@ -149,14 +149,14 @@ public:
   std::map< unsigned, TermGenerator > d_tg_alloc;
   unsigned d_tg_gdepth;
   int d_tg_gdepth_limit;
-  
+
   //all functions
   std::vector< TNode > d_funcs;
   //function to kind map
   std::map< TNode, Kind > d_func_kind;
   //type of each argument of the function
   std::map< TNode, std::vector< TypeNode > > d_func_args;
-  
+
   //access functions
   unsigned getNumTgVars( TypeNode tn );
   bool allowVar( TypeNode tn );
@@ -364,6 +364,16 @@ private:
   std::vector< TypeEnumerator > d_typ_enum;
   //get nth term for type
   Node getEnumerateTerm( TypeNode tn, unsigned index );
+  //predicate for type
+  std::map< TypeNode, Node > d_typ_pred;
+  //get predicate for type
+  Node getPredicateForType( TypeNode tn );
+  //
+  void getEnumerateUfTerm( Node n, unsigned num, std::vector< Node >& terms );
+  //
+  void getEnumeratePredUfTerm( Node n, unsigned num, std::vector< Node >& terms );
+  // uf operators enumerated
+  std::map< Node, bool > d_uf_enum;
 public:  //for property enumeration
   //process this candidate conjecture
   void processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth );
@@ -396,8 +406,12 @@ private:  //information about ground equivalence classes
   Node getGroundEqc( TNode r );
   bool isGroundEqc( TNode r );
   bool isGroundTerm( TNode n );
+  //has enumerated UF
+  bool hasEnumeratedUf( Node n );
   // count of full effort checks
   unsigned d_fullEffortCount;
+  // has added lemma
+  bool d_hasAddedLemma;
   //flush the waiting conjectures
   unsigned flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth );
 public:
@@ -420,7 +434,7 @@ private:
   int optFilterScoreThreshold();
   unsigned optFullCheckFrequency();
   unsigned optFullCheckConjectures();
-  
+
   bool optStatsOnly();
 };
 
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index efe1b1098..16df9d9a9 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -169,4 +169,6 @@ option conjectureFilterCanonical --conjecture-filter-canonical bool :read-write
  filter based on canonicity
 option conjectureFilterModel --conjecture-filter-model bool :read-write :default true
  filter based on model
+option conjectureGenGtEnum --conjecture-gen-gt-enum=N int :default 0
+ number of ground terms to generate for model filtering
 endmodule