Come posso accedere alla mappatura delle variabili utilizzata durante il bit-blasting?

Question

Sto modificando uno strumento che utilizza Z3 (in particolare l'API Python) per risolvere i vincoli di bitvector. Ho bisogno di utilizzare un particolare SAT esterna risolutore al posto del Z3 interno uno, quindi sono primo bit-sabbiatura utilizzando la tattica

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

dopo di che posso in modo relativamente facile scaricare le clausole in un file DIMACS. Il problema è la mappatura del modello proposizionale risultante su un modello dei vincoli originali: per quanto posso dire, l'API Python non fornisce un modo per accedere al convertitore del modello corrispondente a una tattica. È vero? In tal caso, può essere fatto utilizzando un'API diversa o esiste un modo più semplice? Fondamentalmente ho solo bisogno di sapere come le variabili proposizionali nelle clausole CNF finali corrispondono alle variabili bitvector originali.

Answer 1

Questo sembra uno scopo piuttosto speciale. Il più semplice sarà probabilmente quello di strumentare la conversione goal2sat (e ricompilare Z3) per salvare una tabella di traduzione in un file. Non credo che nessuna delle funzionalità esposte sull'API ti fornisca queste informazioni.

Answer 2

Ho avuto lo stesso problema e l'ho risolto senza modificare Z3. Ecco un esempio in Python. (Sulla base di una example di 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) 

Per ogni posizione i della Bitvector x introduciamo una nuova variabile booleana xi e richiediamo che xi è uguale alla posizione di i-esimo del Bitvector. I nomi delle variabili booleane vengono preservati durante il bit-blasting.