projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c118e34) | patch
(proof-new) Refactor skolemization (#4586)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 9 Jun 2020 21:36:25 +0000 (16:36 -0500)
committerGitHub <noreply@github.com>
Tue, 9 Jun 2020 21:36:25 +0000 (16:36 -0500)
commit2a518941922855626c015a73572a5a9a5a2d0ed7
treefda12a6d12ebb8e8896fa2301543013f0d1e09c7tree
parentc118e34b040eddffe0e2155645b47c811188c82acommit | 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.
src/expr/skolem_manager.cpp diff | blob | history
src/expr/skolem_manager.h diff | blob | history