W jaki sposób mogę uzyskać dostęp do mapowania zmiennych używanych podczas bitco-blastingu?

Question

Modyfikuję narzędzie, które wykorzystuje Z3 (w szczególności API Pythona) do rozwiązywania ograniczeń bitwektora. Muszę korzystać z określonego zewnętrznego SAT Solver zamiast wewnętrznego Z3 jednym, więc jestem pierwszy bit piaskowania przy użyciu taktyki

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

po którym można stosunkowo łatwo zrzucić klauzule do pliku DIMACS. Problem polega na odwzorowywaniu uzyskanego modelu propozycyjnego z powrotem na model pierwotnych ograniczeń: na ile mogę to stwierdzić, API Pythona nie zapewnia dostępu do konwertera modelu odpowiadającego taktyce. Czy to prawda? Jeśli tak, czy można to zrobić przy użyciu innego interfejsu API, czy też istnieje łatwiejszy sposób? Zasadniczo po prostu muszę wiedzieć, w jaki sposób zmienne zdaniowe w końcowych klauzulach CNF odpowiadają pierwotnym zmiennym bitvector.

Answer 1

To brzmi całkiem celowo. Najprościej będzie najprawdopodobniej obstawić konwersję goal2sat (i rekompilować Z3), aby zapisać tabelę tłumaczeń w pliku. Nie sądzę, aby jakakolwiek funkcjonalność wyeksponowana przez API dawała ci te informacje.

Answer 2

Miałem ten sam problem i rozwiązałem go bez modyfikowania Z3. Oto przykład w Pythonie. (Na podstawie example przez 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) 

Dla każdej pozycji i na bitvector x wprowadzamy nową zmienną logiczną XI i wymagają xi jest równy i-tej pozycji bitvector. Nazwy zmiennych boolowskich są zachowywane podczas bitco-blastingu.