时间戳

首页 > 解决方案 > 变量是否有最大值大小？

z3 - 变量是否有最大值大小？

问题描述

假设我有以下（故意简单的）约束小节：

..... SOME STUFF .....

(declare-const I Int)
(assert (and (>= I 0) (<= I 1)))

(define-fun W () Int
    2251799813685248
)

..... MORE STUFF .....

(maximize (* I W))
(check-sat)
(get-model)

我给 W 的尺寸是不是太大了？或者更一般地说，Z3 中是否可以分配最大大小值（例如，如果变量存储为常规 ints/floats/longs/etc 而不是可变精度）？

标签： z3

解决方案

一个Int值对应于一个数学整数。它可以是任意大小。没有最大值。

对于调整大小的版本，您应该使用 bit-vectors:(_ BV n)是 size 的位向量的类型n，它遵循机器算术规则。

推荐阅读