z3位向量运算简化答案答案

【问题标题】：z3 bitvector operation simplified answerz3位向量运算简化答案
【发布时间】：2018-07-23 14:38:46
【问题描述】：

在进行位向量运算时，是否有一种更简单的方法可以立即获得答案，例如。 a=100万，b=0，什么是a&b（答案：0）

此方法有效，但必须引入虚拟变量来存储答案：

(declare-const a (_ BitVec 64))
(declare-const b (_ BitVec 64))
(declare-const ans (_ BitVec 64))
(assert (= a (_ bv1000000 64)))
(assert (= b (_ bv0000000 64)))
(assert (= ans (bvand a b)))
(check-sat)
(get-model)

这种方法是我想要的，但我的代码给出了一个 demorgan 身份：

(declare-const a (_ BitVec 64))
(declare-const b (_ BitVec 64))
(simplify (bvand a b))

【问题讨论】：

标签： z3 bitvector

【解决方案1】：

您可以使用该模型来评估任意表达式，例如：

(declare-const a (_ BitVec 64))
(declare-const b (_ BitVec 64))
(assert (= a (_ bv1000000 64)))
(assert (= b (_ bv0000000 64)))
(check-sat)
(eval (bvand a b))

说

sat
#x0000000000000000

【讨论】：

【解决方案2】：

我没有测试，但是像 (apply (then propagate-values simplify)) 这样的东西应该可以解决问题

【讨论】：