z3_factorial_test.py

# http://fstar-lang.org/tutorial/book/under_the_hood/uth_smt.html#designing-a-library-with-smt-patterns
from z3 import *

Fuel = Datatype('Fuel')
Fuel.declare('ZFuel')
Fuel.declare('SFuel', ('pred', Fuel))
Fuel = Fuel.create()
ZFuel = Fuel.ZFuel
SFuel = Fuel.SFuel

Factorial = Function('factorial', IntSort(), IntSort())
FactorialFueled = Function('factorialFueled', Fuel, IntSort(), IntSort())

s = Solver()
fuel0 = Const('fuel0', Fuel)
x0 = Int('x0')
s.add(ForAll([fuel0, x0], 
    FactorialFueled(SFuel(fuel0), x0) == If(x0 <= 0, 1, x0 * FactorialFueled(fuel0, x0 - 1)), 
    patterns=[FactorialFueled(SFuel(fuel0), x0)],
    weight=0,
    qid="equation_with_fuel_SMTEncoding.factorial.fuel_instrumented"))

fuel1 = Const('fuel1', Fuel)
x1 = Int('x1')
s.add(ForAll([fuel1, x1], 
    FactorialFueled(SFuel(fuel1), x1) == FactorialFueled(ZFuel, x1),
    patterns=[FactorialFueled(SFuel(fuel1), x1)],
    qid="fuel_irrelevance_SMTEncoding.factorial.fuel_instrumented"))

maxFuel = Const('maxFuel', Fuel)

x2 = Int('x2')
s.add(ForAll([x2], 
    FactorialFueled(maxFuel, x2) == Factorial(x2),     
    patterns=[Factorial(x2)],
    qid="fuel_correspondence_SMTEncoding.factorial.fuel_instrumented"))


s.add(maxFuel == SFuel(SFuel(ZFuel)))
s.add(Factorial(2) == 2)

#print(s.sexpr())
r = s.check()
print(r)
if r == sat:
    print(s.model())