Adding dReal to JavaSMT #313

[juliusbrehme]

Integrating dReal to JavaSMT.

Problems with dReal:

• dReal does not support UF's
• dReal does not support existential quantifier
• dReal uses delta-precision, therefore Integer formulas are unsound:
  • Example: x_1 != x_2 && x_1 < 1 && x_2 < 1 && 0 <= x_1 && 0 <= x_2 should be unsatisfiable, but it is not (see Issue)
  • Division with Integer does not work correctly (see Issue)
  • Because integer division does not work properly, the result of modularCongruence() in IntegerFormulaManager is not always correct, because integer division is used.
• It is not possible to create an integer number with BigInteger, only if the number is smaller than 1.0E9.

[juliusbrehme]

Proposal for integrating trigonometric functions:

dReal does support trigonometric functions. Trigonometric functions are not supported in JavaSMT, but this could be implemented in RationalFormula. Other solvers do support them as well, like Z3. dReal has the following trigonometric functions, they can be found in expression.h and in Dreal.java:

• sin()
• cos()
• tan()
• asin()
• acos()
• atan()
• atan2()
• sinh()
• cosh()
• tanh()

[daniel-raffler]

I've just added a build script for packaging the dReal solver backend. It is still quite basic and will only repackage the binaries that are povided by the dReal team. Building the project ourselves is quite involved as it depends on libibex and the build tool bazel, neither of which is available in the Ubuntu repositories. They can be installed from ppa, but this still requires root access.

Also note that the library does have quite a few dependencies that will have to be installed locally:

daniel@ZenBook:~/workspace/java-smt$ ldd libdreal-4.21.06.2-gf93bdcc.so
libnlopt.so.0 => /lib/x86_64-linux-gnu/libnlopt.so.0 (0x0000758d78bfd000)
libClpSolver.so.1 => /lib/x86_64-linux-gnu/libClpSolver.so.1 (0x0000758d78ab7000)
libClp.so.1 => /lib/x86_64-linux-gnu/libClp.so.1 (0x0000758d7893e000)
libCoinUtils.so.3 => /lib/x86_64-linux-gnu/libCoinUtils.so.3 (0x0000758d78825000)
liblapack.so.3 => /lib/x86_64-linux-gnu/liblapack.so.3 (0x0000758d78000000)
libblas.so.3 => /lib/x86_64-linux-gnu/libblas.so.3 (0x0000758d78789000)
libopenblas.so.0 => /lib/x86_64-linux-gnu/libopenblas.so.0 (0x0000758d75528000)
...

@baierd Could you upload the binaries, please?