如何在 Z3 中对位向量进行零/符号扩展？

【问题标题】：How to zero/sign extend bitvectors in Z3?如何在 Z3 中对位向量进行零/符号扩展？
【发布时间】：2016-11-15 08:32:48
【问题描述】：

我无法使用 Z3 SMT 接口对位向量执行零扩展。根据我通过阅读资料了解到的情况，有用于此的函数，它们可用于各种绑定（C、C++、Python 等），但 SMT 接口的教程不知道如何调用它们。

使用 SMT QF_BV 逻辑标准中的 zero_extend 也无济于事 - Z3 表示 unsupported。

【问题讨论】：

标签： z3 smt

【解决方案1】：

原来zero_extend 和其他一些函数是parametric 的，可能类似于C++ 中的foo<T>。要调用此类函数，需要使用特殊语法：

(declare-const a (_ BitVec 1))
(declare-const b (_ BitVec 2))
(assert (= b ((_ zero_extend 1) a)))
(check-sat)
(get-model)

使用((_ zero_extend i) x) 而不是(zero_extend i x) 会得到正确的结果：

sat
(model
  (define-fun a () (_ BitVec 1) #b0)
  (define-fun b () (_ BitVec 2) #b00)
)

【讨论】：