Транзитивное замыкание в Z3 / Z3py - PullRequest
Новая
       16

Транзитивное замыкание в Z3 / Z3py

0 голосов
/ 07 июня 2019

Контекст: я использую руководство по программированию Z3: https://theory.stanford.edu/~nikolaj/programmingz3.html

Похоже, что в Z3 теперь есть встроенная поддержка транзитивного замыкания, но на данный момент он доступен только через Z3py: https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-transitive-closure

У меня есть два вопроса:

(1) Есть ли какие-либо способы доступа к TransitiveClosure через другие API или к исполняемому файлу напрямую через "z3 -in", или это только для Z3py намомент?

(2) Должен ли TransitiveClosure взаимодействовать с push и pop?Ранее мы построили основную ветку на этой неделе (commit 2788f72bbb6bfd6bdad2da2b4c37ef1bb502469d) и запустили следующий пример: 

from z3 import *
B = BoolSort()
S = DeclareSort('S')
a, b, c = Consts('a b c', S)
R = Function('R', S, S, B)
TCR = TransitiveClosure(R)
s = Solver()

s.add(R(a, b) == True)
s.push()     # If this line is uncommented (or both are) the result is sat, which is wrong.
s.add(TCR(a, b) == False)
s.push()     # But if THIS line is uncommented (or neither are), the result is unsat, which is correct.

print(s)
print(s.check())

Как показывают комментарии, вызов push () между утверждениями о R и его транзитивным замыканием, кажется, нарушаетсвязь между двумя отношениями.Не уверен, что это ошибка или мое недоразумение ...

1 Ответ

0 голосов
/ 07 июня 2019

Судя по всему, он также доступен через API C / C ++:

https://github.com/Z3Prover/z3/blob/62de187d02d8d2e7a3667a31753c508f7c73aaa1/src/api/c%2B%2B/z3%2B%2B.h#L637-L639

Я не думаю, что он доступен из интерфейса SMTLib (что вы подразумеваете под z3 -in, я полагаю), поскольку он сам возвращает отношение; и такие конструкции высшего порядка обычно не допускаются в SMTLib. (Но, конечно, может быть «магический» переключатель; z3, как известно, экспериментирует с функциональностью, которая не является частью SMTLib.)

Относительно того, должен ли он работать с push / pop: я не думаю, что движок с фиксированной запятой в z3 допускает пошаговое решение; поэтому я не удивлен, что он ведет себя хаотично. Вы должны обязательно сообщить об этом поведении на их проблемном сайте (https://github.com/Z3Prover/z3/issues), чтобы они могли по крайней мере выдать сообщение об ошибке, если вы попытаетесь делать инкрементные вещи, вместо того, чтобы выплевывать вводящую в заблуждение информацию. (Или, возможно, вы столкнулись с ошибкой! это также было бы полезно для них.)

...