Age | Commit message (Collapse) | Author |
|
This further renames kind SET_INTERSECTION to SET_INTER.
|
|
|
|
This prefixes sets kinds with SET_ and relation kinds with
RELATION_. It also prefixes the corresponding SMT-LIB operators with
'set.' and relation operators with 'rel.'.
|
|
This PR simplifies the cmake setup to only build either shared or statically. It also attempts to fix windows builds, both shared and static.
|
|
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 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 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 PR adds api::Solver::getOptionInfo() that returns information about a single option, including its name, aliases, current and default value and its domain.
|
|
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/.
|
|
|
|
|
|
|
|
|
|
This example does not serve the purpose of documenting how to use the
new API. It uses Command, which is not available via the API, and it's
not worth the effort to migrate it.
|
|
|
|
|
|
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.
|
|
|
|
|
|
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.
|