From 583ee11728875fc7b1a848c57cd2da92bb906b4a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick-github@luehne.de>
Date: Fri, 26 Jan 2018 17:23:54 +0100
Subject: [PATCH] Add detailed statistics in YAML format

---
 main.c | 63 +++++++++++++++++++++++++++++++++++++++++-----------------
 1 file changed, 45 insertions(+), 18 deletions(-)

diff --git a/main.c b/main.c
index 4d58d9a..0950af1 100644
--- a/main.c
+++ b/main.c
@@ -73,22 +73,10 @@ void givememorystatistics() {
     unsigned text;//       text (code)
     unsigned lib;//        library
     unsigned data;//       data/stack
-    int MB;
 
     fscanf(pf, "%u %u %u %u %u %u", &size, &resident, &share, &text, &lib, &data);
 
-    MB = ((double)size)/256.0;
-
-    printf("total size %.3f %s\n",
-	   /*
-	   resident size: %u\n
-	   shared pages : %u\n
-	   text (code)  : %u\n
-	   library      : %u\n
-	   data/stack   : %u\n",
-	   */
-	   (MB < 700.0) ? MB : MB / 1024.0,
-	   (MB < 700.0) ? "MB" : "GB");
+    printf("memoryConsumption:\n  total: %.1f # [MB]\n", ((double)size)/256.0);
   }
   fclose(pf);
 }
@@ -727,24 +715,63 @@ int main(int argc,char **argv) {
 
   encoding();
 
-  printf("total time %.2f preprocess %.2f \n",
+  printf("\n\n# statistics in YAML format\n---\n");
+
+  printf("runtime:\n  total: %.2f # [s]\n  preprocessing: %.2f # [s]\n",
 	 time2real(time10ms() - TIMEstart),
 	 time2real(TIMEpreprocess - TIMEstart));
 
   givememorystatistics();
 
-  printf("max. learned clause length %i\n",stats_longest_learned);
+  printf("maxLearnedClauseLength: %i\n",stats_longest_learned);
+
+  int solutionIndex = -1;
+
+  for (int i = 0; seqs[i].sati; i++)
+  {
+    if (seqs[i].sati->value != 1)
+      continue;
+
+    solutionIndex = i;
+    break;
+  }
+
+  const auto planLength = seqs[solutionIndex].sati->nOfTPoints - 1;
+
+  int numberOfActions = 0;
+
+  const satinstance sati = seqs[solutionIndex].sati;
+
+  for (int t = 0; t < sati->nOfTPoints - 1; t++)
+    for (int i = 0; i < sati->nOfActions; i++)
+      if (vartruep(sati,TACT(i,t)))
+        numberOfActions++;
+
+  printf("plan:\n  length: %i\n  actions: %i\n", planLength, numberOfActions);
 
   if(flagOutputDIMACS == 0) {
-    printf("t val conflicts decisions variables\n");
+    printf("iterations:\n");
     i = 0;
     do {
-      printf("%i %i %i %i %i\n",seqs[i].sati->nOfTPoints-1,seqs[i].sati->value,seqs[i].sati->conflicts,seqs[i].sati->decisions,seqs[i].sati->nOfVars);
+      printf("  - horizon: %i\n",seqs[i].sati->nOfTPoints-1);
+      printf("    result: ");
+      if (seqs[i].sati->value == 0)
+        printf("unsatisfiable");
+      else if (seqs[i].sati->value == 1)
+        printf("satisfiable");
+      else
+        printf("unknown");
+      printf("\n");
+      printf("    conflicts: %i\n",seqs[i].sati->conflicts);
+      printf("    decisions: %i\n",seqs[i].sati->decisions);
+      printf("    variables: %i\n",seqs[i].sati->nOfVars);
       i += 1;
-    } while(i*outputTimeStep+firstTimePoint <= lastTimePoint && seqs[i].sati && seqs[i-1].sati->value != 1);
+    } while(i*outputTimeStep+firstTimePoint <= lastTimePoint && seqs[i].sati);// && seqs[i-1].sati->value != 1);
       //    } while(i*outputTimeStep+firstTimePoint < lastTimePoint);
   }
 
+  printf("...\n");
+
  }
 
 #ifdef SHOWMALLOCSTATS