diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2019-01-24 11:45:12 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-01-24 11:45:12 -0800 |
| commit | 467ef8692009f440bda74083d476131ff1e88b51 (patch) | |
| tree | ef5aea2eed34b283a34f09cdd7f5a9707387498f /test/unit | |
| parent | 495787793b07a05f384824c92eef4e26d92228fc (diff) | |
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>
Diffstat (limited to 'test/unit')
0 files changed, 0 insertions, 0 deletions