patrick
/
madagascar
1
0
Fork 0
Code Issues Pull Requests Releases Activity

Add detailed statistics in YAML format

This commit is contained in:
Patrick Lühne 2018-01-26 17:23:54 +01:00
parent 46bdb212de
commit 583ee11728
No known key found for this signature in database
GPG Key ID: 05F3611E97A70ABF
1 changed files with 45 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

63
main.c
View File

@ -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