Z3 API Parametric datatypes, how?

Apr 30, 2014 at 3:39 PM
Edited Apr 30, 2014 at 7:59 PM

i'm using Z3 for my phd thesis. In a first attempt i just used the smtlibparse function for convenience since i had my formulas converted to smtlib format.

Now I wanted to use the api, since converting formulas to smtlib formated strings, and then parse them with z3 is a bit cumbersome and has slow performance.

I started to look at the api and I couldn't found how I can define parametric datatypes like this one

"(declare-datatypes (T) ((Ref (mk-ref (inner T)))))"

I would appreciate your help,


Edit: I've read that I should post this kind of questions in Stackoverflow. I've done that now, sorry for the mistake, thanks