c# - Z3 solver for string based constraints -

i trying use z3 solve string constraints using z3 c# api.

so far, have researched examples z3 seems support number based algebraic expressions such :

x > 0 y = x + 1  y < 3 

which can expressed using z3 c# api as:

using (context ctx = new context()) {     expr x = ctx.mkconst("x", ctx.mkintsort());     expr y = ctx.mkconst("y", ctx.mkintsort());     expr 0 = ctx.mknumeral(0, ctx.mkintsort());     expr 1 = ctx.mknumeral(1, ctx.mkintsort());     expr 3 = 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(); } 

is there way evaluate string based expressions such as:

string s1; string s2: string s3; s3=s1+s2; 

any string based constraints appreciated.

z3 not support strings primitive data-type. give z3-str try, though (https://github.com/z3str/z3-str).

there s3 system nus, described in ccs 2014.