100 Languages Speedrun: Episode 23: Ruby Z3

Let's talk about something I made.
Once upon a time, "logic programming" was a big thing. The idea was to just give the computer a bunch of mathematical statements, and have it do the math and logic to arrive at answer. There were even whole languages like Prolog centered around this.
This approach basically died out. As it turns out logic programming languages are bad at everything other than logic. And it also turns out the forms of logic they're based on ("Horn clauses") are bad for logic as well.
The modern approach is to use general purpose programming language, and some kind of constraint solver engine (also known as theorem prover etc. - this field is really suffering from inconsistent terminology). In this episode we'll explore Microsoft Research's Z3. I didn't like any of its existing bindings, so I created Ruby bindings for it that I consider far superior, and we'll be covering this here.
Installation
To get Ruby Z3 going, you'll need to run these on OSX, or some obvious equivalent on other platforms. It's best to use latest version:
$ brew install z3
$ gem install z3
Getting Started
Let's write some very simple Z3 programs. Since you're probably new to constraint solvers, I'll go slow, as there will be a few concepts to explain on the way.
Let's try to solve 2 + X = 4.
#!/usr/bin/env ruby

require "z3"

solver = Z3::Solver.new
solver.assert 2 + Z3.Int("X") == 4

if solver.satisfiable?
  model = solver.model
  puts "X = #{model[Z3.Int("X")]}"
else
  puts "There are no solutions"
end
Which prints rather unsurprising:
$ ./x_plus_2_equals_4
X = 2
What is going on here?
  • first we create a solver instance - we'll generally create a new one for each problem we're solving
  • then we give the solver some equations
  • these equations contain variables, which are basically "symbols with types". Instead of saying 2 + Z3.Var("X") == 4 and telling it Z3.Var("X") is an integer separately, each variable carries both its name and its type (called "sort" in Z3, mostly to avoid confusion with programming language types).
  • once we're done, we ask Z3 if what it got is satisfiable?
  • if yes, we ask for a model - model is like a dictionary of assignments of variables to values. If there are many possible models, Z3 will only give us one.
  • then we ask the model what's the value of X and print it
  • Ruby allows operator overloading including == operator. This is much more readable than typing out something like Z3.Equals(Z3.Add(Z3.Number(2), Z3.Int("X")), Z3.Number(4))).
    There are a few caveats. The biggest one is that and/&&, or/||, and ?: are not overloadable in Ruby, so we'd need to use & and | instead.
    If you're curious, they cannot be regular methods - methods evaluate their arguments first, then run method code. In case of these, the right side evaluates or doesn't depending on what the left side does.
    SEND + MORE = MONEY
    Let's try another quick one, the famous "verbal arithmetic puzzle" SEND+MORE=MONEY. Every letter stands for a different digit, and initial digits cannot be zero.
    #!/usr/bin/env ruby
    
    require "z3"
    
    solver = Z3::Solver.new
    letters = %w[s e n d m o r e m o n e y].uniq.to_h{|letter| [letter, Z3.Int(letter)]}
    
    letters.each_value do |var|
      solver.assert var >= 0
      solver.assert var <= 9
    end
    
    solver.assert letters["m"] != 0
    solver.assert letters["s"] != 0
    
    solver.assert Z3.Distinct(*letters.values)
    
    send = 1000 * letters["s"] + 100 * letters["e"] + 10 * letters["n"] + letters["d"]
    more = 1000 * letters["m"] + 100 * letters["o"] + 10 * letters["r"] + letters["e"]
    money = 10000 * letters["m"] + 1000 * letters["o"] + 100 * letters["n"] + 10 * letters["e"] + letters["y"]
    
    solver.assert send + more == money
    
    if solver.satisfiable?
      model = solver.model
      model.each do |var, value|
        puts "#{var}=#{value}"
      end
      puts "#{model[send]} + #{model[more]} = #{model[money]}"
    else
      puts "There are no solutions"
    end
    Which prints:
    $ ./send_more_money
    d=7
    e=5
    m=1
    n=6
    o=0
    r=8
    s=9
    y=2
    9567 + 1085 = 10652
    There's a lot going on here, so let's take it step by step:
  • writing Z3.Int(letter) can get rather tedious, so I created a dictionary {"s" => Z3.Int("s"), ...} to make the code a bit more concise.
  • for every letter variable, we tell the solver that var >= 0 and var <= 9
  • for initial letter variables, we tell the solver that they're not 0, as per rules of the puzzle
  • not everything can use operator overloading - for example to tell the solver that all variables are distinct, we use special Z3.Distinct(var1, var2, ...) instead of double nested loop of var1 != var2
  • we calculate what would SEND, MORE, and MONEY be with just some normal * and +
  • we check if it's satisfiable
  • if yes, we ask for a model
  • we can do interesting thing with the model - we can ask it to print all variables it knows about and their values
  • but the model can also evaluate expressions (if they only use known variables) like SEND, MORE, and MONEY
  • The whole code is just delightful.
    Fibonacci
    Z3 has support for many very fancy things like functions, sets, and so on, but it's best if we limit ourselves to just simplest sorts for now. For an extremely simple Fibonacci solver, let's just declare integer variables called "fib(0)" to "fib(100)":
    #!/usr/bin/env ruby
    
    require "z3"
    
    solver = Z3::Solver.new
    
    fib = (0..100).map{|i| Z3.Int("fib(#{i})")}
    
    solver.assert fib[0] == 0
    solver.assert fib[1] == 1
    
    (2..100).each do |i|
      solver.assert fib[i] == fib[i-1] + fib[i-2]
    end
    
    if solver.satisfiable?
      model = solver.model
      fib.each do |var|
        puts "#{var}=#{model[var]}"
      end
    else
      puts "There are no solutions"
    end
    Which prints just what we'd expect:
    $ ./fib
    fib(0)=0
    fib(1)=1
    fib(2)=1
    fib(3)=2
    fib(4)=3
    fib(5)=5
    fib(6)=8
    fib(7)=13
    fib(8)=21
    fib(9)=34
    fib(10)=55
    fib(11)=89
    fib(12)=144
    fib(13)=233
    fib(14)=377
    fib(15)=610
    fib(16)=987
    fib(17)=1597
    fib(18)=2584
    fib(19)=4181
    fib(20)=6765
    ...
    fib(90)=2880067194370816120
    fib(91)=4660046610375530309
    fib(92)=7540113804746346429
    fib(93)=12200160415121876738
    fib(94)=19740274219868223167
    fib(95)=31940434634990099905
    fib(96)=51680708854858323072
    fib(97)=83621143489848422977
    fib(98)=135301852344706746049
    fib(99)=218922995834555169026
    fib(100)=354224848179261915075
    We didn't have to tell Z3 how to evaluate this series, just how the variables are related to each other. Z3 Integers have unlimited size, and it's super fast (<0.1s on my laptop, mostly just startup time).
    Reverse Fibonacci
    That's probably not too impressive, so let's try something fancier. What if we only told Z3 what's fib(42) and fib(69) and asked it for the rest?
    #!/usr/bin/env ruby
    
    require "z3"
    
    solver = Z3::Solver.new
    
    fib = (0..100).map{|i| Z3.Int("fib(#{i})")}
    
    solver.assert fib[42] == 267914296
    solver.assert fib[69] == 117669030460994
    
    (2..100).each do |i|
      solver.assert fib[i] == fib[i-1] + fib[i-2]
    end
    
    if solver.satisfiable?
      model = solver.model
      fib.each do |var|
        puts "#{var}=#{model[var]}"
      end
    else
      puts "There are no solutions"
    end
    Yes, that works just as well as the previous version, printing identical output!
    Sudoku Solver
    The Sudoku Solver is the FizzBuzz equivalent for constraint solvers, so let's write one!
    #!/usr/bin/env ruby
    
    require "z3"
    
    sudoku = %w[
      _6_5_9_4_
      92_____76
      __1___9__
      7__6_3__9
      _________
      3__4_1__7
      __6___7__
      24_____65
      _9_1_8_3_
    ]
    
    solver = Z3::Solver.new
    
    vars = (0..8).map{|y|
      (0..8).map{|x|
        Z3.Int("cell[#{x},#{y}]")
      }
    }
    
    # All cells are 1-9
    vars.flatten.each do |var|
      solver.assert var >= 1
      solver.assert var <= 9
    end
    
    # Cells match sudoku grid if it already has numbers
    9.times do |y|
      9.times do |x|
        if sudoku[y][x] =~ /\d/
          solver.assert vars[y][x] == sudoku[y][x].to_i
        end
      end
    end
    
    # Each row has distinct numbers
    vars.each do |row|
      solver.assert Z3.Distinct(*row)
    end
    
    # Each column has distinct numbers
    vars.transpose.each do |col|
      solver.assert Z3.Distinct(*col)
    end
    
    # Each box has distinct numbers
    [0, 3, 6].each do |i|
      [0, 3, 6].each do |j|
        cells = vars[i, 3].flat_map{|row| row[j, 3]}
        solver.assert Z3.Distinct(*cells)
      end
    end
    
    if solver.satisfiable?
      model = solver.model
      9.times do |y|
        9.times do |x|
          print model[vars[y][x]]
        end
        print "\n"
      end
    end
    And it does exactly what we want:
    $ ./sudoku
    863579241
    925314876
    471826953
    714683529
    689752314
    352491687
    136245798
    248937165
    597168432
    The example is a bit longer, but there's nothing complicated here, it's just a list of assertions about what we want, Z3 does some Underpants Gnomes Magic, and then we print the result and profit!
    Since we're using Ruby, it would be very easy to extend it with reading sudoku from a file, any kind of fancy formatting, or putting it as a web service. This is something logic programming languages like Prolog really struggled wit, but general purpose lanugages are great at.
    Proving facts about Bit Vectors
    After integers and booleans, the next most common sort would likely be fixed-size integer bit vectors, that is signed and unsigned ints used in most lower level programming languages.
    Theorem provers can be used in a few ways. The way we used Z3 so far is by feeding it a list of assertions. It then either constructs a model that satisfies the assertions, or it proves that it's impossible (... or takes million years to finish so you'll never know).
    Sometimes we're interested in the model, and theorem prover telling us it can't be done is sort of a fail, like Sudoku that's impossible to solve.
    But sometimes we want the opposite. We want to make sure X is true. So we send Z3 a list of assertions, then we send it not X, and ask for a model. If it says imposible, then this proves X. Otherwise the model is the counterexample, so we not only know X is not always true, but we have an example for it.
    Let's take one simple bit trick from the Bit Twiddling Hacks site, and implement it incorrectly - "Determining if an integer is a power of 2".
    #!/usr/bin/env ruby
    
    require "z3"
    
    solver = Z3::Solver.new
    v = Z3.Bitvec("v", 64)
    
    naive_is_power_of_two = Z3.Or(*(0..63).map{|i| v == 2**i})
    tricky_is_power_of_two = (v & (v - 1)) == 0
    
    theorem = (tricky_is_power_of_two == naive_is_power_of_two)
    
    solver.assert !theorem
    
    if solver.satisfiable?
      counterexample = solver.model
      puts "Counterexample exists:"
      counterexample.each do |n,v|
        puts "* #{n} = #{v}"
      end
    else
      puts "There are no counterexamples, it always holds."
    end
    And let's give it a go:
    $ ./power_of_two
    Counterexample exists:
    * v = 0
    Damn, the theorem is wrong, and doesn't hold for v = 0!
    Let's walk through the code:
  • Z3.Bitvec("v", 64) declared v as 64-bit bit vector (int64 or such in most low level languages). Z3 doesn't distinguish between "signed" and "unsigned" bitvectors - for operations where it matters like >, it provides .signed_gt and .unsigned_gt versions, but most things (+, *, ==, &, |) etc. work the same.
  • we construct naive_is_power_of_two as (v == 1) | (v == 2) | (v == 4) | ... | (v == 2**63). Z3.Or(s1, s2, s3, ...) is a shortcut, as it's very common code. As I mentioned before, Ruby's || cannot be overloaded so we need to use either | or Z3.Or.
  • we construct tricky_is_power_of_two to be our trick operation. For bitvectors, Z3 provides bit operations like &, |, ^ etc., in addition to regular arithmetic. Z3 generally cannot do bit operations on unlimited size integers.
  • we ask Z3 if it can give us any example where our theorem tricky_is_power_of_two == naive_is_power_of_two could be false
  • and it does
  • Let's try to fix it:
    #!/usr/bin/env ruby
    
    require "z3"
    
    solver = Z3::Solver.new
    v = Z3.Bitvec("v", 64)
    
    naive_is_power_of_two = Z3.Or(*(0..63).map{|i| v == 2**i})
    tricky_is_power_of_two = (v != 0) & ((v & (v - 1)) == 0)
    
    theorem = (tricky_is_power_of_two == naive_is_power_of_two)
    
    solver.assert !theorem
    
    if solver.satisfiable?
      counterexample = solver.model
      puts "Counterexample exists:"
      counterexample.each do |n,v|
        puts "* #{n} = #{v}"
      end
    else
      puts "There are no counterexamples, it always holds."
    end
    And this time it works:
    $ ./power_of_two_2
    There are no counterexamples, it always holds.
    It would be completely impractical to brute force check all 2**64 possible values, but for Z3 it's no big deal.
    Physics Textbook Problems
    #!/usr/bin/env ruby
    
    # A race car accelerates uniformly from 18.5 m/s to 46.1 m/s in 2.47 seconds.
    # Determine the acceleration of the car and the distance traveled.
    
    require "z3"
    
    solver = Z3::Solver.new
    
    a = Z3.Real("a")
    v0 = Z3.Real("v0")
    v1 = Z3.Real("v1")
    t = Z3.Real("t")
    d = Z3.Real("d")
    
    solver.assert a == (v1 - v0) / t
    solver.assert v0 == 18.5
    solver.assert v1 == 46.1
    solver.assert t == 2.47
    solver.assert d == (v0 + v1) / 2 * t
    
    if solver.satisfiable?
      model = solver.model
      model.each do |var, value|
        puts "#{var}=#{value}"
      end
    else
      puts "There are no solutions"
    end
    Let's give it a try:
    $ ./physics
    a=2760/247
    d=79781/1000
    t=247/100
    v0=37/2
    v1=461/10
    For Real numbers, Z3 will use exact rational form by default. You can turn them into fixed floating point numbers for display with .to_f.
    Z3 also has computer-style fixed-sized floats, if you want to prove some facts about Quake's inverse square root algorithm.
    I could be going, but the episode is already quite long. Z3 gem comes with many examples, including crazy things like Regular Expression Crossword Solver - which takes a crossword where the hints are regular expressions and cells are letters, and figures out the solution.
    Should you use Z3?
    Absolutely! Z3 is the best constraint solver engine out there, and it's very popular for serious uses like hacking CTF competitions.
    When using Z3 or any other constraint solver, it's important to remember than performance can be extremely unpredictable. Some sets of constraints can be solved in a few seconds, while others can take days, even though they look very similar. If you let users throw data at your constraint solver, it's best to put it in a separate process, with proper timeouts and error handling.
    Should you use Ruby Z3?
    Z3 comes with a few officially supported languages, of which the only one worth considering is Python. I didn't love that version, so I created Ruby bindings, which I think are a bit better overall, but nobody can fault you if you prefer Python.
    There's a small issue that Z3 has some experimental features which aren't very stable from version to version, so the Ruby gem might take longer to update than officially maintained Python version. But that doesn't affect any of the common use cases (like booleans, integers, bit vectors, reals, floats etc.).
    Code

    31

    This website collects cookies to deliver better user experience

    100 Languages Speedrun: Episode 23: Ruby Z3