如何通过java-api在z3中生成字符串const [关闭]

Question

如何在 z3 中通过 java-api 生成字符串 const？对于整数，ctx.mkInt(int a) 生成一个值为 a 的 IntExpr，ctx.mkIntConst("a") 生成一个名为“a”的 IntExpr。但是，对于字符串，我只能找到ctx.mkString("a")，它只是一个 SeqExpr，其值为“a”，类似于 ctx.mkInt。所以我想要的是类似ctx.mkStringConst("a") 但没有这样的功能。

我在python api中找到，我想要的只是str = String("a")

Answer 1

试试下面的。

String variable_name="foo";
Expr variable = context.mkConst(context.mkSymbol(variable_name), context.mkStringSort());