如何确定不同变量之间的符号关系（而非具体数值）
我需要一种方法，可以以编程的方式确定方程中变量之间的符号关系。
例如，对于任意x，给定3ax - bx = 0，我想确定b 必须等于3a。
当我尝试使用像Z3这样的工具来合成这些值时，我得到的是具体数值，而不是符号表达式。到目前为止我找到的最接近的东西是 Z3的 get_implied_equalities。但这似乎需要事先知道期望的等式是什么，而我并不清楚。
我知道过去使用Z3时这并不是可能的（参见：Symbolic variables in z3），但我不知道这个限制是Z3特有的，还是普遍存在的技术难题。我愿意尝试任何工具（虽然最好是有一个C 接口、我可以通过FFI调用的那种）。
解决方案
显然不能用Z3来实现，因为它是一个SMT求解器，因此对于这个用例根本不可行，你需要一个符号代数系统之类的工具。
例如， Redlog 就有一个C 接口，非常适合完成这项工作。
站内所有文章版权归属LeftHeroAI导航站，无授权禁止任何主体转载、抄袭、复制内容，亦不得私自架设镜像站点。一经侵权，本站将通过法律途径追责。
相关文章
汇集全球数千款 AI 工具，每日持续更新，配套 AI 开发学习资源，轻松用 AI 提升工作效率。快捷键 Ctrl+D/⌘+D 一键收藏本站。