Java API

The Java API of 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.


Using Self-Contained cvc5 Java API JAR

Starting from version 1.2.1, a JAR file containing the cvc5 Java API and all required native libraries is available on the release page for each version. To use it, download the appropriate JAR file for your platform. For example, if your computer runs Linux x86_64, download cvc5-Linux-x86_64-java-api.jar to a working directory.

To compile the QuickStart.java example provided in the quickstart guide , ensure the file is in the same directory as the JAR. Then, run:

$ javac -cp "cvc5-Linux-x86_64-java-api.jar" ./QuickStart.java -d .

After compilation, execute the example with:

$ java -cp "cvc5-Linux-x86_64-java-api.jar:." QuickStart # Replace : with ; on Windows
  expected: sat
  result: sat
  value for x: 1/6
  value for y: 1/6
  value for x - y: 0/1
  computed correctly
  expected: unsat
  result: unsat
  unsat core size: 3
  unsat core:
  (< 0 a)
  (< 0 b)
  (< (+ a b) 1)

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)

Javadoc API Documentation

Package io.github.cvc5

Package io.github.cvc5.modes