z3 - 2つのboolexprが等しいかどうか

Question

2つのboolexprb1、b2が与えられたと言う

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

Z3用の.netAPIを使用して、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