"nested" data definitions

[nikivazou]

Can I define "nested" data definitions in z3, for example, I want to define a term that contains a predicate that contains a term, as follows:

(declare-datatypes (T) 
  (
    (Pred (predSelector (predValue T)))
    (Term (termPredSelector (termPredValue (Pred Term))))
  )
)

But I get the error

unknown sort `Pred`

In Haskell language, I want to encode the following data type

data Pred l 
  = Pred l

data Term l 
  = TPred (Pred (Term l))

[NikolajBjorner]

You can declare datatypes according to the SMTLIB 2.6 specification. This allows for nested datatypes. The spec is on http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf The syntax you use is a non-standard format that was introduced in Z3 long before this spec was introduced. It does not support nested datatypes.

[nikivazou]

Thanks @NikolajBjorner !

I tried to use the SMTLIB syntax to define List (copy-pasted from the spec you sent) and is not accepted by the ruse4fun Z3 version:

https://rise4fun.com/Z3/5TOcZ

I typed

(declare-datatypes ((List 1))  (
  ( par ( T ) ( ( nil ) ( cons ( car T ) ( cdr ( List T )) )))
))

and got Z3(1, 21): ERROR: invalid sort parameter, symbol or ')' expected

[LeventErkok]

Web version of Z3 is rather old (4.4.2 I think). If you try this on an a more recent version (4.8.0 for instance), you actually get:

(error "line 1 column 28: sort already defined List")

And the fix is easy: Once you rename List to MyList (or whatever you like), z3 4.8.0 accepts it just fine.

[NikolajBjorner]

Right. We keep pre defining List as polymorphic for convenience of the tutorial, but it can't be be redeclared.

[NikolajBjorner]

Is there something that should be fixed?

[nikivazou]

Nothing to be fixed. Thanks a lot!