diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-01 13:35:07 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-11-01 13:35:07 -0500 |
| commit | 13e452be03bef09e2f54f42e2bc42383505ffcea (patch) | |
| tree | 39695fe22d387bc84bc49d20831a19648d55011f /src/theory/rep_set.cpp | |
| parent | be11fae39055f213586058ec9129d1276f724b0e (diff) | |
CBQI BV choice expressions (#1296)
* Use Hilbert choice expressions for cbqi bv. Failing in debug due to TNode issues currently.
* Minor
* Make unique bound variables for choice functions in BvInstantor, clean up.
* Incorporate missing optimizations
* Clang format
* Unused field.
* Minor
* Fix, add regression.
* Fix regression.
* Fix bug that led to incorrect cleanup of instantiations.
* Add missing regression
* Improve handling of choice rewriting.
* Fix
* Clang format
* Use canonical variables for choice functions in cbqi bv.
* Add regression
* Clang format.
* Address review.
* Clang format
Diffstat (limited to 'src/theory/rep_set.cpp')
0 files changed, 0 insertions, 0 deletions