| Age | Commit message (Collapse) | Author |
|---|
|
This PR adds Result.java ResultTest.java and cvc5_Result.cpp to the java api.
|
|
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
|
|
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 documentation to java kinds.
|
|
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 adds features to the KindsParser for saving and looking up the documentation comment associated with each Kind. This PR does not make use of it yet, but future PRs can query for the comment to automatically add it to language binding documentation (e.g., Python / Java bindings).
|
|
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 removes two headers for exceptions from options.h, and instead pushes the includes to a couple of source files.
|
|
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 PR adds documentation for api::Statistics and api::Stat, as well as further explanations in sphinx.
It also adds a custom css to our sphinx theme that slightly changes how inline code blocks look.
|
|
This commit changes how defaults are set and how the SMT solver is initialized so that proofs can be used fully with (new) unsat cores. Three modes of unsat cores are established now:
the upcoming assumption-based cores, which are incompatible with producing proofs (but enable proofs for preprocessing)
cores based on the SAT proof, which are incompatible with producing proofs (but enable proofs for preprocessing and the SAT solver)
cores based on the full proof, which are unrestricted
All the modes activate proofs but lead to errors if the user requires proofs but is not in the full proofs mode for cores.
|
|
This commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
|
|
Add getNumIndices to Op
|
|
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 PR finally removes the SExpr class. SMT-LIB compatible output is retained by using new on-the-fly conversion to s-expression strings. This finally allows us to remove includes to integer and rational from smt_engine.h.
In detail:
- a new set of toSExpr() methods is implemented that converts certain types to s-expression strings (without an intermediate class representing s-expressions)
- SmtEngine::getInfo() returns a string instead of SExpr and uses the new toSExpr methods
- SmtEngine::getStatistic() is removed
- SExpr class is removed
- d_commandVerbosity uses int instead of Integer
|
|
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.
|
|
This PR improves/fixes printing of statistics when the solver has been aborted, i.e. when we use printSafe(), and a few other minor issues with the new statistics setup.
add toString() methods for TypeConstant, api::Kind to allow for automatic printing by print_safe<>()
improve kindToString() to avoid std::stringstream
fix newlines between statistics in printSafe()
make printing of histograms consistent
make --stats-all, --stats-expert and --stats-every-check automatically enable --stats (and vice versa)
|
|
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
|
|
This PR improves the documentation of the api::Kind enum. Note that the docs for many of the enum values should still be improved. This PR merely makes sure that everything that is already there is actually output (/* vs /**) and properly rendered (missing spacing between lists, some formulas, etc).
|
|
|
|
This PR refactors how we collect statistics.
It splits the current statistic values into the values and a proxy object. The actual values now live inside the registry (making the ownership model way easier) while the proxy object are handed to whoever wants to collect a new statistic.
It also extends the C++ API to obtain and inspect the statistics.
To change the ownership, this PR needs to touch every single statistic in the whole codebase and change how it is registered.
|
|
|
|
This commit adds a new option to produce unsat cores based on our proof infrastructure (whereas previously we could only do so if we were also checking unsat cores) and the corresponding changes to the default settings to account for it. Since now options::unsatCores() and options::produceProofs() are incompatible, several parts of the code where we tested if we were in "old unsat cores mode", by testing the former and the negation of the latter options, are updated accordingly.
This commit also changes how SMT engine sets things by disabling proofs in the theory engine if we are in unsat core mode.
|
|
When a command is invoked, its result/status may be printed depending on its current verbosity, which (for probably an outdated reason) is stored in SMTEngine. One of my previous PRs modified the SMTEngine to return the verbosity as an sexpr. The modification works correctly when the output language is SMT2, but it breaks down with the AST output language, which prints sexprs in a different way. This PR fixes this bug by making SMTEngine return options as strings instead of sexpr.
|
|
This PR generalizes TypeNode::isFinite / TypeNode::isInterpretedFinite with TypeNode::getCardinalityClass. It then uses this method to fix our computation of when a type should be treated as finite.
Fixes #4260, fixes #6100 (that benchmark now says unknown without an error).
|
|
|
|
|
|
|
|
|
|
|
|
This configures the initial setup for generating Api documentation with
Sphinx via Breathe and Doxygen. All fixes in the documentation of the
cvc5.h header are for the purpose of eliminating warnings. This PR does
not check for completeness of the documentation, and does not yet tweak
the documentation to be nice, beautiful and consistent, which is
postponed to future PRs.
Configure with `--docs`, and then make. This will generate a `docs`
directory in the build directory. The Sphinx documentation can be found
at `build/docs/sphinx/index.html`. Doxygen documentation is only
generated as xml under `build/docs/doxygen`.
This PR further proposes a new style for copyright headers. If this
style is approved, I will submit a PR to update the update_copyright.pl
script.
|
|
Only regenerate files if dependencies changed. This avoids unnecessary
rebuilds of the Cython code.
|
|
Currently, NodeBuilder takes a single template argument: An integer
that determines the expected number of arguments. This argument is used
to determine the size of the d_inlineNvChildSpace array. This array is
used to construct nodes inline. The advantage of this is that we don't
have to allocate a NodeValue on the heap for the node under
construction until we are sure that the node is new. While templating
the array size may save some stack space (or avoid a heap allocation if
we statically know that we a fixed number of children and that number is
greater than 10), it complicates the code and leads to longer compile
times. Thus, this commit removes the template argument and moves some of
the NodeBuilder code to a source file for faster compilation.
CPU build time before change (debug build): 2429.68s
CPU build time after change (debug build): 2228.44s
Signed-off-by: Andres Noetzli noetzli@amazon.com
|
|
|
|
|
|
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 does some minor refactorings in preparation for the new statistics: some renamings, removal of now obsolete code and usage of references instead of pointers.
|
|
|
|
This is in preparation for a MPFR floating-point literal implementation.
We will need to have both literal kinds return a symFPU unpacked float
via `getSymUF()` in order to be able to plug it into the fp_converter.
For this, it makes sense to have the traits implemented and to be
included separately, so that they can also be included in the MPFR
implementation.
|
|
This fixes the type rule for to_real to match SMT-LIB: its argument must be an integer.
This required fixing the TPTP parser which has a more relaxed semantics for to_real / to_rat.
This also fixes Solver::isReal, which should return false if we are the integer type.
Fixes #6208.
|
|
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.
|
|
|
|
This PR changes ResetCommand to not call SmtEngine::reset but instead reconstruct the api::Solver object. This makes SmtEngine::reset obsolete and removes it, and moves the original options from SmtEngine to api::Solver.
The motivation for this change is twofold:
The ResetCommand should not use SmtEngine directly, but only through the API (i.e. Solver).
As soon as the statistics data lives within the registry, we need to re-register statistics after resetting the SmtEngine. We can now do this within the api::Solver constructor.
|
|
|
