Set Solver for string constraints

Question

I'm trying to implement a solver for a problem (which requires string manipulations) using z3 in python. I've tried reading documentation, but there aren't enough informations. I've also tried to read z3str documentation but I can't find a way to make my examples working.

I would like to set :

len(string) = 8
string[6] = 'a'
string_possible_characters = '3456789a'
string.count("6") = 2

Is it better to use in this case something like itertools (permutations + combinations) ?

Answer 1

z3 can solve such problems with relative ease. There's a bit of a learning curve regarding the use of the API, but it's well worth investing in. Having said that, if your constraints are relatively simple and strings are short, enumerating them and checking the constraints using regular programming can be a quick and effective alternative. But for longer strings and more complicated constraints, z3 would be a great choice for this sort of problem.

Here's how I would code your example in Python:

# Bring z3 to scope
from z3 import *

# Grab a solver
s = Solver ()

# Create a symbolic string
string = String('string')

# len(string) = 8
s.add(Length(string) == 8)

# string[6] = 'a'
s.add(SubSeq(string, 6, 1) == StringVal('a'))

# string_possible_characters = '3456789a'
chars    = Union([Re(StringVal(c)) for c in '345789a'])   # Note I left 6 out on purpose!
six      = Re(StringVal('6'))

# string.count("6") = 2
# Create a regular expression that matches exactly two occurences
# of 6's and any other allowed character in other positions
template = Concat(Star(chars), six, Star(chars), six, Star(chars))

# Assert our string matches the template
s.add(InRe(string, template))

# Get a model
res = s.check()
if res == sat:
    print s.model()
else:
    print "Solver said:",
    print res

When I run it, I get:

[string = "634436a9"]

which satisfies all your constraints. You can build on this template to model other constraints. Relevant part of the API is here: https://z3prover.github.io/api/html/z3py_8py_source.html#l10190

Note that Python isn't the only API that provides access to Z3 regular-expressions and strings; almost all other high-level bindings to z3 include some level of support, including C/C++/Java/Haskell etc. And depending on the abstractions provided by those bindings, these constraints might even be easier to program. For instance, here's the same problem coded using the SBV Haskell package, which uses z3 as the underlying solver:

{-# LANGUAGE OverloadedStrings #-}

import Data.SBV

import qualified Data.SBV.String as S
import           Data.SBV.RegExp

p :: IO SatResult
p = sat $ do s <- sString "string"

             let others   = KStar $ oneOf "345789a"
                 template = others * "6" * others * "6" * others

             constrain $ S.length s        .== 8
             constrain $ S.strToCharAt s 6 .== literal 'a'
             constrain $ s `match` template

When run, this program produces:

*Main> p
Satisfiable. Model:
  string = "649576a8" :: String

As you see, Haskell encoding is rather concise and easy to read, while encodings in other languages (such as C, Java etc.) are likely to be more verbose. Of course, you should pick a host language that works the best for you, but if you've freedom to do so, I'd recommend the Haskell bindings for ease of use. Details are here: http://hackage.haskell.org/package/sbv