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

Question

I'm modifying a tool which uses Z3 (specifically the Python API) to solve bitvector constraints. I need to use a particular external SAT solver instead of the internal Z3 one, so I'm first bit-blasting using the tactic

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

after which I can relatively easily dump the clauses to a DIMACS file. The problem is mapping the resulting propositional model back to a model of the original constraints: as far as I can tell, the Python API doesn't provide a way to access the model converter corresponding to a tactic. Is this true? If so, can it be done using a different API, or is there an easier way altogether? Basically I just need to know how the propositional variables in the final CNF clauses correspond to the original bitvector variables.

Answer 1

This sounds pretty special purpose. The easiest will likely be that you instrument the goal2sat conversion (and recompile Z3) to save a translation table in a file. I don't think any of the functionality exposed over the API would give you this information.

Answer 2

I had the same problem and solved it without modifying Z3. Here is an example in python. (Based on an example by Leonardo.)

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)

For every position i of the bitvector x we introduce a new boolean variable xi and require that xi is equal to the i-th position of the bitvector. The names of boolean variables are preserved during bit-blasting.