I have a context with only the following datatype declaration:
EnumSort signal = ctx.mkEnumSort("signal", "red", "yellow", "green");
What I want is to get an equivalent SMTLIB representation of the above declaration, something like the following:
(declare-datatypes () ((signal red yellow green)))
How do I convert this? I tried creating a solver for this context and then doing solver.toString() but it doesn't print anything unless I use this declaration in an assertion.
You can only convert to smtlib from a Solver (or Optimize) object. Think of context as a "manager" of sorts, that is independent of smt-lib or any particular representation. And you are correct that you'll have to assert something about this object, which is rather annoying.
Having said that, internally your signal value will be stored as a Sort object: https://z3prover.github.io/api/html/classz3_1_1sort.html. (In your case, whatever the Java equivalent of this class is.) In theory, one can then scrutinize this object to figure out it's a datatype, get the constructors etc., to do the translation by hand; but that'll be quite representation dependent and likely to be error-prone in the long run.