时间戳

首页 > 解决方案 > 说明 SMT 类型；变量截断中的错误？允许 Bool*Int

z3 - 说明 SMT 类型；变量截断中的错误？允许 Bool*Int

问题描述

我有以下问题：

A. 如果我有一个变量 x，我声明它（案例 1）为 Bool（案例 2）为 Int 并断言 x=0 或 x=1（案例 3）为 Int 并声明 0<=x<= 1. 在每种情况下，Z3 或者更普遍的 SMT 会发生什么？由于事情发生在 SAT 而不是 SMT 级别，是否需要（案例 1）？你这里有一些参考文件吗？

B. 我在 Python 中有以下语句（用于使用 Z3 Python API）

    tmp.append(sum([self.a[i * self.nrVM + k] * componentsRequirements[i][1] for i 
    in range(self.nrComp)]) <= self.MemProv[k])

其中 a 被声明为 Z3 Int 变量（0 或 1），componentsRequirements 是一个 Python 变量，它被视为浮点数，self.MemProv 被声明为 Z3 Real 变量。

奇怪的是，对于 componentsRequirements 的浮点值，例如 0.5，求解器构建的约束将其视为 0 而不是 0.5。例如在：

    (assert (<= (to_real (+ 0 (* 0 C1_VM2)
            (* 0 C2_VM2)
            (* 2 C3_VM2)
            (* 2 C4_VM2)
            (* 3 C5_VM2)
            (* 1 C6_VM2)
            (* 0 C7_VM2)
            (* 2 C8_VM2)
            (* 1 C9_VM2)
            (* 2 C10_VM2)))
StorageProv2))

上面的 0 实际上应该是 0.5。当将 a 更改为 Real 值时，会考虑浮点数，但我们承认这是因为 a 的语义。我尝试在 a 和 componentsRequirements 之间使用交换性，但没有成功。

C. 如果我想使用 x 作为 Bool 类型并将其乘以一个 Int，我当然会在 Z3 中得到一个错误（Bool*Real/Int not allowed）。有没有办法克服这个问题，但保持两个乘数的类型？在这个意义上的一个例子是上面的（a - Bool, componentsRequirements - Real/Int）： a[i * self.nrVM + k] * componentsRequirements[i][1]

谢谢

标签： z3smtz3py

解决方案

关于A

帕特里克对此给出了很好的解释。在实践中，你真的必须尝试看看会发生什么。由于启发式何时/如何开始，不同的问题可能会表现出不同的行为。我认为这里没有一般的经验法则。我个人的偏好是将布尔值保留为布尔值并根据需要进行转换，但这主要是从编程/维护的角度来看，而不是从效率的角度来看。

关于B

您的“除法”被截断问题很可能与此相同：检索 Z3Py 中的值会产生意外结果

你可以是明确的和写的1.0/2.0等等；或使用：

 from __future__ import division

在程序的顶部。

关于C

SMTLib 是一种强类型语言；你不能乘以一个布尔值。您必须先将其转换为数字。类似的东西(* (ite b 1 0) x)，b你的布尔值在哪里。或者您可以编写一个自定义函数来为您执行此操作并调用它；就像是：

(define-fun mul_bool_int ((b Bool) (i Int)) Int (ite b i 0))
(assert (= 0 (mul_bool_int false 5)))
(assert (= 5 (mul_bool_int true 5)))

推荐阅读