How to implement Peano Arithmetic using Z3 Theorem prover?

I study Z3 Theorem prover and want to implement Peano Arithmetic. I did it in Prolog and now I want to make using Satisfiability Modulo Theories Solver.

The following code is my implementation of the addition. I do not understand why it runs in a very long search for a model and then produces: Z3Exception: model is not available.

Can you please suggest how to implement Peano Arithmetic (add, mul, less)?

from z3 import *

s = Solver()

Nat = Datatype('Nat')
Nat.declare('Z')
Nat.declare('S', ('pred', Nat))
Nat = Nat.create()

Z = Nat.Z
S = Nat.S

P = Function('P', Nat, Nat, Nat, BoolSort())
x, y, z = Consts('x y z', Nat)

s.add(P(Z,Z,Z))
s.add(ForAll([x], P(Z, x, x)))   
s.add(ForAll([x], P(x, Z, x))) 
s.add(ForAll([x,y,z], Implies(P(S(x), y, S(z)), P(x, y, z)))) 

x1 = Const('x1', Nat)
s.add(P(S(Z), S(Z), x1))

if s.check():
  print(s.model())

Solution

The "efficient" SMTLib way of doing this is to add recursive definitions for the functions. While what you wrote codes the intent correctly, it doesn't work well with the way SMT-solvers deal with recursive definitions. Instead, do the following:

from z3 import *

Nat = Datatype('Nat')
Nat.declare('Z')
Nat.declare('S', ('pred', Nat))
Nat = Nat.create()
pred = Nat.pred
Z    = Nat.Z
S    = Nat.S

P       = RecFunction('P', Nat, Nat, Nat)
addArg1 = FreshConst(Nat)
addArg2 = FreshConst(Nat)

RecAddDefinition( P
                , [addArg1, addArg2]
                , If(addArg1 == Z, addArg2, S(P(pred(addArg1), addArg2)))
                )

Now, P is the addition over naturals. We can use it like this:

x1 = Const('x1', Nat)

s = Solver()
s.add(x1 == P(S(Z), S(Z)))

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

This prints:

sat
[x1 = S(S(Z))]

Correctly calculating x1 to be 2. Or, you can ask:

s = Solver()
s.add(S(S(Z)) == P(x1, x1))

And you get:

sat
[x1 = S(Z),
 P = [else ->
      If(Var(0) == Z, Var(1), S(P(pred(Var(0)), Var(1))))]]

(You can ignore the assignment to P; it's how it is stored in the model.)

While this is how recursive definitions are handled in SMTLib, I should add that such definitions are hard to deal with in the SMTLib formalism. In particular, any theorem that requires induction over Nat will be hard to prove, if not impossible, since SMT-solvers don't do induction, at least not yet.