From 0287acb1180db269c5dd0fe0dad8f2fa925ba0b9 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Wed, 16 Jan 2019 09:52:42 -0800 Subject: Bugfix: LFSC clause equality (#2801) * Bugfix: LFSC clause equality My implementation of clause equality had an undocumented assumption that the clauses didn't have any duplicate literals. Now that assumption is gone, and the tests suite has been expanded. * Added an empty clause test * Typo fix: Yoni Co-Authored-By: alex-ozdemir * Address Yoni's comments * Remove a duplicate clause_eq test. * Add an ordering clause_eq test. * Improve the documentation of clause_eq. --- proofs/signatures/drat.plf | 90 ++++++++++++++++++++++++++++------------ proofs/signatures/drat_test.plf | 91 +++++++++++++++++++++++++++++++++++++++++ proofs/signatures/lrat.plf | 8 ++++ 3 files changed, 162 insertions(+), 27 deletions(-) (limited to 'proofs/signatures') 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 ; -- cgit v1.2.3