Java API
The Java API for cvc5 mostly mirrors the C++ API and supports operator overloading, iterators, and exceptions. There are a few differences from the C++ API, such as using arbitrary-precision integer pairs, specifically, pairs of Java BigInteger objects, to represent rational numbers. The quickstart guide gives a short introduction, and more examples can be found here.
For most applications, the Solver class is the main entry point to cvc5. The class hierarchy of cvc5 package provides more details on the individual classes.
Building cvc5 Java API
$ git clone https://github.com/cvc5/cvc5
$ cd cvc5
$ ./configure.sh production --java-bindings --auto-download --prefix=build/install
$ cd build
$ make
$ make install
$ ls install/lib
cmake libcvc5jni.so libcvc5parser.so libcvc5parser.so.1 libcvc5.so
libpicpoly.a libpicpolyxx.a libpoly.so libpoly.so.0 libpoly.so.0.1.9
libpolyxx.so libpolyxx.so.0 libpolyxx.so.0.1.9 objects-Production
$ ls install/share/java/
cvc5-0.0.5-dev.jar cvc5.jar
# compile example QuickStart.java with cvc5 jar file
$ javac -cp "install/share/java/cvc5.jar" ../examples/api/java/QuickStart.java -d .
# run example QuickStart with cvc5 jar file and cvc5 shared libraries
$ java -cp "install/share/java/cvc5.jar:." "-Djava.library.path=install/lib" QuickStart
expected: sat
result: sat
value for x: 1/6
value for y: 1/6
expected: unsat
result: unsat
unsat core size: 3
unsat core:
(< 0 a)
(< 0 b)
(< (+ a b) 1)
Package io.github.cvc5
class Command
class Datatype
class DatatypeConstructor
class DatatypeConstructorDecl
class DatatypeDecl
class DatatypeSelector
class Grammar
class InputParser
class Op
class OptionInfo
class Pair<K,V>
class Result
class Solver
class Sort
class Stat
class Statistics
class SymbolManager
class SynthResult
class Term
class TermManager
class Triplet<A,B,C>
class Utils
enum Kind
enum RoundingMode
enum ProofRule
exception CVC5ApiException
exception CVC5ApiOptionException
exception CVC5ApiRecoverableException
Package io.github.cvc5.modes
enum BlockModelsMode
enum FindSynthTarget
enum InputLanguage
enum LearnedLitType
enum ProofComponent