Z3Py 如何使用 Pi 和 e

【问题标题】：Z3Py how to use Pi and eZ3Py 如何使用 Pi 和 e
【发布时间】：2018-08-10 10:25:02
【问题描述】：

在Z3Py中是否可以使用pi、e等非代数实数？

我不想运行任何 C 程序，而是直接从 Z3 Python API 运行

【问题讨论】：

stackoverflow.com/q/46886468/1166898 的副本
@CJDennis 重复目标没有答案。
@svgrafov 如果是这样，我会提出关闭标志。如果看起来像其中一位贡献者在评论中回答。
@CJDennis 这是一个一年前的问题，建议查看本机 Java API。我不知道Python中是否有类似的东西，我问过是否有可能避免它（因为我读过那个问题）

标签： z3 z3py

【解决方案1】：

SMT 求解器通常不支持非代数数。话虽如此，您可以通过三角函数间接在z3中获得pi，（sin，cos等）；但支持不完整。（这意味着对于大多数输入，求解器最有可能返回 unknown。）

有关相关问题，请参阅此答案：Support of trigonometric functions ( e.g.: cos, tan) in Z3

【讨论】：

猜你喜欢

1970-01-01
1970-01-01
1970-01-01
1970-01-01
1970-01-01
1970-01-01
1970-01-01
1970-01-01
2013-01-12

相关资源

下载 2023-02-06
下载 2023-02-17
下载 2023-02-15

最近更新更多

热门标签

Java Python linux javascript Mysql C# Docker 算法前端 SpringBoot Redis Vue spring 设计模式 .net core .net kubernetes c++ 数据库数据结构大数据 js 机器学习微服务 Android Go 程序员面试 JVM ASP.net core 云原生人工智能后端 PHP git CSS golang k8s Nginx Django mybatis 深度学习多线程 React 架构 devops 爬虫云计算 Spring Boot LeetCode