6 Commits

Author SHA1 Message Date
Gereon Kremer
13d891a718 Add some missing API tests (#8669)
This PR adds a couple of simple API tests for parts of the API that are not covered yet.
2022-04-29 00:47:10 +00:00
Mathias Preiner
d01e59c13b Update copyright headers for release 1.0 (#8539) 2022-04-05 20:38:57 +00:00
Andres Noetzli
c93de62d8b Move Java package to io.github.cvc5 (#8469)
Previously, we were using io.github.cvc5.api to mirror the C++
namespace that the API was in. The namespace of the C++ API changed to
simply cvc5 and so this commit updates the Java package accordingly.
2022-03-31 04:09:03 +00:00
mudathirmahgoub
c56a361253 Patch cross reference in Kind.java documentation (#8458)
This PR patches cross reference links in Kind.java comments for now until a proper way is implemented that handles documentation for cpp, python and Java API.
2022-03-30 21:58:08 +00:00
Andrew Reynolds
bf8ec7d9f1 Update checkSynth and checkSynthNext to return SynthResult (#8382)
Also extends to non-trivial unit test of SynthResult.

Note this also changes the expected output when using --sygus-out=status from unsat/sat/unknown to feasible/infeasible/fail (the option is used mostly just for our regressions). The output mode status-or-def is now equivalent to standard and is hence deleted.
2022-03-25 20:00:14 +00:00
Andrew Reynolds
ba24986fe2 Add SynthResult to the API (#8370)
Does not modify the code to return a SynthResult yet, just adds the class.

Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
2022-03-23 21:56:33 +00:00