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

除了dejvuth的回答：

SMT 语言有据可查（参见 smt-lib.org），对于这个特定问题，FixedSizeBitVectors theory 和 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 表达式的函数。

Answer 2

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

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