z3relationsmtsat-solvers

Can we define relations in Z3?

I am new to z3 SMT solver. I need to define a relation, instead of a function. I mean a function that can return more than one value. I looked up the tutorial, and couldn't find anything. I appreciate if you can help me in this regard.

Thanks a lo.

Solution

  • Use one of the logics that supports the ArrayEx theory, which provides the Array sort and associated functions for manipulating arrays. You can then have your functions return array values which can contain arbitrarily many Ints or Bools or whatever.

    This SMT tutorial is a good resource that gathers many SMT details into one place.