SMT解算器中的数据类型，同时支持普通加法、异或和运算

Question

我试图解决一些布尔变量的非线性方程，同时我想计算汉明权重（即涉及布尔变量的正规加法）

我使用的是Z3 Smt Sovler&；Bitvec允许这样做，但似乎对可以传递到方程式中的单项式的数量有一些限制

因此，我正在寻找其他解决办法

问题:

x1,x2,......, x100 = boolean variables

我必须解决：

x1 + x2 + .... + x100 = 58

以及一些非线性方程组。 我附加了一个示例代码来显示错误

我请求您帮助我，因为我是Z3 smt solver的新手

代码：

from z3 import *

N = [BitVec('n%d'%i,7) for i in range(40)]

EQ = [N[0] ^ N[13] ^ N[19] ^ N[35] ^ N[39] ^ N[2]&N[25] ^ N[3]&N[5] ^ N[7]&N[8] ^ N[14]&N[21] ^ N[16]&N[18] ^ N[22]&N[24] ^ N[26]&N[32] ^ N[33]&N[36]&N[37]&N[38] ^ N[10]&N[11]&N[12] ^ N[27]&N[30]&N[31] ==1 ]

print(EQ[0])

Output:
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ^
... ==
...

同时，如果我减少单项式的数量，那么它给出了正确的表达式

Answer 1

这是因为漂亮的打印机限制了它的打印量（以减少大量输出），而不是z3的内部限制

您可以通过在from z3 import *之后添加以下行来提高限制：

set_option(max_args=10000000, max_lines=1000000, max_depth=10000000, max_visited=1000000)

您可以调整数字以满足您的需要，但以上内容应足以解决所有感兴趣的实际问题。如果我将这一行添加到您的程序中，我会将其视为输出：

n0 ^
n13 ^
n19 ^
n35 ^
n39 ^
n2 & n25 ^
n3 & n5 ^
n7 & n8 ^
n14 & n21 ^
n16 & n18 ^
n22 & n24 ^
n26 & n32 ^
n33 & n36 & n37 & n38 ^
n10 & n11 & n12 ^
n27 & n30 & n31 ==
1

我想这正是你所期待的

如果要在一行中查看所有内容，请使用以下设置：

set_option(max_args=10000000, max_width=1000000, max_lines=1, max_depth=10000000, max_visited=1000000)