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
+#VERSION = -DMPDOWNLOAD
-EXECUTABLE=Mp
+#EXECUTABLE=Mp
 # Uncomment for Madagascar C with the planning heuristic as default (MpC)
-#VERSION = -DCMPDOWNLOAD
+VERSION = -DCMPDOWNLOAD
-#EXECUTABLE=MpC
+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 ID %i decisions %i conflicts %i variables)\n",sati->id,sati->decisions,sati->conflicts,sati->nOfVars);
+  printf("SAT (%i decisions %i conflicts)\n",sati->decisions,sati->conflicts);
 #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
 
-int truep(fma *f) {
+inline int truep(fma *f) {
   fmalist *fs;
   switch(f->t) {
   case natom: return (onelits[f->a] != 1);

main.c

@@ -35,14 +35,6 @@
 #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];
 
@@ -81,10 +73,22 @@ 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);
 
-    printf("memoryConsumption:\n  total: %.1f # [MB]\n", ((double)size)/256.0);
+    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");
   }
   fclose(pf);
 }
@@ -207,96 +211,7 @@ 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;
@@ -737,9 +652,6 @@ 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) {
@@ -776,9 +688,6 @@ 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();
@@ -811,7 +720,6 @@ 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);
   }
   
@@ -819,7 +727,23 @@ int main(int argc,char **argv) {
 
   encoding();
 
-  printStatistics();
+  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);
+  }
 
  }