diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2019-01-16 09:52:42 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-01-16 09:52:42 -0800 |
commit | 0287acb1180db269c5dd0fe0dad8f2fa925ba0b9 (patch) | |
tree | 767ed45ac5f3df764384d4287406ca9ba1537c29 /proofs/signatures/drat_test.plf | |
parent | 1e6293daa3f6d61c9035e22ee76448b46dd83ce8 (diff) |
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.
Diffstat (limited to 'proofs/signatures/drat_test.plf')
-rw-r--r-- | proofs/signatures/drat_test.plf | 91 |
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 |