Bit patlatmada kullanılan değişken haritalamaya nasıl erişebilirim?

Question

Bitvector kısıtlamalarını çözmek için Z3 (özellikle Python API'sı) kullanan bir aracı değiştiriyorum. Ben iç Z3 biri çözücü yerine belirli bir dış SAT kullanmak gerekir, bu yüzden ilk ben nispeten kolayca DIMACS dosyasına maddeleri dökümü tarihten sonra taktik

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

kullanarak bit patlatma değilim. Sorun, ortaya çıkan teklif modelini orijinal kısıtlamaların bir modeline yeniden haritalamaktır: Anlayabildiğim kadarıyla, Python API'si bir taktiğe karşılık gelen model dönüştürücüsüne erişmek için bir yol sağlamaz. Bu doğru mu? Öyleyse, farklı bir API kullanarak yapılabilir mi, yoksa daha kolay bir yol var mı? Temel olarak, sadece son CNF maddelerinde önerilen değişkenlerin orijinal bitvektör değişkenlerine nasıl karşılık geldiğini bilmem gerekiyor.

Answer 1

Bu oldukça özel amaçlı bir ses çıkarır. En kolayı, bir dosyada bir çeviri tablosunu kaydetmek için target2sat dönüşümünü (ve Z3'ü yeniden derleme) kullanmanızdır. API üzerinden gösterilen hiçbir işlevselliğin size bu bilgiyi vereceğini düşünmüyorum.

Answer 2

Aynı problemi yaşadım ve Z3'ü değiştirmeden çözdüm. İşte python'da bir örnek. (Leonardo tarafından example dayanarak). I bitvector x her konumu için

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) 

yeni bir Boolean değişkeni xi tanıtmak ve xi bitvector i'nci konuma eşit olmasını gerektirir. Boole değişkenlerinin isimleri, bit patlatma sırasında korunur.