New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

DRAT proof output #15

Open

c-cube opened this issue Aug 17, 2018 · 1 comment

Labels

Collaborator

c-cube commented Aug 17, 2018

No description provided.

Owner

Gbury commented Aug 23, 2018

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)

c-cube added the enhancement label

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment