io.github.cvc5

Class Utils

java.lang.Object

io.github.cvc5.Utils

public class Utils
extends Object

Constructor Summary

Constructors

Constructor and Description
Utils()

Method Summary

Modifier and Type	Method and Description
static <K> Pair<K,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 String	getRational(Pair<BigInteger,BigInteger> pair) Convert a pair of BigIntegers to a rational string a/b
static Pair<BigInteger,BigInteger>	getRational(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 jni library.
static void	validateUnsigned(int[] integers, String name)
static void	validateUnsigned(int integer, String name)
static void	validateUnsigned(long[] integers, String name)
static void	validateUnsigned(long integer, String name)

Methods inherited from class java.lang.Object

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

Constructor Detail

Utils

public Utils()

Method Detail

loadLibraries

public static void loadLibraries()

Load cvc5 jni library.

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,
                                    String name)
                             throws CVC5ApiException

Throws:

CVC5ApiException

validateUnsigned

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

Throws:

CVC5ApiException

validateUnsigned

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

Throws:

CVC5ApiException

validateUnsigned

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

Throws:

CVC5ApiException

getPairs

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

getRational

public static Pair<BigInteger,BigInteger> getRational(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 String getRational(Pair<BigInteger,BigInteger> pair)

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

Parameters:

pair - The pair of big integers.

Returns:

The rational string.