如何访问位爆破时使用的变量映射？

Question

我正在修改一个工具，它使用 Z3（特别是 Python API）来解决位向量约束。我需要使用特定的外部 SAT 求解器而不是内部 Z3 求解器，所以我首先使用策略

进行位爆破

Then('simplify', 'bit-blast', 'tseitin-cnf')

之后我可以相对轻松地将子句转储到 DIMACS 文件中。问题是将生成的命题模型映射回原始约束的模型：据我所知，Python API 没有提供访问与策略对应的模型转换器的方法.这是真的？如果是这样，是否可以使用不同的 API 来完成，或者是否有更简单的方法？基本上我只需要知道最后的CNF子句中的命题变量如何对应于原始的位向量变量。

Answer 1

这听起来很特别。最简单的方法可能是检测 goal2sat 转换（并重新编译 Z3）以保存文件中的翻译 table。我认为 API 上公开的任何功能都不会为您提供此信息。

Answer 2

我遇到了同样的问题，没有修改Z3就解决了。这是 python 中的示例。（基于莱昂纳多的 example。）

from z3 import BitVec, BitVecSort, Goal, If, Then, Bool, solve
import math

x = BitVec('x', 16)
y = BitVec('y', 16)
z = BitVec('z', 16)

g = Goal()

bitmap = {}
for i in range(16):
    bitmap[(x,i)] = Bool('x'+str(i))
    mask = BitVecSort(16).cast(math.pow(2,i))
    g.add(bitmap[(x,i)] == ((x & mask) == mask))

g.add(x == y, z > If(x < 0, x, -x))

print g

# t is a tactic that reduces a Bit-vector problem into propositional CNF
t = Then('simplify', 'bit-blast', 'tseitin-cnf')
subgoal = t(g)
assert len(subgoal) == 1
# Traverse each clause of the first subgoal
for c in subgoal[0]:
    print c

solve(g)

对于位向量x的每个位置i，我们引入一个新的布尔变量xi，并要求xi等于位向量的第i个位置。布尔变量的名称在位爆破期间被保留。

如何访问位爆破时使用的变量映射？

How can I access the variable mapping used when bit-blasting?

z3

z3py