yices2
yices2 copied to clipboard
SRI-CSL
Python EF solving
Is there support for exists-forall (linear real arithmetic) solving using the Python API? If so, can you please point me to some examples?
More exactly: The Yices API does not export the exists-forall solver, so it's not directly available in the Python API either. But, you can implement an exists/forall solver using the Python bindings.
You would have to implement the EF solver in python using the API. I am unclear on the benefits of this, though I suppose it would make rapid prototyping tweaks to the algorithm somewhat simpler.
I guess start with Bruno's paper and then grok the code
Apologies for commenting on an old issue, but am I to understand that there is no way to solve exists/forall problems through the Python API? I've tried setting the logic to no avail, I either get that it is not supported or that:
The function yices_assert_formula failed because: the context does not support quantifiers
I'm doing model enumeration, and I'd like to add some universally quantified constraints. The alternative is to use a CEGIS approach but that is redundant if the solver already supports EF solving.
Is the only option to use Yices through the smt-lib interface? Also is LIA not supported? only BV and LRA?
I just noticed that Yices has a yices_generalize_model function, which I could use to implement an equivalent CEGIS loop in Python. I also noticed that function only works on BOOL, BV and LRA, alas I need LIA :(
This is not documented but LIA is supported (but it's not heavily tested). Feel free to try.
Hi Bruno, I finally got a chance to try it, works amazingly well. I was able to find all solutions to my problem 2 orders of magnitude faster than with a naive blocking search. Interestingly Z3 and CVC4 cannot compete, neither in the naive blocking case nor with their internal FOL solvers.
Would be nice if Yices could handle exists/forall through the API directly, so I could send the same problem to Yices and to Z3/CVC4 though.