Как я могу определить аксиому в Z3py? - PullRequest
Новая
       9

Как я могу определить аксиому в Z3py?

0 голосов
/ 15 января 2020

Я должен сделать аксиомы в 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 Ответ

0 голосов
/ 15 января 2020

Вы, вероятно, имеете в виду этот фрагмент кода: 

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`).

Не совсем уверен, с чем вы боретесь. Пожалуйста, задайте конкретный c вопрос. Вы пытались запустить этот код? Это произвело то, что вы ожидали?

...