relation vs function

Stream: Veil

[Mark R. Tuttle]

Could you add guidance in the State and Theory Components section of the documentation on how to choose between a relation and a function?

In your blog post example FloodSet, for example, you use relation decision : node → value → Bool where I would have used function decision: node -> value so I don't have to prove that decisions are unique.

I think the answer is going to be that SMT somehow performs better with relations than with functions, so the proof overhead is worth it.

[George Pîrlea]

Will do!

The gist is to always use a relation if you can. A function, if you think about it, is a relation r with the two following assumptions:

invariant [coherence] ∀ x y z, r x y ∧ r x z → y = z
invariant [totality] ∀ x, ∃ y, r x y

A relation with just the coherence axiom is a partial function. If that is good enough for modelling your state, you should use that.

I think the answer is going to be that SMT somehow performs better with relations than with functions.

Yes. The totality assumption potentially takes your specification outside the decidable fragment of first order logic.

A function is equivalent to a ∀∃ quantifier alternation (intuition: ∀∃ introduces a Skolem function in the solver), which solvers can struggle with in some cases.

You can find more details at: https://microsoft.github.io/ivy/decidability.html