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.

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 ;