如何在python中使用Z3在十六进制中找到相同的十进制数

编程问答 2022-05-28

问题描述

我的任务是：

输入 10023678（作为十进制数）

输出 10023678（作为十六进制数：）

我已经使用位向量逻辑中的 SMT-LIB 公式解决了这个问题。但我很想知道如何在 python 中使用“import z3”

.smt2 输入代码：

(set-logic QF_BV)
(set-option :produce-models true)
(declare-fun x () (_ BitVec 32))

(assert (= ((_ extract 3 3) x) ((_ extract 3 3 ) (bvnot(bvxor x x)))))
(assert (= ((_ extract 4 4) x) ((_ extract 4 4) (bvnot(bvxor x x)))))
(assert (= ((_ extract 5 5) x) ((_ extract 5 5) (bvnot(bvxor x x)))))
(assert (= ((_ extract 6 6) x) ((_ extract 6 6) (bvnot(bvxor x x)))))
(assert (= ((_ extract 9 9) x) ((_ extract 9 9) (bvnot(bvxor x x)))))
(assert (= ((_ extract 10 10) x) ((_ extract 10 10) (bvnot(bvxor x x)))))
(assert (= ((_ extract 12 12) x) ((_ extract 12 12) (bvnot(bvxor x x)))))
(assert (= ((_ extract 13 13) x) ((_ extract 13 13) (bvnot(bvxor x x)))))
(assert (= ((_ extract 17 17) x) ((_ extract 17 17) (bvnot(bvxor x x)))))
(assert (= ((_ extract 28 28) x) ((_ extract 28 28) (bvnot(bvxor x x)))))

(check-sat)
(get-model)
(exit)

输出：

sat
(
  (define-fun x () (_ BitVec 32)
    #x10023678)
)

解决方法

您的问题非常令人困惑：您说的是“将输入 10023678 转换为输出..”但是您发布的 SMTLib 程序没有输入。您只是断言了一些约束，z3 为您提供了满足这些约束的解决方案。

忽略这一点，将给定代码转换为 Z3py 相对容易。请注意，(bvxor x x) 是任何 0 的 x 位向量：如果你 xor 一个数字本身，你只会得到 0。然后，bvnot (bvxor x x) 只是由全 1 组成的位向量。因此，对右侧 extract 的调用始终返回包含 1 的单个 1 位向量。考虑到这一点，z3py 中的解决方案是：

from z3 import *

x = BitVec('x',32)

s = Solver()
def is_set(i):
    s.add(Extract(i,i,x) == BitVecVal(1,1))

is_set( 3)
is_set( 4)
is_set( 5)
is_set( 6)
is_set( 9)
is_set(10)
is_set(12)
is_set(13)
is_set(17)
is_set(28)

print(s.check())
print(hex(s.model()[x].as_long()))

当我运行这个时，我得到：

sat
0x10023678

希望这能帮助您入门！

pythonsmtz3