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, 8 insertions, 0 deletions

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 ;