1

Closed

doubt on multidimensional arrays

description

I am using z3 and I face following problem:

arr[5][5] is my two dimensional array.

In my code I am assigning bit-vector to one of the row of the array in the following manner.
arr[i]=write_bv (write_bv is bit-vector of size 5 )
I want to store write_bv bit-vector at the 'ith row' of arr.
(declare-fun arr () (Array (_ BitVec 3) (Array (_ BitVec 3) (_ BitVec 1) )))
(store arr i write_bv)
The above code give error as sort-mismatch.
So how should one write such cases.

Thanks,
Dinesh
Closed Dec 27, 2012 at 4:23 PM by leodemoura
This is not a work item.

comments

leodemoura wrote Dec 27, 2012 at 4:22 PM

Please consider using Stackoverflow (http://stackoverflow.com/questions/tagged/z3) for asking questions about Z3. The issue tracker is for reporting bugs and problems with Z3. Stackoverflow provides a far better interface for Q&A.

Regarding your question, Z3 does not provide "casting" operators like the ones found in programming languages such as C. The sorts (_ BitVec 5) and (Array (_ BitVec 3) (_ BitVec 1)) are incompatible, and Z3 does not provide any functionality for converting values from one to the other. In the SMT 2.0 format, everything is explicit, we have to do the "casting" ourselves. One advantage is that (unlike C) the semantics of every expression is well defined.

Sign in to add a comment