# Matrix Computation by bitvectors

22 views

### 陳宏毅

Aug 25, 2017, 8:54:45 AM8/25/17
to pySMT
How could I generate a legal matrix data structure, with data type: bit vector.
I think this may speed up the computation time.
But I have no idea how to combine these two together.

Hoping that someone could provide me a hint.
Thanks,
Sorry for bothering.

Hung-Yi Chen.

### Andrea Micheli

Aug 25, 2017, 9:29:16 AM8/25/17
to 陳宏毅, pySMT
Dear Hung-Yi,
it really depends on what you want to do.

If you want to express a problem in which you have a fixed-size M*N matrix of bit-vectors variables, then you can simply create M*N variables via pysmt.
For example:
from pysmt.shortcuts import get_model, Symbol, And, BVUGE, BV
from pysmt.typing import BVType

M = 4
N = 3

# create a matrix of 8-bit BV variables
var_matrix = [[] for _ in range(M)]
for i in range(M):
for j in range(N):
v = Symbol("cell_%d_%d" % (i, j), BVType(8))
var_matrix[i].append(v)

# Impose some constraints on the variables
# In this example, we require that the value of cell (i,j)
# is greater or equal to i+j
f = And(BVUGE(var_matrix[i][j], BV(j+i, width=8))
for i in range(M) for j in range(N))

m = get_model(f)
assert m is not None

# Print the result
for i in range(M):
for j in range(N):
v = var_matrix[i][j]
print("Value for cell (%d, %d) is %s" % (i, j, m[v]))

Instead, if you want to encode an unknown-sized matrix of bit-vectors constraining the possible values you can use the theory of arrays.
For example:
from pysmt.shortcuts import get_model, Symbol, And, BVUGE, BV, Select, Int
from pysmt.typing import INT, BVType, ArrayType

# Create an array INT -> INT -> BV, that is a 2D matrix with integer
# indexes and BV values
arr = Symbol("matrix", ArrayType(INT, ArrayType(INT, BVType(8))))

# Impose some constraints
M = 4
N = 3
f = And(BVUGE(Select(Select(arr, Int(i)), Int(j)), BV(j+i, width=8))
for i in range(M) for j in range(N))

m = get_model(f)
assert m is not None

# Print the result: not that the size of the matrix is infinite, we
# can ask the value for any integer index!
for i in range(-M, 2*M):
for j in range(-N, 2*N):
v = Select(Select(arr, Int(i)), Int(j))
print("Value for cell (%d, %d) is %s" % (i, j, m[v]))

Hope this helps,

Andrea

--
You received this message because you are subscribed to the Google Groups "pySMT" group.
To unsubscribe from this group and stop receiving emails from it, send an email to pysmt+unsubscribe@googlegroups.com.
To post to this group, send email to py...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

### 陳宏毅

Aug 28, 2017, 5:14:22 AM8/28/17
to pySMT
Dear Andrea:

Thanks a lot for your previous help.
There's a case that I want to use the BV operations (BVAdd, BVMul....) in pysmt to implement the matrix operations (MatAdd, MatMul.....)
I have some prepared constant matrices.
So I need to transfer the constant matrices defined in numpy.uint8 to BV format.

Is there any solution to cope with the format transformation problem.
Since I want to first implement a complicated matrix computations, then detect its SAT problem.

def Mat2BVMAT(Mat):
m = Mat.shape
n = Mat.shape
for i in range(m):
for j in range(n):
BV_mat[i][j] = BV(Mat[i][j], 8)
return BV_mat

BV_W1 = Mat2BVMAT(W1)

===== Errors =======
pysmt.exceptions.PysmtTypeError: Invalid type in constant. The type was:<type 'numpy.uint8'>

Feeling sorry that I am new to pysmt.
The question may be trivial to you all.

Best regards,
Hung-Yi

To unsubscribe from this group and stop receiving emails from it, send an email to pysmt+un...@googlegroups.com.