Conversation
Otherwise Yices may put SMTLIB quotes around the name
When compiled with --thread-safety Yices should be reentrant
The issue has been fixed in the new version and "(" characters in variable names now get quoted
|
@kfriedberger |
|
@daniel-raffler |
kfriedberger
left a comment
kfriedberger
left a comment
There was a problem hiding this comment.
Overall looks good. I will make a deeper test the next days.
| */ | ||
| DEFINE_FUNC(int, 1has_1mcsat) WITHOUT_ARGS | ||
| CALL0(int, has_mcsat) | ||
| INT_RETURN |
There was a problem hiding this comment.
We could maybe add BOOL_RETURN for such methods.
Thanks! I've been able to build the binaries in the 18.04 image Should I build with --thread-safety or --enable-mcsat? Unfortunately these options can't be combined and I'm not quite sure which one is more important to us |
# Conflicts: # lib/ivy.xml # src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java # src/org/sosy_lab/java_smt/solvers/yices2/Yices2Model.java # src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java # src/org/sosy_lab/java_smt/test/VariableNamesTest.java
Just FYI, support for unsat cores in MCSAT has been merged into master (both through SMTLib2 input and through API calls): SRI-CSL/yices2#578. It will be part of the upcoming Yices release 2.8. |
|
Thank you for that info! Both features are actually requested by users that i talk to a lot currently! |
# Conflicts: # src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java # src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java # src/org/sosy_lab/java_smt/test/SolverFormulaWithAssumptionsTest.java
|
The branch has now been switched to MCSAT, and I'll add interpolation support in the next few days. Unfortunately the We may be able to ship two binaries, one for MCSAT and one that allows parallel contexts, similar to how the issue is handled in MathSAT/OptiMathSAT. At run-time users can then choose which version to use when opening their If this turns out to be too complex, we may also consider adding a global lock for Yices, and simply forbidding all access that does not come from the original thread |
Despite what the website says, both options appear to be compatible. However, there are some issues, possibly linked to unsat core, where Yices fails to terminate
4 participants
Hello,
this PR updates Yices to version 2.7.0 and closes #402. Other than that the new version mainly includes improvements to the MCSat solver, which we're not using at the moment. Here is a full changelog.
Yices2 has some additional features that we may want to include:
unsat core(yet?)unsat core, but no interpolation or non-linear arithmetic--thread-safetyoption that allows multiple solver instances to run in parallelQF_BVlogicIn this PR I stuck with Dpll as solver and just enabled the
--thread-safetyoption. We could still add MCSat support and maybe even the external SAT solvers. Yices then picks the solver based on the logic, which would give us the best feature set. The big downside is that MCSat is not compatible with--thread-safety, which means that multiple parallel solver instances are not possible