如何在Z3py中定义公理？

Question

我必须在Z3中做一个公理，但是我观看了https://ericpony.github.io/z3py-tutorial/advanced-examples.htm（使用量词建模）的示例，但我不了解大多数内容。我希望有人可以给我一个Z3py小公理的例子，以帮助我理解

Answer 1

您可能指的是这段代码：

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()

公理不过是量化的断言（请参阅如何使用axioms将列表s.add添加到求解器），并且它们通常与未解释的函数有关。 （在这种情况下，为subtype和array_of`。）>

不太确定自己在做什么。请问一个具体问题。您是否尝试运行此代码？它产生了您所期望的吗？