Карманное руководство по Z3

Преамбула

"Человеческий мозг это пустой чердак. Дурак так и делает: тащит туда нужное и не нужное. И наконец наступает момент, когда самую необходимую вещь туда не запихнешь, или наоборот не достанешь..."

В.Б. Ливанов (из к/ф "Шерлок Холмс и доктор Ватсон")

Данное руководство не охватывает весь функционал SMT решателя. Оно написано для таких ситуаций, когда человеку срочно нужно вспомнить, подсмотреть как реализовать ту или иную его идею, не тратя много времени на поиск информации, отладку и т.д. Иными словами это руководство — шпаргалка, затрагивающая лишь часто применяемое.

Типы данных

• x = Int('x')

  
  

• y = Real('y')

  
  

• z = Bool('z')

  
  

• s = String('s')

  
  

• x, y, z = Ints('x y z')

  
  

• x, y, z = Reals('x y z')

  
  

• x, y, z = Bools('x y z')

  
  

• x, y, z = Strings('x y z')

  
  

• v = BitVec('v', N) # N — размер бит-вектора

  
  

• X = IntVector('X', N)

  
  

• Y = RealVector('Y', N)

  
  

• Z = BoolVector('Z', N)

  
  

• A = Array('A', b, c) # b — область определения, с — диапазон

  
  

• Select(A, i) # все равно что A[i]

  
  

• Store('A', i, a) # возвращает массив A c a на i-ой позиции

  
  

• FloatingPoint = FP('fp', FPSort(ebits, sbits)) # формат IEEE 754

  
  

• v = BitVecVal(10, 32) # бит-вектор 0x0000000a

  
  

• str = StringVal("aaaaa")

  
  

• c = Const(5, IntSort())

  
  

Регулярные выражения

reg = Re('re')

re = Loop( reg, L, U ) # L — нижняя граница, U — верхняя граница

Ex:

re = Loop( Re('a') , 2, 5)

print( simplify( InRe( "aaaa", re ) ) )

print( simplify( InRe( "a", re ) ) )

Out:

True

False

Операции

Логические связки

• And(a, b)

  
  

• Not(a)

  
  

• Or(a, b)

  
  

• Xor(a, b)

  
  

• Implies(a, b) # a == b для булевых a и b

  
  

Строки

• PrefixOf(substr, str)

  
  

• SuffixOf(substr, str)

  
  

• Concat(str1, str2)

  
  

• Length(str)

  
  

Другие полезные функции

• Sum(a, b, c)

Out:

0 + a + b + c

• Product(a, b, c)

Out:

1 * a * b * c

• Distinct(x, y)

Out:

x != y

• simplify(Distinct(x, y, z), blast_distinct=True)

Out:

And(Not(x == y), Not(x == z), Not(y == z))

• Extract(L, U, 'x') # L — верхняя граница, U — нижняя граница

Ex:

s = Solver()

x = BitVec('x', 8)

k = Extract(3, 0, x)

s.add(k == BitVecVal(10,4))

s.check()

print(s.model())

Out:

x = 10

• LShR(x, i) # x >> i

  
  

• RotateLeft(a, i)

  
  

• RotateRight(a, i)

  
  

Solver

SMT Solver — уже готовое универсальное решение.

s = Solver()

s = SolverFor('proc') # выбрать процедуру принятия решений

• s.push/pop() # создать/вернуть изменения

  
  

• s.statistics() # посмотреть внутренние счетчики решателя

  
  

• s.assertions() # посмотреть какие утверждения лежат в решателе

  
  

• set_option() # установить опции для решателя

  
  

Ex:

set_option(precision=10)    #   точность 10 знаков после запятой (вывод может быть усечен решателем с помощью знака "?" )

• s.check() # проверить модель на наличие решений ( возможны 3 состояния: sat/unsat/unknown )

  
  

• simplify() # упрощение модели

  
  

• s.sexpr() # извлечение состояния в SMT-LIB2

  
  

• s.model() # модель решения

  
  

• s.reset() # сбросить состояние решателя

  
  

Оптимизации

Оптимизация модели для переменной t

o = Optimize()

• o.maximize(t)

  
  

• o.minimize(t)

  
  

Ex:

x1, x2, x3, x4, x5, m = Reals('x1 x2 x3 x4 x5 m')

o = Optimize()

o.add(-5 * x1 - 5 * x2 + 0 * x3 + 0 * x4 + 20 * x5 == 2 )

o.add( 0 * x1 +5 * x2 - 10 * x3 + 0 * x4 - 5 * x5 == 3 )

o.add( 0 * x1 -5 * x2 + 0 * x3 - 15 * x4 + 15 * x5 == 1 )

o.add( x1>=0, x2>=0, x3>= 0, x4>= 0, x5>= 0)

o.add( 0 * x1 -1 * x2 + 0 * x3 + 0 * x4 - 0.5 * x5 == m )

h = o.maximize(m)

if o.check() == sat:

    print(o.lower(h))

    print(o.model())

Out:

h =  -6/5
[x3 = 0, x5 = 2/5, m = -6/5, x4 = 0, x1 = 1/5, x2 = 1]

Понятие цели

Goal (цель) — это ограничения которые мы даем решателю. Обработка цели происходит в соответствии с тактикой. Тактика превращает цель в подцели. Цель решаема, если хотя бы одна подцель решаема.

g = Goal()

g.add(...)

Копирование Goal

c = Context()

g2 = g.translate(c)

Тактики

Тактика позволяет изменить набор ограничений для цели. Для создания тактик используются комбинаторы.

• tactics() — посмотреть доступные тактики

  
  

• tactic_description('tactic_name') — посмотреть описание тактики

  
  

Ex:

g = Goal()

x, y = Ints('x y')

g.add(x == y + 1)

t  = With(Tactic('add-bounds'), add_bound_lower=0, add_bound_upper=10)

g2 = t(g)

print(g2.as_expr())

Out:

And(x == y + 1, x <= 10, x >= 0, y <= 10, y >= 0)

Комбинаторы тактик

• Then(t, s) # t — тактика цели

  
  

• OrElse(t, s) # s — тактика подцели

  
  

• Repeat(t)

  
  

• TryFor(t, ms) # ms — милисекунды

  
  

• With(t, params) # params — параметры для тактики

  
  

Ex:

Then('simplify', 'nlsat').solver()

Арифметики

Таблица логик

Советы

Решатели для строк

• s.set( "smt.string.solver","seq" )

  
  

• s.set( "smt.string.solver","z3str3" )

  
  

Принудительные минимизации

• s.set( "smt.core.minimize","true" )

Ссылки

На мой взгляд самое приятное описание

Справочник

SMT логики

Примеры: раз и два