This PR adds new targets, `build-cppapitests` and `cppapitests`, for
building and running the C++ API tests, and uses `build-apitests` and
`apitests` for building and running the API tests across all languages
(C++, C, Python, etc.). It also adds a new target, `pyapitests`, for
running the Python API tests, and fixes the `capitests` target to run
the correct set of C API tests. In addition, it moves all issue-related
Python API tests to their own directory, as is already done for the C++
and C API tests.
This adds `stable` as a build type, which is similar to `safe` but
permits incomplete proofs in regressions and the use of regular options
with `no-support:` fields.
This ensures that regressions pass when configuring in `safe-mode`. Note
that *all* regression testers must now take into account whether we are
in a safe-mode (safe mode itself is not a new tester).
This makes the following changes:
- `safe-mode: yes|no` is now an entry in `--show-config`
- LibPoly and Cocoa are disabled by default when configuring with
`safe-mode`. We give a warning if the user specified otherwise.
- A few regressions are updated to have the appropriate options.
- Option and logic exceptions that are "admissible" in safe mode are
updated to contain the text `"in safe mode"`.
- Various options that are used in run_regression.py are upgraded to
"common" to ensure safe-mode is compatible with the tester. Removes a
few unecessary options in run_regression.py.
- Disables a number of unit tests and examples (in the CMake) that are
not applicable in safe mode.
- Adds a CI job to test a safe-mode build.
Note that the CPC tester fails due to not guarding against some unsafe
operators in the rewriter. I will address this in a separate PR.
I increased cmake's minimum version in order to use the FindPython module, which allows the build system to specify python versions that are supported. Currently the support is extended to 3.6 through 3.10. I also removed some backward compatible conditions that do not apply anymore provided that cmake's minimum version is guaranteed to be 3.12.
MacOS builds are reenabled in ci.yml.
Organizing the PR a bit:
we hook up the subtheories to TheoryFf
we expose FF-related things via the C++/Pytohn API and SMT-LIB2 interface.
we add a bunch of tests against these interfaces.
This PR removes the expand_list_arg decorator from the python API. It was used to allow calling a function f(x, *args) with a list as second argument and automatically expand the list into *args. While it merely allows for calling f(x, l) instead of f(x, *l), it adds considerable complexity to the code and documentation. Thus, following the Zen of python (have only one way to do it) we remove this decorator. This is also consistent with the pythonic API, were we made the same decision.
Removes checkEntailed from Solver.
Removes isEntailed, isNotEntailed, isEntailedUnknown from Result.
Removes isSubsortOf, isFunctionLike, getUninterpretedSortName, getSortConstructorName from Sort.
Updates examples and unit tests.
This PR does multiple things:
- the kinds are changed from custom objects to a proper enum.Enum class
(including according changes to the cython code and the kind generation scripts)
- all examples and tests are modified to account for the change how to use kinds
(Kind instead of kinds)
- add docstrings to the kind enum values
- add a custom documenter that properly renders enums via autodoc
- extend doxygen setup so that we can write comments as rst (allowing us to copy
the documentation for kinds from the cpp api to the other apis)
