Last thing, when a prover returns that a task is valid, I'd like to be
able to kill the other ones (I was doing this with a kill(2) syscall
before). Would it be possible to have such a thing with a function
using call_prover as argument?
2017-10-23 13:59 GMT+02:00 Pierre-Yves Strub :
>
stract away the unix pid. Regarding your
> request of having a way to call for available answers from multiple
> provers, the function
>
> Call_prover.forward_results
>
> should be what you look for.
>
> If something is missing for you in this API, we would be glad to
> complet
Sorry, my sentence is unclear: We're not using sessions but are
already using Driver.prove_task which returns a
Call_provers.prover_call (as the
call_on_*).
2017-10-23 13:12 GMT+02:00 Pierre-Yves Strub :
> Thank you for your answer. Yes, I was speaking about process ID that
> were avai
le provers (in a non-active way, i.e. without
spamming query_call). I'm ok to move to any API as long as I can call
multiple provers on a task and wait until on prover succeeds.
Best. Pierre-Yves.
2017-10-23 11:47 GMT+02:00 Johannes Kanig :
> Dear Pierre-Yves,
>
> On 10/23/2017 06:
Dear all,
I'm trying to update EasyCrypt from Why3 0.87 to 0.88. Up to now, we
were using the Why3 API to run provers on a task that we create
programmatically. To start multiple provers in parallel, we were
running our home made machinery that was relying on PID. This API has
now been removed (if
Hi,
Do you know if there exists a Why3 driver for boolector? I can't find
one after a quick search.
Best. Pierre-Yves.
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Hi,
Is there any plan to add a "resource limit" option (for
provers/drivers supporting this) in the Why3 API. For instance, see
this (for Z3):
https://github.com/Z3Prover/z3/issues/56
If not, I may try to add this on my own and send a patch.
Best,
-- Pierre-Yves.
___
