DRAT proof output

[c-cube]

[Gbury]

As far as I can tell, for the pure SAT fragment, DRAT and DRUP are the same thing, right ?

If anyone wants to try doing this, it's very easy:

• RUP output can be achieved by printing the contents of the learnt_clauses vector (in order)
• DRUP output can use the same system for forgetting clauses as the one used in the Coq backend (see the count_uses and clean functions)