| Age | Commit message (Collapse) | Author |
|---|
|
This PR refactors java package name from cvc5 to io.github.cvc5.api.
It also refactor the names of cpp and java files.
|
|
A life of solver object was simple before summer. Then it got complicated with getDifficulty, optional proofs getProof, more assumptions addSygusAssume, and finally different options to choose from OptionInfo.
This PR attempts to prepare solver objects for this new life.
|
|
This makes cardinality constraints nullary operators. This eliminates hacks for supporting these previously.
It also removes an unimplemented kind CARDINALITY_VALUE.
Notice that the parser and printer now do not use a common syntax for cardinality constraints, this will be resolved on followup PRs.
|
|
This makes a push to fix our windows nightly builds. It does a couple of things:
- remove `CVC5_WINDOWS_BUILD` and check `CMAKE_SYSTEM_NAME` instead
- use `CMAKE_SHARED_LIBRARY_SUFFIX` instead of `so`
- properly set `IMPORTED_IMPLIB` on imported shared libraries
- fix the GMP build, where the header is different for shared and static builds
- fix the find&sed patching for libpoly
- add `CVC5_EXPORT` to nested types in the API
- remove `CVC5_EXPORT` from enums
- add `-Dcvc5_obj_EXPORTS` to actually enable exports
- Fix how template function `safe_print` is exported.
|
|
@alex-ozdemir
|
|
Fixes #7430.
|
|
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 addresses one of the issues related to #6605.
|
|
|
|
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.
|
|
|
|
When compiling cvc5 with clang-13, it will emit lots of warnings of usages of `std::iterator` as it's deprecated since C++17.
The recommended implementation of iterators is to manually define the following five types:
```
template< class Iter >
struct iterator_traits;
difference_type Iter::difference_type
value_type Iter::value_type
pointer Iter::pointer
reference Iter::reference
iterator_category Iter::iterator_category
```
And the iterator-related types could be accessed by for example `typename std::iterator_traits<Iter>::value_type value`.
This pull request performs the fix, and the program is semantically equivalent before and after the fix.
References:
https://en.cppreference.com/w/cpp/iterator/iterator_traits
https://en.cppreference.com/w/cpp/iterator/iterator
|
|
This introduces a new versioning mechanism that allows for better automation.
|
|
This adds recent API functions that were added to terms.
It also uses BigInteger now for integer terms.
|
|
This PR modifies the API function Term::getRealValue() to always return a fraction. Beforehand, it would return rationals in fractional notation (15/2) and integers in decimal notation (2.0).
|
|
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 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 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 fixes some docstrings that are not properly indented for sphinx.
|
|
|
|
This is in preparation for renaming SmtEngine to SolverEngine.
|
|
This PR adds the cmake setup to generate javadoc documentation for the java API and integrates it into the sphinx documentation. Right now, we simply link to the javadoc. This PR also modifies a bunch of javadoc comments to use proper javadoc syntax.
|
|
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 finishes the implementation of the Java API.
It also includes all java files in the build along with their unit tests.
|
|
constraint (#7268)
Since ~1 year ago, we insist that the location and data types of the separation logic heap are set upfront, analogous to the set-logic command. This means that the separation logic empty heap constraint does not need to be annotated with its types.
This makes SEP_EMP a nullary Boolean operator instead of binary predicate (taking dummy arguments whose types specify the heap type). It changes the smt2 extended syntax from (_ emp T1 T2) to sep.emp.
|
|
Previously, SymFPU was an optional dependency but it is now required.
The comments in the API were not updated to reflect that. This commit
fixes the comments.
|
|
This adds Statistics and Stat to the Java API
|
|
This adds Sort.java SortTest.java and cvc5_Sort.cpp to the java api.
|
|
This PR eliminates the Output macro together with the associated output stream (stored in a static variable). It is replaces by a set of simple utility functions of the Env class, and we instead use the output stream from options.base.out.
To achieve this, a couple of quantifier classes are now derived from EnvObj.
|
|
|
|
This changes cvc5 to use a single `NodeManager` per thread (using
`thread_local`). We have decided that this is more convenient because
nodes between solvers in the same thread could be exchanged and that
there isn't really an advantage of having multiple `NodeManager`s per
thread.
One wrinkle of this change is that `NodeManager::init()` must be called
explicitly before the `NodeManager` can be used. This code can currently
not be moved to the constructor of `NodeManager` because the code
indirectly calls `NodeManager::currentNM()`, which leads to a loop
because the `NodeManager` is created in `NodeManager::currentNM()`.
Further refactoring is required to get rid of this restriction.
|
|
Adds smt2 parsing, printing and API support for get-difficulty. Adds unit tests.
|
|
Adds support for global assumptions in sygus files.
Also guards against cases of declare-const, which should be prohibited in sygus.
|
|
This PR adds a new api::Solver::isOutputOn() method, including unit tests for both isOutputOn() and getOutput().
|
|
This commit adds Op.java OpTest.java and cvc5_Op.cpp to the java api.
|
|
Allow access to the Output() macro via the API.
|
|
This commit adds Datatype.java DatatypeTest.java and cvc5_Datatype.cpp to the java api.
|
|
DatatypeDecl.java, DatatypeSelector.java (#6390)
Add DatatypeConstructor.java, DatatypeConstructorDecl.java, DatatypeDecl.java, DatatypeSelector.java and their corresponding c++ files
|
|
This PR adds a missing check in the API for getOptionInfo().
|
|
This changes our implementation of GetModelCommand so that we use the API to print the model.
It simplifies smt::Model so that this is a pretty printing utility, and not a layer on top of TheoryModel.
It adds getModel as an API method for returning the string representation of the model, analogous to our current support for getProof.
This eliminates the last call to getSmtEngine() from the command layer.
|
|
This PR refactors the driver to no longer directly access the Options object, but instead use Solver::getOption() or Solver::getOptionInfo().
|
|
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 PR adds kind BAG_MAP to bags.
|
|
|
|
This PR adds a new API function Solver::getDriverOptions() which is used to communicate special options that (a) can not be properly communicated via getOption() and (b) need to be available in the driver (in a type-safe manner).
As of now, this concerns the input stream and output streams.
Furthermore, this PR refactors the driver to obtain them via the driver options instead of using the (deprecated) Solver::getOptions() method.
|
|
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
|
