IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.
Other
79
stars
24
forks
source link
disable e-matching by default, adding option to turn it on #4
We've been working on a model that produces queries that cause Z3 to diverge. On a hunch, I tried running the same .smt2 query with Z3's e-matching quantifier-instantiation strategy disabled, and it now returns a result in a (relatively) timely fashion.
If I understand correctly, checking formulas in FAU should really never be using e-matching anyways, right? Or is it supposed to be harmless to have it turned on anyways, and just assume it doesn't get used (or only gets used in an interleaved fashion with MBQI, or something)? Anyway, it appears to risk divergence to have it turned on, at least in some cases!
(Interestingly, this only works if I also run ivy with incremental=false, which I do not really understand the effects of in terms of quantifier instantiation -- or any other bit of Z3 internals -- but it at least does work then!)
We've been working on a model that produces queries that cause Z3 to diverge. On a hunch, I tried running the same
.smt2query with Z3's e-matching quantifier-instantiation strategy disabled, and it now returns a result in a (relatively) timely fashion.If I understand correctly, checking formulas in FAU should really never be using e-matching anyways, right? Or is it supposed to be harmless to have it turned on anyways, and just assume it doesn't get used (or only gets used in an interleaved fashion with MBQI, or something)? Anyway, it appears to risk divergence to have it turned on, at least in some cases!
(Interestingly, this only works if I also run ivy with
incremental=false, which I do not really understand the effects of in terms of quantifier instantiation -- or any other bit of Z3 internals -- but it at least does work then!)