diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2018-12-16 17:49:34 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-12-16 17:49:34 -0800 |
commit | bc40c176eb1205452e824ec9d89dc9a7c76cbd67 (patch) | |
tree | f2d9cc364da89e0a3b76a94054a35d3efdacaa47 /src/proof/bitvector_proof.cpp | |
parent | f5b05e8cc794fa5cad43f5827b84cca4c702dde2 (diff) |
DRAT Signature (#2757)
* DRAT signature
Added the DRAT signature to CVC4.
We'll need this in order to compare three BV proof pipelines:
1. DRAT -> Resolution -> Check
2. DRAT -> LRAT -> Check
3. DRAT -> Check (this one!)
Tested the signature using the attached test file. i.e. running
```
lfscc sat.plf smt.plf lrat.plf drat.plf drat_test.plf
```
* Added type annotations for tests
* Respond to Yoni's review
* Apply Yoni's suggestions from code review
Documentation polish
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Whoops, missed a spot or two
Diffstat (limited to 'src/proof/bitvector_proof.cpp')
0 files changed, 0 insertions, 0 deletions