diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-09 16:36:25 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-09 16:36:25 -0500 |
| commit | 2a518941922855626c015a73572a5a9a5a2d0ed7 (patch) | |
| tree | fda12a6d12ebb8e8896fa2301543013f0d1e09c7 /.github | |
| parent | c118e34b040eddffe0e2155645b47c811188c82a (diff) | |
(proof-new) Refactor skolemization (#4586)
This PR refactors skolemization in SkolemManager so that we use a "curried" form, where witnesses for a variable x is based on the existential where the prefix up to x has already been skolemized.
This additionally adds more utility functions that will be used in the internal proof checker for quantifiers.
Diffstat (limited to '.github')
0 files changed, 0 insertions, 0 deletions