z3 - 两个 boolexpr 是否相等

Question

给定两个 boolexpr b1,b2 说

b1=x1>=4&&x2>=5
b2=x2>=5&&x1>=4

我们可以使用 Z3 的 .net API 来了解 b1 和 b2 是否实际上是相同的约束？)（意思是b1和b2允许的x1和x2的值是一样的）

Answer 1

是的。你想证明 b1 等于 b2，你可以通过证明 b1 == b2 的否定是不可满足的。这是一个示例，展示了如何在 Z3Py 中执行此操作，您可以在 .NET API 中使用基本相同的步骤：http ://rise4fun.com/Z3Py/M4R1

x1, x2 = Reals('x1 x2')

b1=And(x1>=4, x2>=5)
b2=And(x2>=5, x1>=4)

s = Solver()
proposition = b1 == b2 # assertion is whether b1 and b2 are equal
s.add(Not(proposition))
# proposition proved if negation of proposition is unsat
print s.check() # unsat 

b1=And(x1>=3, x2>=5) # note difference
b2=And(x2>=5, x1>=4)
s = Solver()
proposition = b1 == b2
s.add(Not(proposition))
print s.check() # sat