Playing with Z3 Theorem Prover

Once again it’s Christmas time which, to me, means time for leisure. While I am not an avid gamer, sometimes I play simple, non-engaging games on my phone. One of the games in particular is Calculator: The Game.  It is a very simple game and your goal is to calculate a number within some operation count limit. Here is a screenshot.

For example, in this particular level your goal is to calculate -120 within 4 moves. Here is brief description of the operations you can apply:

Let’s give these operations proper names: Mul5, Sub6 and Append4. The solution is to apply these operations in the following order:

I love to play this kind of games for about 10-15 minutes. So yesterday, after I played for a bit, my mind was drifting and I was in the perfect mood for learning something new. Part of my mind was still busy with the game, so I took the opportunity to learn a bit about Z3 Theorem Prover. Googling for “Z3 tutorial” and following the first search result landed me on the rise4fun Z3 page. It’s a wonderful online playground for Z3. I skimmed over the tutorial and felt confident enough that I get the basics, so I decided to give it a try.

First, we have to define Mul5, Sub6 and Append4 operations.

(define-fun Mul5 ((x Int)) Int (* x 5))
(define-fun Sub6 ((x Int)) Int (- x 6))
(define-fun Append4 ((x Int)) Int
    (ite (< x 0) (- (* x 10) 4) (+ (* x 10) 4))
)

Then we have to model the gameplay. We have 4 moves (steps) and on each step we have to apply exactly one operation. We can model each step as follows:

c1*Mul5 + c2*Sub6 + c3*Append4

The integer coefficients c1, c2 and c3 are constrained as follows:

0 <= c1 <= 1
0 <= c2 <= 1
0 <= c3 <= 1
c1 + c2 + c3 = 1

This guarantees us that exactly one operation will be applied on each step. Let’s code it for step 1.

(declare-fun s1Mul5 () Int)
(declare-fun s1Sub6 () Int)
(declare-fun s1Append4 () Int)
(assert (and (<= 0 s1Mul5) (<= s1Mul5 1)))
(assert (and (<= 0 s1Sub6) (<= s1Sub6 1)))
(assert (and (<= 0 s1Append4) (<= s1Append4 1)))
(assert (= 1 (+ s1Mul5 s1Sub6 s1Append4)))

(define-fun Step1 ((x Int)) Int
    (+ (* s1Mul5 (Mul5 x)) (* s1Sub6 (Sub6 x)) (* s1Append4 (Append4 x)))
)

The code for steps 2, 3 and 4 is similar to the code for step 1. Finally, the result from each step should be the input value for the next step.

(define-fun Level38 ((x Int)) Int
    (Step4 (Step3 (Step2 (Step1 x))))
)

I guess my game model is clumsy but this is what I’ve got with after 30 minutes skimming over the tutorial and playing with the examples. Finally, we can test our model as follows:

(assert (= (Level38 0) -120))

(check-sat)
(get-model)

Here is the output.

sat
(model
  (define-fun s1Mul5 () Int
    0)
  (define-fun s1Sub6 () Int
    0)
  (define-fun s1Append4 () Int
    1)
  (define-fun s2Mul5 () Int
    0)
  (define-fun s2Sub6 () Int
    1)
  (define-fun s2Append4 () Int
    0)
  (define-fun s3Mul5 () Int
    0)
  (define-fun s3Sub6 () Int
    0)
  (define-fun s3Append4 () Int
    1)
  (define-fun s4Mul5 () Int
    1)
  (define-fun s4Sub6 () Int
    0)
  (define-fun s4Append4 () Int
    0)
)

So, Z3 calculated the sequence s1Append4, s2Sub6, s3Append4, s4Mul5 satisfies our model which is indeed a solution for that game level. You can find the full code here and you can play with it on the rise4fun playground as well. Let’s try to find a solution for another end goal, say -130 instead of -120.

(assert (= (Level38 0) -130))

(check-sat)
(get-model)

Here is the output for new solution.

sat
(model
  (define-fun s1Mul5 () Int
    0)
  (define-fun s1Sub6 () Int
    1)
  (define-fun s1Append4 () Int
    0)
  (define-fun s2Mul5 () Int
    0)
  (define-fun s2Sub6 () Int
    1)
  (define-fun s2Append4 () Int
    0)
  (define-fun s3Mul5 () Int
    0)
  (define-fun s3Sub6 () Int
    0)
  (define-fun s3Append4 () Int
    1)
  (define-fun s4Mul5 () Int
    0)
  (define-fun s4Sub6 () Int
    1)
  (define-fun s4Append4 () Int
    0)
)

Indeed, if you the apply the following steps s1Sub6, s2Sub6, s3Append4, s4Sub6 you will get end result -130.

In closing, I would say that using Z3 seems quite intuitive and easy. Z3 provides bindings for C/C++, Java, .NET, Python and ML/OCalm which makes it accessible from most popular programming languages.