Merge pull request #453 from sosy-lab/fix-library-symlinks

Remove a broken symlink to a native library on arm64 and update the README for windows binaries.

Author: daniel-raffler

lib/native/arm64-linux/libopensmtjava.so

@@ -0,0 +1,24 @@
+<!--
+This file is part of JavaSMT,
+an API wrapper for a collection of SMT solvers:
+https://github.com/sosy-lab/java-smt
+
+SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
+
+# How to install a SMT solver library for Windows (arm64) for developers of JavaSMT
+
+Currently, the only native solver that is supported on Windows for arm64 is Z3. The Java based
+solvers SMTInterpol and Princess are also available and will simply work out of the box. To use
+Z3 on arm64 its native libraries first need to be linked or copied to this directory. This can
+be done just as described in the `README` for Windows on x86 [here](../x86_64-windows/README.md)
+
+Either link the library as admin:
+- `mklink libz3.dll ..\..\java\runtime-z3\arm64\libz3.dll`
+- `mklink libz3java.dll ..\..\java\runtime-z3\arm64\libz3java.dll`
+
+...or copy the library files directly to this folder:
+- `copy ..\..\java\runtime-z3\arm64\libz3.dll libz3.dll`
+- `copy ..\..\java\runtime-z3\arm64\libz3java.dll libz3java.dll`

lib/native/arm64-windows/README.md

@@ -25,41 +25,41 @@ which are either to create symlinks or to copy the library files.
 Symbolic links allow for an automatic update as soon as a dependency is changed via Ant/Ivy.
 Windows does not allow user-space symlinks, but requires administrator rights to create them.
 Thus, we cannot check them into the repository. Please execute the following as administrator
-in the current directory `lib/native/x86_64-windows`:
+in the current directory `lib\native\x86_64-windows`:
 
 For Z3:
-- mklink libz3.dll ..\..\java\runtime-z3\x64\libz3.dll
-- mklink libz3java.dll ..\..\java\runtime-z3\x64\libz3java.dll
+- `mklink libz3.dll ..\..\java\runtime-z3\x64\libz3.dll`
+- `mklink libz3java.dll ..\..\java\runtime-z3\x64\libz3java.dll`
 
 For MathSAT5:
-- mklink mpir.dll ..\..\java\runtime-mathsat\mpir.dll
-- mklink mathsat.dll ..\..\java\runtime-mathsat\mathsat.dll
-- mklink mathsat5j.dll ..\..\java\runtime-mathsat\mathsat5j.dll
+- `mklink mpir.dll ..\..\java\runtime-mathsat\x64\mpir.dll`
+- `mklink mathsat.dll ..\..\java\runtime-mathsat\x64\mathsat.dll`
+- `mklink mathsat5j.dll ..\..\java\runtime-mathsat\x64\mathsat5j.dll`
 
 For Bitwuzla:
-- mklink libbitwuzlaj.dll ..\..\java\runtime-bitwuzla\libbitwuzlaj.dll
+- `mklink libbitwuzlaj.dll ..\..\java\runtime-bitwuzla\x64\libbitwuzlaj.dll`
 
 ### With a direct copy of the library:
 
 An alternative simple solution (without the need of administrator rights) is to copy over
-those files from the `lib\java\runtime-*\` directory into the current directory `lib/native/x86_64-windows`:
+those files from the `lib\java\runtime-*\` directory into the current directory `lib\native\x86_64-windows`:
 Please note that this copy process needs to be repeated after each update of a solver library via Ant/Ivy dependencies.
 
 For Z3:
-- copy ..\..\java\runtime-z3\x64\libz3.dll libz3.dll
-- copy ..\..\java\runtime-z3\x64\libz3java.dll libz3java.dll
+- `copy ..\..\java\runtime-z3\x64\libz3.dll libz3.dll`
+- `copy ..\..\java\runtime-z3\x64\libz3java.dll libz3java.dll`
 
 For MathSAT5:
-- copy ..\..\java\runtime-mathsat\mpir.dll mpir.dll
-- copy ..\..\java\runtime-mathsat\mathsat.dll mathsat.dll
-- copy ..\..\java\runtime-mathsat\mathsat5j.dll mathsat5j.dll
+- `copy ..\..\java\runtime-mathsat\x64\mpir.dll mpir.dll`
+- `copy ..\..\java\runtime-mathsat\x64\mathsat.dll mathsat.dll`
+- `copy ..\..\java\runtime-mathsat\x64\mathsat5j.dll mathsat5j.dll`
 
 For Bitwuzla:
-- copy ..\..\java\runtime-bitwuzla\libbitwuzlaj.dll libbitwuzlaj.dll
+- `copy ..\..\java\runtime-bitwuzla\x64\libbitwuzlaj.dll libbitwuzlaj.dll`
 
 Or simply use a wildcard:
-- copy ..\..\java\runtime-*\*dll .\
-- copy ..\..\java\runtime-*\x64\*dll .\
+- `copy ..\..\java\runtime-*\*dll .\`
+- `copy ..\..\java\runtime-*\x64\*dll .\`
 
 ## Additional dependencies: