Better stats printing for oracle

Fixing

Author: msoos

src/oracle/oracle.cpp

@@ -23,6 +23,7 @@
 #include "oracle.h"
 #include "constants.h"
 
+#include <cstdint>
 #include <iostream>
 #include "utils.h"
 using std::cout;
@@ -109,15 +110,26 @@ void Oracle::ClearSolCache() {
 
 bool Oracle::SatByCache(const vector<Lit>& assumps) {
     const uint32_t mult = vars+1;
+    if (stats.total_cache_lookups % 1000 == 199 && verb >= 3) {
+        cout << "c o [oracle] cache"
+            << " usefulness: "
+            << std::setprecision(0) << std::fixed << (double)stats.cache_useful/(double)stats.total_cache_lookups*100.0 << "%"
+            << std::setprecision(2)
+            << " elements in cache: " << sol_cache.size()/mult
+            << " cache size distrib for lookup: " << cache_lookup[0].size() << " -- " << cache_lookup[1].size()
+            << endl;
+    }
+
+    stats.total_cache_lookups++;
     assert(sol_cache.size()%mult == 0);
 
     if (cache_lookup_frequencies.empty()) {
         cache_lookup_frequencies.resize(vars+1, 0);
     }
-    assert(cache_lookup_frequencies.size() == vars+1);
+    assert(cache_lookup_frequencies.size() == (uint32_t)vars+1);
 
     for (const Lit& l : assumps) cache_lookup_frequencies[VarOf(l)]++;
-    if ((stats.sat_by_cache_calls % 1000 == 999)) {
+    if ((stats.total_cache_lookups % 1000 == 999)) {
         vector<uint32_t> occs_int(mult, 0);
         const uint64_t sz = sol_cache.size();
         for (uint64_t i = 0; i < sz; i+=mult) {
@@ -179,14 +191,7 @@ bool Oracle::SatByCache(const vector<Lit>& assumps) {
             if (ok) return true;
         }
     }
-    stats.sat_by_cache_calls++;
     stats.mems += checks/20;
-    if (stats.sat_by_cache_calls % 100 == 99 && verb >= 3) {
-        cout << "c o [oracle]-cache found: " << found << " cache var: " << cache_lookup_var
-            << "orig sz: " << sol_cache.size()/mult
-            << " cache size: " << cache_lookup[0].size() << " -- " << cache_lookup[1].size()
-            << endl;
-    }
 
     // Not in the cache
     return false;

src/oracle/oracle.h

@@ -79,7 +79,7 @@ struct Stats {
     int64_t restarts = 0;
     int64_t cache_useful = 0;
     int64_t cache_added = 0;
-    int64_t sat_by_cache_calls = 0;
+    int64_t total_cache_lookups = 0;
     void Print() const;
 };
 

src/oracle_use.cpp

@@ -34,6 +34,7 @@ THE SOFTWARE.
 #include "time_mem.h"
 #include "varreplacer.h"
 #include "distillerbin.h"
+#include <iomanip>
 
 using namespace CMSat;
 
@@ -276,9 +277,9 @@ bool Solver::oracle_vivif(int fast, bool& backbone_found) {
             << " T-remain: " << stats_line_percent(tot_bin_mems-oracle_bin_mems_used, tot_bin_mems) << "%"
             << " T: " << std::setprecision(2) << (end_bin_tme - start_bin_time));
 
-    verb_print(1, "[oracle-vivif-bin]"
-            << " cache-used: " << oracle.getStats().cache_useful
-            << " cache-added: " << oracle.getStats().cache_added
+    verb_print(1, "[oracle-vivif] cache usefulness: "
+            << std::setprecision(0) << std::fixed << (double)oracle.getStats().cache_useful/(double)oracle.getStats().total_cache_lookups*100.0 << "%"
+            << std::setprecision(2)
             << " total T: " << std::setprecision(2) << (cpuTime() - start_vivif_time));
     return solver->okay();
 }
@@ -597,14 +598,20 @@ bool Solver::oracle_sparsify(bool fast)
 
     //cout << "New cls size: " << clauses.size() << endl;
     //Subsume();
+    //
+    auto safe_div = [](uint32_t a, uint32_t b) {
+        if (b == 0) return 0.0;
+        return (double)a/(double)b*100.0;
+    };
 
     verb_print(1, "[oracle-sparsify] removed: " << removed
         << " of which bin: " << removed_bin
         << " tot considered: " << tot_cls
         << " ccnr useful: " << ccnr_useful
         << " oracle uknown: " << unknown
-        << " cache-used: " << oracle.getStats().cache_useful
-        << " cache-added: " << oracle.getStats().cache_added
+        << " cache useful: " << std::setprecision(0) << std::fixed
+        << safe_div(oracle.getStats().cache_useful, oracle.getStats().total_cache_lookups)*100.0 << "%"
+        << std::setprecision(2)
         << " learnt-units: " << oracle.getStats().learned_units
         << " T: " << (cpuTime()-my_time) << " buildT: " << build_time);