diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2019-11-18 16:41:07 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-11-18 16:41:07 -0800 |
commit | b732c86723668bd73094fa9a2719760a91cd9981 (patch) | |
tree | e9acf5f0397884b4348822600be0ca5f3abaefa4 /proofs/signatures | |
parent | 17f0468c1656aa91d7cc5e3174a797312a9364c3 (diff) |
Signature documentation update (#3476)
This comment was slightly out-of-date.
Diffstat (limited to 'proofs/signatures')
-rw-r--r-- | proofs/signatures/drat.plf | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/proofs/signatures/drat.plf b/proofs/signatures/drat.plf index 9f1ec00a9..2f70bbfbd 100644 --- a/proofs/signatures/drat.plf +++ b/proofs/signatures/drat.plf @@ -11,7 +11,8 @@ ; Both are detailed in this paper, along with their differences: ; http://fmv.jku.at/papers/RebolaPardoBiere-POS18.pdf ; -; This signature checks **Specified DRAT**. +; This signature contains implementations for a checker for each. +; **Specified DRAT** is first. ; A DRAT proof itself: a list of addition or deletion instructions. (declare DRATProof type) @@ -23,7 +24,8 @@ ; Functional Programs ; ; ==================== ; -; Are two clauses equal (in the set sense) +; Are two clauses equal (i.e., if interpretted as sets of literals, are those +; sets equal?) ; ; Assumes that marks 1,2,3,4 are clear for the constituent variables, and ; leaves them clear afterwards. @@ -44,9 +46,11 @@ ; the mark 2 means (seen as - in c1, but not yet in c2) ; the mark 4 means (seen as - in c1) ; -; This implementation is robust to literal order, repeated literals, and -; literals of opposite polarity in the same clause. It is true equality on sets -; literals. +; This implementation **does not**: +; 1. assume that clauses do not have duplicates +; (so the clause [x v x v ~y] is an accceptable input) +; 2. assume that clauses are non-tautological +; (so the clause [x v ~x] is an acceptable input) ; ; TODO(aozdemir) This implementation could be further optimized b/c once c1 is ; drained, we need not continue to pattern match on it. |