仓库源文，站点原文

继半年前 用z3解逻辑题后，现在用其解一次方程（组）。仍用 z3-solver 库，python 3.12。

鸡兔方程

>>> from z3 import *
>>> 鸡, 兔 = Reals('鸡 兔')
>>> solve(鸡+兔 == 2, 2*鸡+4*兔 == 6)
[兔 = 1, 鸡 = 1]
>>> solve(鸡+兔 == 10, 2*鸡+4*兔 == 28)
[兔 = 4, 鸡 = 6]

不明问题

在误用 = 后，即便改用了 ==，也会报错如下：

>>> x= Reals('x')
>>> solve(x+2=3)
  File "<stdin>", line 1
    solve(x+2=3)
          ^^^^
SyntaxError: expression cannot contain assignment, perhaps you meant "=="?
>>> solve(x+2==3)
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
TypeError: can only concatenate list (not "int") to list

如果用对 == 的话，则仍有效：

>>> solve(鸡+1 == 2)
[鸡 = 1]

但这个报错在重新赋值未知量后，仍会出现，不知为何：

>>> x= Reals('x')
>>> solve(x+1 == 2)
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
TypeError: can only concatenate list (not "int") to list
>>> 鸡= Reals('鸡')
>>> solve(鸡+1 == 2)
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
TypeError: can only concatenate list (not "int") to list
>>> 鸡, 兔 = Reals('鸡 兔')
>>> solve(鸡+1 == 2)
[鸡 = 1]

注意最后一次设了两个未知量，仍旧用同样的方程，就又有效了。

重启python环境尝试：

>>> from z3 import *
>>> x= Reals('x')
>>> solve(x+1 == 2)
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
TypeError: can only concatenate list (not "int") to list
>>> x,y = Reals('x y')
>>> solve(x+1 == 2)
[x = 1]

貌似与声明单个和多个未知量有关。

这个就很摸不着头脑，欢迎指教。

另外，= 和 == 的混淆还蛮容易发生，尤其对于刚从数学表达式转到编程的时候。

草稿：

>>> from z3 import *
>>> x= Reals('x')
>>> solve(2*x+4=10)
  File "<stdin>", line 1
    solve(2*x+4=10)
          ^^^^^^
SyntaxError: expression cannot contain assignment, perhaps you meant "=="?
>>> solve(2*x+4==10)
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
TypeError: can only concatenate list (not "int") to list
>>> solve(2*x==10)
no solution
>>> solve(2*x == 10)
no solution
>>>

>>> from z3 import *
>>> x, y = Reals('x y')
>>> solve(x-y == 3, 3*x-8*y == 4)
[y = 1, x = 4]
>>> solve(x-y == 4, 3*x-8*y == 4)
[y = 8/5, x = 28/5]
>>> solve(x-2 == 3)
[x = 5]
>>> solve(2*x == 10)
[x = 5]
>>> solve(2*x == 13)
[x = 13/2]
>>> # 为何？
>>> x= Reals('x')
>>> solve(2*x+4==10)
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
TypeError: can only concatenate list (not "int") to list
>>> solve(2*x==10)
no solution
>>> solve(2*x == 10)
no solution
>>> solve(x-2 == 3)
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
TypeError: unsupported operand type(s) for -: 'list' and 'int'
>>> 鸡, 兔 = Reals('鸡 兔')
>>> solve(鸡+兔 == 10, 2*鸡+4*兔 == 28)
[兔 = 4, 鸡 = 6]