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
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
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
ide, that I would like this driver addition to be used by my Z3 or CVC4? I couldn't find any satisfactory solution.
-extra-configoption is poorly documented, and trying to use with a file, say
[prover_modifiers] prover = "CVC4" driver = "my.drv"
does not seem to do anything. Is it supposed to work?
- What other alternative do I have?