Exposing solvers returning `unknown`

[Lukas-Dresel]

So, @rhelmot , @zardus , @ltfish: we have an interesting dilemma on our hands now where we implemented a portfolio frontend dishing the constraints out to multiple different solvers and returning the first answers received by any of the solvers.

However, some solvers, e.g. CVC4, return unknown almost immediately for some constraints they can't deal with. This means we now need to be able to differentiate between unknown, unsat and sat results returned from solvers in order to only accept answers in the portfolio that are certain. What do you think is the best way to deal with this?

[rhelmot]

Implement unknown as an exception the same way as I got halfway through doing in order to support timeouts better?

On Thu, Sep 6, 2018 at 1:26 PM Lukas Dresel notifications@github.com wrote:

So, @rhelmot https://github.com/rhelmot , @zardus https://github.com/zardus , @ltfish https://github.com/ltfish: we have an interesting dilemma on our hands now where we implemented a portfolio frontend dishing the constraints out to multiple different solvers and returning the first answers received by any of the solvers.

However, some solvers, e.g. CVC4, return unknown almost immediately for some constraints they can't deal with. This means we now need to be able to differentiate between unknown, unsat and sat results returned from solvers in order to only accept answers in the portfolio that are certain. What do you think is the best way to deal with this?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/angr/claripy/issues/89, or mute the thread https://github.com/notifications/unsubscribe-auth/ACYg9WnKfGFNEs1Z7Hq69YbLJIwJBkZHks5uYYT_gaJpZM4Wdp8P .

[Lukas-Dresel]

We have the following ideas to deal with this issue:

• Expose a function, I'll call it check_satisfiability for now, that actually returns the solver response as it is received, so 'SAT', 'UNSAT' or 'UNKNOWN'
• Throw a ResultUnknown exception
• Make satisfiable return None in the case of unknown, this would still evaluate to False

Right now I think this list is in the order of our preference as we think what the cleanest solutions are.

[rhelmot]

We already have a function, it's called satisfiable(). We can just make it return members of an enum who we override the __nonzero__ such that SAT is truthy and the rest are falsey. I like that idea the best.

[zardus]

I agree with @rhelmot. Let's go for an enum, with only SAT being truthy. If we also override __eq__ to evaluate to z3.sat and "sat" as well, then I think we'll have a nice universal solution.

[github-actions[bot]]

This issue has been marked as stale because it has no recent activity. Please comment or add the pinned tag to prevent this issue from being closed.

[github-actions[bot]]

This issue has been marked as stale because it has no recent activity. Please comment or add the pinned tag to prevent this issue from being closed.

[rhelmot]

This is now solved as of #285 - there are multiple kinds of unknowns, each of which gets a different kind of exception raised for them.