Z3Py在動態網絡中檢查信念的例子

Question

爲了更好地理解Z3（或更具體的Z3Py），我想實現紙Checking Beliefs in dynamic Networks中的直接示例。

這是我工作的代碼：

from z3 import * 

fp = Fixedpoint() 

dst = BitVec('dst', 3) 
src = BitVec('src', 3) 
dst_next = BitVec('dst_next', 3) 
src_next = BitVec('src_next', 3) 

fp.declare_var(dst, src, dst_next, src_next) 

rels = {} 

for c in ['A', 'R1', 'R2', 'R3', 'B', 'D']: 
    f = Function(c, BitVecSort(3), BitVecSort(3), BoolSort()) 
    rels[c] = f 
    fp.register_relation(f) 
    fp.set_predicate_representation(f, 'doc') 

# Guards 
g12 = And(Extract(2, 1, dst) == 0b10, Extract(2, 1, dst) == 0b01) 
g13 = And(Not(g12), Extract(2, 2, dst) == 0b1) 
g2b = Extract(2, 1, dst) == 0b10 
g3d = Extract(2, 2, src) == 0b1 
g32 = And(Not(g3d), Extract(2, 2, dst) == 0b1) 
ld = And(src_next == src, dst_next == dst) 
set0 = And(src_next == src, dst_next == dst & 0b101) 

# Relations 
fp.rule(rels['R1'](dst_next, src_next), And(rels['R2'](dst, src), g12, ld)) 
fp.rule(rels['R1'](dst_next, src_next), And(rels['R3'](dst, src), g13, ld)) 
fp.rule(rels['R2'](dst_next, src_next), And(rels['B'](dst, src), g2b, ld)) 
fp.rule(rels['R3'](dst_next, src_next), And(rels['D'](dst, src), g3d, ld)) 
fp.rule(rels['R3'](dst_next, src_next), And(rels['R2'](dst, src), g32, set0)) 
fp.rule(rels['A'](dst, src), rels['R1'](dst, src)) 

fp.fact(rels['B'](dst, src)) 

#print(fp) 
print(fp.query(rels['A'](dst, src))) 
print(fp.get_answer()) 

此打印正確的答案：

sat 
Or(And(Var(0) == 5, Var(1) == 2), 
    And(Var(0) == 4, Var(1) == 2), 
    And(Var(0) == 4, Var(1) == 3), 
    And(Var(0) == 5, Var(1) == 1), 
    And(Var(0) == 4, Var(1) == 0), 
    And(Var(0) == 5, Var(1) == 3), 
    And(Var(0) == 5, Var(1) == 0), 
    And(Var(0) == 4, Var(1) == 1)) 

所以我的問題是現在可以Z3Py做的結果，並打印出類似這樣的一些位向量「壓縮」 And(Var(0) == 10*, Var(1) == 0**？如果我想通過R3獲得從B到A的所有數據包，我可以簡單地使用fp.query(rels['A'](dst, src), rels['R3'](dst, src))，還是必須將關係R2去除到R1？

謝謝！

Answer 1

它應該能夠。您需要設置default_relation = doc（以啓用該論文中描述的立方體表示的差異）。 （不確定如何從Python做到這一點，但我希望API支持，否則讓我們知道）。