Guide de poche du Z3

Préambule

"Le cerveau humain est un grenier vide. Un imbécile fait exactement cela: y traîne le nécessaire et l'inutile. Et enfin, il arrive un moment où vous ne poussez pas la chose la plus nécessaire là ou vice versa ..."

V.B. Livanov (extrait du 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")

  
  

Minimisation forcée

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

Références

À mon avis, la description la plus agréable

Annuaire

Logique SMT

Exemples: un et deux