projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ccfe07f) | patch
Change output of getRealValue to a fraction. (#6692)
authorAlex Ozdemir <aozdemir@hmc.edu>
Tue, 8 Jun 2021 06:42:59 +0000 (23:42 -0700)
committerGitHub <noreply@github.com>
Tue, 8 Jun 2021 06:42:59 +0000 (06:42 +0000)
commitd265cc611581c1d5da16283008d4fcb95eab74dd
treeef2d2b48afa3a4dca1986739e1cbcaf43bfe1a75tree
parentccfe07f8daba372d2d88b249aa27fe78ad22ed54commit | diff
Change output of getRealValue to a fraction. (#6692)

Our documentation for `toPythonObj` says that real values are represented as Fractions. However, getRealValue yields a float approximation thereof.

We should probably stick to Fractions, since they allow us to precisely capture values in LRA. Also, that's more aligned with the C++ API, which returns a string representation of the (unapproximated) Rational.

Also, document some (potential) weirdness with calling mkReal on floating-point values.
src/api/python/cvc5.pxi diff | blob | history
test/python/unit/api/test_term.py diff | blob | history
test/python/unit/api/test_to_python_obj.py diff | blob | history