Allow user to customize drivers
Here is a short example of what a user of Why3 may want to do, but can't do it easily for the moment. Imagine I want to add a new symbol, that could have been already in Why3 stdlib but it is not. Say for example I want to add operators that given a bitvector of size 16, return the two bytes it is made of. As a user, I can define my own theory, say bvmisc.mlw
, containing
theory T
use bv.BV8
use bv.BV16
function lsb BV16.t : BV8.t
function msb BV16.t : BV8.t
end
For my examples, I can import my own lib, using option -L
for example. But in this case, I know that solvers like Z3 or CVC4 can support these operators very nicely. So I would like to make an complement to their drivers. I can design my own driver file, say my.drv
, containing
theory bvmisc.T
syntax function lsb "((_ extract 7 0) %1)"
syntax function msb "((_ extract 15 8) %1)"
end
But then how am I supposed to tell why3, either for commands prove
or ide
, that I would like this driver addition to be used by my Z3 or CVC4? I couldn't find any satisfactory solution.
- the
-extra-config
option is poorly documented, and trying to use with a file, saymy.conf
, containing
[prover_modifiers]
prover = "CVC4"
driver = "my.drv"
does not seem to do anything. Is it supposed to work?
- What other alternative do I have?