用其他类型替换SymPy符号(Z3Py)
提问于 2018-06-17 05:56:19
我使用SymPy表达式来计算表达式，比如a + 3 * b，然后我想用Z3来验证它(例如，所有正a, b的a + 3 * b > 0 )。
我找不到用a, b对象替换SymPy符号的方法，在一般情况下，用Z3对象替换Z3符号。
import sympy
from z3 import *
a = sympy.Symbol('a')
b = sympy.Symbol('b')
t = Real('t')
w = Real('w')
e = a + 3 * b
e = e.subs({a:t, b:w}) # does nothing?
e = e.replace(a, t).replace(b, w) # e = t + 3 * w
And(True, e > 0) # raises z3.z3types.Z3Exception还会通过将3替换为RealVal('3')引发异常。
目前，我正在对字符串进行操作，并最终使用exec来更改上述类型和表达式，但我计划停止使用exec。
回答 1
Stack Overflow用户
回答已采纳
发布于 2018-06-17 07:24:32
不能将交感表达式与z3py表达式混合和匹配。它们是不同的内部数据结构。但是，您可以遍历渐近表达式并创建相应的z3表达式，但必须单独执行。请注意，对subs的调用在渐近世界中执行一个替换:正在发生替换，但结果表达式仍然是一个同情表达式。(而且很可能是非法的:如果您确实尝试在其上使用任何渐近函数，则很可能会从它本身得到类似的异常。)
您需要开发一个函数，该函数接受一个渐近表达式，并为您提供一个z3py表达式。
据我所知，没有任何“正式”函数可以这样做，但是详细信息请参见这个(有点过时的)答案：How to use Z3py and Sympy together，您可能可以从那里使用代码来实现您的目的。(粗略地猜测:由于同情的丰富性和不可避免的不匹配，完成从同情到z3py的完全转换很可能是不可能的，但您很可能会得到一个处理用例的转换器。)
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/50897324
复制
社区富文本编辑器全新改版！诚邀体验～
全新交互，全新视觉，新增快捷键、悬浮工具栏、高亮块等功能并同时优化现有功能，全面提升创作效率和体验
腾讯云开发者
