Panduan Saku ke Z3

Pembukaan

"Otak manusia adalah loteng kosong. Orang bodoh melakukan hal itu: menyeret yang perlu dan tidak perlu ke sana. Dan akhirnya tiba saatnya ketika kamu tidak mendorong benda yang paling penting di sana atau sebaliknya ..."

V.B. Livanov (dari film "Sherlock Holmes and Dr. Watson")

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")

  
  

Minimalisasi Paksa

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

Referensi

Menurut saya deskripsi yang paling menyenangkan

Direktori

Logika SMT

Contoh: satu dan dua