From 3ff5a32a45f2830acc4600b38332a287db4cf60a Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 28 Oct 2014 12:54:33 +0100
Subject: [PATCH] Improve stats in conjecture generator, minor cleanup.

---
 .../quantifiers/conjecture_generator.cpp      | 44 ++++++++++---------
 src/theory/quantifiers/conjecture_generator.h |  1 +
 2 files changed, 24 insertions(+), 21 deletions(-)

diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index f491adc7c..871d4ddc6 100755
--- 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;
       }
       eq::EqualityEngine * ee = getEqualityEngine();
+      d_conj_count = 0;
 
       Trace("sg-proc") << "Get eq classes..." << std::endl;
       d_op_arg_index.clear();
@@ -826,7 +827,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
           break;
         }
       }
-
+      Trace("sg-stats") << "Total conjectures considered : " << d_conj_count << std::endl;
       if( Trace.isOn("thm-ee") ){
         Trace("thm-ee") << "Universal equality engine is : " << std::endl;
         eq::EqClassesIterator ueqcs_i = eq::EqClassesIterator( &d_uequalityEngine );
@@ -865,7 +866,8 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
 unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth ) {
   if( !d_waiting_conjectures_lhs.empty() ){
     Trace("sg-proc") << "Generated " << d_waiting_conjectures_lhs.size() << " conjectures at depth " << ldepth << "/" << rdepth << "." << std::endl;
-    if( !optStatsOnly() && (int)addedLemmas<options::conjectureGenPerRound() ){
+    if( (int)addedLemmas<options::conjectureGenPerRound() ){
+      /*
       std::vector< unsigned > indices;
       for( unsigned i=0; i<d_waiting_conjectures_lhs.size(); i++ ){
         indices.push_back( i );
@@ -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() );
         std::sort( indices.begin(), indices.end(), scs );
       }
-      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() ){
-          if( d_waiting_conjectures_score[indices[i]]>=optFilterScoreThreshold() ){
-            //we have determined a relevant subgoal
-            Node lhs = d_waiting_conjectures_lhs[indices[i]];
-            Node rhs = d_waiting_conjectures_rhs[indices[i]];
-            if( options::conjectureFilterCanonical() && ( getUniversalRepresentative( lhs )!=lhs || getUniversalRepresentative( rhs )!=rhs ) ){
-              //skip
+      //if( doSort && d_waiting_conjectures_score[indices[0]]<optFilterScoreThreshold() ){
+      */
+      unsigned prevCount = d_conj_count;
+      for( unsigned i=0; i<d_waiting_conjectures_lhs.size(); i++ ){
+        if( d_waiting_conjectures_score[i]>=optFilterScoreThreshold() ){
+          //we have determined a relevant subgoal
+          Node lhs = d_waiting_conjectures_lhs[i];
+          Node rhs = d_waiting_conjectures_rhs[i];
+          if( options::conjectureFilterCanonical() && ( getUniversalRepresentative( lhs )!=lhs || getUniversalRepresentative( rhs )!=rhs ) ){
+            //skip
+          }else{
+            Trace("sg-engine") << "*** Consider conjecture : " << lhs << " == " << rhs << std::endl;
+            Trace("sg-engine-debug") << "      score : " << d_waiting_conjectures_score[i] << std::endl;
+            if( optStatsOnly() ){
+              d_conj_count++;
             }else{
-              Trace("sg-engine") << "*** Consider conjecture : " << lhs << " == " << rhs << std::endl;
-              Trace("sg-engine-debug") << "      score : " << d_waiting_conjectures_score[indices[i]] << std::endl;
               std::vector< Node > bvs;
               for( std::map< TypeNode, unsigned >::iterator it = d_pattern_var_id[lhs].begin(); it != d_pattern_var_id[lhs].end(); ++it ){
                 for( unsigned i=0; i<=it->second; i++ ){
@@ -918,14 +921,13 @@ unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, in
                 break;
               }
             }
-          }else{
-            if( doSort ){
-              break;
-            }
           }
         }
       }
       Trace("sg-proc") << "...have now added " << addedLemmas << " conjecture lemmas." << std::endl;
+      if( optStatsOnly() ){
+        Trace("sg-stats") << "Generated " << (d_conj_count-prevCount) << " conjectures at depth " << ldepth << "/" << rdepth << "." << std::endl;
+      }
     }
     d_waiting_conjectures_lhs.clear();
     d_waiting_conjectures_rhs.clear();
@@ -1286,7 +1288,7 @@ int ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) {
         Trace("sg-cconj") << "     #witnesses for " << it->first << " : " << it->second.size() << std::endl;
       }
     }else{
-      score = 0;
+      score = 1;
     }
 
     Trace("sg-cconj") << "  -> SUCCESS." << std::endl;
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index 59d908fec..462fadfce 100755
--- 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 );
 private: //for debugging
   std::map< TNode, unsigned > d_em;
+  unsigned d_conj_count;
 public:
   //term generation environment
   TermGenEnv d_tge;
-- 
2.30.2