如何在Z3py中定义公理？
如何在Z3py中定义公理？
提问于 2020-01-16 03:26:45
我不得不用Z3做一个公理，但是我看了https://ericpony.github.io/z3py-tutorial/advanced-examples.htm (使用量词建模)的例子，我对大多数事情都不理解。我希望有人能给我一个Z3py中的小公理的例子，帮助我理解。
我执行的示例是：
Type = DeclareSort('Type')
subtype = Function('subtype', Type, Type, BoolSort())
array_of = Function('array_of', Type, Type)
root = Const('root', Type)
x, y, z = Consts('x y z', Type)
axioms = [ ForAll(x, subtype(x, x)),
ForAll([x, y, z], Implies(And(subtype(x, y), subtype(y, z)),
subtype(x, z))),
ForAll([x, y], Implies(And(subtype(x, y), subtype(y, x)),
x == y)),
ForAll([x, y, z], Implies(And(subtype(x, y), subtype(x, z)),
Or(subtype(y, z), subtype(z, y)))),
ForAll([x, y], Implies(subtype(x, y),
subtype(array_of(x), array_of(y)))),
ForAll(x, subtype(root, x))
]
s = Solver()
s.add(axioms)
print s
print s.check()
print "Interpretation for Type:"
print s.model()[Type]
print "Model:"
print s.model()问题是我不理解输出。
[root = Type!val!0,
subtype = [else ->
Or(And(If(Var(0) == Type!val!1,
Type!val!1,
Type!val!0) ==
Type!val!1,
If(Var(1) == Type!val!1,
Type!val!1,
Type!val!0) ==
Type!val!1),
And(If(Var(0) == Type!val!1,
Type!val!1,
Type!val!0) ==
Type!val!0,
If(Var(1) == Type!val!1,
Type!val!1,
Type!val!0) ==
Type!val!1),
And(If(Var(0) == Type!val!1,
Type!val!1,
Type!val!0) ==
Type!val!0,
If(Var(1) == Type!val!1,
Type!val!1,
Type!val!0) ==
Type!val!0))],
array_of = [else -> Type!val!1]]因为这个原因，我需要检查一个小例子，以便更好地理解它是如何工作的
回答 1
Stack Overflow用户
发布于 2020-01-16 03:45:04
您可能指的是这段代码：
Type = DeclareSort('Type')
subtype = Function('subtype', Type, Type, BoolSort())
array_of = Function('array_of', Type, Type)
root = Const('root', Type)
x, y, z = Consts('x y z', Type)
axioms = [ ForAll(x, subtype(x, x)),
ForAll([x, y, z], Implies(And(subtype(x, y), subtype(y, z)),
subtype(x, z))),
ForAll([x, y], Implies(And(subtype(x, y), subtype(y, x)),
x == y)),
ForAll([x, y, z], Implies(And(subtype(x, y), subtype(x, z)),
Or(subtype(y, z), subtype(z, y)))),
ForAll([x, y], Implies(subtype(x, y),
subtype(array_of(x), array_of(y)))),
ForAll(x, subtype(root, x))
]
s = Solver()
s.add(axioms)
print s
print s.check()
print "Interpretation for Type:"
print s.model()[Type]
print "Model:"
print s.model()axiom只不过是一种量化的断言(请参阅如何使用s.add将列表axioms添加到求解器)，它们通常是关于未解释的函数的。(在本例中为subtype和array_of`)。
不太清楚你在为什么而挣扎。请提出一个具体的问题。你试过运行这段代码了吗？它是否产生了您所期望的结果？
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/59758334
复制相关文章
相似问题
腾讯云开发者
