Add signal handler for SIGTERM

As the benchmark runner doesn’t send a SIGINT but a SIGTERM, the signal
handler printing the statistics wasn’t triggered.

Makefile

@@ -1,17 +1,17 @@
 # 2012 (C) Jussi Rintanen, jrintanen.jr@gmail.com
 
 # Uncomment for Madagascar with the planning heuristic as default (Mp)
-#VERSION = -DMPDOWNLOAD
-#EXECUTABLE=Mp
+VERSION = -DMPDOWNLOAD
+EXECUTABLE=Mp
 # Uncomment for Madagascar C with the planning heuristic as default (MpC)
-VERSION = -DCMPDOWNLOAD
-EXECUTABLE=MpC
+#VERSION = -DCMPDOWNLOAD
+#EXECUTABLE=MpC
 # Uncomment for Madagascar with VSIDS as default (M)
 #VERSION = -DVSIDS
 #EXECUTABLE=M
 #ARCH=-m32
 
-INSTRUMENT = #-g -ggdb -pg
+INSTRUMENT = -g -ggdb -pg
 
 CONFIGURATION= -DLBD -DREPRTHREE -DWEIGHTS #-DFUIP #-DMULTICORE #-DSPREAD -DCOSTS -DCFMA  -DCP3
 

clausesets.c

@@ -1524,7 +1524,7 @@ int solve0(satinstance sati,int conflictstogo,int restart) {
   sati->value = 0;
   return 0;
  SAT:
-  printf("SAT (%i decisions %i conflicts)\n",sati->decisions,sati->conflicts);
+  printf("SAT (%i ID %i decisions %i conflicts %i variables)\n",sati->id,sati->decisions,sati->conflicts,sati->nOfVars);
 #ifdef COSTS
   printf("FINAL COST %i.\n",sati->currentcost);
   sati->costbound = sati->currentcost;

invariants.c

@@ -304,7 +304,7 @@ inline int ctruep(cfma f) {
 }
 #endif
 
-inline int truep(fma *f) {
+int truep(fma *f) {
   fmalist *fs;
   switch(f->t) {
   case natom: return (onelits[f->a] != 1);

main.c

@@ -35,6 +35,14 @@
 #include <omp.h>
 #endif
 
+int numberOfGroundActionsAfterParsing = -1;
+int numberOfStateVariablesAfterParsing = -1;
+
+int numberOfGroundActionsAfterSimplification = -1;
+int numberOfStateVariablesAfterSimplification = -1;
+
+int maxSizeOfStronglyConnectedComponents = -1;
+
 char state_for_random[256];
 char dump_for_random[256];
 
@@ -73,22 +81,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);
 }
@@ -211,7 +207,96 @@ void processheuristic(char *decls) {
 
 }
 
+void printStatistics()
+{
+  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));
+
+  printf("maxLearnedClauseLength: %i\n",stats_longest_learned);
+
+  if (numberOfGroundActionsAfterParsing > -1)
+    printf("groundActions:\n  afterParsing: %i\n",numberOfGroundActionsAfterParsing);
+  if (numberOfGroundActionsAfterSimplification > -1)
+    printf("  afterPreprocessing: %i\n",numberOfGroundActionsAfterSimplification);
+  if (numberOfStateVariablesAfterParsing > -1)
+    printf("stateVariables:\n  afterParsing: %i\n",numberOfStateVariablesAfterParsing);
+  if (numberOfStateVariablesAfterSimplification > -1)
+    printf("  afterPreprocessing: %i\n",numberOfStateVariablesAfterSimplification);
+
+  if (maxSizeOfStronglyConnectedComponents > -1)
+    printf("stronglyConnectedComponents:\n  maxSize: %i\n",maxSizeOfStronglyConnectedComponents);
+
+  int solutionIndex = -1;
+
+  for (int i = 0; seqs[i].sati; i++)
+  {
+    if (seqs[i].sati->value != 1)
+      continue;
+
+    solutionIndex = i;
+    break;
+  }
+
+  printf("plan:\n  found: ");
+
+  if (solutionIndex < 0)
+    printf("false\n");
+  else
+  {
+    printf("true\n");
+
+    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("  length: %i\n  actions: %i\n", planLength, numberOfActions);
+  }
+
+  if(flagOutputDIMACS == 0) {
+    if (seqs[0].sati)
+      printf("iterations:\n");
+    int i = 0;
+    while(i*outputTimeStep+firstTimePoint < lastTimePoint && seqs[i].sati) {
+      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;
+    }// && seqs[i-1].sati->value != 1);
+      //    } while(i*outputTimeStep+firstTimePoint < lastTimePoint);
+  }
+
+  printf("...\n");
+}
+
+void handleSignal()
+{
+  printStatistics();
+  exit(0);
+}
+
 int main(int argc,char **argv) {
+  signal(SIGINT, handleSignal);
+  signal(SIGTERM, handleSignal);
+
   int i,j;
 
   syntacticclass sclass;
@@ -652,6 +737,9 @@ int main(int argc,char **argv) {
 
    NEWgroundoperators();
   
+   numberOfGroundActionsAfterParsing = nOfActions;
+   numberOfStateVariablesAfterParsing = nOfAtoms;
+
    printf("Parser: %i ground actions and %i state variables\n",nOfActions,nOfAtoms);
 
    if(flagShowInput) {
@@ -688,6 +776,9 @@ int main(int argc,char **argv) {
 
   if(flagEliminateConverses) mergecontras();
 
+  numberOfGroundActionsAfterSimplification = nOfActions;
+  numberOfStateVariablesAfterSimplification = nOfAtoms;
+
   printf("Simplified: %i ground actions and %i state variables\n",nOfActions,nOfAtoms);
 
   sortactions();
@@ -720,6 +811,7 @@ int main(int argc,char **argv) {
     int maxsize;
     TIMEdisabling = time10ms();
     maxsize = scc(nOfActions);
+    maxSizeOfStronglyConnectedComponents = maxsize;
     printf(" %.2f secs (max SCC size %i)\n",time2real(time10ms() - TIMEdisabling),maxsize);
   }
   
@@ -727,23 +819,7 @@ int main(int argc,char **argv) {
 
   encoding();
 
-  printf("total time %.2f preprocess %.2f \n",
-	 time2real(time10ms() - TIMEstart),
-	 time2real(TIMEpreprocess - TIMEstart));
-
-  givememorystatistics();
-
-  printf("max. learned clause length %i\n",stats_longest_learned);
-
-  if(flagOutputDIMACS == 0) {
-    printf("t val conflicts decisions\n");
-    i = 0;
-    do {
-      printf("%i %i %i %i\n",seqs[i].sati->nOfTPoints-1,seqs[i].sati->value,seqs[i].sati->conflicts,seqs[i].sati->decisions);
-      i += 1;
-    } while(i*outputTimeStep+firstTimePoint <= lastTimePoint && seqs[i].sati && seqs[i-1].sati->value != 1);
-      //    } while(i*outputTimeStep+firstTimePoint < lastTimePoint);
-  }
+  printStatistics();
 
  }