Формализация достижимости в z3py

Я попытаюсь объяснить, почему это переходит из состояния в режим ожидания, но не обращаю внимания на то, как кодировать достижимость. Вкратце, проблема в том, что si3 и si5 влекут за собой, что p (x, y) ложно для всех x и y. Когда вы раскомментируете / утверждаете «p (x, y) == True», это утверждает и si3, и si5 и приводит к противоречию.

Более подробно, давайте утвердим «p (x, y) == True». Это должно быть так, что от s1 до s5 удерживаются от:

s.add( Implies (p(x,y)==True, Exists([x,y], And(si1==True,si2==True,si3==True,si4==True,si5==True))) )
; |- Exists([x,y], And(si1==True,si2==True,si3==True,si4==True,si5==True))
; |- And(si1==True,si2==True,si3==True,si4==True,si5==True) as the existential bindings for x and y are not instantiated in any subformula.

Мы можем разбить si3, чтобы сделать вывод, что это эквивалентно тому, что все L (x, y) ложны.

si3= ForAll([u,x,y], And(L(u,x)==False, L(y,u)==False) ) 
; moving the forall across the and we get
And (ForAll([u,x,y], L(u,x)==False), ForAll([u,x,y], L(y,u)==False) ) 
; dropping unused variables
And(ForAll([u,x], L(u,x)==False), ForAll([u,y], L(y,u)==False) ) 
; which are the same statement up to variable renaming. So
ForAll([x,y], L(x,y)==False)

Используя s3, мы можем заменить все экземпляры L (-, -) в s5, чтобы получить:

s5=ForAll([x,y,z], Implies (And (p(x,y)==True, L(x,z)==False,L(y,z)==False), L(x,y)==True))
; replacing L(-,-) with False and reducing False==False and False==True gives:
ForAll([x,y,z], Implies (And (p(x,y)==True, True, True), False))
; which is equivalent to
ForAll([x,y], p(x,y)==False)

Это противоречит p (x, y) == True. (Обратите внимание, что это другое связывание x и y, чем в квантификаторах.)

Одна удовлетворительная модель - «u = x = y = z = i = j = 0» и «p (0,0) = False». Как только "p (x, y)" ложно, s1 - s5 могут быть проигнорированы для удовлетворения формулы. (Я немного ошибаюсь, говоря здесь «модель», но, надеюсь, интуиция ясна.)

В качестве общего предложения я бы предложил переименовать переменные, которые связаны квантификаторами, чтобы устранить двусмысленность. В следующей строке торчат 3 разные копии «x» и «y».

s.add( Implies (p(x,y)==True, Exists([x,y], And(si1==True,si2==True,si3==True,si4==True,si5==True))) )

В «p (x, y)» есть несвязанные x и y верхнего уровня, версия, ограниченная «Exists ([x, y], ...)» (у которой нет экземпляров), и версии, связанные с si1 по si5. Может быть, ты сможешь уследить за этим, но мне это сложно.

Я смог обновить свою формализацию следующим образом, теперь я получил удовлетворительное решение, но все еще не могу найти отдельные значения для промежуточных узлов: i, j, z

from z3 import*

L= Function('L', IntSort(), IntSort(),BoolSort())
p=Function('p', IntSort(), IntSort(), BoolSort())

u=Int('u')
x=Int('x')
y=Int('y')
z=Int('z')
i=Int('i')
j=Int('j')

s=Solver()

s.add(And(x>=0, x<=5, y>=0,y<=5, u>=0,u<=5,i>=0,i<=5, j>=0,j<=5,z>=0,z<=5))

#si_1
s.add(ForAll(x,  And( L(x,x)==False,p(x,x)==False )))

#si_2
s.add(ForAll([x,y], And(L(x,y)==L(y,x), p(x,y)==p(y,x))))


#si_3
s.add(ForAll([x,y], Implies(p(x,y)==True,  Exists([i,j,z], And( L(x,i)==True, L(i,j)==True,L(j,z)==True,L(z,y)==True)))))


#si_4
s.add(ForAll([x,y,z], Implies (And (p(x,y)==True, L(x,z)==False,L(y,z)==False), L(x,y)==True) ))


s.add(p(x,y)==True)




result=s.check()
model = s.model()

print result, model

Согласно ограничению si_3:

    s.add(ForAll([x,y], Implies(p(x,y)==True,  Exists([i,j,z], And( L(x,i)==True, L(i,j)==True,L(j,z)==True,L(z,y)==True)))))

Я должен получить разные значения для i, j и z, поскольку si_1 гарантирует, что L (x, x) будет ложным:

s.add(ForAll(x,  And( L(x,x)==False,p(x,x)==False )))

Что мне следует изменить, чтобы получить разные значения i, j, z, и они не должны быть одинаковыми ...