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