如何解决使用 Z3 产生整数结果的整数除法?

Posted

技术标签:

【中文标题】如何解决使用 Z3 产生整数结果的整数除法?【英文标题】:How to solve integer divisions that produces integer result using Z3? 【发布时间】:2021-11-30 20:22:36 【问题描述】:

假设我有一个 z3 表达式:

c = z3.Int("x")
Expr = (-c) / 2

是否可以使用 Z3 找到任何 C 以使表达式计算为整数?

例如,如果 c==1,则整个方程的计算结果应为 -0.5,因此不是整数。

我尝试使用提醒==0 方法对问题进行建模

>>> from z3 import *
>>> c = Int("c")
>>> s = Solver()
>>> s.add(((-c) %2)==0)
>>> s.check()
sat

这显然是不正确的。更改为 c = Real("c") 会出现异常:

>>> c = Real("c")
>>> s = Solver()
>>> s.add(((-c) %2)==0)

Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/usr/local/lib/python3.9/site-packages/z3/z3.py", line 2539, in __mod__
    _z3_assert(a.is_int(), "Z3 integer expression expected")
  File "/usr/local/lib/python3.9/site-packages/z3/z3.py", line 112, in _z3_assert
    raise Z3Exception(msg)
z3.z3types.Z3Exception: Z3 integer expression expected

【问题讨论】:

【参考方案1】:

% 超过整数将被评估为整数余数;所以你提出的实际上工作得很好:

from z3 import *

c = Int("c")
s = Solver()
s.add(((-c) %2)==0)
print(s.check())
print(s.model())

打印出来:

sat
[c = 2]

事实上,模型说c 可以是整数2,而-c%2 将是0,正如人们所期望的那样。

如果您还添加c1 的断言:

from z3 import *

c = Int("c")
s = Solver()
s.add(((-c) %2)==0)
s.add(c == 1)
print(s.check())

然后你得到:

unsat

正如预期的那样。所以,这一切都按要求工作。或许你想问点别的?

【讨论】:

谢谢,现在我明白了。我最初将这些概念误解为“如果它说 sat,那么每个可能的 val 都应该 sat”而不是“必须有一个满足的值,而其他的可能不满足”

以上是关于如何解决使用 Z3 产生整数结果的整数除法?的主要内容,如果未能解决你的问题,请参考以下文章

无论结果如何,支持除以零的最快整数除法是啥?

如何对整数除法的结果进行四舍五入?

如何在 Java 中舍入整数除法并获得 int 结果? [复制]

如何在 C# 中计算整数的除法和模数?

整数除以小数的结果是啥?

python3使除法结果为整数