标签：Real 约束条件 求解 python 语法 Int print import Z3
一个简单的实例
问题描述：解不等式a+b<2,a>=0,b>=0的整数a和b
from z3 import *
a = Int('a')#定义一个整形 a
b = Int('b')#定义一个整形 b
s = Solver()#生成一个约束求解器
s.add(a+b<2)#添加约束条件 a+b<2
s.add(a>=0)#添加约束条件 a>=0
s.add(b>=0)#添加约束条件 b>=0
print(s.check())#检查约束求解器是否有解，如果有,返回sat; 如果不满足,返回unsat
print(s.model())#输出结果
执行结果：
- 在Z3中，除了整形（Int），还可求取实数型（Real），浮点型（Float16、Float32、Float64、Float128），布尔型（Bool）等
- 运算符有<，<=，>，> =，==和！=
- 虽然这个不等式的结果有很多，但约束求解器只能求出一个结果，后续会讲到求解多种结果的方法
另一种求解方法：solver
问题描述：求解满足下列条件：a+b<2,a>=0,b>=0的整数a和b
from z3 import *
a = Int('a')#定义一个整形 a
b = Int('b')#定义一个整形 b
solve(a+b<2,a>=0,b>=0)#将a和b的约束条件写在括号里用逗号分割
执行结果：
这种方法虽然书写简单，但在约束条件太多的情况，不容易理解
Real类型的简单使用
问题描述：求解3x=1时，x的值
from z3 import *
x = Real('x')
solve(3*x == 1)
set_option(rational_to_decimal=True)
solve(3*x == 1)
执行结果：
Real类型的数据求解默认为分数形式，如果设置rational_to_decimal=True则结果位小数形式，默认显示小数点后10位，10位后用？表示后面还有
实数型小数保留问题：precision
问题描述：求解满足下列条件：a+b<2,a>=0,b>=0的整数a和b
from z3 import *
x = Real('x')
y = Real('y')
s = Solver( ) #生成一个约束求解器
s.add(x**2 + y**2 == 3) #添加约束条件：x的平方加y的平方等于3
s.add(x**3 == 2) #添加约束条件：x的三次方等于2
set_option(precision=30)#输出结果保留小数点后30位
print(s.check())#检查约束求解器是否有解，如果有,返回sat; 如果不满足,返回unsat
print(s.model())#输出结果
执行结果：
Not和Or的简单使用
公式简化：Simplify
问题描述：简化公式x + y + 2*x + 3
from z3 import *
x = Int('x')
y = Int('y')
print (simplify(x + y + 2*x + 3))
print (simplify(x < y + x + 2))
print (simplify(And(x + 1 >= 3, x**2 + x**2 + y**2 + 2 >= 5)))
执行结果：
主要用于对复杂公式的自动化简化
标签：Real,约束条件,求解,python,语法,Int,print,import,Z3 来源： https://blog.csdn.net/qq_37400312/article/details/112268489
本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享； 2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关； 3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关； 4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除； 5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。