Add one to an argument

Reverse run the add1 function. Note that the generated SMTLib will have the function add1 itself defined. You can verify this by running the below in verbose mode.

>>> add1Example
Satisfiable. Model:
  x = 4 :: Integer

Sum of numbers from 0 to the given number. Since this is a recursive definition, we cannot simply symbolically simulate it as it wouldn't terminat. So, we use the function generation facilities to define it directly in SMTLib. Note how the function itself takes a "recursive version" of itself, and all recursive calls are made with this name.

Prove that sumToN works as expected.

We have:

>>> sumToNExample
Satisfiable. Model:
  s0 =  5 :: Integer
  s1 = 15 :: Integer

Coding list-length recursively. Again, we map directly to an SMTLib function.

Calculate the length of a list, using recursive functions.

We have:

>>> lenExample
Satisfiable. Model:
  s0 = [1,2,3] :: [Integer]
  s1 =       3 :: Integer

A simple mutual-recursion example, from the z3 documentation. We have:

>>> pingPong
Satisfiable. Model:
  s0 = 1 :: Integer

Usual way to define even-odd mutually recursively. Unfortunately, while this goes through, the backend solver does not terminate on this example. See evenOdd2 for an alternative technique to handle such definitions, which seems to be more solver friendly.

Another technique to handle mutually definitions is to define the functions together, and pull the results out individually. This usually works better than defining the functions separately, from a solver perspective.

Extract the isEven function for easier use.

Extract the isOdd function for easier use.

We can prove 20 is even and definitely not odd, thusly:

>>> evenOdd2
Satisfiable. Model:
  s0 =    20 :: Integer
  s1 =  True :: Bool
  s2 = False :: Bool

Ackermann function, demonstrating nested recursion.

We can prove constant-folding instances of the equality ack 1 y == y + 2:

>>> ack1y
Satisfiable. Model:
  s0 = 5 :: Integer
  s1 = 7 :: Integer

Expecting the prover to handle the general case for arbitrary y is beyond the current scope of what SMT solvers do out-of-the-box for the time being.