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

Question

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

在python中，我想要的只是简单的str = String("a")。

Answer 1

试试看以下几点。

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