diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-19 12:27:40 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-19 12:27:40 -0600 |
| commit | f172b30bfe18a24416fd61f4aa5ce3dea583296e (patch) | |
| tree | 3c27f17b24e6095ce7ad4b5ec3f50e407412d378 /src/parser/memory_mapped_input_buffer.cpp | |
| parent | 3654512dd8b341c5725e550d438b23508493b991 (diff) | |
Add nested quantifier elimination module (#5422)
This has static utilities for doing nested quantifier elimination and some data structures for maintaining a context-dependent set of quantified formulas that have been processed.
This is work towards CVC4/cvc4-wishues#26, and work reimplementation of the option --ceqgi-nested-qe.
Diffstat (limited to 'src/parser/memory_mapped_input_buffer.cpp')
0 files changed, 0 insertions, 0 deletions