Age | Commit message (Collapse) | Author |
|
This PR enables CI for java tests by adding --java-bindings to ci.yml.
It also replaces the unreliable finalize method and instead uses AutoCloseable and explicit close method to clean up dynamic memory allocated by java native interface.
The PR fixes compile errors for SolverTest.java and runtime errors for Solver.defineFun.
|
|
This PR is step towards enabling -o raw-benchmark for regressions. It creates a define-fun command for each named term. This allows us to reparse dumped benchmarks containing named terms, but we still lose track of those terms and do not print them in response to (get-assignment) and (get-unsat-core) commands. This PR also simplifies the interface for DefineFunCommand interface and removes support for (define ...) command.
|
|
This PR refactors java package name from cvc5 to io.github.cvc5.api.
It also refactor the names of cpp and java files.
|
|
This PR adds a binary/SMT-LIBv2 quickstart example, based on the cpp quickstart example.
|
|
This PR removes the conversion of rationals to double in favour of properly handling them as rationals (as pairs of integers) in the C++ quickstart example.
|
|
For some reason, we didn't have any SMT-LIB (or rather SyGuS) example files for the SyGuS examples yet.
This PR adds these missing examples.
|
|
This PRs updates java examples using the new Java API, by converting C++ examples to Java.
Examples CVC4Streams.java and PipedInput.java are removed since they are not longer supported by the API.
All examples are not included in the build which would be added in a future PR.
|
|
This commit removes support for the extended `(check-sat <term>)` command which overlaps in functionality with the standard `(check-sat-assuming (<prop_literal>*))` command.
|
|
This changes mkTuple -> tuple and tupSel -> tuple_select.
This is in line with the most recent syntax for tuples in preparation for the theory of tables in smt2.
|
|
This commit removes the support for the CVC language and converts all *.cvc regression tests to SMT-LIBv2.
|
|
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 is a translation of quickstart.cpp to python.
|
|
SyGuS examples will come later.
|
|
This PR adds a theory reference page for the transcendental extension.
|
|
|
|
|
|
|
|
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
|
|
This migrates page https://cvc4.github.io/sets-and-relations.
It further adds the SMT2 version of examples/api/cpp/sets.cpp and adds
test/regress/regress0/rels/relations-ops.smt2 as smtlib example for
relations.
|
|
This is to make it consistent with the name of the SMT-LIB operator
(fp.add).
|
|
This PR adds (most of) the existing examples to the documentation, and does some other minor updates on the documentation. Some details:
- for consistency, all cpp examples are moved from examples/api to examples/api/cpp
- add capabilities for SMT-LIB examples, and two simple smt2 examples
- more docs/examples/*.rst files
- two new documentation categories: installation (how to obtain, compile and install cvc5) and binary (about the cvc5 binary)
|
|
|
|
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 uses custom methods for printing the synthesis solutions instead of Solver::printSynthSolution, which is going to be removed by #6521.
|
|
(Z3 exposes it to facilitate custom hashes)
|
|
This commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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 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 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
|
|
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.
|
|
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 PR adds examples for using the sygus python api.
The examples are obtained from the examples of the cpp sygus api.
|
|
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 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.
|
|
This removes obsolete examples for the old API in preparation of making
the old API private. Examples for the new API are renamed from
*-new.cpp to *.cpp.
|
|
Fixes #2846. One of the challenges of the Java bindings is that the
garbage collector can delete unused objects at any time in any order.
This is an issue with CVC4's API because we require all `Expr`s to be
deleted before the corresponding `ExprManager`. In the past, we were
using `NewGlobalRef`/`DeleteGlobalRef` on the wrapper object of
`ExprManager`. The problem is that we can have multiple instances of the
wrapper that internally all refer to the same `ExprManager`. This commit
implements a different approach where the Java wrappers hold an explicit
reference to the `ExprManager`. The commit also removes some unused or
unimportant API bits from the bindings.
|
|
|
|
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.
|
|
Currently, our CVC4Config file is never including the CVC4 Java targets
because of a typo in `cmake/CVC4Config.cmake.in`. For this reason, our
build system for the examples would never actually build the examples.
Fixing this issue brought up another issue in our Relations Java example
that was using an outdated `System.loadLibrary()` call. This commit
fixes the typo and the example.
Note: Most changes in `Relations.java` were caused by ClangFormat.
|
|
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.
|