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.

1 files changed, 91 insertions, 0 deletions

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