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

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

diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index eb7f4b2aa2041e081d4ddbc4c6b94cd88756de94..23e2b88ba10da68b4e38c856a4121791aa624f4e 100755 (executable)
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -129,7 +129,7 @@ public:
   Node getTerm();\r
   //debug print\r
   void debugPrint( const char * c, const char * cd );\r
-  \r
+\r
   //conjecture generation\r
   ConjectureGenerator * d_cg;\r
   //the current number of enumerated variables per type\r
@@ -149,14 +149,14 @@ public:
   std::map< unsigned, TermGenerator > d_tg_alloc;\r
   unsigned d_tg_gdepth;\r
   int d_tg_gdepth_limit;\r
-  \r
+\r
   //all functions\r
   std::vector< TNode > d_funcs;\r
   //function to kind map\r
   std::map< TNode, Kind > d_func_kind;\r
   //type of each argument of the function\r
   std::map< TNode, std::vector< TypeNode > > d_func_args;\r
-  \r
+\r
   //access functions\r
   unsigned getNumTgVars( TypeNode tn );\r
   bool allowVar( TypeNode tn );\r
@@ -364,6 +364,16 @@ private:
   std::vector< TypeEnumerator > d_typ_enum;\r
   //get nth term for type\r
   Node getEnumerateTerm( TypeNode tn, unsigned index );\r
+  //predicate for type\r
+  std::map< TypeNode, Node > d_typ_pred;\r
+  //get predicate for type\r
+  Node getPredicateForType( TypeNode tn );\r
+  //\r
+  void getEnumerateUfTerm( Node n, unsigned num, std::vector< Node >& terms );\r
+  //\r
+  void getEnumeratePredUfTerm( Node n, unsigned num, std::vector< Node >& terms );\r
+  // uf operators enumerated\r
+  std::map< Node, bool > d_uf_enum;\r
 public:  //for property enumeration\r
   //process this candidate conjecture\r
   void processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth );\r
@@ -396,8 +406,12 @@ private:  //information about ground equivalence classes
   Node getGroundEqc( TNode r );\r
   bool isGroundEqc( TNode r );\r
   bool isGroundTerm( TNode n );\r
+  //has enumerated UF\r
+  bool hasEnumeratedUf( Node n );\r
   // count of full effort checks\r
   unsigned d_fullEffortCount;\r
+  // has added lemma\r
+  bool d_hasAddedLemma;\r
   //flush the waiting conjectures\r
   unsigned flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth );\r
 public:\r
@@ -420,7 +434,7 @@ private:
   int optFilterScoreThreshold();\r
   unsigned optFullCheckFrequency();\r
   unsigned optFullCheckConjectures();\r
-  \r
+\r
   bool optStatsOnly();\r
 };\r
 \r

diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index efe1b109834d656b58653fb79e988dfcbbc4a327..16df9d9a9d5ba0d4d31f16a6c32bede86dfc4e39 100644 (file)
--- 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