voila

I hereby claim:

To claim this, I am signing this object:

	/*
	How many different ways can we make change of $ 1.00, given half-dollars, quarters, dimes, nickels, and pennies? More generally, can we write a procedure to compute the number of ways to change any given amount of money?

	This problem has a simple solution as a recursive procedure.
	Suppose we think of the types of coins available as arranged in some order. Then the following relation holds:

	The number of ways to change amount a using n kinds of coins equals

	the number of ways to change amount a using all but the first kind of coin, plus
	the number of ways to change amount a - d using all n kinds of coins, where d is the denomination of the first kind of coin.

	from z3 import *

	Jug, (Big, Small) = EnumSort(
	'Jug', ['Big', 'Small'])
	Act, (FillBig, FillSmall, EmptyBig, EmptySmall, BigToSmall, SmallToBig) = EnumSort(
	'Act', ['FillBig', 'FillSmall', 'EmptyBig', 'EmptySmall', 'BigToSmall', 'SmallToBig'])

	#m = 10
	for n in range(5, 10):
	print("n = {}".format(n))

	(declare-const n Int)
	(declare-datatypes () ((Jug Big Small)))
	(declare-datatypes () ((Act FillBig FillSmall EmptyBig EmptySmall BigToSmall SmallToBig)))
	(declare-fun vol (Jug Int) Int)
	(declare-fun act (Int) Act)

	(assert (= n 6))
	(assert (= (act 0) EmptyBig))
	(assert (= (vol Big 0) 0))
	(assert (= (vol Small 0) 0))

	/* Impose an ordering on the State. */
	open util/ordering[State]
	open util/integer

	/* Stores the jugs level */
	sig State { small, big:Int }

	/* initial state */
	fact { first.small = 0 && first.big = 0 }