Polymorphic Functions in SMTLIB2 / Z3

1
votes

Am I correct in understanding that one cannot create "polymorphic" functions in Z3 or SMTLIB2? e.g. I'd like to write something like:

(declare-fun Prop (A) Bool)
(declare-fun x1   ()  Int)
(declare-fun x2   ()  Bool)
(assert (and (Prop x1) (Prop x2)))

(I guess I can get something like this by declaring a union type for Int + Bool and then making Prop work for the union type, but wanted to double check first that it was not possible to use parametric polymorphism directly?)

Thanks!

1
z3smt

1 Answers

2
votes

That is indeed correct. SMTLib uses a many-sorted first-order logic; so in your example A can be any sort, but it has to be a known sort; not a type-parameter.

Having said that, SMTLib does allow uninterpreted sorts; that is, you can introduce new sorts with no underlying representation. (Just like uninterpreted functions.) Then, you can have injection functions to this sort, and sort of simulate what you want. (I know, bad pun.)

Here's an example how you can do that in your favorite language Ranjit: https://gist.github.com/LeventErkok/163362a59060188f5e62

When run, it generates the following SMT-Lib code, which shows what you'd need to generate yourself, give or take: https://gist.github.com/LeventErkok/920aba57cf8cb1810b4a

And here's the Haskell output for that very example:

Satisfiable. Model: x1 = 0 :: SInteger x2 = False

Of course, you can get fancy and query the SMT-solver for an interpretation of the uninterpreted-functions used during the construction; but none of that is natively supported by SMTLib. Though Z3 will give you a model if you ask it nicely, and if you're willing to parse the somewhat obscure and unfortunately non-standard output. Here it is for this example: https://gist.github.com/LeventErkok/54cee74eb3def22dfb5f

Also note that you'll in general need to give certain axioms on your injections; like they are one-to-one and disjoint from each other; which is also possible in SMTLib, though in general these will require quantifiers and thus might cause the solver to respond "unknown" since you go into the semi-decidable territory.