diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/signatures/drat.plf | 90 | ||||
| -rw-r--r-- | proofs/signatures/drat_test.plf | 91 | ||||
| -rw-r--r-- | proofs/signatures/lrat.plf | 8 |
3 files changed, 162 insertions, 27 deletions
diff --git a/proofs/signatures/drat.plf b/proofs/signatures/drat.plf index b529ff893..d777a143a 100644 --- a/proofs/signatures/drat.plf +++ b/proofs/signatures/drat.plf @@ -25,14 +25,29 @@ ; Are two clauses equal (in the set sense) ; -; Since clauses are sets, it is insufficient to do list equality +; Assumes that marks 1,2,3,4 are clear for the constituent variables, and +; leaves them clear afterwards. +; +; Since clauses are sets, it is insufficient to do list equality. ; We could sort them, but that would require defining an order on our variables, ; and incurring the cost of sorting. +; +; ; Instead, we do the following: -; 1. Sweep the first clause, marking variables with flags 1 (pos) and 2 (neg) -; 2. Sweep the second clause, erasing marks. -; 3. Unsweep the first clause, returning FALSE on marks. -; Also unmarking +; 1. Sweep the first clause, marking variables with flags 1,3 (pos) and 2,4 (neg) +; 2. Sweep the second clause, erasing marks 1,2. Returning FALSE if no mark 3,4. +; 3. Unsweep the first clause, returning FALSE on marks 1,2. +; Also unmarking 3,4, and 1,2 if needed +; +; So the mark 1 means (seen as + in c1, but not yet in c2) +; the mark 3 means (seen as + in c1) +; 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. +; ; TODO(aozdemir) This implementation could be further optimized b/c once c1 is ; drained, we need not continue to pattern match on it. (program clause_eq ((c1 clause) (c2 clause)) bool @@ -43,30 +58,51 @@ (cln tt) ((clc c2h c2t) (match c2h - ((pos v) (ifmarked1 - v - (do (markvar1 v) (clause_eq c1 c2t)) - ff)) - ((neg v) (ifmarked2 - v - (do (markvar2 v) (clause_eq c1 c2t)) - ff)))))) + ((pos v) + (ifmarked1 + v + (do (markvar1 v) + (clause_eq c1 c2t)) + (ifmarked3 + v + (clause_eq c1 c2t) + ff))) + ((neg v) + (ifmarked2 + v + (do (markvar2 v) + (clause_eq c1 c2t)) + (ifmarked4 + v + (clause_eq c1 c2t) + ff))))))) ((clc c1h c1t) (match c1h - ((pos v) (do - (markvar1 v) - (let res (clause_eq c1t c2) - (ifmarked1 - v - (do (markvar1 v) ff) - res)))) - ((neg v) (do - (markvar2 v) - (let res (clause_eq c1t c2) - (ifmarked2 - v - (do (markvar2 v) ff) - res)))))))) + ((pos v) + (ifmarked3 + v + (clause_eq c1t c2) + (do (markvar3 v) + (do (markvar1 v) + (let res (clause_eq c1t c2) + (do (markvar3 v) + (ifmarked1 + v + (do (markvar1 v) ff) + res))))))) + ((neg v) + (ifmarked4 + v + (clause_eq c1t c2) + (do (markvar4 v) + (do (markvar2 v) + (let res (clause_eq c1t c2) + (do (markvar4 v) + (ifmarked2 + v + (do (markvar2 v) ff) + res))))))))))) + ; Does this formula contain bottom as one of its clauses? (program cnf_has_bottom ((cs cnf)) bool diff --git a/proofs/signatures/drat_test.plf b/proofs/signatures/drat_test.plf index f2f2c7286..57de39111 100644 --- a/proofs/signatures/drat_test.plf +++ b/proofs/signatures/drat_test.plf @@ -1,4 +1,95 @@ ;depends on drat.plf +(declare TestSuccess type) + +; Test for clause_eq +(declare test_clause_eq + (! a clause + (! b clause + (! result bool + (! (^ + (bool_and + (bool_eq (clause_eq a b) result) + (bool_and + (bool_eq (clause_eq b a) result) + (bool_and + (bool_eq (clause_eq a a) tt) + (bool_eq (clause_eq b b) tt)))) + tt) + TestSuccess))))) + +(check + (% a var + (% b var + (@ c1 (clc (pos a) (clc (neg b) cln)) + (@ c2 (clc (pos a) (clc (neg b) cln)) + (: TestSuccess + (test_clause_eq c1 c2 tt))))))) + +(check + (% a var + (% b var + (@ c1 (clc (neg a) (clc (neg b) cln)) + (@ c2 (clc (pos a) (clc (neg b) cln)) + (: TestSuccess + (test_clause_eq c1 c2 ff))))))) + +(check + (% a var + (% b var + (@ c1 (clc (pos a) (clc (pos b) cln)) + (@ c2 (clc (pos a) (clc (neg b) cln)) + (: TestSuccess + (test_clause_eq c1 c2 ff))))))) + +(check + (% a var + (% b var + (@ c1 (clc (pos a) (clc (pos a) cln)) + (@ c2 (clc (pos a) (clc (neg b) cln)) + (: TestSuccess + (test_clause_eq c1 c2 ff))))))) + +(check + (% a var + (% b var + (@ c1 (clc (neg b) (clc (pos a) (clc (neg a) cln))) + (@ c1 (clc (neg a) (clc (neg b) (clc (pos a) cln))) + (: TestSuccess + (test_clause_eq c1 c2 ff))))))) + + +(check + (% a var + (% b var + (@ c1 (clc (pos a) (clc (pos a) (clc (neg b) cln))) + (@ c2 (clc (pos a) (clc (neg b) cln)) + (: TestSuccess + (test_clause_eq c1 c2 tt))))))) + +(check + (% a var + (% b var + (@ c1 (clc (pos a) (clc (pos a) (clc (neg b) cln))) + (@ c2 (clc (pos a) (clc (neg b) (clc (neg b) cln))) + (: TestSuccess + (test_clause_eq c1 c2 tt))))))) + +(check + (% a var + (% b var + (@ c1 (clc (pos a) (clc (pos a) (clc (neg a) cln))) + (@ c2 (clc (pos a) (clc (neg a) (clc (neg a) cln))) + (: TestSuccess + (test_clause_eq c1 c2 tt))))))) + +(check + (% a var + (% b var + (@ c1 cln + (@ c2 (clc (pos a) (clc (neg a) (clc (neg a) cln))) + (: TestSuccess + (test_clause_eq c1 c2 ff))))))) + (declare check_rat (! f cnf (! c clause diff --git a/proofs/signatures/lrat.plf b/proofs/signatures/lrat.plf index ae6cbd101..ea1d90537 100644 --- a/proofs/signatures/lrat.plf +++ b/proofs/signatures/lrat.plf @@ -18,6 +18,14 @@ (program bool_or ((l bool) (r bool)) bool (match l (ff r) (tt tt))) (program bool_and ((l bool) (r bool)) bool (match l (tt r) (ff ff))) (program bool_not ((b bool)) bool (match b (tt ff) (ff tt))) +(program bool_eq ((l bool) (r bool)) bool + (match l + (tt (match r + (tt tt) + (ff ff))) + (ff (match r + (tt ff) + (ff tt))))) ; =================== ; ; Working CNF formula ; |