.datalog формат с использованием Z3

Question

Я пытаюсь использовать расширение Z3: muZ с ограничениями с фиксированной запятой после этого урока: https://rise4fun.com/Z3/tutorial/fixedpoints.

Как отмечено в этом руководстве, принимаются три различных текстовых формата ввода. Базовый каталог данных является одним из этих принятых форматов.

У меня есть программы этой формы, указанные в руководстве:

Z 64

P0(x: Z) input

Gt0(x : Z, y : Z) input

R(x : Z) printtuples

S(x : Z) printtuples

Gt(x : Z, y : Z) printtuples

Gt(x,y) :- Gt0(x,y).

Gt(x,y) :- Gt(x,z), Gt(z,y).

R(x) :- Gt(x,_).

S(x) :- Gt(x,x0), Gt0(x,y), Gt0(y,z), P0(z).

Gt0("a","b").

Gt0("b","c").

Gt0("c","d").

Gt0("a1","b").

Gt0("b","a1").

Gt0("d","d1").

Gt0("d1","d").

P0("a1").

Как я могу разобрать эти программы, используя Z3Py (или Z3).

Answer 1

Если вы поместите текст этой программы в файл (скажем, a.datalog), вы можете напрямую вызвать z3 на нем. (Обратите внимание, что расширение должно быть datalog).

Когда я это делаю, я получаю:

$ z3 a.datalog
Tuples in Gt:
        (x=a(0),y=b(1))
        (x=b(1),y=c(2))
        (x=c(2),y=d(3))
        (x=a1(4),y=b(1))
        (x=b(1),y=a1(4))
        (x=d(3),y=d1(5))
        (x=d1(5),y=d(3))
        (x=a(0),y=c(2))
        (x=a(0),y=a1(4))
        (x=b(1),y=d(3))
        (x=c(2),y=d1(5))
        (x=a1(4),y=c(2))
        (x=a1(4),y=a1(4))
        (x=b(1),y=b(1))
        (x=d(3),y=d(3))
        (x=d1(5),y=d1(5))
        (x=a(0),y=d(3))
        (x=a1(4),y=d(3))
        (x=b(1),y=d1(5))
        (x=a(0),y=d1(5))
        (x=a1(4),y=d1(5))
Tuples in R:
        (x=a(0))
        (x=b(1))
        (x=c(2))
        (x=a1(4))
        (x=d(3))
        (x=d1(5))
Tuples in S:
        (x=a(0))
        (x=a1(4))
Time: 3ms
Parsing: 0ms, other: 1ms

Это то, что вы пытаетесь сделать?