What's the difference between interpreted and uninterpreted function in Z3?

0
votes

While reading Fast LCF-style proof reconstruction for Z3 I read that there are interpreted functions like + or forall in Z3's language. I guess there are also uninterpreted functions. What's the difference between the two?

1
z3

1 Answers

2
votes

They are functions that have a name and signature but no definition, see Uninterpreted Function.