Как я могу получить доступ к отображению переменных, используемому при дробеструйной обработке?

Question

Я модифицирую инструмент, который использует Z3 (в частности, API-интерфейс Python) для решения ограничений битового вектора. Мне нужно использовать конкретный внешний SAT-решатель вместо внутреннего Z3, так что я первым делом использую тактику

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

после чего я могу относительно легко вывести предложения в файл DIMACS. Проблема состоит в том, чтобы сопоставить полученную пропозициональную модель с моделью исходных ограничений: насколько я могу судить, API-интерфейс Python не предоставляет способа доступа к конвертеру модели, соответствующему тактике. Это правда? Если да, то можно ли это сделать с помощью другого API или есть более простой способ? По сути, мне просто нужно знать, как пропозициональные переменные в заключительных предложениях CNF соответствуют исходным переменным битового вектора.

Answer 1

Это звучит довольно особенное назначение. Вероятно, проще всего будет применить преобразование goal2sat (и перекомпилировать Z3), чтобы сохранить таблицу перевода в файл. Я не думаю, что какая-либо функциональность, предоставляемая через API, даст вам эту информацию.

Answer 2

У меня была такая же проблема, и я решил ее без модификации Z3. Вот пример в Python. (По примеру Леонардо.)

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)

Для каждой позиции i битового вектора x мы вводим новую логическую переменную xi и требуем, чтобы xi равнялась i-й позиции битового вектора. Имена логических переменных сохраняются во время битовой обработки.