Package io.github.cvc5

Class Utils

  • public class Utils
extends java.lang.Object

    • Field Summary

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

    • Constructor Summary

      Constructors 
      Constructor Description
      Utils()  

    • Method Summary

      All Methods Static Methods Concrete Methods 
      Modifier and Type Method 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 java.util.List<java.lang.String> readLibraryFilenames​(java.lang.String pathInJar)
      Reads a text file from the specified path within the JAR file and returns a list of library filenames.
      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

    • Constructor Detail

      • Utils

        public Utils()

    • Method Detail

      • readLibraryFilenames

        public static java.util.List<java.lang.String> readLibraryFilenames​(java.lang.String pathInJar)
                                                             throws java.io.IOException,
                                                                    java.lang.UnsatisfiedLinkError
        Reads a text file from the specified path within the JAR file and returns a list of library filenames.
        Parameters:
        pathInJar - The path to the text file inside the JAR
        Returns:
        a list of filenames read from the file
        Throws:
        java.lang.UnsatisfiedLinkError - If the text file does not exist
        java.io.IOException - If an I/O error occurs

      • transferTo

        public static void transferTo​(java.io.InputStream inputStream,
                              java.io.FileOutputStream outputStream)
                       throws java.lang.Exception
        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.lang.Exception - If an I/O error occurs during reading or writing
        See Also:
        InputStream.transferTo(OutputStream)

      • loadLibraryFromJar

        public static void loadLibraryFromJar​(java.nio.file.Path tempDir,
                                      java.lang.String path,
                                      java.lang.String filename)
                               throws 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.lang.Exception - If the library cannot be found, the filename lacks an extension, or any I/O operation fails during extraction.
        java.lang.UnsatisfiedLinkError - If the library cannot be located at the specified path.

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

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