Python API (seems to be) missing string to code conversions

[LeventErkok]

I don't seem to be able to find the Python functions corresponding to code conversion:

       ; (str.to_code s) is the code point of the only character of s, 
       ; if s is a singleton string; otherwise, it is -1. 
       (str.to_code String Int) 

       ; (str.from_code n) is the singleton string whose only character is
       ; code point n if n is in the range [0, 196607]; otherwise, it is the 
       ; empty string.
       (str.from_code Int String) 

Are these missing from the Python API? (Or maybe they're there but named differently. I wasn't able to locate.)

[NikolajBjorner]

At this point you can do

CharToInt(S[0]) 
If(And(0 <= N, N <  196607), Unit(CharFromBv(Int2BV(N, 17))), "")

These functions, str.to_code and str.from_code came several years after initial functionality and were initially not supported.
So were not exposed of the API so far.

[LeventErkok]

Alas, these don't seem to be available from Python either:

$ ag CharToInt
src/api/java/Context.java
2289:        return (IntExpr) Expr.create(this, Native.mkCharToInt(nCtx(), ch.getNativeObject()));

src/api/dotnet/Context.cs
2710:        public IntExpr CharToInt(Expr ch)
$ ag CharFromBV
src/api/dotnet/Context.cs
2728:        public Expr CharFromBV(BitVecExpr bv)

Looks like CharToInt is available in Java and C#, and CharFromBV is only available in C#.

[LeventErkok]

I should add there's really no urgency on this; though of course it'd be nice to have them in due course.

[NikolajBjorner]

They were added yesterday or the day before yesterday in response to a different issue

[NikolajBjorner]

You can now

print(StrFromCode(65), simplify(StrFromCode(65)))
print(StrToCode("A"), simplify(StrToCode("A")))

and see

str.from_code(65) "A"
str.to_code("A") 65

[LeventErkok]

Thanks! These do work nicely indeed..