| Age | Commit message (Collapse) | Author |
|---|
|
|
|
DEFAULT_HEADER in src/api/parsekinds.py is essentially unused since both genkinds.py scripts pass the kinds header to the script. The current value of DEFAULT_HEADER does not work for the scripts since the working directory for genkinds.py is in src/api/{java,python}.
|
|
Fixes #6260.
Signed-off-by: Nicolaas <nweidema@usc.edu>
|
|
This PR migrates CLN to a new Find script and adds the possibility to install CLN if not found in the system.
Also, it does a bit of cleanup.
|
|
|
|
|
|
In current master, the following fails whenever <name> contains a /:
./configure.sh --python-bindings --name=<name>
The reason is that src/api/python/genkinds.py adds a directory to the python path while relying on the fact that the build directory is located directly under the main repo directory, which is not the case if <name> contains a /.
This PR fixes this by having cmake determine the right directory to add to the python path.
|
|
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.
|
|
The build system (cmake) will automatically generate an export header
cvc4_export.h, which makes sure that the correct export features are
defined depending on the compiler and target platform. The macro CVC4_EXPORT
replaces CVC4_PUBLIC and its usage is reduced by 2/3.
Co-authored-by: Gereon Kremer <nafur42@gmail.com>
|
|
|
|
|
|
printModel no longer makes sense if the list of declared symbols is managed outside the solver.
Also, mkConst needs a variant to distinguish a provided name of "" vs. a name that is not provided.
|
|
This adds proper support for the (declare-heap (T U)) command, which declares the type of the heap in separation logic. This command is part of the standard for separation logic.
This previous was handled in an ad-hoc way where the type of the heap would be inferred on demand. This was a poor solution and has led to a number of issues related to when the heap is inferred.
Fixes #5343, fixes #4926.
Work towards CVC4/cvc4-wishues#22.
|
|
This PR removes mkSingleton from the API after removing subtyping from set theory and introducing mkInteger to the API.
Instead the user needs to use Solver::mkTerm(api::SINGLETON, element) where element has the right type.
Internally NodeManager::mkSingleton(type, element) is still needed to determine the type of the set.
Other changes:
Renamed Solver::mkTerm(Op op, .. functions to Solver::mkTermFromOp(Op op, ...
Added mkTermFromOp to the python API
|
|
This PR adds mkInteger to the API and update mkReal to ensure that the returned term has real sort.
The parsers are modified to parse numbers like "0" "5" as integers and "0.0" and "15.0" as reals.
This means subtyping is effectively eliminated from all theories except arithmetic.
Other changes:
Term::isValue is removed which was introduced to support parsing for constant arrays. It is no longer needed after this PR.
Benchmarks are updated to match the changes in the parsers
Co-authored-by: Andrew Reynolds andrew-reynolds@uiowa.edu
|
|
This PR removes Solver::getAssignment command from the API as there is no way to assign names to terms in the API. It also removes ExpandDefinitionsCommand, an internal functionality in CVC4.
|
|
|
|
This PR removes subtyping for sets theory due to issues like #4502, #4507 and #4631.
Changes:
Add SingletonOp for singletons to specify the type of the single element in the set.
Add mkSingleton to the solver to enable the user to pass the sort of the single element.
Update smt and cvc parsers to use mkSingleton when the kind is SINGLETON
|
|
Fixes #5024. This commit adds a conversion from constant string terms to
native Python Unicode strings in Term.toPythonObj() and improves
Solver.mkString() to accept strings containing characters outside of
the printable range.
|
|
This PR addresses issue https://github.com/CVC4/CVC4/issues/5014. It simply interprets the SMT-LIB string representation and produces a Python object. It currently supports booleans, ints, reals, bit-vectors, and arrays. The method (`toPythonObj`) is only valid to call if `isConst` returns true.
|
|
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.
|
|
Fixes #4942. The Python API was missing some methods related to
datatypes. Most importantly, it was missing mkDatatypeSorts, which
meant that datatypes with unresolved placeholders could not be resolved.
This commit adds missing methods and ports the corresponding tests of
datatype_api_black.h to Python. The commit also adds support for
__getitem__ in Term.
|
|
When testing the API examples, Python examples were not included. This
commit changes that and fixes multiple minor issues that came up once
the tests were enabled:
- It adds `Solver::supportsFloatingPoint()` as an API method that
returns whether CVC4 is configured to support floating-point numbers
or not (this is useful for failing gracefully when floating-point
support is not available, e.g. in the case of our floating-point
example).
- It updates the `expections.py` example to use the new API.
- It fixes the `sygus-fun.py` example. The example was passing a _set_
of non-terminals to `Solver::mkSygusGrammar()` but the order in which
the non-terminals are passed in matters because the first non-terminal
is considered to be the starting terminal. The commit also updates the
documentation of that function.
- It fixes the Python API for datatypes. The `__getitem__` function had
a typo and the `datatypes.py` example was crashing as a result.
|
|
|
|
This commit extends the Python API with support for SyGuS functionality.
This required the addition of a nullary constructor for `Grammar` in the C++ API.
A unit test is also included, and is a translation of the corresponding C++ API unit test.
Examples are not added yet, but are ready and planned for a next PR (in order to keep this one shorter).
|
|
Commit 9678f58a7fedab4fc061761c58382f4023686108 added front end support
for sequences. This commit extends that support to the Python API. It
also adds simple C++ and Python examples that demonstrate how the API
works for sequences.
|
|
This commit ports over the sort_black tests to the pytest infrastructure to test the Python bindings. It also adds missing functionality that was revealed during the testing.
|
|
This commit extends the API to support the retrieval of heap/nil term
when separation logic is used and changes the corresponding system test
accordingly. This commit is in preparation of making the constructor of
`ExprManager` private.
|
|
I noticed recently that getKind for Op and Term was not correct in the python bindings. This PR would add maps to keep track of the Kind objects and the Python names (which are different from the C++ Kind names). Then a Python `kind` only needs the integer representation of a `Kind` to be constructed. Now, in `getKind` it can just pass the integer representation when constructing a `kind`.
|
|
Fixes #4552. Fixes #4555. The SMT-LIB standard mandates that definitions
are kept when `:global-declarations` are enabled. Until now, CVC4 was
keeping track of the symbols of a definition correctly but lost the body
of the definition when the user context was popped. This commit fixes
the issue by adding a `global` parameter to
`SmtEngine::defineFunction()` and `SmtEngine::defineFunctionRec()`. If
that parameter is set, the definitions of functions are added at level 0
to `d_definedFunctions` and the lemmas for recursive function
definitions are kept in an additional list and asserted during each
`checkSat` call. The commit also updates new API, the commands, and the
parsers to reflect this change.
|
|
|
|
This PR would change the Python API to wrap the C++ Result class instead of translating it to a pure Python class. This is more convenient because there are several possibilities other than sat/unsat/unknown. Furthermore, this PR updates the bitvectors.py example which had an incorrect function name "checkEntailment" and adds a floating point example contributed by Eva Darulova.
|
|
This is the first batch of API guards, mainly extending existing guards
in the Solver object with checks that Ops, Terms, Sorts, and datatype objects
are associated to this solver object.
This further changes how DatatypeConstructorDecl objects are created. Previously,
they were not created via the Solver object (while DatatypeDecl was). Now, they are
created via Solver::mkDatatypeConstructorDecl, consistent with how DatatypeDecl
objects are created.
|
|
|
|
|
|
|
|
This renames api::Solver::checkValidAssuming to checkEntailed and
removes api::Solver::checkValid. Internally, SmtEngine::query is renamed
to SmtEngine::checkEntailed, and these changes are further propagated to
the Result class.
|
|
Supporting SMT-LIB's (reset) command on the API level is dangerous and not required -- it's sufficient to just destroy the solver object and create a new one if necessary. It's dangerous because invalidated objects can be passed in after a reset, and we would need to find a clean way to guard against this. We want to guard against this in the future, but for now it is cleaner to make it explicit (by not having this functionality in the API but forcing the user to destroy and recreate the solver object) that these objects can't be reused.
|
|
Removes DatatypeSelectorDecl and DatatypeDeclSelfSort. Add selectors is now inlined. A special case is added for the "self selector", instead of using a class as a dummy argument.
I updated the Python files, although would be helpful to double check this is correct.
Co-authored-by: makaimann <makaim@stanford.edu>
|
|
* Remove getIndices for Kinds
* Test importing pycvc4
* Distutils install for pycvc4
* Use full path for cvc4kinds prefix
* Remove zip_safe option (not needed for distutils)
* Automatically clean up setup.py intermediate files
* Rely on make install to install pycvc4
* Run make install when testing python bindings
* Fix: Check importing pycvc4 when python bindings are built
* Remove one -Wshadow warning for cython-generated files
* Put the fake kinds submodule in generated __init__.py
* Remove unnecessary file permission options in python CMakeLists
* Respect install prefix unless in a virtualenv
* Handle python2 print function
* Use VIRTUAL_ENV environment variable to check if in python virtualenv
* Add header and documentation to setup.py.in
* Capitalize CVC4 in PyCVC4Install
* Update src/api/python/CMakeLists.txt
Co-Authored-By: Mathias Preiner <mathias.preiner@gmail.com>
* Simplify CMakeLists for setup.py configuration
* Shorten virtualenv check with Mathias's suggestion
* Set TRAVIS_CVC4_PYTHON_BINDINGS to no in other builds
* minor: bash syntax fix
* Move pycvc4 import check to makeInstallCheck
* Include installed pycvc4 location on PYTHONPATH
* Better way to set PYTHONPATH
Co-authored-by: Mathias Preiner <mathias.preiner@gmail.com>
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
|
|
|
