两个 boolexpr 是否相等 [英] Whether two boolexpr are equal

问题描述

给定两个 booleexpr b1,b2说

Given two boolexpr b1,b2 say

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

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

Can we use .net API for Z3 to know whether b1 and b2 are actually the same constraint? )(meaning that the value of x1 and x2 allowed by b1 and b2 are the same)

推荐答案

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

Yes. You want to prove that b1 equals b2, which you can do by showing the negation of b1 == b2 is unsatisfiable. Here's an example showing how to do this in Z3Py, and you can use basically the same steps in the .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

这篇关于两个 boolexpr 是否相等的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！