diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2019-12-06 07:51:54 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-12-06 07:51:54 -0800 |
| commit | 499aa5641e2b830f60159c2ce1c791bf4d45aac1 (patch) | |
| tree | 600ada9e557b8c22f15c37440b109bd5470c95f1 /src/expr/node_manager.cpp | |
| parent | 008d6b51baec353f45324e1d9407d898866cf688 (diff) | |
[proof] Eliminate side-condition from ER signature (#3230)
* [proof] Eliminate the side condition in er.plf
By tweaking the axioms a bit, I got rid of the lone SC in the Extended
Resolution signature.
* [proof] Changed er_proof.cpp in line with signature
The new signature requires slightly different proof printing.
* [proof] clang-format er_proof.cpp
* Fix tests
* [proof] Actually delete the SC
* Apply suggestions from code review
Co-Authored-By: yoni206 <yoni206@users.noreply.github.com>
* Add LFSC-checking unit test for ER proof
* Gate the lfsc invocation on the build system
* Properly gate the lfsc check on the build system
* gate the plf_signatures forward def on the build system
Diffstat (limited to 'src/expr/node_manager.cpp')
0 files changed, 0 insertions, 0 deletions