z3 满足条件时激活表达式

Question

假设我有约束条件：[x > 2, y > 1, x < 10]，我想在 y==1 时添加条件 x%4 == 0 并获得所有结果，我在 Z3 中该怎么做？

我为解决的结果添加了阻塞约束并对其进行迭代以获得所有可能的 SAT 结果，但我发现它只会忽略值 y == 1.

下面是我用来测试的代码，它没有给出解决方案。

>>> x, y = Ints('x y')
>>> x = If(y == 1, x%4==0, x)
>>> F = [x > 2, y == 1, x < 10]
>>> solve(F)
no solution

Answer 1

这个呢？

from z3 import *

x, y = Ints('x y') 

s = Solver()

s.add(x > 2, y == 1, x < 10)
s.add(If(y == 1, (x % 4) == 0, True))

print(s.check())
print(s.model())

对于 y == 1，如果 (x % 4) == 0，则满足约束条件。否则，无论如何都会满足约束条件。

Answer 2

可以使用逻辑蕴涵：

Implies(y == 1, (x % 4) == 0)

这在语义上等同于@Axel Kemper 的回答，但我认为逻辑上更直接并且不需要 else 子句。（它还将 then 分支限制为布尔值，提供更多 type-safety。这在像 Python 这样所有内容都是动态类型的语言中很重要。）

z3 满足条件时激活表达式

z3 activate expression when conditions are met

python

z3