search

prove-rs / z3.rs

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

model value extraction #219

Open AdamGlass opened 1 year ago

AdamGlass commented 1 year ago

Is there a way to get value assignments out of the model without having a reference to the variable handy?

Basically i built a Int expression during a recursive process and one of the children created an integer variable. I build my computation, get Optimize to do its thing and get a model. I can print the model and see the solution including the variable name. Model::Eval wants that variable reference. Is there another way to get that reference by name after the fact? Or to enumerate the variables. An alternative is to clearly thread the the reference through the recursion but I'll take something simpler if i can get it.

thanks, Adam

HKalbasi commented 1 year ago

If the variable has name, wouldn't Int::new_const("name") work?

AdamGlass commented 1 year ago

I was worried it had to be a reference to the same instance.

HKalbasi commented 1 year ago

It would be the case if you use fresh_const, but with new_const you just need to pick the same name.