| Age | Commit message (Collapse) | Author |
|---|
|
PR changes:
Refactor python/genkinds.py by separating parsing from file generation.
Add java/genkinds.py to generate file Kind.java.
Enable java API in ./configure.sh with "under development" warning.
|
|
|
|
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
|
|
strings (#4702)
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
|
|
This commit makes the ExprManager constructor private and updates the
initialization of subsolvers, unit tests, and system tests accordingly.
This is a step towards making options part of SmtEngine instead of
NodeManager.
|
|
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.
|
|
|
|
|
|
Adds option --ninja to configure.sh.
|
|
|
|
example/translator expects an input file to translate but none was provided in the ctest call.
This caused the ctest call to hang and wait for input on stdin in some configurations (in
particular in the nightlies).
|
|
|
|
Required for consistent naming of tests, unit test names now also use
the test naming scheme <category>/<subdir>/<test name>, e.g.,
unit/theory/theory_bv_white.
|
|
|
|
|
|
|
|
|
|
|
|
|
