如何利用Z3解算器解决位向量矩阵的乘法和逻辑蕴涵问题？

Question

我试图用python和z3来描述一个约束解算器。这个包含三个位向量矩阵的收缩是X[i]=X[j]-->(R1[i]*X=R1[j]*X)&(R1[i]*X=R1[j]*X)&(R1[i]*X=R1[j]*X)

X、R1、R2、R3是3×3的位向量矩阵

我找到了一些线索：

Traceback (most recent call last):
  File "<stdin>", line 3, in <module>
  File "D:\Z3\z3-master\z3-master\build\python\z3\z3.py", line 1613, in Implies
b = s.cast(b)
  File "D:\Z3\z3-master\z3-master\build\python\z3\z3.py", line 1369, in cast
    _z3_assert(is_expr(val), "True, False or Z3 Boolean expression expected. Received %s" % val)
  File "D:\Z3\z3-master\z3-master\build\python\z3\z3.py", line 92, in _z3_assert
    raise Z3Exception(msg)
z3.z3types.Z3Exception: True, False or Z3 Boolean expression expected. Received [[ True  True  True]]

如何调试？你知道吗

为了解决位向量矩阵乘法问题，我在z3之外引入了numpy，numpy可以解决乘法问题。你知道吗

from z3 import*
from numpy import*

X=[[BitVec("x_%s_%s"%(i+1,j+1),16) for j in range(3)] for i in range(3)];
s=Solver();
s.add(X[0][1]==0);s.add(X[0][2]==0);s.add(X[1][2]==0);
a=BitVecVal(1,16);b=BitVecVal(0,16);
r_1=[[b,b,a],[b,b,a],[b,b,b]]
r_2=[[b,b,b],[b,b,b],[a,a,b]]
r_3=[[a,b,b],[a,b,b],[b,b,b]]
import numpy as np
mr1=np.matrix(r_1)
mr2=np.matrix(r_2);mr3=np.matrix(r_3);mXx=np.matrix(X);
for p in range(0,2,1):
      for q in range(0,2,1):
          s.add(Implies((X[p]==X[q]),(((mr1[p]*mXx)==(mr1[q]*mXx))&((mr2[p]*mXx)==(mr2[q]*mXx))&((mr3[p]*mXx)==(mr3[q]*mXx)))))
s.check()