我试图在矩阵上执行一些符号计算(用符号作为矩阵的条目),之后我会有一些可能的解决方案.我的目标是根据约束选择解决方案/解决方案.
例如,M是一个矩阵,其中一个元素作为symbol.该矩阵将具有2个特征值,一个是正的,一个是负的.使用z3我试图找出唯一的负值,但我无法这样做,因为a被定义为一个符号,除非我将其转换为实际值,否则我不能将其写为约束.
我该怎么办？是否有任何方法可以将(符号)转换为实数或整数,以便我可以将其用作约束s.add(a>0)
from sympy import*
from z3 import*
from math import*
a=Symbol('a')
M=Matrix([[a,2],[3,4]]) m=M.eigenvals();
s=Solver()
s.add(m<0)
print(s.check())
model = s.model() print(model)
我一直在努力解决一个包含某些术语绝对值的小问题.在z3中,不支持abs()函数.在python中有,但我最终必须将它传递给z3py.有什么方法可以通过它将绝对运算符的术语从python传递给z3,还是有其他方法吗？以下是一个小例子的代码.
`
x = Int('x')
y = Int('y')
x= abs(2-y)
s=Solver()
s.add(x>0)
s.add(y>0)
s.check()
m=s.model()
print m`
答案应该是y = 1,这是删除abs()时的情况.有没有办法用绝对值函数来解决这个问题？ABS().或者有什么方法可以在python中解决它,然后我可以将它传递给z3.我也尝试过同情,但它不起作用.