search

prove-rs / z3.rs

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

[Feature Request] Reading AST of uninterpreted functions from models. #213

Open daemontus opened 2 years ago

daemontus commented 2 years ago

Hi!

I am looking to somehow retrieve the information about uninterpreted functions produced as part of a Model object in some concise manner.

At the moment, I can "reconstruct" the function input-by-input by running Model::eval, but this is tedious at best (for finite domains) and impossible at worst (for infinite domains).

I noticed z3-sys has some low level representation for this (Z3_func_interp) which isn't exposed in z3 yet. I'd be perfectly happy to write a PR with a wrapper for it myself (and maybe also wrap some other utility methods of the Model struct).

I just wanted to ask whether such PR would be welcome (e.g. there isn't already a larger work-in-progress which implements this) and whether there are any possible issues that you can foresee arising while implementing this?

Pat-Lafon commented 1 year ago

Hey @daemontus, is this something you ever pursued? I find myself interested in this kind of functionality

daemontus commented 1 year ago

Not yet :( I still have it on my todo list, but unfortunately it hasn't really been a priority and I'm not quite sure how soon it will be. So if you have the need and the time, feel free to go for it :D