Package io.github.cvc5

Class Utils

java.lang.Object
io.github.cvc5.Utils
public final class Utils extends Object
A utility class containing static helper methods commonly used across the application.

This class is not meant to be instantiated. All methods are static and stateless.

  • Nested Class Summary

    Nested Classes
    Modifier and Type
    Class
    Description
    static enum 
    Utils.OS
    Represent the operating system types supported by cvc5.

  • Field Summary

    Fields
    Modifier and Type
    Field
    Description
    static final String
    LIBPATH_IN_JAR
    The base path inside the JAR where native libraries are stored.

  • Method Summary

    Modifier and Type
    Method
    Description
    static <K> Pair<K,Long>[]
    getPairs(Pair<K,? extends io.github.cvc5.AbstractPointer>[] abstractPointers)
    Convert an array of Pair objects, where the second element extends AbstractPointer, into an array of Pair objects with the second element as a Long representing the native pointer.
    static long[]
    getPointers(io.github.cvc5.IPointer[] objects)
    Extract native pointer values from a one-dimensional array of IPointer objects.
    static long[][]
    getPointers(io.github.cvc5.IPointer[][] objects)
    Extract native pointer values from a two-dimensional matrix of IPointer objects.
    static Proof[]
    getProofs(long[] pointers)
    Construct an array of Proof objects from an array of native 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)
    Construct an array of Sort objects from an array of native pointers.
    static Term[]
    getTerms(long[] pointers)
    Construct an array of Term objects from an array of native pointers.
    static void
    loadLibraries()
    Load cvc5 native libraries.
    static void
    loadLibraryFromJar(Path tempDir, String path, String filename)
    Load a native library from a specified path within a JAR file and loads it into the JVM.
    static void
    transferTo(InputStream inputStream, FileOutputStream outputStream)
    Transfer all bytes from the provided InputStream to the specified FileOutputStream.
    static void
    validateUnsigned(int[] integers, String name)
    Validate that all elements in the given array are non-negative (unsigned).
    static void
    validateUnsigned(int integer, String name)
    Validate that the specified integer is non-negative (unsigned).
    static void
    validateUnsigned(long[] integers, String name)
    Validate that all elements in the given array are non-negative (unsigned).
    static void
    validateUnsigned(long integer, String name)
    Validate that the specified long integer is non-negative (unsigned).

    Methods inherited from class java.lang.Object

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

  • Field Details

    • LIBPATH_IN_JAR

      public static final String LIBPATH_IN_JAR
      The base path inside the JAR where native libraries are stored.
      See Also:

  • Method Details

    • transferTo

      public static void transferTo(InputStream inputStream, FileOutputStream outputStream) throws IOException
      Transfer 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:
      IOException - If an I/O error occurs during reading or writing

    • loadLibraryFromJar

      public static void loadLibraryFromJar(Path tempDir, String path, String filename) throws FileNotFoundException, Exception
      Load a native library from a specified path within a JAR file and loads it into the JVM.
      Parameters:
      tempDir - The temporary directory where the extracted native library will be written.
      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:
      FileNotFoundException - If the library cannot be found
      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)
      Construct an array of Sort objects from an array of native pointers.
      Parameters:
      pointers - The array of pointers.
      Returns:
      Sorts array from array of Sort pointers.

    • getTerms

      public static Term[] getTerms(long[] pointers)
      Construct an array of Term objects from an array of native pointers.
      Parameters:
      pointers - The array of pointers.
      Returns:
      Terms array from array of Term pointers.

    • getProofs

      public static Proof[] getProofs(long[] pointers)
      Construct an array of Proof objects from an array of native pointers.
      Parameters:
      pointers - The array of pointers.
      Returns:
      proofs array from array of Proof pointers

    • getPointers

      public static long[] getPointers(io.github.cvc5.IPointer[] objects)
      Extract native pointer values from a one-dimensional array of 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)
      Extract native pointer values from a two-dimensional matrix of 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
      Validate that the specified integer is non-negative (unsigned).
      Parameters:
      integer - The integer value to validate
      name - A name to use in the exception message for identification
      Throws:
      CVC5ApiException - if the value is negative

    • validateUnsigned

      public static void validateUnsigned(long integer, String name) throws CVC5ApiException
      Validate that the specified long integer is non-negative (unsigned).
      Parameters:
      integer - The long value to validate
      name - A name to use in the exception message for identification
      Throws:
      CVC5ApiException - if the value is negative

    • validateUnsigned

      public static void validateUnsigned(int[] integers, String name) throws CVC5ApiException
      Validate that all elements in the given array are non-negative (unsigned).
      Parameters:
      integers - The array of integers to validate
      name - A name to use in the exception message for identification
      Throws:
      CVC5ApiException - if any element in the array is negative

    • validateUnsigned

      public static void validateUnsigned(long[] integers, String name) throws CVC5ApiException
      Validate that all elements in the given array are non-negative (unsigned).
      Parameters:
      integers - The array of long integers to validate
      name - A name to use in the exception message for identification
      Throws:
      CVC5ApiException - if any element in the array is negative

    • getPairs

      public static <K> Pair<K,Long>[] getPairs(Pair<K,? extends io.github.cvc5.AbstractPointer>[] abstractPointers)
      Convert an array of Pair objects, where the second element extends AbstractPointer, into an array of Pair objects with the second element as a Long representing the native pointer.
      Type Parameters:
      K - The type of the first element in the pairs.
      Parameters:
      abstractPointers - The input array of pairs with AbstractPointer as the second element.
      Returns:
      An array of pairs where the second element is the native pointer value as a Long.

    • 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.