26 views

Skip to first unread message

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.

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, BVfrom pysmt.typing import BVTypeM = 4N = 3# create a matrix of 8-bit BV variablesvar_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+jf = 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 resultfor 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, Intfrom pysmt.typing import INT, BVType, ArrayType# Create an array INT -> INT -> BV, that is a 2D matrix with integer# indexes and BV valuesarr = Symbol("matrix", ArrayType(INT, ArrayType(INT, BVType(8))))# Impose some constraintsM = 4N = 3f = 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.

Aug 28, 2017, 5:14:22 AM8/28/17

to pySMT

Dear Andrea:

Feeling sorry that I am new to pysmt.

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'>

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.

Aug 30, 2017, 8:49:15 AM8/30/17

to pySMT

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

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

Then this works.

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

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu