9 Commits

Author SHA1 Message Date
mudathirmahgoub
590af04a10 Remove reference to solver from java objects (#9147) 2022-10-04 17:06:02 +00:00
Gereon Kremer
6007962d5e Add test coverage for almost everything from the Java API (#8723)
This PR adds tests for almost everything that is not yet covered by the java API tests.
2022-05-10 14:55:44 +00:00
Mathias Preiner
d01e59c13b Update copyright headers for release 1.0 (#8539) 2022-04-05 20:38:57 +00:00
Andrew Reynolds
df6ce0361d Rename mkSygusGrammar to mkGrammar (#8544) 2022-04-02 19:40:41 +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
7ae28c6038 Properly guard commands in the SyGuS API (#8390)
This commit ensures we don't segfault in the SyGuS API (for non-text inputs) if the option sygus is not set to true. It also renames mkSygusVar to declareSygusVar for consistency with the sygus input format.

For SyGuS API inputs, we now use the option sygus to true instead of setting the language to sygus2.

This furthermore changes a few details in set-defaults regarding the relationship between the language, the sygus option, and when to apply default options for sygus.

It also adds a unit test for checkSynth.
2022-03-25 02:21:44 +00:00
mudathirmahgoub
690a392656 Enable CI for Junit tests (#7436)
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-11-03 21:32:10 +00:00
mudathirmahgoub
60c9b49809 Refactor java package name from cvc5 to io.github.cvc5.api (#7340)
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-22 23:00:06 +00:00