满足条件时，z3会激活表达式

问题描述

假设我有约束条件：[x > 2,y > 1,x < 10]，并且我想在x%4 == 0时添加条件y==1，并获得所有结果，我该如何在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

解决方法

那呢？

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，则满足约束。 否则，无论如何都会满足约束条件。

,

您可以使用逻辑含义：

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

从语义上讲，它等效于@Axel Kemper的答案，但我认为从逻辑上讲是更直接的，不需要else子句。 （这也将then分支限制为布尔值，从而提供了更多的类型安全性。这对于像Python这样可以动态键入所有内容的语言非常重要。）