io.github.cvc5

Class Utils

java.lang.Object

io.github.cvc5.Utils

public class Utils
extends java.lang.Object

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	Utils.OS

Field Summary

Fields

Modifier and Type	Field and Description
static java.lang.String	LIBPATH_IN_JAR

Constructor Summary

Constructors

Constructor and Description
Utils()

Method Summary

Modifier and Type	Method and Description
static <K> Pair<K,java.lang.Long>[]	getPairs(Pair<K,? extends io.github.cvc5.AbstractPointer>[] abstractPointers)
static long[]	getPointers(io.github.cvc5.IPointer[] objects)
static long[][]	getPointers(io.github.cvc5.IPointer[][] objects)
static Proof[]	getProofs(long[] pointers)
static java.lang.String	getRational(Pair<java.math.BigInteger,java.math.BigInteger> pair) Convert a pair of BigIntegers to a rational string a/b
static Pair<java.math.BigInteger,java.math.BigInteger>	getRational(java.lang.String rational) Convert a rational string a/b to a pair of BigIntegers
static Sort[]	getSorts(long[] pointers)
static Term[]	getTerms(long[] pointers)
static void	loadLibraries() Load cvc5 native libraries.
static void	loadLibraryFromJar(java.nio.file.Path tempDir, java.lang.String path, java.lang.String filename) Loads a native library from a specified path within a JAR file and loads it into the JVM.
static void	transferTo(java.io.InputStream inputStream, java.io.FileOutputStream outputStream) Transfers all bytes from the provided InputStream to the specified FileOutputStream.
static void	validateUnsigned(int[] integers, java.lang.String name)
static void	validateUnsigned(int integer, java.lang.String name)
static void	validateUnsigned(long[] integers, java.lang.String name)
static void	validateUnsigned(long integer, java.lang.String name)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

LIBPATH_IN_JAR

public static final java.lang.String LIBPATH_IN_JAR

See Also:

Constant Field Values

Constructor Detail

Utils

public Utils()

Method Detail

transferTo

public static void transferTo(java.io.InputStream inputStream,
                              java.io.FileOutputStream outputStream)
                       throws java.io.IOException

Transfers all bytes from the provided InputStream to the specified FileOutputStream.

Note: This method replicates the functionality of InputStream#transferTo(OutputStream), which was introduced in Java 9 (currently, the minimum required Java version is 1.8)

Parameters:

inputStream - The input stream from which data is read

outputStream - The output stream to which data is written

Throws:

java.io.IOException - If an I/O error occurs during reading or writing

loadLibraryFromJar

public static void loadLibraryFromJar(java.nio.file.Path tempDir,
                                      java.lang.String path,
                                      java.lang.String filename)
                               throws java.io.FileNotFoundException,
                                      java.lang.Exception

Loads a native library from a specified path within a JAR file and loads it into the JVM.

Parameters:

path - The path inside the JAR where the library is located (e.g., "/cvc5-libs").

filename - The name of the library file (e.g., "libcvc5.so").

Throws:

java.io.FileNotFoundException - If the library cannot be found

java.lang.Exception - If an I/O error occurs or the library cannot be loaded

loadLibraries

public static void loadLibraries()

Load cvc5 native libraries.

getSorts

public static Sort[] getSorts(long[] pointers)

Parameters:

pointers - The array of pointers.

Returns:

Sorts array from array of Sort pointers.

getTerms

public static Term[] getTerms(long[] pointers)

Parameters:

pointers - The array of pointers.

Returns:

Terms array from array of Term pointers.

getProofs

public static Proof[] getProofs(long[] pointers)

Parameters:

pointers - The array of pointers.

Returns:

proofs array from array of pointers

getPointers

public static long[] getPointers(io.github.cvc5.IPointer[] objects)

Parameters:

objects - The one dimensional array of pointers.

Returns:

Pointers from one dimensional array.

getPointers

public static long[][] getPointers(io.github.cvc5.IPointer[][] objects)

Parameters:

objects - The two dimensional array of pointers.

Returns:

Pointers from two dimensional matrix.

validateUnsigned

public static void validateUnsigned(int integer,
                                    java.lang.String name)
                             throws CVC5ApiException

Throws:

CVC5ApiException

validateUnsigned

public static void validateUnsigned(long integer,
                                    java.lang.String name)
                             throws CVC5ApiException

Throws:

CVC5ApiException

validateUnsigned

public static void validateUnsigned(int[] integers,
                                    java.lang.String name)
                             throws CVC5ApiException

Throws:

CVC5ApiException

validateUnsigned

public static void validateUnsigned(long[] integers,
                                    java.lang.String name)
                             throws CVC5ApiException

Throws:

CVC5ApiException

getPairs

public static <K> Pair<K,java.lang.Long>[] getPairs(Pair<K,? extends io.github.cvc5.AbstractPointer>[] abstractPointers)

getRational

public static Pair<java.math.BigInteger,java.math.BigInteger> getRational(java.lang.String rational)

Convert a rational string a/b to a pair of BigIntegers

Parameters:

rational - The rational string.

Returns:

The pair of big integers.

getRational

public static java.lang.String getRational(Pair<java.math.BigInteger,java.math.BigInteger> pair)

Convert a pair of BigIntegers to a rational string a/b

Parameters:

pair - The pair of big integers.

Returns:

The rational string.