3

当我尝试通过 python api 在 z3 的定点求解器上使用推送和弹出操作进行回溯时,求解器抛出“引擎不支持操作”异常。

b = Bool('b')
a = Bool('a')
s = Fixedpoint()
s.register_relation(a.decl())
s.register_relation(b.decl())
s.fact(a)
s.push()
s.rule(b, a)
s.query(b)
s.pop()

z3py 在定点求解器上是否不支持 push 和 pop 操作?

4

0 回答 0