How can I access the variable mapping used in bitmap?

Question

I am modifying a tool that uses Z3 (in particular the Python API) to address the limitations of the bitvector. I need to use a specific external SAT solver instead of the internal Z3, so I start bit processing using tactics

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

after which I can relatively easily dump sentences into a DIMACS file. The problem is comparing the resulting sentence model with the original constraint model: as far as I can tell, the Python API does not provide a way to access the model converter that matches the tactics. It's true? If so, can this be done using another API, or is there an easier way? Basically, I just need to know how the propositional variables in the final CNF sentences correspond to the original bit-path variables.

Answer 1

This sounds like a pretty special purpose. The easiest way is likely to be that you use the goal2sat transform (and recompile Z3) to save the translation table to a file. I do not think that any function displayed through the API will provide you with this information.

Answer 2

I had the same problem and it was solved without changing Z3. Here is an example in python. (Based on 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 each position i of the bitvector x, we introduce a new logical variable xi and require that xi be equal to the ith position of the bitvector. The names of boolean variables are saved during bit blasting.