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
$ cd cvc5
$ ./ production --java-bindings --auto-download --prefix=build/install
$ cd build
$ make
$ make install

$ ls install/lib
  libpicpoly.a  libpicpolyxx.a  objects-Production
$ ls install/share/java/
  cvc5-0.0.5-dev.jar  cvc5.jar

# compile example with cvc5 jar file
$ javac -cp "install/share/java/cvc5.jar" ../examples/api/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

Package io.github.cvc5.modes