projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d80303a) | patch
FP value support in python API (#6644)
authoryoni206 <yoni206@users.noreply.github.com>
Tue, 1 Jun 2021 09:40:54 +0000 (02:40 -0700)
committerGitHub <noreply@github.com>
Tue, 1 Jun 2021 09:40:54 +0000 (11:40 +0200)
commite7dccb880f08e14004501c827cd1c199a936cb64
treedb4f6494eb458e254a9db3e23d17769a7b34aa0dtree
parentd80303ab28c0e14e41feaf16123f9fe5e50be0eccommit | diff
FP value support in python API (#6644)

This PR adds new is* functions from the cpp API to the python API.
In particular, it adds getFloatingPointValue() function from the cpp API.
A test (translated from term_black.cpp) is added.

getFloatingPointValue() returns a tuple, and so this requires importing an instance of tuples into cython.
src/api/python/cvc5.pxd diff | blob | history
src/api/python/cvc5.pxi diff | blob | history
test/python/unit/api/test_term.py diff | blob | history