CODEWITHSUNDEEP
c#z3
Priyanka
Priyanka

Reputation: 418

Z3 solver for string based constraints

I am trying to use Z3 to solve string constraints using Z3 C# API.

So far, i have researched examples but Z3 seems to support only number based algebraic expressions such as :

x > 0
y = x + 1 
y < 3

which can be 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 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();
}

Is there any way to evaluate string based expressions such as:

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

Any help with string based constraints will be appreciated.

Upvotes: 2

Views: 2867

Answers (2)

vanbastelaer
vanbastelaer

Reputation: 398

Note that Z3 supports String type now with some limitations. Reference here: Z3 solver for string based constraints

Upvotes: 0

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

Z3 does not by itself support strings as a primitive data-type. You could give z3-str a try, though (https://github.com/z3str/Z3-str).

There is also the S3 system from NUS, described in ccs 2014.

Upvotes: 1

Related Questions