summaryrefslogtreecommitdiff
path: root/examples
AgeCommit message (Collapse)Author
2021-11-10sets: Rename set.intersection to set.inter. (#7622)Aina Niemetz
This further renames kind SET_INTERSECTION to SET_INTER.
2021-11-09sets: Update theory reference and smt2 examples. (#7602)Aina Niemetz
2021-11-08sets: Rename kinds with a more consistent naming scheme. (#7595)Aina Niemetz
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.'.
2021-11-04Refactor cmake to build either static or shared (#7534)Gereon Kremer
This PR simplifies the cmake setup to only build either shared or statically. It also attempts to fix windows builds, both shared and static.
2021-11-03Enable CI for Junit tests (#7436)mudathirmahgoub
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.
2021-10-28Add a `define-fun` command for each `:named` term. (#7308)Abdalrhman Mohamed
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.
2021-10-22Refactor java package name from cvc5 to io.github.cvc5.api (#7340)mudathirmahgoub
This PR refactors java package name from cvc5 to io.github.cvc5.api. It also refactor the names of cpp and java files.
2021-10-07Add a binary / SMT-LIB quickstart (#7315)Gereon Kremer
This PR adds a binary/SMT-LIBv2 quickstart example, based on the cpp quickstart example.
2021-10-07Replace doubles by rationals in C++ quickstart (#7317)Gereon Kremer
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.
2021-10-04Add sygus examples to documentation (#7303)Gereon Kremer
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.
2021-10-01Update java examples using the new Java API (#7225)mudathirmahgoub
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.
2021-09-30Refactor our static builds (#7251)Gereon Kremer
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).
2021-09-29Remove support for extended `(check-sat <term>)` command. (#7270)Abdalrhman Mohamed
This commit removes support for the extended `(check-sat <term>)` command which overlaps in functionality with the standard `(check-sat-assuming (<prop_literal>*))` command.
2021-09-29Update the syntax for tuples in smt2 (#7265)Andrew Reynolds
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.
2021-09-22Remove CVC language support (#7219)Mathias Preiner
This commit removes the support for the CVC language and converts all *.cvc regression tests to SMT-LIBv2.
2021-08-30Add API function to obtain information about a single option (#6980)Gereon Kremer
This PR adds api::Solver::getOptionInfo() that returns information about a single option, including its name, aliases, current and default value and its domain.
2021-08-23api: Require size argument for mkBitVector. (#6998)Aina Niemetz
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).
2021-08-19Make the python quickstart example run using ctest (#7023)yoni206
2021-07-29Python quick start example (#6939)yoni206
This is a translation of quickstart.cpp to python.
2021-07-06Porting C++ API examples to SMT-LIB examples (#6789)Haniel Barbosa
SyGuS examples will come later.
2021-07-05Add doc page about transcendentals (#6755)Gereon Kremer
This PR adds a theory reference page for the transcendental extension.
2021-06-23docs: Add quickstart guide. (#6782)Aina Niemetz
2021-06-16Make symfpu a required dependency. (#6749)Aina Niemetz
2021-06-15CVC4 -> cvc5 in cpp API examples (#6746)Haniel Barbosa
2021-06-15An example for a quick start guide (#6686)yoni206
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
2021-06-09docs: Migrate sets and relations theory reference. (#6698)Aina Niemetz
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.
2021-05-27FP: Rename FLOATINGPOINT_PLUS to FLOATINGPOINT_ADD. (#6628)Aina Niemetz
This is to make it consistent with the name of the SMT-LIB operator (fp.add).
2021-05-26Add more examples to the documentation (#6569)Gereon Kremer
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)
2021-05-21BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)Aina Niemetz
2021-05-20Avoid using printSynthSolution in the python API and examples (#6564)yoni206
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.
2021-05-14Stop using the solver for printing sygus synthesis solutions. (#6530)Abdalrhman Mohamed
This PR uses custom methods for printing the synthesis solutions instead of Solver::printSynthSolution, which is going to be removed by #6521.
2021-05-14Add getId function to python API (#6523)Alex Ozdemir
(Z3 exposes it to facilitate custom hashes)
2021-04-21Goodbye CVC4, hello cvc5! (#6371)Mathias Preiner
This commits changes the build system to cvc5 and removes the remaining occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
2021-04-20Remove support for CVC3 language. (#6369)Aina Niemetz
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-09Rename CVC4_ macros to CVC5_. (#6327)Aina Niemetz
2021-04-05New C++ Api: Rename and move headers. (#6292)Aina Niemetz
2021-04-01Delete hashsmt example. (#6263)Aina Niemetz
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.
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-20Generate cvc/Kind.java for the java API (#6143)mudathirmahgoub
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.
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2020-12-02Update copyright headers.Aina Niemetz
2020-11-20Updates to API in preparation for using symbol manager for model (#5481)Andrew Reynolds
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.
2020-11-05Remove mkSingleton from the API (#5366)mudathirmahgoub
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
2020-10-29Add mkInteger to the API (#5274)mudathirmahgoub
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
2020-10-04Remove subtyping for sets theory (#5179)mudathirmahgoub
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
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
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.
2020-09-01[API] Fix Python Examples (#4943)Andres Noetzli
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.
2020-08-03Examples for using sygus python api (#4822)yoni206
This PR adds examples for using the sygus python api. The examples are obtained from the examples of the cpp sygus api.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback