Search code examples
z3smtformal-languagesformal-verification

How to model struct in z3?

Given a struct like this:

struct MyStruct {
uint[10] a;
uint b;
bool c;
};
Mystruct m;

My problem is how to model variable m using z3? a trivial solution is to split m into multiple variables: m.a, m.b, m.c. However, it is not extensible (in my opinion). Are there any better solution supported by z3 ? thanks!

I am trying to model struct in z3 !

Solution

  • The standard way to do this in SMTLib is to use datatypes. See Section 4.2.3 of https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf. Here's the "pair" example from that document:

    (declare-datatypes ((Pair 2)) ((par (X Y) ((pair (first X) (second Y))))))

    Note that the above is parametric, i.e., it allows you to create pairs with differing types in them. You can monomorphize it:

    (declare-datatypes ((Pair 0)) ((pair (first int) (second bool)))

    and use the tags a/b/c etc. to add your own fields with the types you want. See the SMTLib document for details.

    If you are using a higher-level API (like that from Haskell, Python, Scala) etc; they might provide easier ways to do the same; you need to check their own documentation. In particular, if you're using z3py, See https://ericpony.github.io/z3py-tutorial/advanced-examples.htm, in the section titled "Datatypes."

    Note that SMTLib/z3 structs can even be recursive, i.e., the fields can contain values of type that you are defining. You can even make mutually recursive datatypes. It seems you do not need those facility here, but the same mechanism should work for you just fine.