Nauka Z3py - Czy istnieje wsparcie dla macierzy i pętli

Question

Przechodzę Z3py i mam pytanie, jak korzystać z API w kilku konkretnych przypadkach. Poniższy kod jest uproszczoną wersją czegoś, co ostatecznie chciałbym użyć Z3 dla. Oto niektóre z moich pytań: 1. Czy istnieje sposób na utworzenie dowolnie długiej tablicy wartości, takiej jak zmienna "a" poniżej? 2. Czy możesz uzyskać dostęp do każdego elementu tablicy w pętlach przez Z3py? 3. Czy możliwe jest przypisanie wyniku do oryginalnej zmiennej lub czy potrzebna jest nowa zmienna? Czy konwersja do CNF automatycznie doda unikalny identyfikator? (tj. a + = b)

Ogólnie, jestem zagubiony, jak zastosować API Z3py do czegoś podobnego do poniższego algorytmu, w którym rozwiązanie zależy od "b". Każda pomoc lub wskazówki są doceniane, dziękuję.

import sys 
import struct 

a = "\xff\x33\x01\x88\x02\x11\x03\x55" 
b = sys.stdin.read(1) #a byte of user input - value 'a' is good 
c = '' 
d = '' 

for x in range(len(a)): 
    c += struct.pack('B', int(a[x].encode('hex'), 16)^int(b.encode('hex'), 16)) 

print c.encode('hex') 

second = '\x23\x23' 
x = 0 
while x < len(c): 
    d += struct.pack('h', int(c[x:x+1].encode('hex'), 16)^int(second.encode('hex'), 16)) 
    x += 2 

print d.encode('hex') 

if d == '\xbd\x23\x43\x23\x40\x23\x41\x23': 
    print "Good" 
else: 
    print "Bad" 

Answer 1

Możemy to osiągnąć, pisząc program w języku Python, który generuje wyrażenie Z3. Używamy pętli i list Pythona (możemy również używać tablic) w tym programie, ale listy te zawierają wyrażenia "symboliczne" Z3 zamiast wartości Pythona. Wynikowa lista d jest listą wyrażeń Z3 zawierających b. Następnie, pytamy Z3, aby znaleźć b tak, że elementy d są "równe" z znakami w łańcuchu '\xbd\x23\x43\x23\x40\x23\x41\x23'. Oto kod:

from z3 import * 

def str2array(a): 
    """ 
    Convert a string into a list of Z3 bit-vector values of size 8 
    """ 
    return [ BitVecVal(int(a[x].encode('hex'), 16), 8) for x in range(len(a)) ] 

a = str2array("\xff\x33\x01\x88\x02\x11\x03\x55") 
# 'a' is a list of Z3 bitvector constants. 
print "a:", a 
# The elements of 'a' may look like Python integers but they are Z3 expressions. 
# We can use the method sexpr() to get these values in SMT 2.0 syntax. 
print [ a_i.sexpr() for a_i in a ] 

# b is a Z3 symbolic variable. 
b = BitVec('b', 8) 

# We compute a list 'c' of Z3 expressions from 'a' and 'b'. 
# We use Python list comprehensions but we can also use a for-loop. 
c = [ a_i^b for a_i in a ] 

print "c:", c 

second = '\x23\x23' 
# We convert 'second' in a Z3 bit-vector value of size 16 
second = BitVecVal(int(second.encode('hex'), 16), 16) 
print "second:", second 

# The Z3 operation Concat concatenates two or more bit-vector expressions. 
d = [] 
x = 0 
while x < len(c): 
    # c[x] is a Bit-vector of size 8, second is a Bit-vector of size 16. 
    # In Z3, we have to do the "casting" ourselves. 
    # We use ZeroExt(8, c[x]) to convert c[x] into a Bit-vector of size 16, 
    # by adding 0-bits. 
    d.append(ZeroExt(8, c[x])^second) 
    x += 2 
print "d:", d 

goal = str2array('\xbd\x23\x43\x23\x40\x23\x41\x23') 
print "goal:", goal 
# Note that, len(goal) == 2*len(d) 
# We can use Concat to concatenate adjacent elements. 

# We want each element of d[i] == Concat(goal[2*i], goal[2*i+1]) 
# We can use Z3 to find the 'b' that will satisfy these constraints 

s = Solver() 
# 's' is a Z3 solver object 
i = 0 
while i < len(d): 
    s.add(d[i] == Concat(goal[2*i+1], goal[2*i])) 
    i += 1 
print s 
# Now, 's' contains a set of equational constraints. 
print s.check() 
print s.model()