diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-27 10:32:32 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-27 10:32:32 -0600 |
| commit | 8795787c2ef337e73b46778b99f5bfa6c2a19f93 (patch) | |
| tree | 0989e95f24c2eeedd177d2281069d266b31d971d /src/preprocessing | |
| parent | a6d3c9e7fb765704f34815900712b10e85687edc (diff) | |
(proof-new) Improvements to quantifiers engine and instantiate interfaces (#5814)
This makes printing instantiations done at the SmtEngine level instead of deeply embedded within the Instantiate module. This provides much better flexibility for future uses of instantiations (e.g. how they are minimized in the new proof infrastructure).
Note this PR breaks the functionality that instantiations are minimized based on the old unsat cores infrastructure (see the disabled regression). This will be fixed once proof-new is fully merged.
Diffstat (limited to 'src/preprocessing')
0 files changed, 0 insertions, 0 deletions