How to multiply a variable Boolean matrix by a Boolean vector in Z3 in a nice way? The sizes of the matrix and of vectors are known and fixed.
In my case there is only one matrix and there is no need to pass it as an argument or return it as a result of a function, so the matrix can be global.
Does it help if the matrix is a square matrix?
My current solution is:
; Maybe some other matrix representation would be better?
(declare-datatypes () ((ColumnIndex c0 c1 c2)))
(declare-fun column (ColumnIndex) (_ BitVec 4))
(define-fun scalarTimesVector ((a (_ BitVec 1)) (v (_ BitVec 4))) (_ BitVec 4)
(ite (= a #b1) v (_ bv0 4))
)
(define-fun matrixTimesVector ((vector (_ BitVec 3))) (_ BitVec 4)
(bvor
(scalarTimesVector ((_ extract 0 0) vector) (column c0))
(scalarTimesVector ((_ extract 1 1) vector) (column c1))
(scalarTimesVector ((_ extract 2 2) vector) (column c2))
)
)
What you are doing is just fine, especially given your matrix size is constant and never change. SMTLib has no notion of loops, although recent versions do allow recursive definitions of functions that can be used for this effect. See this answer for a different but related question on how to use recursion: https://stackoverflow.com/a/51140049/936310. However, I'd recommend sticking to your current code for simplicity and wider support from a variety of solvers.
In my mind, SMTLib should really be "generated" instead of directly used; and most tools use it this way. If your programming needs get more complicated, I'd recommend using a higher-level interface instead. There are interfaces to Z3 and other solvers from pretty much any language you can imagine. Python and Haskell provide really high-level bindings that get rid of most of the boilerplate for you. You also have low-level bindings from C/C++/Java if that's your choice. See using floating point arithmetic with Z3 C++ APIs for a comparison of the styles.