z3.rs
z3.rs copied to clipboard
Exposing application parameters
It would be useful to expose application parameters, such as the high
and low
limits of a Z3_OP_EXTRACT
.
The python bindings expose them with a params()
method on FuncDeclRef
, which may be a good way here as well.
For my specific application I only need access to integer parameters (for extract, zero and sign extend), but it makes sense to think of the other parameter types too. I may have time to work on this, but I don't have a clear idea of what would be a good api to expose.
A little followup, I implemented a possible API for this over at dp1/z3.rs/decl-params.
I wrapped the possible result types in a DeclParam
enum, and the intention is that accessing a parameter would work like this (ast
here is a Dynamic
):
if ast.is_app() && ast.decl().kind() == DeclKind::ZERO_EXT {
let DeclParam::Int(amt) = ast.decl().nth_param(0).unwrap() else { unreachable!(); };
println!("ZeroExt by {amt} bits");
}
If there's any interest I can open a PR for it, or rework it if there's a better solution