windows下安装并在python中使用Z3

1.下载z3的source code

2.安装VS2019(旧版的VS基本绝迹了)，社区版就行，安装时候要勾选python（应该不是必须，待验证），c++桌面

命令行中，进入z3的目录，然后python scripts/mk_make.py 

3.打开 "D:\Program Files (x86)\Microsoft Visual Studio\2019\Community\Common7\Tools\VsDevCmd.bat"，或者开始菜单的developer  command prompt for vs 2019

4.

4.1 在命令行中使用z3:

在这个命令行中，进入z3下的build目录中，nmake，等上一个小时左右

在cmd中输入z3 -h，出现如下信息说明安装成功

4.2 在python中安装z3模块:

developer  command prompt for vs 2019中执行

python -m pip install z3-solver

5.demo

下面写一个z3最小化的python代码，官方demo：

(declare-const x Int)

(declare-const y Int)

(assert (< x 4))

(assert (< (- y x) 1))

(assert (> y 1))

(minimize (+ x y))

(check-sat)

(get-objectives)

这是命令行中的执行方式，在python中对应如下代码：

from z3 import *

o = Optimize ()

i = Int('x')

j=Int('y')

o.add (i <4)

o.add ((j-i)<1)

o.add(j>1)

o.minimize(i+j)

print o.sexpr()

print o.check()

print o.model()

执行结果是：

(declare-fun x () Int)

(declare-fun y () Int)

(assert (< x 4))

(assert (< (- y x) 1))

(assert (> y 1))

(minimize (+ x y))

(check-sat)

sat

[y = 2, x = 2]

由此可知在z3中，model是指满足已有约束的解

此外如果add多个约束，这些约束间是and的关系，例如c1,c2,c3三个约束，add(and(c1,c2))，add(c3)与add(c1,c2,c3)效果是一样的