Z3：如何将 int 排序转换为 boolean 排序

【问题标题】：Z3: how to convert an int sort to a boolean sortZ3：如何将 int 排序转换为 boolean 排序
【发布时间】：2014-12-19 12:03:42
【问题描述】：

我想在Z3中将bitvector理论转化为int理论，遇到“bvnot”操作时，我把它换成“not”，这是一个简单的例子：

(assert (= (bvnot (ite (bvsle t0 #x0a) #b1 #b0)) #b1)) 改造后： (assert (= (not (ite (

然而，Z3 报告了这个断言的错误： not 的无效函数应用，位置 1 的参数排序不匹配，预期 Bool 但给定 Int

如何将 int 排序转换为 boolean 排序？坦克！

晋

【问题讨论】：

标签： z3 smt

【解决方案1】：

你已经准备好了所有东西，但是常量 1 和 0 不是布尔值；对应的值为true 和false，也就是说，这应该可以：

(assert (= (not (ite (< t0 10) true false)) true))

【讨论】：

是的，这行得通！但我想知道是否有一些转换函数可以将 int 排序转换为布尔排序，例如 int2bv 或 bv2int，它们将 int 排序和位向量相互转换。谢谢！
不，没有这样的功能，因为没有普遍认可的方式来执行这种转换，例如，不清楚 '3' 是否与 'true' 或 'false 相同'。在您的情况下，实现转换的首选方式与您所做的完全一样。（如果我们要将它作为一个函数添加，这正是我们内部要做的。）