projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5652f1b) | patch
FP: Refactor, rewrite and clean up word blasting. (#6802)
authorAina Niemetz <aina.niemetz@gmail.com>
Tue, 29 Jun 2021 16:18:55 +0000 (09:18 -0700)
committerGitHub <noreply@github.com>
Tue, 29 Jun 2021 16:18:55 +0000 (16:18 +0000)
commit877b75447b27da04d81ff3ee91eaad7bf00ea083
tree6acd62dc49475dfdb949f25a0a54b8a6e6f1244ftree
parent5652f1bcb3702ff60ebe3248a6e027a3138d5c99commit | 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.
src/theory/fp/fp_converter.cpp diff | blob | history