Z3 位向量操作

Question

如何使用 'repeat' 和 'rotate_left' 位向量运算？

更一般地说，我在哪里可以找到 Z3 使用的 SMT2 脚本格式的位向量操作的详细文档？

我找到的所有内容似乎都只是转到教程，或损坏的链接：
https://github.com/Z3Prover/z3/wiki/Documentation
http://research.microsoft.com/en-us/um/redmond/projects/z3/old/documentation.html

试图通过猜测来理解 "repeat"、"rotate_left" 和 "rotate_right" 一直令人沮丧。我不知道如何使用它们。例如

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

给予

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

文档在哪里？希望他们没有解释，因为所有这些都是标准的，我也查看了 smt-lib.org 但也没有列出这些细节。好郁闷

Answer 1

对于你的例子，你应该这样写

(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)

你会得到

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

我经常使用的一个好文档是它的API。

Answer 2

除dejvuth的回答外：

SMT 语言有很好的文档记录（请参阅 smt-lib.org），对于这个特定问题，FixedSizeBitVectors theory and the QF_BV logic 定义是相关的。后者包含重复的定义：

((_ repeat i) (_ BitVec m) (_ BitVec i*m))
- ((_ repeat i) x) means concatenate i copies of x

除此之外，David Cok 还写了一篇出色的 SMT2 tutorial。

Z3 API 中的函数名称与语法允许的 SMT2 中的函数名称相同，在这种情况下带有前缀 Z3_mk_ 以指示它们是构造 Z3 表达式的函数。

Z3 位向量操作

Z3 bitvector operations

bitvector

smt

z3