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

【问题标题】：Z3 solver for string based constraints用于基于字符串的约束的 Z3 求解器
【发布时间】：2023-03-22 15:57:02
【问题描述】：

我正在尝试使用 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;

任何有关基于字符串的约束的帮助将不胜感激。

【问题讨论】：

标签： c# z3

【解决方案1】：

Z3 本身并不支持将字符串作为原始数据类型。不过，你可以试试 z3-str (https://github.com/z3str/Z3-str)。

还有来自 NUS 的 S3 系统，在 ccs 2014 中进行了描述。

【讨论】：

【解决方案2】：

请注意，Z3 现在支持 String 类型，但有一些限制。参考这里：Z3 solver for string based constraints

【讨论】：