Language bindings: Enable catching of exceptions (#2813)
authorAndres Noetzli <andres.noetzli@gmail.com>
Tue, 9 Jun 2020 12:44:24 +0000 (05:44 -0700)
committerGitHub <noreply@github.com>
Tue, 9 Jun 2020 12:44:24 +0000 (07:44 -0500)
commitc1f8d64f3bc73fe27527046c521c2327e8e310d8
treed308f508366a68b00eec06729a2d90a1c977b482
parent61734b41b7b96e7e7cbf46021a357d840d64b42e
Language bindings: Enable catching of exceptions (#2813)

Fixes #2810. SWIG relies on throw specifiers to determine which
exceptions a method can throw. The wrappers generated by SWIG catch
those C++ exceptions and turn them into exceptions for the target
language. However, we have removed throw specifiers because they have
been deprecated in C++11, so SWIG did not know about any of our
exceptions. This commit fixes the issue using the %catches directive,
declaring that all methods may throw a CVC4::Exception or a general
exception. Note: This means that users of the language bindings will
just receive a general CVC4::Exception instead of more specific
exceptions like TypeExceptions. Given that we are planning to have a
single exception type for the new CVC4 API, this seemed like a natural
choice.
Additionally, the commit (significantly) simplifies the mapping of C++
to Java exceptions and fixes an issue with Python exceptions not
inheriting from BaseException. Finally, the commit adds API examples
for Java and Python, which demonstrate catching exceptions, and adds
Python examples as tests in our build system.
cmake/CVC4Config.cmake.in
examples/CMakeLists.txt
examples/SimpleVC.py
examples/api/java/CMakeLists.txt
examples/api/java/Exceptions.java [new file with mode: 0644]
examples/api/python/CMakeLists.txt [new file with mode: 0644]
examples/api/python/exceptions.py [new file with mode: 0644]
src/base/exception.i
src/cvc4.i