Apr 30, 2014 at 2:39 PM
Edited Apr 30, 2014 at 6: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