两个 boolexpr 是否相等答案

【问题标题】：Whether two boolexpr are equal两个 boolexpr 是否相等
【发布时间】：2012-09-05 13:59:26
【问题描述】：

给定两个布尔表达式 b1,b2 说

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

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

【问题讨论】：

标签： z3

【解决方案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

【讨论】：