You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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:
(declare-sortNode0)
(declare-funlock_msg (Node) Bool)
; mutual exclusion: no two clients think they hold the lock simultaneously
(assert (forall ((n1 Node) (n2 Node))
(=> (and (lock_msg n1) (lock_msg n2)) (= n1 n2)))
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:
So, clearly Datatype is the wrong module to be pulling new_const from. However, no such function exists in uninterpreted. 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:
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: