-
Notifications
You must be signed in to change notification settings - Fork 102
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Constructing an uninterpreted sort value? #190
Comments
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
My apologies if I am driving z3.rs incorrectly; I'm new to Rust and this library, and reasonably new to SMT solvers in general. Please let me know if my question is nonsense!
I'd like to write code in z3.rs more or less equivalent to the following smt2 code:
In Python, I'd probably do it like so:
Defining a new sort and the lock_msg function in Rust-land is reasonably straightforward, but in order to construct the universal I need to be able to supply bounds and a pattern, which seems to necessitate constructing an uninterpreted value as I did in Python. Thinking that
ast::Datatype::new_const
would do the trick, I wrote something like the following:Constructing n1 panics, however:
So, clearly
Datatype
is the wrong module to be pullingnew_const
from. However, no such function exists inuninterpreted
. Is this something that is missing from the library, am I just missing where it is, or, am I totally out to lunch in general?Thanks for your time.
The text was updated successfully, but these errors were encountered: