Z3PY：如何将公式转换为NNF格式？

发布于 2025-01-29 04:55:54 字数 221 浏览 4 评论 0原文

我想使用Z3PY将公式转换为其NNF格式。例如，

鉴于

Or(Not(And(i1, Not(And(i0, i4, i1, i2)))), And(i3, i1, i2))

我要

Or(Not(i1), And(i0, i4, i1, i2), And(i3, i1, i2))

谢谢

原文

I wanted to convert a formula to its NNF format using z3py. For e.g.,

Given

Or(Not(And(i1, Not(And(i0, i4, i1, i2)))), And(i3, i1, i2))

I want

Or(Not(i1), And(i0, i4, i1, i2), And(i3, i1, i2))

Thanks

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

温柔女人霸气范 2025-02-05 04:55:54

您可以使用nnf策略，然后使用简化：

from z3 import *

i0, i1, i2, i3, i4 = Bools("i0 i1 i2 i3 i4")
g = Goal()
g.add(Or(Not(And(i1, Not(And(i0, i4, i1, i2)))), And(i3, i1, i2)))
print(g)
t = Then(Tactic('nnf'), Tactic('simplify'))
print(t(g))

此打印：

[Or(Not(And(i1, Not(And(i0, i4, i1, i2)))), And(i3, i1, i2))]
[[Or(And(i0, i4, i1, i2), And(i3, i1, i2), Not(i1))]]

结果是目标列表；但是单身目标与您的公式相同。（一个目标可以将公式分为许多部分，因此可以输出列表。）

You can use the nnf tactic, followed by simplify:

from z3 import *

i0, i1, i2, i3, i4 = Bools("i0 i1 i2 i3 i4")
g = Goal()
g.add(Or(Not(And(i1, Not(And(i0, i4, i1, i2)))), And(i3, i1, i2)))
print(g)
t = Then(Tactic('nnf'), Tactic('simplify'))
print(t(g))

This prints:

[Or(Not(And(i1, Not(And(i0, i4, i1, i2)))), And(i3, i1, i2))]
[[Or(And(i0, i4, i1, i2), And(i3, i1, i2), Not(i1))]]

the result is a list of goals; but a singleton goal is the same as your formula. (A goal can split a formula into many parts, and hence the list output.)

回复收藏 0 原文

~没有更多了~