diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2018-12-11 11:46:38 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-12-11 11:46:38 -0800 |
| commit | 1c114dc487d94d72ebf3453611c42b28777d6482 (patch) | |
| tree | a1d925be3874d86c8442566db4bc6e8b0e02fa9d /proofs/signatures/sat.plf | |
| parent | e1dc39321cd4ab29b436025badfb05714f5649b3 (diff) | |
LRAT signature (#2731)
* LRAT signature
Added an LRAT signature. It is almost entirely side-conditions, but it
works.
There is also a collection of tests for it. You can run them by invoking
```
lfscc smt.plf sat.plf lrat.plf lrat_test.plf
```
* Update proofs/signatures/lrat.plf per Yoni's suggestion.
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Responding to Yoni's comments.
* Removed unused varaibles
Some tests declared `var`s which were unused.
Now they don't.
Diffstat (limited to 'proofs/signatures/sat.plf')
| -rw-r--r-- | proofs/signatures/sat.plf | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/proofs/signatures/sat.plf b/proofs/signatures/sat.plf index b95caa8fd..8f40aa8bf 100644 --- a/proofs/signatures/sat.plf +++ b/proofs/signatures/sat.plf @@ -19,8 +19,8 @@ ; code to check resolutions -(program append ((c1 clause) (c2 clause)) clause - (match c1 (cln c2) ((clc l c1') (clc l (append c1' c2))))) +(program clause_append ((c1 clause) (c2 clause)) clause + (match c1 (cln c2) ((clc l c1') (clc l (clause_append c1' c2))))) ; we use marks as follows: ; -- mark 1 to record if we are supposed to remove a positive occurrence of the variable. @@ -49,7 +49,7 @@ (match m (tt (do (ifmarked4 v v (markvar4 v)) c')) (ff (do (ifmarked4 v (markvar4 v) v) (markvar2 v) (clc l c'))))))))) - ((concat_cl c1 c2) (append (simplify_clause c1) (simplify_clause c2))) + ((concat_cl c1 c2) (clause_append (simplify_clause c1) (simplify_clause c2))) ((clr l c1) (match l ; set mark 1 to indicate we should remove v, and fail if |