Documentation.SBV.Examples.Puzzles.Jugs

Solves the classic water jug puzzle: We have 3 jugs. The capacity of the jugs are 8, 5, and 3 gallons. We begin with the 8 gallon jug full, the other two empty. We can transfer from any jug to any other, completely topping off the latter. We want to end with 4 gallons of water in the first and second jugs, and with an empty third jug. What moves should we execute in order to do so?

Documentation

data Jug

A Jug has a capacity (i.e., maximum amount of water it can hold), and content, showing how much it currently has. The invariant is that content is always non-negative and is at most the capacity.

Constructors

Jug

Fields

• capacity :: Integer
• content :: SInteger

Instances

Generic Jug

Defined in Documentation.SBV.Examples.Puzzles.Jugs

Associated Types

type Rep Jug

Defined in Documentation.SBV.Examples.Puzzles.Jugs

type Rep Jug = D1 ('MetaData "Jug" "Documentation.SBV.Examples.Puzzles.Jugs" "sbv-10.12-inplace" 'False) (C1 ('MetaCons "Jug" 'PrefixI 'True) (S1 ('MetaSel ('Just "capacity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer) :*: S1 ('MetaSel ('Just "content") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SInteger)))

Methods

from :: Jug -> Rep Jug x

to :: Rep Jug x -> Jug

Mergeable Jug

Defined in Documentation.SBV.Examples.Puzzles.Jugs

Methods

symbolicMerge :: Bool -> SBool -> Jug -> Jug -> Jug

select :: (Ord b, SymVal b, Num b, Num (SBV b)) => [Jug] -> Jug -> SBV b -> Jug

type Rep Jug

Defined in Documentation.SBV.Examples.Puzzles.Jugs

type Rep Jug = D1 ('MetaData "Jug" "Documentation.SBV.Examples.Puzzles.Jugs" "sbv-10.12-inplace" 'False) (C1 ('MetaCons "Jug" 'PrefixI 'True) (S1 ('MetaSel ('Just "capacity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer) :*: S1 ('MetaSel ('Just "content") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SInteger)))

transfer :: Jug -> Jug -> (Jug, Jug)

Transfer from one jug to another. By definition, we transfer to fill the second jug, which may end up filling it fully, or leaving some in the first jug.

initJugs :: (Jug, Jug, Jug)

At the beginning, we have an full 8-gallon jug, and two empty jugs, 5 and 3 gallons each.

solved :: (Jug, Jug, Jug) -> SBool

We've solved the puzzle if 8 and 5 gallon jugs have 4 gallons each, and the third one is empty.

moves :: [(SInteger, SInteger)] -> (Jug, Jug, Jug)

Execute a bunch of moves.

puzzle :: IO ()

Solve the puzzle. We have:

>>> puzzle
# of moves: 0
# of moves: 1
# of moves: 2
# of moves: 3
# of moves: 4
# of moves: 5
# of moves: 6
# of moves: 7
1 --> 2
2 --> 3
3 --> 1
2 --> 3
1 --> 2
2 --> 3
3 --> 1

Here's the contents in terms of gallons after each move: (8, 0, 0) (3, 5, 0) (3, 2, 3) (6, 2, 0) (6, 0, 2) (1, 5, 2) (1, 4, 3) (4, 4, 0)

Note that by construction this is the minimum length solution. (Though our construction does not guarantee that it is unique.)