Age | Commit message (Collapse) | Author |
|
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
|
|
|
|
|
|
|
|
|
|
Uses new nested-qe utility for eliminating nested quantification before doing quantifier elimination.
Fixes CVC4/cvc4-wishues#26
Fixes #5484.
|
|
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.
|
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback