diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-06-29 09:18:55 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-29 16:18:55 +0000 |
| commit | 877b75447b27da04d81ff3ee91eaad7bf00ea083 (patch) | |
| tree | 6acd62dc49475dfdb949f25a0a54b8a6e6f1244f /src/theory/arith/nl/cad/cdcac.h | |
| parent | 5652f1bcb3702ff60ebe3248a6e027a3138d5c99 (diff) | |
FP: Refactor, rewrite and clean up word blasting. (#6802)
This rewrites the word blasting function FpConverter::convert to be
easier to follow and read. It further cleans up several things.
This additionally prepares for allowing to convert incoming facts rather
than terms registered with theory FP. That is, when word blasting more
lazily, in preNotifyFact rather than in registerTerm.
Diffstat (limited to 'src/theory/arith/nl/cad/cdcac.h')
0 files changed, 0 insertions, 0 deletions