| Age | Commit message (Collapse) | Author |
|---|
|
This PR adds documentation for the Sort python API.
|
|
Adds leftover missing unit tests for new API call for mkCardinalityConstraint from eeb78c8.
|
|
@alex-ozdemir
|
|
This adds two missing functions to the python API, along with tests for them. It also adds a missing test for the cpp API.
|
|
|
|
This PR adds documentation to the python class Op, Grammar, Result, and for API enums.
Additionally, documentation for isNull functions in the datatype classes is added for the python API, and a small change in the cpp API documentation is introduced.
|
|
|
|
This introduces a new versioning mechanism that allows for better automation.
|
|
This PR adds a couple of improvements to our documentation setup
- add an explicit dependency on the extension so that sphinx rebuilds pages appropriately when an extension is modified
- sphinx now emits warnings for examples that are not implemented in all languages (smt2, cpp, java and python)
- add -v to make the sphinx output more log-file friendly
- avoid a warning when the java bindings (and thus java docs) are not build
- replace file(WRITE by configure_file to avoid rather common erroneous rebuilds of python docs
- fix a reference to a label in the python docs
- suppress timestamps in javadoc output to avoid docs-ci being triggered for every PR
- improve placeholder message when java bindings are disabled
|
|
This PR fixes some docstrings that are not properly indented for sphinx.
|
|
This PR does a major refactoring on how we organize our builds to allow both shared and static builds. We now build the libraries using object libraries to allow building the libraries both dynamically and statically in the same build folder, though the static library is optional (ENABLE_STATIC_LIBRARY). The binary is linked either dynamically or statically (depending on ENABLE_STATIC_BINARY).
|
|
|
|
|
|
This adds the last two remaining API methods required for implementing the text output of get-model on the API side.
A followup PR will implement GetModelCommand on the API side and eliminate the (last remaining) call to getSmtEngine() from the command layer.
This PR does some minor reorganization of the model cores code to account for the new interface. It also removes a deprecated interface from TheoryModel.
|
|
While working on API documentation for python, I noticed that isNull is not wrapped
by the python API. It is also not tested in the cpp API tests. This PR fixes both issues,
and also updates the python api tests accordingly.
|
|
|
|
This removes support for creating bit-vectors from a string without a
size argument. We further also now require that the base argument is
always given (it has no default value).
|
|
This PR removes explicit ownership of the options object from the main function and replaces it by an api::Solver object. To achieve this, it does a number of minor changes:
- api::Solver not takes a unique_ptr<Options> in its constructor
- CommandExecutor only holds a reference to (a unique ptr of) the api::Solver
- the main functions accesses options via the solver
|
|
This PR makes several fixes to the wheel building infrastructure for manylinux2014.
don't statically link to Python (see: this section of PEP-513)
use standard 'build' directory. I noticed that the wheel infrastructure uses directory 'build' to prepare the wheel anyway, so it doesn't make a lot of sense for us to use a separate working directory. I tried changing the name of the build directory in setuptools by setting member variables in initialize_options but that didn't seem to work and I decided it wasn't worth the effort. The wheel should be built in a clean environment anyway, i.e., docker.
find the correct include directory and python library paths for building on manylinux2014 using skbuild. manylinux2014 has several versions of python installed in /opt/python. The CMake infrastructure can't find the necessary information (plus the libraries are deleted from the docker image to save space -- the library is just set to a generic libpython<version>.a). Instead, this PR would manually set them via CMake options.
to allow setting the python information, I extended the configure.sh script to allow directly setting CMake options. There are definitely other options here if you'd rather not change configure.sh. My reasoning was that it could be useful in other situations and I just marked it as an advanced feature. Another approach would be to use skbuild directly in the CMake infrastructure. I didn't like that solution because it would make the CMakeLists.txt more complicated and it wouldn't follow the standard CMake/Cython/Python approach which means we won't benefit from future improvements to that CMake infrastructure. Plus, this issue should only come up on systems with non-standard installations of Python, such as manylinux. This approach (setting CMake options) is basically what scikit-build does automatically if we had used that infrastructure directly.
|
|
This PR adds a script for building a wheel distribution for pycvc5. It automatically reads the top-level CMakeLists.txt to obtain the current version number, and then runs the standard setup from setuptools with an extension command class that configures and builds cvc5 with Python bindings. This wheel file is sufficient for uploading to Pypi. Although, note that we need to build for different operating systems and different Python versions because of the extension modules.
Note: another option is to use the scikit-build instead of doing the configuring and building manually. However, I ran into some issues when the setup.py file was not at the top-level. Because we prefer to have it hidden in a sub-folder, I took the manual route for now. In the future, we could consider changing this.
|
|
Unit tests are translated from https://github.com/cvc5/cvc5/blob/master/test/unit/api/op_black.cpp
to python.
The only thing that is not faithfully translated is that the `cpp` tests expect the template function `[getIndices](https://github.com/cvc5/cvc5/blob/master/src/api/cpp/cvc5.h#L841)` to fail when an inappropriate type is given to it, while in the [`python` API](https://github.com/cvc5/cvc5/blob/90d19f7cdbaf41e389bdcbd099471f658a35ce98/src/api/python/cvc5.pxi#L343) this function is not a template, but just tries every supported type.
For example, the following line is not translated:
https://github.com/cvc5/cvc5/blob/90d19f7cdbaf41e389bdcbd099471f658a35ce98/test/unit/api/op_black.cpp#L206
|
|
This PR translates the cpp API unit tests about results to python.
The original cpp file is: https://github.com/cvc5/cvc5/blob/master/test/unit/api/result_black.cpp
The translation made rise to one addition to the python API:
The UnknownExplanation object from the cpp API was represented by a string in the python API.
Now we have a more faithful representation, as an enum.
|
|
This commit (follow #6553) adds more functions and unit tests for python API.
Subsequent PR will include additional missing functions and unit tests.
1. Adding getNullSort() and mkEmptyBag() functions.
2. Allowing mkOp() with a list of arguments (previously allowed at most 2).
3. Allowing mkString() with additional boolean argument useEscSequences.
4. Corresponding changes to the tests.
|
|
|
|
Our documentation for `toPythonObj` says that real values are represented as Fractions. However, getRealValue yields a float approximation thereof.
We should probably stick to Fractions, since they allow us to precisely capture values in LRA. Also, that's more aligned with the C++ API, which returns a string representation of the (unapproximated) Rational.
Also, document some (potential) weirdness with calling mkReal on floating-point values.
|
|
This commit adds unit tests that are translated from `datatype_api_black.cpp`. One API function is also added to the python API.
This is the last part of the python api unit tests for datatypes.
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
|
|
This PR adds missing API functions from the cpp Term API to the python API.
Corresponding tests are translated from term_black.cpp.
|
|
This commit makes the following additions, in order to sync the python API with the cpp API.
1. adding `getName` functions to datatypes related classes
2. allowing `mkDatatypeSorts` with 1 or 2 arguments (previously allowed only 2).
3. In case there is a second argument to `mkDatatypeSorts`, we make sure it is a set.
4. Corresponding changes to the tests.
|
|
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.
|
|
Following #6496 , this PR adds new getters to the python API, as well as tests for them. This makes toPythonObj simpler.
A future PR will add more getters to the python API.
Co-authored-by: Gereon Kremer nafur42@gmail.com
|
|
This PR fixes an issue in the python API for datatypes, and also introduces tests translated from https://github.com/cvc5/cvc5/blob/master/test/unit/api/datatype_api_black.cpp
The next PR will translate more tests and will also introduce missing functions in the python API for datatypes.
|
|
This PR removes copied CMake files for the pycvc5 Cython target, and instead adds a dependency on scikit-build (where those CMake files originated anyway). This keeps us up to date with fixes. Furthermore, the PR switches from distutils to the more modern setuptools. This does add another dependency but it's a fairly reasonable one. setuptools is not part of the base Python distribution, but my understanding is that it is now the de facto standard, and most package managers install it automatically with Python. The main motivation for switching is in preparation for building wheels.
This PR is a piece of this old one (#5657) which I am closing and splitting up.
|
|
The function printSynthSolution declared here is going to be removed in #6521.
This PR removes it from the python API.
Following #6530, this PR also replaces its usages in the examples by a utility function.
For this, we also add support for getSynthSolutions in the python API.
|
|
This PR does some minor improvements to the API:
- remove getConstSequenceElements(), use getSequenceValue() instead
- improve documentation for Term
|
|
This PR adds more getter functions for api::Term to retrieve values from constant terms (and terms that the average API use might consider constant).
It also introduces std::wstring as regular representation for string constants instead of std::vector<uint32> for the SMT-LIB parser and the String class.
|
|
This PR adds some functions that are missing in the python API, along with unit tests for them.
The unit tests are translated from https://github.com/cvc5/cvc5/blob/master/test/unit/api/term_black.cpp
|
|
|
|
This PR adds some functions that are missing in the python API, along with unit tests for them.
Subsequent PR will include additional missing functions.
Also includes a yapf run to reformat the test file.
Co-authored-by: Makai Mann makaim@stanford.edu
|
|
This removes the special case of TUPLE_UPDATE and RECORD_UPDATE in favor of the more general datatype update.
Datatype update is handled analogously to APPLY_SELECTOR / APPLY_TESTER.
|
|
|
|
This PR makes generating the python part of our API documentation more reliable. If python bindings are enabled, it makes the docs target depend on pycvc5 and renders a warning into the documentation if python bindings are disabled.
To make the dependency on pycvc5 work properly, it changes the python bindings build so that the library is directly put in the right place and avoid the manual rename, so that the pycvc5 target actually points to the correct file.
Unfortunately, this means we need to build libcvc5 when building docs with python bindings enabled.
|
|
This PR adds the basic setup for including the python API in our sphinx documentation and shows how it works using the Datatype class as an example. In detail
- it enables sphinx.ext.autodoc and makes sure the generated pycvc5 is in the search path
- adds a index page for the python API
- adds a page for the Datatype class
- adds docstrings for the Datatype class
- does some finetuning (remove source locations, but adds signature information)
|
|
This PR replaces all api::*HashFunction objects by specializations of std::hash. std::hash is meant to be extended in this way, and it allows for a much cleaner usage of std::unordered_set and std::unordered_map with these types.
|
|
This commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
|
|
This adds the command declare-pool to the public API. It also adds parsing support for this feature, lifts the internal kinds to public kinds, adds an example regression, and a unit test for the new declare-pool solver method.
|
|
This PR does the following:
1. removes old python sort API test
2. creates a new python sort API test, obtained by translating the (entire) cpp unit test https://github.com/CVC4/CVC4/blob/master/test/unit/api/sort_black.cpp
3. adds support for bags and datatype selectors/testers domain/codomain in the python API.
|
|
This renames everything but GitHub links and build system related
macros. Switching the build system to cvc5 will be the last step in the
renaming process.
|
|
|
|
|
|
Only regenerate files if dependencies changed. This avoids unnecessary
rebuilds of the Cython code.
|
