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.

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 

class AbstractPlugin

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 Proof

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 Result.UnknownExplanation

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

enum ProofFormat

Java API

Building cvc5 Java API

Javadoc API Documentation

Package io.github.cvc5

Package io.github.cvc5.modes

Javadoc API Documentation 

Package io.github.cvc5 

Package io.github.cvc5.modes 