prove-rs / z3.rs

Rust bindings for the Z3 solver.
347 stars 110 forks source link

Exposing application parameters #238

Open dp1 opened 1 year ago

dp1 commented 1 year ago

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.

dp1 commented 1 year ago

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