Правильный способ добавить ограничения, избегая ошибки «отрицание не стратифицировано» с помощью Fixedpoint (механизм регистрации данных) - PullRequest
Новая
       8

Правильный способ добавить ограничения, избегая ошибки «отрицание не стратифицировано» с помощью Fixedpoint (механизм регистрации данных)

0 голосов
/ 25 апреля 2019

Я играю с Fixedpoint и журналом данных в Z3 (используя интерфейс Python), поскольку я пытаюсь воспроизвести некоторые функции Alloy в личном проекте.

Я написал очень простой "родитель ипример "предка": 

s = Fixedpoint()
s.set(engine="datalog")

P = FiniteDomainSort("Person", 16)

X = Var(0, P)
Y = Var(1, P)
Z = Var(2, P)

# parent(X, Y)  "X is parent of Y"
parent = Function("parent", P, P, BoolSort())

# ancestor(X, Y)  "X is ancestor of Y"
ancestor = Function("ancestor", P, P, BoolSort())

s.register_relation(parent, ancestor)

# x is ancestor of y follows from x being parent of y
s.rule(
    ancestor(X, Y),
    parent(X, Y))

# x is ancestor of y follows from x being parent of z and z being ancestor of y
s.rule(
    ancestor(X, Y),
    And(
        parent(X, Z),
        ancestor(Z, Y)))

# facts
alice = FiniteDomainVal(0, P)
bob = FiniteDomainVal(1, P)
mary = FiniteDomainVal(2, P)
luke = FiniteDomainVal(4, P)
eve = FiniteDomainVal(3, P)

s.fact(parent(alice, bob))
s.fact(parent(bob, mary))
s.fact(parent(mary, luke))

Пока все работает нормально, если я не добавлю "необоснованные" факты, такие как parent(bob, bob) или And(parent(alice, bob), parent(bob, alice)).Как я могу добавить правила, которые делают всю модель ненасыщенной, когда указаны неверные факты?

Некоторые из моих первых попыток были связаны с добавлением правил с отрицаниями в теле, приводящими к ошибке «слоистого отрицания».Я также пытался добавить аксиомы с assert_exprs, но, похоже, они не учитываются при запросах (и нет доступного метода модели check).

Мое текущее решение включает в себя добавление «неверного»отношение, которое я могу проверить на пустоту: 

invalid = Function("invalid", P, BoolSort())
s.register_relation(invalid)

s.rule(
    invalid(X),
    And(
        parent(X, Y),
        parent(Y, X)))

Тогда я знаю, что моя модель "правильная", когда s.query(invalid(X)) == unsat.Действительно, добавление факта parent(bob, bob) гарантирует, что invalid(X) сат.

Есть лучший способ?

Спасибо!

...