Skip to content
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

Open
dijkstracula opened this issue Apr 12, 2022 · 0 comments
Open

Constructing an uninterpreted sort value? #190

dijkstracula opened this issue Apr 12, 2022 · 0 comments

Comments

@dijkstracula
Copy link

dijkstracula commented Apr 12, 2022

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-sort Node 0)
(declare-fun lock_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)))

In Python, I'd probably do it like so:

node = z3.DeclareSort('node')
lock_msg = z3.Function('lock_msg', node, z3.BoolSort())

N1, N2 = z3.Consts('N1 N2', node)
s.assert(z3.Forall([N1, N2], z3.Implies(z3.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:

    let node_sort = z3::Sort::uninterpreted(&ctx, z3::Symbol::from("node"));
    let lock_msg = z3::FuncDecl::new(&ctx, "lock_msg", &[&node_sort], &z3::Sort::bool(&ctx));

...
    let n1 = z3::ast::Datatype::new_const(&ctx, "N1", &node_sort);
    let n2 = z3::ast::Datatype::new_const(&ctx, "N2", &node_sort);

    let n1_n2_pattern = z3::Pattern::new(&ctx, &[&n1, &n2]);
...
        &z3::ast::forall_const(&ctx, &[&n1, &n2], &[&n1_n2_pattern], 
            &z3::ast::Bool::and(&ctx, &[&lock_msg.apply(&[&n1]).as_bool().unwrap(),
                                    &lock_msg.apply(&[&n2]).as_bool().unwrap()])
                .implies(&n1._eq(&n2)))

Constructing n1 panics, however:

thread 'main' panicked at 'assertion failed: `(left == right)`
  left: `Uninterpreted`,
 right: `Datatype`', /Users/ntaylor/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-0.11.2/src/ast.rs:1641:9

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant