基于字符串约束的Z3求解器

我正在尝试使用Z3 c# API来解决字符串约束。

到目前为止，我已经研究了一些例子，但Z3似乎只支持基于数字的代数表达式，如:

x > 0
y = x + 1 
y < 3

可以用z3 c# API表示为:

using (Context ctx = new Context())
{
    Expr x = ctx.MkConst("x", ctx.MkIntSort());
    Expr y = ctx.MkConst("y", ctx.MkIntSort());
    Expr zero = ctx.MkNumeral(0, ctx.MkIntSort());
    Expr one = ctx.MkNumeral(1, ctx.MkIntSort());
    Expr three = ctx.MkNumeral(3, ctx.MkIntSort());
    Solver s = ctx.MkSolver();
    s.Assert(ctx.MkAnd(ctx.MkGt((ArithExpr)x, (ArithExpr)zero), ctx.MkEq((ArithExpr)y, 
        ctx.MkAdd((ArithExpr)x, (ArithExpr)one)), ctx.MkLt((ArithExpr)y, (ArithExpr)three)));
    Console.WriteLine(s.Check());
    Model m = s.Model;
    foreach (FuncDecl d in m.Decls)
            Console.WriteLine(d.Name + " -> " + m.ConstInterp(d));
    Console.ReadLine();
}

是否有方法计算基于字符串的表达式，如:

string S1;
string S2:
string S3;
S3=S1+S2;