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