java-smt
java-smt copied to clipboard
sosy-lab
JavaSMT - Unified Java API for SMT solvers.
`AbstractUFManager` currently forbids boolean arguments for UFs: https://github.com/sosy-lab/java-smt/blob/8fd9bff46bb6d1741b900a9d61fb02cd9045c582/src/org/sosy_lab/java_smt/basicimpl/AbstractUFManager.java#L53-L55 Why is that the case? Can it be allowed? If I remove that check, and run the following test, it works on...
Z3 provides not only `check-sat` but also `check-sat-using ` in SMTLib, so probably also via the API. This can be used to let Z3 use different solving strategies, which might...
The current build targets for publishing solver binaries are suboptimal because they make it easy to (accidentally) build and publish solver binaries that are broken or depend on libraries on...
The newest version of MathSat5 supports directly solving mathematical functions like pi, sin, cos, exp. We should add nice methods for this into the API, maybe also with an option...
With SMTInterpol, the following code fails: ``` bmgr.makeVariable("select"); ``` Exception: ``` de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: Function select is already defined. at de.uni_freiburg.informatik.ultimate.logic.NoopScript.declareFun(NoopScript.java:120) at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.declareFun(SMTInterpol.java:1885) at org.sosy_lab.solver.smtinterpol.SmtInterpolEnvironment.declareFun(SmtInterpolEnvironment.java:304) at org.sosy_lab.solver.smtinterpol.SmtInterpolFormulaCreator.makeVariable(SmtInterpolFormulaCreator.java:84) at org.sosy_lab.solver.smtinterpol.SmtInterpolBooleanFormulaManager.makeVariableImpl(SmtInterpolBooleanFormulaManager.java:55) at org.sosy_lab.solver.smtinterpol.SmtInterpolBooleanFormulaManager.makeVariableImpl(SmtInterpolBooleanFormulaManager.java:1) at...
If sosy-lab.common indeed has potentially zero-overhead (when disabled) timers, tracking statistics inside JavaSMT would be very nice.
Currently, we never deallocate `msat_term`s. Mathsat5 has a function `msat_gc_env`, which can be called periodically for this purpose. This can be enabled at least as an option.
This PR integrates the new CVC5 (successor of CVC4) into JavaSMT.
Hello everyone, this patch set removes all auto generated code and adds a new swig script instead. This will help simplify upgrades to new Bitwuzla versions as changes to the...
