Improve stats in conjecture generator, minor cleanup.

diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index f491adc7c3f4c620757d7eff798bbe62f2127667..871d4ddc65f99dde4116168d3a82e0f87a9636fc 100755 (executable)
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -390,6 +390,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
         Trace("sg-engine") << "---Conjecture Engine Round, effort = " << e << "---" << std::endl;\r
       }\r
       eq::EqualityEngine * ee = getEqualityEngine();\r
+      d_conj_count = 0;\r
 \r
       Trace("sg-proc") << "Get eq classes..." << std::endl;\r
       d_op_arg_index.clear();\r
@@ -826,7 +827,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
           break;\r
         }\r
       }\r
-\r
+      Trace("sg-stats") << "Total conjectures considered : " << d_conj_count << std::endl;\r
       if( Trace.isOn("thm-ee") ){\r
         Trace("thm-ee") << "Universal equality engine is : " << std::endl;\r
         eq::EqClassesIterator ueqcs_i = eq::EqClassesIterator( &d_uequalityEngine );\r
@@ -865,7 +866,8 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
 unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth ) {\r
   if( !d_waiting_conjectures_lhs.empty() ){\r
     Trace("sg-proc") << "Generated " << d_waiting_conjectures_lhs.size() << " conjectures at depth " << ldepth << "/" << rdepth << "." << std::endl;\r
-    if( !optStatsOnly() && (int)addedLemmas<options::conjectureGenPerRound() ){\r
+    if( (int)addedLemmas<options::conjectureGenPerRound() ){\r
+      /*\r
       std::vector< unsigned > indices;\r
       for( unsigned i=0; i<d_waiting_conjectures_lhs.size(); i++ ){\r
         indices.push_back( i );\r
@@ -877,21 +879,22 @@ unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, in
         scs.d_scores.insert( scs.d_scores.begin(), d_waiting_conjectures_score.begin(), d_waiting_conjectures_score.end() );\r
         std::sort( indices.begin(), indices.end(), scs );\r
       }\r
-      if( doSort && d_waiting_conjectures_score[indices[0]]<optFilterScoreThreshold() ){\r
-        //do splitting on demand (TODO)\r
-\r
-      }else{\r
-        for( unsigned i=0; i<indices.size(); i++ ){\r
-          //if( d_waiting_conjectures_score[indices[i]]<optFilterScoreThreshold() ){\r
-          if( d_waiting_conjectures_score[indices[i]]>=optFilterScoreThreshold() ){\r
-            //we have determined a relevant subgoal\r
-            Node lhs = d_waiting_conjectures_lhs[indices[i]];\r
-            Node rhs = d_waiting_conjectures_rhs[indices[i]];\r
-            if( options::conjectureFilterCanonical() && ( getUniversalRepresentative( lhs )!=lhs || getUniversalRepresentative( rhs )!=rhs ) ){\r
-              //skip\r
+      //if( doSort && d_waiting_conjectures_score[indices[0]]<optFilterScoreThreshold() ){\r
+      */\r
+      unsigned prevCount = d_conj_count;\r
+      for( unsigned i=0; i<d_waiting_conjectures_lhs.size(); i++ ){\r
+        if( d_waiting_conjectures_score[i]>=optFilterScoreThreshold() ){\r
+          //we have determined a relevant subgoal\r
+          Node lhs = d_waiting_conjectures_lhs[i];\r
+          Node rhs = d_waiting_conjectures_rhs[i];\r
+          if( options::conjectureFilterCanonical() && ( getUniversalRepresentative( lhs )!=lhs || getUniversalRepresentative( rhs )!=rhs ) ){\r
+            //skip\r
+          }else{\r
+            Trace("sg-engine") << "*** Consider conjecture : " << lhs << " == " << rhs << std::endl;\r
+            Trace("sg-engine-debug") << "      score : " << d_waiting_conjectures_score[i] << std::endl;\r
+            if( optStatsOnly() ){\r
+              d_conj_count++;\r
             }else{\r
-              Trace("sg-engine") << "*** Consider conjecture : " << lhs << " == " << rhs << std::endl;\r
-              Trace("sg-engine-debug") << "      score : " << d_waiting_conjectures_score[indices[i]] << std::endl;\r
               std::vector< Node > bvs;\r
               for( std::map< TypeNode, unsigned >::iterator it = d_pattern_var_id[lhs].begin(); it != d_pattern_var_id[lhs].end(); ++it ){\r
                 for( unsigned i=0; i<=it->second; i++ ){\r
@@ -918,14 +921,13 @@ unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, in
                 break;\r
               }\r
             }\r
-          }else{\r
-            if( doSort ){\r
-              break;\r
-            }\r
           }\r
         }\r
       }\r
       Trace("sg-proc") << "...have now added " << addedLemmas << " conjecture lemmas." << std::endl;\r
+      if( optStatsOnly() ){\r
+        Trace("sg-stats") << "Generated " << (d_conj_count-prevCount) << " conjectures at depth " << ldepth << "/" << rdepth << "." << std::endl;\r
+      }\r
     }\r
     d_waiting_conjectures_lhs.clear();\r
     d_waiting_conjectures_rhs.clear();\r
@@ -1286,7 +1288,7 @@ int ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) {
         Trace("sg-cconj") << "     #witnesses for " << it->first << " : " << it->second.size() << std::endl;\r
       }\r
     }else{\r
-      score = 0;\r
+      score = 1;\r
     }\r
 \r
     Trace("sg-cconj") << "  -> SUCCESS." << std::endl;\r

diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index 59d908fec8eb94593579a4543acf4ea675b829a7..462fadfcef0cf695e567ede60cf905ebb9335847 100755 (executable)
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -342,6 +342,7 @@ private:  //information regarding the terms
   void registerPattern( Node pat, TypeNode tpat );\r
 private: //for debugging\r
   std::map< TNode, unsigned > d_em;\r
+  unsigned d_conj_count;\r
 public:\r
   //term generation environment\r
   TermGenEnv d_tge;\r