search

SRI-CSL / yices2

The Yices SMT Solver
https://yices.csl.sri.com/
GNU General Public License v3.0
368 stars 46 forks source link

Python EF solving #86

Open umangm opened 6 years ago

umangm commented 6 years ago

Is there support for exists-forall (linear real arithmetic) solving using the Python API? If so, can you please point me to some examples?

ianamason commented 6 years ago

Sadly I think it is currently not possible.

BrunoDutertre commented 6 years ago

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.

umangm commented 6 years ago

Any pointers on that?

ianamason commented 6 years ago

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

sirwhinesalot commented 3 years ago

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?

sirwhinesalot commented 3 years ago

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 :(

BrunoDutertre commented 3 years ago

This is not documented but LIA is supported (but it's not heavily tested). Feel free to try.

sirwhinesalot commented 3 years ago

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.