java-smt
java-smt copied to clipboard
sosy-lab
JavaSMT - Unified Java API for SMT solvers.
This is not a critical feature, but apparently it's possible. See: http://blog.httrack.com/blog/2013/08/23/catching-posix-signals-on-android/ https://github.com/xroche/coffeecatch
If a native solver cannot be loaded, JavaSMT throws an `InvalidConfigurationException` with the message The SMT solver is not available on this machine because of missing libraries (). You may...
We currently use a modified version of CVC4 from https://github.com/kfriedberger/CVC4 where all finalizers are disabled to avoid several SegFaults. The problem appears sometimes on Java8 and more often on Java11....
Some solvers allow to create symbols (and UFs) with identical names and different sorts. We should discuss whether we want to avoid such inconsistencies and how to react when creating...
All solvers allow to define nullary UFs, i.e., UFs without arguments. For some solvers, the returned formula can be used just like a plain symbol/variable and is even comparable, i.e....
[OpenSMT2](http://verify.inf.usi.ch/content/opensmt2) supports interpolation (for some theories). A description how to compile OpenSMT2 can be found [on their websites](http://verify.inf.usi.ch/opensmt-compilation). A student (from GSoC) will be working on the integration into JavaSMT....
# So far this is the progress made on adding STP solver to java-smt: - Create a Build Script which can automatically: - Clone and Build STP, - Generate the...
# So far this is the progress made on adding opensmt solver to java-smt: - Create a basic sample (simpler than the more elaborate existing ones) to use the java-smt...
SMTInterpol already does this, now we do it for all other solvers as well. This basically re-adds 36e47b5b (which was only for Z3), but in a more memory-efficient way (`Stream.distinct()`...
Currently it is not properly defined which versions of standard libraries we assume for the native binaries we ship, i.e., on which distributions in which versions these binaries are usable....