时间戳

首页 > 解决方案 > 使用 z3Py 证明两个表达式范围的等价/不同

python - 使用 z3Py 证明两个表达式范围的等价/不同

问题描述

from z3 import *

s = Solver()

a, b = Ints("a b")
s.add(a > 2)
s.add(b > 0)
s.add(Or(Exists(a, ForAll(b, a != b)), Exists(b, ForAll(a, a != b))))

s.check() # print "unsat"

我试图证明 和 范围的a差异b。这可以通过定位超出范围的b值的赋值来完成。1a

但是，上面的程序给出了意想不到的unsat. 我想知道为什么以及是否有更有效的方法来实现这一目标。

标签： pythonz3

解决方案

ForAll确切的意思是：所有数字，即Exists(a, ForAll(b, a != b))始终为假，因为没有Int与所有Ints 不同的东西，因此第三个断言本身是不可满足的。你想要类似的东西s.add(Exists(a, (Exists (b, And(Not(a > 2), b > 0)))))。

另外，请注意您使用了两个不同的aand b。Exists(a, ...)不会对现有变量进行量化，但会引入一个新变量，该变量被意外称为与您的 global (existential) 同名的a, b.

推荐阅读