z3约束器

下载

1
pip install z3-solver

使用

申请变量

#<数据类型>(‘对象名’)

1
2
3
4
5
6
7
8
9
10
x = Inx('x')	#申请整型变量x
x,y,z = BitVecs('x y z',16)	#申请3个位向量，大小为2^16,加's'批量声明

Int()	#整数
Real()	#实数
Bool()	#布尔型
#更改返回类型
IntVal()
Realval()
Ratval()||Q()	#有理数

求解

#默认只会找到满足条件的一组解

1
2
3
4
solve = Solver()	#创建解对象
solve.add()	#添加约束条件
solve.check()	#求解
solve.model()	#输出解，list类型，对象名为下标

函数

simplify()

#将表达式化简

1
2
simplify(<表达式>，som=Ture || mul_to_power=True)	#som表达式转换为单项式，mul_to_power乘方形式
help_simplify()	#其他选项

set_param()

#配置全局变量格式

1
2
set_param(precision=30)  #保留30位的小数
set_param(rational_to_decimal=True) # 以十进制形式表示有理数