Extended DRAT signature to operational DRAT (#2815)
authorAlex Ozdemir <aozdemir@hmc.edu>
Thu, 24 Jan 2019 19:45:12 +0000 (11:45 -0800)
committerGitHub <noreply@github.com>
Thu, 24 Jan 2019 19:45:12 +0000 (11:45 -0800)
commit467ef8692009f440bda74083d476131ff1e88b51
treeef5aea2eed34b283a34f09cdd7f5a9707387498f
parent495787793b07a05f384824c92eef4e26d92228fc
Extended DRAT signature to operational DRAT (#2815)

* Extended DRAT signature to operational DRAT

The DRAT signature now supports both operational and specified DRAT.
That is, either kind of proof will be accepted.

The goal of this implementation of operational DRAT was to re-use as
much of the specified DRAT machinery as possible. However, by writing a
separate operational signature, we could make it much more efficient
(after all, operational DRAT came about because of a push for efficient
cheking).

You can run the new AND old DRAT tests by running

```
lfscc sat.plf smt.plf lrat.plf drat.plf drat_test.plf
```

* Apply suggestions from code review (Yoni)

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
proofs/signatures/drat.plf
proofs/signatures/drat_test.plf