Browse Source

Print more statistics

master
Patrick Lühne 4 years ago
parent
commit
46bdb212de
No known key found for this signature in database GPG Key ID: 5F3611E97A70ABF
  1. 2
      clausesets.c
  2. 4
      main.c

2
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;

4
main.c

@ -736,10 +736,10 @@ int main(int argc,char **argv) {
printf("max. learned clause length %i\n",stats_longest_learned);
if(flagOutputDIMACS == 0) {
printf("t val conflicts decisions\n");
printf("t val conflicts decisions variables\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);
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);
i += 1;
} while(i*outputTimeStep+firstTimePoint <= lastTimePoint && seqs[i].sati && seqs[i-1].sati->value != 1);
// } while(i*outputTimeStep+firstTimePoint < lastTimePoint);

Loading…
Cancel
Save