sbv-10.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
Language | Haskell2010

Documentation.SBV.Examples.Puzzles.Jugs

Description

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?

Synopsis

- data Jug = Jug {
  - capacity :: Integer
  - content :: SInteger
  }
- transfer :: Jug -> Jug -> (Jug, Jug)
- initJugs :: (Jug, Jug, Jug)
- solved :: (Jug, Jug, Jug) -> SBool
- moves :: [(SInteger, SInteger)] -> (Jug, Jug, Jug)
- puzzle :: IO ()

# Documentation

data Jug Source #

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

Instances details

Generic Jug Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Jugs Associated Types type Rep Jug :: Type -> Type Source # Methods from :: Jug -> Rep Jug x Source # to :: Rep Jug x -> Jug Source #
Mergeable Jug Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Jugs Methods symbolicMerge :: Bool -> SBool -> Jug -> Jug -> Jug Source # select :: (Ord b, SymVal b, Num b) => [Jug] -> Jug -> SBV b -> Jug Source #
type Rep Jug Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Jugs

type Rep Jug = D1 ('MetaData "Jug" "Documentation.SBV.Examples.Puzzles.Jugs" "sbv-10.2-H7C8tpOUfNc9yHFfX3krPk" '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) Source #

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) Source #

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

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

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) Source #

Execute a bunch of moves.

puzzle :: IO () Source #

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.)