I'm trying to use the Z3 extension: muZ with fixed-point constraints following this tutorial: https://rise4fun.com/Z3/tutorial/fixedpoints.
As marked in this tutorial, three different text-based input formats are accepted. The basic datalog is one of these accepted formats.
I have programs of this form indicated in the tutorial:
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").
How can I parse these programs using Z3Py (or Z3).
If you put that program text in a file (say a.datalog), you can directly call z3 on it. (Note that the extension has to be datalog).
When I do that, I get:
$ 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
Is this what you're trying to do?