为了更好地理解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的关系?你知道吗
谢谢!你知道吗
它应该能够。您需要设置default_relation=doc(以启用本文中描述的多维数据集差异表示)。 (不确定如何从Python实现,但我希望API支持这一点;否则请告诉我们)。你知道吗
相关问题 更多 >
编程相关推荐