projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1fa8c5b) | patch
Move `RoundingMode` to `cvc5_types.h` (#8427)
authorAndres Noetzli <andres.noetzli@gmail.com>
Tue, 29 Mar 2022 01:13:46 +0000 (18:13 -0700)
committerGitHub <noreply@github.com>
Tue, 29 Mar 2022 01:13:46 +0000 (01:13 +0000)
commitbf2d64336c2d3cda4db39b6b528c2a3fc7e0f792
tree88c0e6290761458d52f11b038ed2c85ddbf56e0atree
parent1fa8c5bd361c1c950127779cc364fa82c25477dacommit | diff
Move `RoundingMode` to `cvc5_types.h` (#8427)

This moves RoundingMode to cvc5_types.h and switches to using the
auto-generated enum bindings. It also fixes the Java-bindings generator
for enums (certain parts were previously hardcoded for Kind) and
extends the unit tests for Solver::mkRoundingMode() to actually check
the value being created.
13 files changed:
examples/api/python/floating_point.py diff | blob | history
src/api/cpp/cvc5.cpp diff | blob | history
src/api/cpp/cvc5.h diff | blob | history
src/api/cpp/cvc5_types.h diff | blob | history
src/api/java/CMakeLists.txt diff | blob | history
src/api/java/genenums.py.in diff | blob | history
src/api/java/io/github/cvc5/api/RoundingMode.java [deleted file] blob | history
src/api/python/cvc5.pxd diff | blob | history
src/api/python/cvc5.pxi diff | blob | history
src/api/python/cvc5_python_base.pyx diff | blob | history
test/unit/api/cpp/solver_black.cpp diff | blob | history
test/unit/api/java/SolverTest.java diff | blob | history
test/unit/api/python/test_solver.py diff | blob | history