Z3 bitvector operations

Question

How does one use the 'repeat' and 'rotate_left' bitvector operations?

More generally, where can I find detailed documentation of bitvector operations in the SMT2 scripting format used by Z3?

Everything I find seems to just go to tutorials, or broken links:
https://github.com/Z3Prover/z3/wiki/Documentation
http://research.microsoft.com/en-us/um/redmond/projects/z3/old/documentation.html

Trying to understand "repeat", "rotate_left", and "rotate_right" by guessing has been frustating. I cannot figure out how to use them. For example

(display (repeat #b01))
(display (repeat #b01 3))
(display (repeat 3))
(display (rotate_left #b0001 2))

gives

"repeat expects one non-zero integer parameter"
"repeat expects one argument"
"operator is applied to arguments of the wrong sort"
"rotate left expects one argument"

Where is the documentation? Hoping they didn't explain because all of this is standard, I also looked at smt-lib.org but that doesn't list these details either. So frustrating.

dejvuth dejvuth · Accepted Answer · 2015-05-19T07:52:52

For your example, you should write something like this

(declare-const a (_ BitVec 2))
(declare-const b (_ BitVec 6))
(assert (= a #b01))
(assert (= b ((_ repeat 3) a)))

(declare-const c (_ BitVec 4))
(declare-const d (_ BitVec 4))
(assert (= c #b0001))
(assert (= d ((_ rotate_left 2) c)))

(check-sat)
(get-model)

You will get

sat
(model 
  (define-fun d () (_ BitVec 4)
    #x4)
  (define-fun c () (_ BitVec 4)
    #x1)
  (define-fun b () (_ BitVec 6)
    #b010101)
  (define-fun a () (_ BitVec 2)
    #b01)
)

A good document that I usually use is its API.

Z3 bitvector operations

2 Answers