java-smt
java-smt copied to clipboard
sosy-lab
JavaSMT - Unified Java API for SMT solvers.
I have an abstraction refinement procedure which iteratively queries the SMT-solver, and in the case of SAT, explores the model returned by the solver to generate refinement clauses. From the...
CVC4 was succeeded by CVC5 and as a consequence support for CVC4 stopped. We should also update to CVC5 as a consequence. This issue tracks the status and problems of...
The [configuration option file](https://sosy-lab.github.io/java-smt/ConfigurationOptions.txt) lists ways to pass additional options to the various underlying solvers, however, it does not list `Z3`. Is it possible to pass arbitrary options to `Z3`?...
I am trying to use JavaSMT within a project that is built with Gradle, and am having difficulties, especially with the Z3 dependencies. [I already posted a question on StackOverflow](https://stackoverflow.com/questions/66894426),...
MathSAT throws an exception if two variables with the same name and different sorts are ever declared. For example: ```kotlin SolverContextFactory.createSolverContext(SolverContextFactory.Solvers.MATHSAT5).use { solverCtx -> val ifm = solverCtx.formulaManager.integerFormulaManager val bfm...
The [MathSAT API](https://mathsat.fbk.eu/apireference.html) contains methods for quantifiers, but it seems that JavaSMT does not expose them. This should be added in order to not hide solver features from users of...
Hey, I'm wondering if there is an option to convert an `IntegerFormula`-Variable into a `BooleanFormula`-Variable somehow. Specifically, I want to have `BooleanFormula `if possible, but if I have to (e.g.`...
hello, is it possible with javaSMT to declare a new Sort like in SMTLIB ? for example : (declare-sort Auto 0)
Currently it is only [weakly documented](https://github.com/sosy-lab/java-smt#multithreading-support) which solvers can use which components in a multi-threaded environment. We should check whether some solvers can use several stacks (for the same context)...
There is a new version of OptiMathSAT, which does not bring anything new, except internal improvements. Normally, such an update would not be worth an issue. However, there is a...