我正在尝试使用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)解析这些程序。你知道吗
如果你把程序文本放在一个文件中(比如
a.datalog
),你可以直接调用z3。(注意扩展名必须是datalog
)。你知道吗当我这么做的时候,我得到:
这就是你想做的吗?你知道吗
相关问题 更多 >
编程相关推荐