如何使用Z3的Python接口

发布网友发布时间：2022-04-24 18:33

共1个回答

热心网友时间：2023-11-01 20:49

Z3支持许多平台以及多种语言接口，这里我们简单介绍其Python接口的使用。
以Mac OS X为例，下载Z3可执行文件后，要设置环境变量PATH和PYTHONPATH：
export PATH=$PATH:<installation path of z3>
export PYTHONPATH=$PYTHONPATH:<installation path of z3>
然后我们编辑一个简单的例子 stock.py：
#!/usr/bin/env python
from z3 import *
def main (argv):
ds = Real('ds')
fs = Real('fs')
ps = Real('ps')
origin = And ( Not (And (0<=ds, 1<=fs, 1<=ps)),
Implies (And (0<=ds, 0<=fs, 0<=ps), ds<=3),
Implies (And (0<=ds, 0<=fs, 0<=ps, fs<=1), ds+fs<=3),
Implies (And (0<=ds, 0<=ps, 1<=fs, ps<=1), ds+ps<=2))
solver2 = Solver()
solver2.add (origin)
solver2.push()
solver2.add (ds == dv/1000)
solver2.add (fs == fv/1000)
solver2.add (ps == pv/1000)
if solver2.check() == sat:
sat_count2 = sat_count2 + 1
solver2.pop()
从31到33行，声明3个实数变量，在35行我们定义一个逻辑公式并在47行加入当前环境中，77行调用check()方法并检查其返回值：sat －－公式有解；unsat －－公式无法满足。注意72，79行的push()和pop()方法是用来暂存和恢复环境。