動的ネットワークの信念をチェックした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からR3へBからAへのすべてのパケットを取得したいのであれば、単にfp.query(rels['A'](dst, src), rels['R3'](dst, src))か、R2とR1を削除する必要がありますか？

ありがとうございます！

Answer 1

これは可能です。 default_relation = docを設定する必要があります（この記事で説明したキューブ表現の違いを有効にするには）。 （正確にはPythonからそれを行う方法はわかりませんが、APIがそれをサポートすることを願っています;そうでなければ私たちに知らせてください）。