diff options
| author | Ying Sheng <sqy1415@gmail.com> | 2019-12-16 11:42:36 -0800 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-16 11:42:36 -0800 |
| commit | 49f0f09c6ef1c04fcd5b088456cea9998cff3c91 (patch) | |
| tree | 0d5746c90c1e7ca3e336a8cfc7417b05c0eecbe8 /src/theory/theory_model.cpp | |
| parent | c101a6b42d1f14bc750fb2328ddd83261148d7ae (diff) | |
Support ackermannization on uninterpreted sorts in BV (#3372)
Support ackermannization on uninterpreted sorts in BV. For uninterpreted sorts, we create a bit-vector sort to replace it. For an uninterpreted sort `S`, if the number of variables within sort `S` is `n`, the replacing bit-vector will have size (log n)+1.
Diffstat (limited to 'src/theory/theory_model.cpp')
0 files changed, 0 insertions, 0 deletions