为什么不能将空字段中的值计数与整数进行比较?

合金只有有限的整数集,因为每个整数在寻找解时都相对昂贵。默认情况下,此集合为:

Int
  ┌──┬──┬──┬──┬──┬──┬──┬──┬─┬─┬─┬─┬─┬─┬─┬─┐⁻¹
  │-8│-7│-6│-5│-4│-3│-2│-1│0│1│2│3│4│5│6│7│  
  └──┴──┴──┴──┴──┴──┴──┴──┴─┴─┴─┴─┴─┴─┴─┴─┘  

当你做7+1时,你实际上得到-8!

试试看……只需在评估器中键入8:

 8
   -8

这实际上不局限于合金、C、C++、Java,大多数其他语言也一样,你通常没有注意到这一点是因为环绕点更高。对于一个Java int,它超过20亿。原因是这些整数存储为一组位。一旦达到最大值,加法就需要额外的位。由于该位不存在,因此将被静默忽略。(事实上,这是一个非常可怕的想法,到目前为止,我还没有见过任何处理这种溢出的代码。)

因此,当最大值为7时,合金中的默认值为,而实际使用的是8。 - 8 !

  # A.f < -8 

我们之所以有这样的恐惧,是因为在合金int中,当它被赋予sat解算器时,它也被打包在一个位集合中。

合金一直在与此斗争,有一个选择,以防止溢出。起初我以为这是天赐的礼物,但自从我意识到它是如何工作的,我就把它禁用了。问题是它删除了可能有效的解决方案。找到一个解决方案并不太糟糕,因为当没有任何解决方案时,您会注意到,但是对于断言来说,这是非常糟糕的,因为断言可能会说,当模型实际有解决方案时,没有任何解决方案。这让我发抖,因为我想依靠一个断言。考虑到实际的用例,我决定在我的模型中显式地处理溢出,因为它们实际上也是最终产品中的一个问题。许多已知的错误是由意外溢出引起的。所以隐藏它们的模型并不是很有用。

你是怎么处理的?它的语法有点奇怪。您必须指定 位宽 整数编码的。因此,您可以将模型更改为:

信号A F:单独A

check {
    no A.f =>
        # A.f < 8 
} for 5 int

这个 for 5 int 将SAT编码的位宽度设置为5位。5位=5^2=32。然后你得到整数-16..15。

这显然是一个巨大的绊脚石。幸运的是,为了使合金在SMT求解器上运行,正在进行着非常出色的工作。SMT溶剂将有一个更自然的数字处理合金,这不会绊倒你。

也就是说,如果您使用的常量整数不适合可用的int集,那么我至少可以尝试生成一个错误。也许你可以提交一个bug?