z3.rs icon indicating copy to clipboard operation
z3.rs copied to clipboard

Published 20 hours ago • verified publisher icon prove-rs

Implement constructing consts of an uninterpreted sort

Open dijkstracula opened this issue 2 years ago • 3 comments

My attempt at addressing https://github.com/prove-rs/z3.rs/issues/190 .

dijkstracula avatar Apr 21 '22 22:04 dijkstracula

Is a new ast type needed? I think a new_const function for Dynamic would do the job.

HKalbasi avatar Dec 21 '22 13:12 HKalbasi

Apologies, I've been ignoring my github notifications over the break. Do you mean that as_uninterpreted() and new_const() should return a Dynamic, removing the new Rust datatype? If you prefer that I can make that change.

dijkstracula avatar Jan 04 '23 22:01 dijkstracula

I don't really understand the need for as_uninterpreted(), since it doesn't enable anything more than Dynamic itself. Do you have a specific use case? For example in case of as_int(), you will get a Int, which you can add it to other Ints or call Int specific functions on it, but there isn't such functions on Uninterpreted. So I think it is possible to remove Uninterpreted and as_uninterpreted without losing functionality.

HKalbasi avatar Jan 04 '23 23:01 HKalbasi