Taschenanleitung zum Z3

Präambel

"Das menschliche Gehirn ist ein leerer Dachboden. Ein Dummkopf tut genau das: schleppt das Notwendige und das Unnötige dorthin. Und schließlich kommt ein Moment, in dem Sie nicht das Notwendigste dorthin schieben oder umgekehrt ..."

V.B. Livanov (aus dem Film "Sherlock Holmes und 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")

  
  

Erzwungene Minimierung

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

Verweise

Meiner Meinung nach die angenehmste Beschreibung

Verzeichnis

SMT-Logik

Beispiele: eins und zwei