12 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
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
Mathias Preiner
467c95cffb api: Use std::optional for symbols in mk* functions. (#8495)
Makes all symbols in mk* functions optional.
2022-04-01 01:10:29 +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
mudathirmahgoub
69643856df Fix some documentation warnings (#8453) 2022-03-30 03:15:58 +00:00
Andrew Reynolds
c914f3eca8 Refactor result class (#8313)
This significantly refactors the internal result class. Entailments and "which" field are deleted, "Sat" is renamed to "Status". Moreover "TYPE_NONE" is made into a status.

Simplifies the usage of this class throughout the code.

It also changes the API Result method isSatUnknown to isUnknown.
2022-03-22 01:27:20 +00:00
Andrew Reynolds
2f1483e2e3 Remove unecessary methods from the API (#8260)
Removes checkEntailed from Solver.
Removes isEntailed, isNotEntailed, isEntailedUnknown from Result.
Removes isSubsortOf, isFunctionLike, getUninterpretedSortName, getSortConstructorName from Sort.

Updates examples and unit tests.
2022-03-14 18:29:30 +00:00
Andrew Reynolds
4972960da7 Check for free variables in several SolverEngine calls (#8130)
Fixes the nightlies due to ensuring that a unit test fails in production (it was failing only in debug).

Fixes #8127.
2022-02-24 18:28:58 +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