LRAT proof stats on stdout

[marijnheule]

When using concurrent solving and checking, the proof is not available. However, I would like to know the size of the LRAT proof: number of clause additions, number of clause deletions, and proof size in bytes. Would it be possible to add this information to stdout together with the other stats after solving a problem?

[arminbiere]

Thanks, good point. We will add it in the next realease.

[arminbiere]

Actually while working on that I realized that this functionality is actually already there. In the 'closing proof' section right after the report lines (with 'c 0 ...' in case of unsatisfiability). You find that information.

% ./build/cadical test/cnf/prime4294967297.cnf /tmp/proof |sed -e '1,/closing proof/d'|head -4
c 
c traced 59235 added and 61650 deleted clauses
c closing file '/tmp/proof'
c after writing 1893787 bytes 1.8 MB

and for LRAT

% ./build/cadical test/cnf/prime4294967297.cnf /tmp/proof --lrat|sed -e '1,/closing proof/d'|head -4
c 
c traced 59235 added and 61650 deleted clauses
c closing file '/tmp/proof'
c after writing 16884655 bytes 16.1 MB

[marijnheule]

Thanks. I missed this.

Marijn