Как использовать Z3 Solver, чтобы решить проблему с умножением матрицы битовых векторов и логическим подтекстом? - PullRequest
Новая
       15

Как использовать Z3 Solver, чтобы решить проблему с умножением матрицы битовых векторов и логическим подтекстом?

0 голосов
/ 09 апреля 2019

Я пытаюсь описать ограничение в 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]]

как его отладить?

Чтобы решить проблему умножения бит-вектор-матрица, я импортирую numpy, кроме z3, 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()
...