Z3 - mkInt() 与 mkIntConst()

Question

以下是等价的吗？

mkInt(3) 和 (IntExpr) mkIntConst("3")?

第二个不是创建一个名为“3”的整数常量，对吧？我想要的是使用mkIntConst 创建一个数值为3 的常量。有可能吗？

Answer 1

mkIntConst创建具有给定名称的符号值。 （所以在你的例子中，变量名为3，它确实不的值为3。

mkInt 使用该值创建一个常量。

所以是的，这些是完全不同的。

请看这里：https://z3prover.github.io/api/html/classcom_1_1microsoft_1_1z3_1_1_context.html#a99be64ea1573a49e683067bf6023ffa4

如果您想创建一个具有值3 的符号值，则使用mkIntConst 创建一个符号值，然后向求解器添加一个断言，表明它等于3。