update README for developers when using SMT solvers on Windows.
There is no way to distinguish Rationals from Integers when it comes to integral numbers.
Thus, we try to normalize them and only return Java-Rationals if required.
We internally try to simplify Rational constants to BigInteger.
@@ -8,7 +8,7 @@ SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
SPDX-License-Identifier: Apache-2.0
-->
-# How to install Z3 for Windows64 for developers of JavaSMT
+# How to install a SMT solver library for Windows (64-bit) for developers of JavaSMT
## Note:
@@ -17,10 +17,14 @@ but only for developing JavaSMT with native solver support on a Windows machine.
## Instruction:
-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:
+There are two ways for providing SMT solver libraries for Windows,
+which are either to create symlinks or to copy the library files.
+
+### With symlinks to the downloaded library:
+
+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:
For Z3:
- mklink libz3.dll ..\..\java\runtime-z3\libz3.dll
@@ -31,6 +35,8 @@ For MathSAT5:
- mklink mathsat.dll ..\..\java\runtime-mathsat\mathsat.dll
- mklink mathsat5j.dll ..\..\java\runtime-mathsat\mathsat5j.dll
+### With a direct copy of the library:
+
An alternative simple solution (without the need of administrator) is to copy over
those files from the `lib\java\runtime-*\` directory into the current directory.
Please note that this needs to be repeated after each update of Ant/Ivy dependencies.
@@ -46,3 +52,9 @@ For MathSAT5:
Or simply use a wildcard:
- copy ..\..\java\runtime-*\*dll .\
+
+## Additional dependencies:
+
+To execute JavaSMT with MathSAT on a Windows system,
+please install the [Visual C++ 2013 Redistributable Package](https://support.microsoft.com/en-us/help/4032938/update-for-visual-c-2013-redistributable-package).
+Otherwise you might get an `UnsatisfiedLinkError` because of the missing system library `msvcr120.dll`.
