projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: fb45de5) | patch
Change behaviour of Term::getRealValue() (#7316)
authorGereon Kremer <nafur42@gmail.com>
Thu, 7 Oct 2021 00:37:08 +0000 (17:37 -0700)
committerGitHub <noreply@github.com>
Thu, 7 Oct 2021 00:37:08 +0000 (17:37 -0700)
commit2f78ed85a8263d7ad632e679034e662091511670
treef5ca91d2ef95ce89e26578eaad36c75a20cf40e9tree
parentfb45de5d7385a1ba9e40237a745720f54d67db92commit | diff
Change behaviour of Term::getRealValue() (#7316)

This PR modifies the API function Term::getRealValue() to always return a fraction. Beforehand, it would return rationals in fractional notation (15/2) and integers in decimal notation (2.0).
src/api/cpp/cvc5.cpp diff | blob | history
src/api/cpp/cvc5.h diff | blob | history
test/unit/api/term_black.cpp diff | blob | history