Matrix Computation by bitvectors

[陳宏毅]

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]

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.
To view this discussion on the web visit https://groups.google.com/d/msgid/pysmt/1496049e-7ca8-4f5f-ad3a-db4b3e3334f2%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[陳宏毅]

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[0]

    n = Mat.shape[1]

    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.

[陳宏毅]

I have tried BV(int(Mat[i][j]), 8)

Then this works.

陳宏毅於 2017年8月28日星期一 UTC+2上午11時14分22秒寫道：