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 <aozdemir@hmc.edu>
* Address Yoni's comments

* Remove a duplicate clause_eq test.
* Add an ordering clause_eq test.
* Improve the documentation of clause_eq.

diff --git a/proofs/signatures/drat.plf b/proofs/signatures/drat.plf
index b529ff893bd2f7dda48dd216288e3e67d1a4fbd0..d777a143a40022ba83f4c3b5753f906e1c7f32e2 100644 (file)
--- 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 f2f2c7286a638552c919ece6c0a184c1439c55a0..57de391112540068fee5aa14afd0225fa0efc7a4 100644 (file)
--- 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 ae6cbd1014a6b9ae8e2f0187a8308485ff59b7ab..ea1d905371b5bb43135a462abf760982fa86b304 100644 (file)
--- 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 ;