java-smt
java-smt copied to clipboard
sosy-lab
JavaSMT - Unified Java API for SMT solvers.
The explanations for installation do not mention all solvers. E.g. CVC4 is missing. The website seems to have only an .exe for windows. Which files are needed and where to...
Some SMT solvers provide the feature to define self-build sorts, such as tuple sorts. We might think of a way, perhaps even a new FormulaManager, to support such a feature....
There are currently 2 SigSevs in the [buildbot](https://buildbot.sosy-lab.org/cpachecker/results/nightly-predicate/00178.nightly-predicate.diff.html#/table) table resulting from the use of interpolation with Mathsat5. I checked the queries with Mathsat directly and those result only in an...
The last column of our [Buildbot table](https://buildbot.sosy-lab.org/cpachecker/results/nightly-predicate/00174.nightly-predicate.diff.html#/table) contains several exceptions from MathSAT5, where PI is already declared (standard symbol in FP theory?) and parsed again from SMTLIB. If this is...
Migrating to JUnit 5 would increase the flexibility and introduce the new features of JUnit 5 to our tests while allowing backwards compatibility with JUnit 4.
Building JavaSMT with the Eclipse compiler works. However executing the steps `ant clean; ant build-project-ecj; ./runExamples.sh` reports an error: Exception in thread "main" java.lang.Error: Unresolved compilation problem: Type safety: Unchecked...
This can be done by adding a Travis job which would create an empty maven project, add last version of JavaSMT as a dependency, and attempt to build it. Otherwise...
We need to document simplification and quantifier elimination (QE) capabilities of several solvers. This is a meta-issue. Feel free to break it into sub-issues. ### MathSAT5 MathSAT5 has a new...
For the solvers where `long` is used as representation of formulas, we currently use the `basicimpl` package and instantiate the generic parameters with `Long`. This means that auto-boxing occurs, for...
While visitors provide very convenient methods for formula transformation, their performance is sometimes suboptimal. Using a following fuzzer (https://gist.github.com/cheshire/c43575a86be1b58e3c40f95f1ba8ec07) , I've tried creating a random integer formula of size 1000,...