时间戳

首页 > 解决方案 > 如何解决使用 Z3 产生整数结果的整数除法？

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

问题描述

假设我有一个 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

标签： z3smt

解决方案

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

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人们所期望的那样。

c如果您还添加以下断言1：

from z3 import *

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

然后你得到：

unsat

正如预期的那样。所以，这一切都按要求工作。也许你想问别的？

推荐阅读