projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 147fd72) | patch
[LRAT] signature robust against duplicate literals (#2743)
authorAlex Ozdemir <aozdemir@hmc.edu>
Wed, 12 Dec 2018 01:19:07 +0000 (17:19 -0800)
committerGitHub <noreply@github.com>
Wed, 12 Dec 2018 01:19:07 +0000 (17:19 -0800)
commit3687e098f4b6a969d265641e413ab05117bf53a7
tree96068c500f13c30490210c405be76da5cccdf8bdtree
parent147fd723e6c13eb3dd44a43073be03a64ea3fe66commit | diff
[LRAT] signature robust against duplicate literals (#2743)

* [LRAT] signature robust against duplicate literals

The LRAT signature previously had complex, surprising, and occasionally
incorrect behavior when given clauses with duplicate literals.

Now it does not. Now clauses have true set semantics, and clauses with
duplicate literals are treated identically to those without.

* Test with logically = but structurally != clauses.
proofs/signatures/lrat.plf diff | blob | history
proofs/signatures/lrat_test.plf diff | blob | history