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

Constructing an uninterpreted sort value?

Open dijkstracula opened this issue 2 years ago • 0 comments

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.

dijkstracula avatar Apr 12 '22 19:04 dijkstracula