Question : DataType To String Conversion

[gmCAD]

When building up a String Variable using Z3 variables (numeric) it is quite easy. Thanks to the API.

from z3 import *
s = Solver()
x, y, z = Ints('x y z')
s.add( x == 1, y == 2, z == x + y, String('output') == StringVal("prefix_") + IntToStr(z) + StringVal("_suffix"))
s.check()
>> sat
s.model()
>> [output = "prefix_3_suffix", z = 3, y = 1, x = 2]

The IntToStr function does the heavy lifting and correctly converts the 'z' Integer result to a String Object.

When dealing with DataTypes, how do you convert the DataType to a String?

Same example as before but this time using DataTypes (well really EnumSort).

from z3 import *
s = Solver()

Color, (red, green, blue) = EnumSort('Color', ('red','green', 'blue'))
c = Const('c', Color)

# How to do the Conversion From DataType To String???
s.add(c == green, String('Output') == StringVal("prefix_") + c + StringVal("_suffix") )
>>  Error !!!!

#Desired Output
[output = "prefix_green_suffix", c = green]

Any help would be greatly appreciated!!!

[NikolajBjorner]

There are no built-in functions that relate algebraic datatypes and strings.
You can define recursive functions over the API and the recursive function can walk an algebraic datatype and produce a string.
Reasoning becomes progressively involved, of course.

There is a use case of a recursive function here:

z3/src/api/python/z3/z3.py

Line 864 in 4c4810c

def RecAddDefinition(f, args, body):

Your color example does not require a recursive function definition, and can be handled directly:

def to_string(c):
      return If(c == green, "Green", If(c == red, "Red", "Blue"))

The recursive function version is:

to_string = RecFunction('to_string', Color, String)
c = Const('c', Color)
RecAddDefinition(to_string, c, If(c == green, "Green", If(c == red, "Red", "Blue")))

Or you can use to_string inside the definition of to_string

to_string = RecFunction('to_string', Color, String)
c = Const('c', Color)
RecAddDefinition(to_string, c, If(c == green, "Green", If(c == red, "Red", to_string(green))))

[gmCAD]

Thank you!