Interleaved trace output

StephanGocht / VeriPB

Verifier for pseudo-Boolean proofs

MIT License

12 stars 1 forks source link

Closed StephanGocht closed 4 years ago

StephanGocht commented 5 years ago

When outputting the trace it might be useful to also print the applied rule (and maybe comments). For example:

* b!=1 (x3), no active decisions
p 0 5 + 7 + 15 + 17 + 37 + 41 + 1 d 0
* ===> 45 (rule 3): +1~x3 >= 1

StephanGocht commented 4 years ago

done.