Guía de bolsillo para el Z3

Preámbulo

"El cerebro humano es un ático vacío. Un tonto hace exactamente eso: arrastra lo necesario y lo innecesario allí. Y finalmente, llega el momento en que no empujas lo más necesario allí o viceversa ..."

V.B. Livanov (de la película "Sherlock Holmes y 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")

  
  

Minimización Forzada

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

Referencias

En mi opinión, la descripción más agradable

Directorio

Lógica SMT

Ejemplos: uno y dos