英文:
how to generate string const in z3 through java-api
问题
In z3's Java API, you can generate a string constant using ctx.mkString("a"). However, there is no direct equivalent to ctx.mkStringConst("a") as in Python.
英文:
How can I generate string const in z3 through java-api? For integer, there are ctx.mkInt(int a) generate an IntExpr with value a and ctx.mkIntConst("a") generate an IntExpr with name "a". However, for string, I can only find ctx.mkString("a"), which is just a SeqExpr with value "a" similar as ctx.mkInt. So what I want is something like ctx.mkStringConst("a") but there is no such function.
I find in python api, what I want is is simply str = String("a")
答案1
得分: 1
尝试以下。
String variable_name = "foo";
Expr variable = context.mkConst(context.mkSymbol(variable_name), context.mkStringSort());
<details>
<summary>英文:</summary>
Try the following.
String variable_name="foo";
Expr variable = context.mkConst(context.mkSymbol(variable_name), context.mkStringSort());
</details>
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论