Modelling generic datatypes for Z3 and or SMT(v2.6)

Question

I would like to model the behaviour of generic datatypes in SMT v2.6. I am using Z3 as constraint solver. I modelled, based on the official example, a generic list as parameterised datatype in the following way:

(declare-datatypes (T) ((MyList nelem (cons (hd T) (tl MyList)))))

I would like the list to be generic with respect to the datatype. Later on, I would like to declare constants the following way:

(declare-const x (MyList Int))
(declare-const y (MyList Real))

However, now I would like to define functions on the generic datatype MyList (e.g., a length operation, empty operation, ...) so that they are re-usable for all T's. Do you have an idea how I could achieve this? I did try something like:

(declare-sort K)
(define-fun isEmpty ((in (MyList K))) Bool
    (= in nelem)
)

but this gives me an error message; for this example to work Z3 would need to do some type-inference, I suppose.

Would be great if you could could give me a hint.

alias alias · Accepted Answer · 2017-12-03T22:10:49

SMT-Lib does not allow polymorphic user-defined functions. Section 4.1.5 of http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf states:

Well-sortedness checks, required for commands that use sorts or terms, are always done with respect to the current signature. It is an error to declare or define a symbol that is already in the current signature. This implies in particular that, contrary to theory function symbols, user-defined function symbols cannot be overloaded.

Which is further expanded in Footnote-29:

The motivation for not overloading user-defined symbols is to simplify their processing by a solver. This restriction is significant only for users who want to extend the signature of the theory used by a script with a new polymorphic function symbol—i.e., one whose rank would contain parametric sorts if it was a theory symbol. For instance, users who want to declare a “reverse” function on arbitrary lists, must define a different reverse function symbol for each (concrete) list sort used in the script. This restriction might be removed in future versions.

So, as you suspected, you cannot define "polymorphic" functions at the user level. But as the footnote indicates, this restriction might be removed in the future, something that will most likely happen as SMT-solvers are more widely deployed. Exactly when that might happen, however, is anyone's guess.

Modelling generic datatypes for Z3 and or SMT(v2.6)

1 Answers