java-smt
java-smt copied to clipboard
sosy-lab
JavaSMT - Unified Java API for SMT solvers.
Yices2 supports enumeration theory. JavaSMT also provides a FormulaManager for enumeration theory. The bindings are missing for that. TODO (incomplete list): - Implement bindings. - Publish Yices2 binary to Ivy...
Adds a debug mode that helps find common user errors - We check that solver structures are only accessed from the thread that created them - We make sure that...
This patch set is a backport of the floating point parts of https://github.com/sosy-lab/java-smt/pull/353 * It adds a new (JNI) method BitwuzlaJNI.bitwuzla_term_value_get_real() that can be used to read-out floating point values...
Integration of the APRON Numeric Abstract Domain Library as a quasi SMT solver supporting Integer, Rational and Boolean. Problems with the implementation: - Apron doesn't support UFs, no evaluation with...
Integrating a parser-interpreter and a code-generator for SMT-LIB2 into JavaSMT as well as the usage of the Princess binary as a solver. Theories supported by parser and generator: Boolean Integer...
Our expectation in CVC5 being able to provide multiple provers that can be used interleaved (or even parallel) based on a common basis (shared types and formulas) was not fulfilled....
Hello everyone, while working on https://github.com/sosy-lab/java-smt/pull/345 I noticed that one of the concurrent tests seems to (occasionally) fail for CVC5. The test case is testBvConcurrencyWithConcurrentContext from SolverConcurrencyTest and you can...
Several problems with unclear cause (to a user not fimilar with JavaSMT) are encountered on a regular basis when using JavaSMT. An example would be usage of a formula in...
The FormulaManagers for Integers, and possibly Rationals, are incomplete in CVC4. They do not support multiplication for example. However, CVC4 supports these operations. We need to analyze which operations are...
The constructor for PrincessFormulaManager passes null for parameter strManager upwards to AbstractFormulaManager. My understanding is that Princess does support strings and regex if combined with the OSTRICH library. Is there...
