report=1 only by default

Author: arminbiere

VERSION

@@ -1 +1 @@
-06k
+06l

options.h

@@ -76,6 +76,7 @@ OPTION (bool,     random_order,          0, 0, 1,     "initial random decision o
 OPTION (unsigned, reduce_interval,       1e3, 1, INF, "reduce base conflict interval") \
 OPTION (bool,     rephase,               1, 0, 1,     "reset saved phases regularly") \
 OPTION (unsigned, rephase_interval,      1e3, 1, INF, "base rephase conflict interval") \
+OPTION (unsigned, report,                1, 0, INF,   "report details for many threads") \
 OPTION (bool,     share_learned,         1, 0, 1,     "export and import learned clauses") \
 OPTION (bool,     shrink,                1, 0, 1,     "shrink (glue 1) learned clauses") \
 OPTION (bool,     simplify,              1, 0, 1,     "elimination, subsumption and substitution") \

report.c

@@ -20,6 +20,9 @@ verbose_report (struct ring *ring, char type, int level)
   if (verbosity < level)
     return;
 
+  if (ring->options.report < ring->id)
+    return;
+
   struct ring_statistics *s = &ring->statistics;
   struct averages *a = ring->averages + ring->stable;
 

vivify.c

@@ -314,20 +314,8 @@ vivify_deduce (struct vivifier * vivifier,
   assert (EMPTY (*ring_clause));
   if (implied != INVALID)
     {
-#if 0
-      struct watch * reason = VAR (implied)->reason;
-      if (is_binary_pointer (reason))
-	assert (lit_pointer (reason) == implied);
-#endif
       for (all_watches (watch, REFERENCES (implied)))
 	{
-#if 0
-	  if (watch == reason)
-	    {
-	      reason = 0;
-	      continue;
-	    }
-#endif
 	  if (is_binary_pointer (watch))
 	    {
 	      assert (lit_pointer (watch) == implied);