问如何在Z3py中定义公理？
EN

Stack Overflow用户

提问于 2020-01-15 19:26:45

回答 1查看 102关注 0票数 0

我不得不用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]]

因为这个原因，我需要检查一个小例子，以便更好地理解它是如何工作的

z3py

python

9.9元起，最快1天搭建自有直播

提供高并发、低延迟、易接入、极速高清的音视频直播服务，适用于直播电商/在线教育/音视频互动等多种场景

回答 1

Stack Overflow用户

发布于 2020-01-15 19: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()