Определение ограничений в Z3 с использованием логических операторов - PullRequest
Новая
       19

Определение ограничений в Z3 с использованием логических операторов

0 голосов
/ 17 декабря 2018

Скажем, я хочу ограничить каждый символ строки набором символов: [a-zA-Z0-9_] используя ограничения Z3, могу ли я использовать логический оператор, чтобы указать это?

Какпример: 

input = [BitVec("input%s" % i, 8) for i in range(10)]

for i in range(10):
  s.add(input[i] >= 0x30 and input[i] <= 0x39)
  s.add(input[i] >= 0x41 and input[i] <= 0x5A)
  s.add(input[i] >= 0x61 and input[i] <= 0x7A)

Это правильно?Любой другой эффективный способ определения ограничений?

Обычно в Python я могу сделать что-то вроде: 

import string

charset = string.uppercase + string.lowercase + string.digits + "_"

for i in charset:
    ...

Можно ли сделать что-то подобное для определения ограничений в Z3?

Спасибо.

1 Ответ

0 голосов
/ 17 декабря 2018

Лучший способ сделать это - просто использовать средства сопоставления регулярных выражений в z3: 

from z3 import *
import string

lower  = Union([Re(c) for c in string.lowercase])
upper  = Union([Re(c) for c in string.uppercase])
digs   = Union([Re(c) for c in string.digits])
uscore = Re('_')

charset = Union(lower, upper, digs, uscore)
lang    = Plus(charset)


s = Solver()
test = String("test")
s.add(Length(test) == 10)
s.add(InRe(test, lang))

print s.check()
print s.model()

Это печатает: 

sat
[test = "9L25ZPC1B8"]

Или вы можете использовать его для проверкипринадлежат ли определенные строки определенному вами регулярному выражению: 

>>> print (simplify(InRe("hEllO_123", lang)))
True
>>> print (simplify(InRe("%$", lang)))
False
...