Custom datatypes [dReal v3.16.04.01] [OSX 10.11.4]

[Nikh13]

Hi,

I have recently moved to dReal from z3 due to its obvious advantage dealing with non-linear theories. However, for some of the problems I have been working on, I wish to declare functions with a non-numeric(i.e string or character) domain.

For e.g in z3: (declare-datatypes () ((State stopped running))) was a supported statement which declared the datatype State with the domain {stopped,running}.

I could then simply declare a function as (declare-fun currentState () State)

and it would set the domain for currentState to {stopped,running}

Is there any way to declare such custom datatypes in dReal as well?

[soonho-tri]

Hi @Nikh13,

Unfortunately, we don't support declare-datatypes. As far as I know, it's an experimental feature which possibly will be included in the next standard of SMTLIB.

We do support Bool, Int, and Real sorts. I think you may encode the datatype using two Bool variables.