3

如何使用“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，但也没有列出这些细节。太令人沮丧了。

4

2 回答 2

3

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

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

于 2015-05-19T07:52:52.620 回答
3

除了 dejvuth 的回答：

SMT 语言有据可查（参见 smt-lib.org），对于这个特定问题，FixedSizeBitVectors 理论和QF_BV 逻辑定义是相关的。后者包含重复的定义：

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

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

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

于 2015-05-20T11:43:17.733 回答