Defining constraints in Z3 using Boolean operators

Question

Let's say, I want to restrict each character of the string to the charset: [a-zA-Z0-9_] using Z3 constraints, can I use a boolean operator to specify that?

As an example:

input = [BitVec("input%s" % i, 8) for i in range(10)]

for i in range(10):
  s.add(input[i] >= 0x30 and input[i] <= 0x39)
  s.add(input[i] >= 0x41 and input[i] <= 0x5A)
  s.add(input[i] >= 0x61 and input[i] <= 0x7A)

Is this correct? Any other efficient way to define constraints?

Usually in Python, I could do something like:

import string

charset = string.uppercase + string.lowercase + string.digits + "_"

for i in charset:
    ...

Can something similar be done to define constraints in Z3?

Thanks.

alias · Accepted Answer · 2018-12-17 07:17:24Z

1

The best way to go about this would be to simply use z3's regular-expression matching facilities:

from z3 import *
import string

lower  = Union([Re(c) for c in string.lowercase])
upper  = Union([Re(c) for c in string.uppercase])
digs   = Union([Re(c) for c in string.digits])
uscore = Re('_')

charset = Union(lower, upper, digs, uscore)
lang    = Plus(charset)


s = Solver()
test = String("test")
s.add(Length(test) == 10)
s.add(InRe(test, lang))

print s.check()
print s.model()

This prints:

sat
[test = "9L25ZPC1B8"]

Or you can use it to test whether particular strings belong to the regular-expression you've defined:

>>> print (simplify(InRe("hEllO_123", lang)))
True
>>> print (simplify(InRe("%$", lang)))
False

answered Dec 17, 2018 at 7:17

alias

30.9k2 gold badges31 silver badges51 bronze badges

Sign up to request clarification or add additional context in comments.

Collectives™ on Stack Overflow

Defining constraints in Z3 using Boolean operators

1 Answer 1

Comments

Your Answer

Linked

Hot Network Questions

Collectives™ on Stack Overflow

1 Answer 1

Comments

Your Answer

Sign up or log in

Post as a guest

Linked

Related