Destructive update for weak head reduction

cvc5 / LFSC

LFSC Proof Checker

Other

11 stars 9 forks source link

Destructive update for weak head reduction #83

Closed ajreynol closed 2 years ago

ajreynol commented 2 years ago

Work in progress, testing CI.

ajreynol commented 2 years ago

I tried two candidate ways of making us fast on this PR (one based on destructive updating within whr() and another based on lazily applying whr()). Both solutions run into fundamental issues that I was not able to resolve.