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 сделать некоторые Bitvector «сжатие» результата и печати что-то вроде And(Var(0) == 10*, Var(1) == 0**? И если бы я хотел получить все пакеты от B до A более R3, могу ли я просто fp.query(rels['A'](dst, src), rels['R3'](dst, src)) или мне нужно удалить отношение R2 к R1?

Спасибо!

Answer 1

Он должен быть в состоянии. Вам нужно установить default_relation = doc (чтобы разрешить разницу в представлении кубов, описанном в этой статье). (точно не знаю, как это сделать с Python, но я надеюсь, что API поддерживает это, в противном случае сообщите нам об этом).