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.Queries.FourFours

Description

A query based solution to the four-fours puzzle. Inspired by http://www.gigamonkeys.com/trees/

    Try to make every number between 0 and 20 using only four 4s and any
    mathematical operation, with all four 4s being used each time.

We pretty much follow the structure of http://www.gigamonkeys.com/trees/, with the exception that we generate the trees filled with symbolic operators and ask the SMT solver to find the appropriate fillings.

Synopsis

- data BinOp
  - = Plus
  - | Minus
  - | Times
  - | Divide
  - | Expt
- type SBinOp = SBV BinOp
- sExpt :: SBV BinOp
- sDivide :: SBV BinOp
- sTimes :: SBV BinOp
- sMinus :: SBV BinOp
- sPlus :: SBV BinOp
- data UnOp
  - = Negate
  - | Sqrt
  - | Factorial
- type SUnOp = SBV UnOp
- sFactorial :: SBV UnOp
- sSqrt :: SBV UnOp
- sNegate :: SBV UnOp
- data T b u
  - = B b (T b u) (T b u)
  - | U u (T b u)
  - | F
- allPossibleTrees :: [T () ()]
- fill :: T () () -> Symbolic (T SBinOp SUnOp)
- sCase :: (Eq a, SymVal a, Mergeable v) => SBV a -> [(a, v)] -> v
- eval :: T SBinOp SUnOp -> Symbolic SInteger
- generate :: Integer -> T () () -> IO (Maybe (T BinOp UnOp))
- find :: Integer -> IO ()
- puzzle :: IO ()

# Documentation

data BinOp Source #

Supported binary operators. To keep the search-space small, we will only allow division by `2` or `4`, and exponentiation will only be to the power `0`. This does restrict the search space, but is sufficient to solve all the instances.

Constructors

Plus |
Minus |
Times |
Divide |
Expt |

#### Instances

Instances details

Data BinOp Source # |

Instance details

Defined in Documentation.SBV.Examples.Queries.FourFours

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BinOp -> c BinOp Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BinOp Source #

toConstr :: BinOp -> Constr Source #

dataTypeOf :: BinOp -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BinOp) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BinOp) Source #

gmapT :: (forall b. Data b => b -> b) -> BinOp -> BinOp Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BinOp -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BinOp -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> BinOp -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> BinOp -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> BinOp -> m BinOp Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BinOp -> m BinOp Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BinOp -> m BinOp Source #

Read BinOp Source # |
Instance details Defined in Documentation.SBV.Examples.Queries.FourFours Methods readsPrec :: Int -> ReadS BinOp Source # readList :: ReadS [BinOp] Source # readPrec :: ReadPrec BinOp Source # readListPrec :: ReadPrec [BinOp] Source #
Show BinOp Source # |
Instance details Defined in Documentation.SBV.Examples.Queries.FourFours Methods showsPrec :: Int -> BinOp -> ShowS Source # show :: BinOp -> String Source # showList :: [BinOp] -> ShowS Source #
Eq BinOp Source # |
Instance details Defined in Documentation.SBV.Examples.Queries.FourFours Methods (==) :: BinOp -> BinOp -> Bool Source # (/=) :: BinOp -> BinOp -> Bool Source #
Ord BinOp Source # |
Instance details Defined in Documentation.SBV.Examples.Queries.FourFours Methods compare :: BinOp -> BinOp -> Ordering Source # (<) :: BinOp -> BinOp -> Bool Source # (<=) :: BinOp -> BinOp -> Bool Source # (>) :: BinOp -> BinOp -> Bool Source # (>=) :: BinOp -> BinOp -> Bool Source # max :: BinOp -> BinOp -> BinOp Source # min :: BinOp -> BinOp -> BinOp Source #
SymVal BinOp Source # |

Instance details

Defined in Documentation.SBV.Examples.Queries.FourFours

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV BinOp) Source #

literal :: BinOp -> SBV BinOp Source #

fromCV :: CV -> BinOp Source #

isConcretely :: SBV BinOp -> (BinOp -> Bool) -> Bool Source #

free :: MonadSymbolic m => String -> m (SBV BinOp) Source #

free_ :: MonadSymbolic m => m (SBV BinOp) Source #

mkFreeVars :: MonadSymbolic m => Int -> m [SBV BinOp] Source #

symbolic :: MonadSymbolic m => String -> m (SBV BinOp) Source #

symbolics :: MonadSymbolic m => [String] -> m [SBV BinOp] Source #

unliteral :: SBV BinOp -> Maybe BinOp Source #

isConcrete :: SBV BinOp -> Bool Source #

isSymbolic :: SBV BinOp -> Bool Source #

HasKind BinOp Source # |

Instance details

Defined in Documentation.SBV.Examples.Queries.FourFours

Methods

kindOf :: BinOp -> Kind Source #

hasSign :: BinOp -> Bool Source #

intSizeOf :: BinOp -> Int Source #

isBoolean :: BinOp -> Bool Source #

isBounded :: BinOp -> Bool Source #

isReal :: BinOp -> Bool Source #

isFloat :: BinOp -> Bool Source #

isDouble :: BinOp -> Bool Source #

isRational :: BinOp -> Bool Source #

isFP :: BinOp -> Bool Source #

isUnbounded :: BinOp -> Bool Source #

isUserSort :: BinOp -> Bool Source #

isChar :: BinOp -> Bool Source #

isString :: BinOp -> Bool Source #

isList :: BinOp -> Bool Source #

isSet :: BinOp -> Bool Source #

isTuple :: BinOp -> Bool Source #

isMaybe :: BinOp -> Bool Source #

isEither :: BinOp -> Bool Source #

showType :: BinOp -> String Source #

SatModel BinOp Source # |
Instance details Defined in Documentation.SBV.Examples.Queries.FourFours Methods parseCVs :: [CV] -> Maybe (BinOp, [CV]) Source # cvtModel :: (BinOp -> Maybe b) -> Maybe (BinOp, [CV]) -> Maybe (b, [CV]) Source #
Show (T BinOp UnOp) Source # | A rudimentary `Show` instance for trees, nothing fancy.
Instance details Defined in Documentation.SBV.Examples.Queries.FourFours Methods showsPrec :: Int -> T BinOp UnOp -> ShowS Source # show :: T BinOp UnOp -> String Source # showList :: [T BinOp UnOp] -> ShowS Source #

type SBinOp = SBV BinOp Source #

Symbolic version of the type `BinOp`.

sExpt :: SBV BinOp Source #

Symbolic version of the constructor `Expt`.

sDivide :: SBV BinOp Source #

Symbolic version of the constructor `Divide`.

sTimes :: SBV BinOp Source #

Symbolic version of the constructor `Times`.

sMinus :: SBV BinOp Source #

Symbolic version of the constructor `Minus`.

sPlus :: SBV BinOp Source #

Symbolic version of the constructor `Plus`.

data UnOp Source #

Supported unary operators. Similar to `BinOp` case, we will restrict square-root and factorial to be only applied to the value @4.

Constructors

Negate |
Sqrt |
Factorial |

#### Instances

Instances details

Data UnOp Source # |

Instance details

Defined in Documentation.SBV.Examples.Queries.FourFours

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> UnOp -> c UnOp Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c UnOp Source #

toConstr :: UnOp -> Constr Source #

dataTypeOf :: UnOp -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c UnOp) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UnOp) Source #

gmapT :: (forall b. Data b => b -> b) -> UnOp -> UnOp Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UnOp -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UnOp -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> UnOp -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> UnOp -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> UnOp -> m UnOp Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UnOp -> m UnOp Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UnOp -> m UnOp Source #

Read UnOp Source # |
Instance details Defined in Documentation.SBV.Examples.Queries.FourFours Methods readsPrec :: Int -> ReadS UnOp Source # readList :: ReadS [UnOp] Source # readPrec :: ReadPrec UnOp Source # readListPrec :: ReadPrec [UnOp] Source #
Show UnOp Source # |
Instance details Defined in Documentation.SBV.Examples.Queries.FourFours Methods showsPrec :: Int -> UnOp -> ShowS Source # show :: UnOp -> String Source # showList :: [UnOp] -> ShowS Source #
Eq UnOp Source # |
Instance details Defined in Documentation.SBV.Examples.Queries.FourFours Methods (==) :: UnOp -> UnOp -> Bool Source # (/=) :: UnOp -> UnOp -> Bool Source #
Ord UnOp Source # |
Instance details Defined in Documentation.SBV.Examples.Queries.FourFours Methods compare :: UnOp -> UnOp -> Ordering Source # (<) :: UnOp -> UnOp -> Bool Source # (<=) :: UnOp -> UnOp -> Bool Source # (>) :: UnOp -> UnOp -> Bool Source # (>=) :: UnOp -> UnOp -> Bool Source # max :: UnOp -> UnOp -> UnOp Source # min :: UnOp -> UnOp -> UnOp Source #
SymVal UnOp Source # |

Instance details

Defined in Documentation.SBV.Examples.Queries.FourFours

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV UnOp) Source #

literal :: UnOp -> SBV UnOp Source #

fromCV :: CV -> UnOp Source #

isConcretely :: SBV UnOp -> (UnOp -> Bool) -> Bool Source #

free :: MonadSymbolic m => String -> m (SBV UnOp) Source #

free_ :: MonadSymbolic m => m (SBV UnOp) Source #

mkFreeVars :: MonadSymbolic m => Int -> m [SBV UnOp] Source #

symbolic :: MonadSymbolic m => String -> m (SBV UnOp) Source #

symbolics :: MonadSymbolic m => [String] -> m [SBV UnOp] Source #

unliteral :: SBV UnOp -> Maybe UnOp Source #

isConcrete :: SBV UnOp -> Bool Source #

isSymbolic :: SBV UnOp -> Bool Source #

HasKind UnOp Source # |

Instance details

Defined in Documentation.SBV.Examples.Queries.FourFours

Methods

kindOf :: UnOp -> Kind Source #

hasSign :: UnOp -> Bool Source #

intSizeOf :: UnOp -> Int Source #

isBoolean :: UnOp -> Bool Source #

isBounded :: UnOp -> Bool Source #

isReal :: UnOp -> Bool Source #

isFloat :: UnOp -> Bool Source #

isDouble :: UnOp -> Bool Source #

isRational :: UnOp -> Bool Source #

isFP :: UnOp -> Bool Source #

isUnbounded :: UnOp -> Bool Source #

isUserSort :: UnOp -> Bool Source #

isChar :: UnOp -> Bool Source #

isString :: UnOp -> Bool Source #

isList :: UnOp -> Bool Source #

isSet :: UnOp -> Bool Source #

isTuple :: UnOp -> Bool Source #

isMaybe :: UnOp -> Bool Source #

isEither :: UnOp -> Bool Source #

showType :: UnOp -> String Source #

SatModel UnOp Source # |
Instance details Defined in Documentation.SBV.Examples.Queries.FourFours Methods parseCVs :: [CV] -> Maybe (UnOp, [CV]) Source # cvtModel :: (UnOp -> Maybe b) -> Maybe (UnOp, [CV]) -> Maybe (b, [CV]) Source #
Show (T BinOp UnOp) Source # | A rudimentary `Show` instance for trees, nothing fancy.
Instance details Defined in Documentation.SBV.Examples.Queries.FourFours Methods showsPrec :: Int -> T BinOp UnOp -> ShowS Source # show :: T BinOp UnOp -> String Source # showList :: [T BinOp UnOp] -> ShowS Source #

type SUnOp = SBV UnOp Source #

Symbolic version of the type `UnOp`.

sFactorial :: SBV UnOp Source #

Symbolic version of the constructor `Factorial`.

sSqrt :: SBV UnOp Source #

Symbolic version of the constructor `Sqrt`.

sNegate :: SBV UnOp Source #

Symbolic version of the constructor `Negate`.

data T b u Source #

The shape of a tree, either a binary node, or a unary node, or the number `4`, represented hear by the constructor `F`. We parameterize by the operator type: When doing symbolic computations, we'll fill those with `SBinOp` and `SUnOp`. When finding the shapes, we will simply put unit values, i.e., holes.

Constructors

B b (T b u) (T b u) |
U u (T b u) |
F |

#### Instances

Instances details

Show (T BinOp UnOp) Source # | A rudimentary `Show` instance for trees, nothing fancy.
Instance details Defined in Documentation.SBV.Examples.Queries.FourFours Methods showsPrec :: Int -> T BinOp UnOp -> ShowS Source # show :: T BinOp UnOp -> String Source # showList :: [T BinOp UnOp] -> ShowS Source #

allPossibleTrees :: [T () ()] Source #

Construct all possible tree shapes. The argument here follows the logic in http://www.gigamonkeys.com/trees/: We simply construct all possible shapes and extend with the operators. The number of such trees is:

    >>> length allPossibleTrees
    640

Note that this is a lot smaller than what is generated by http://www.gigamonkeys.com/trees/. (There, the number of trees is 10240000: 16000 times more than what we have to consider!)

fill :: T () () -> Symbolic (T SBinOp SUnOp) Source #

Given a tree with hols, fill it with symbolic operators. This is the trick that allows us to consider only 640 trees as opposed to over 10 million.

sCase :: (Eq a, SymVal a, Mergeable v) => SBV a -> [(a, v)] -> v Source #

Minor helper for writing "symbolic" case statements. Simply walks down a list of values to match against a symbolic version of the key.

eval :: T SBinOp SUnOp -> Symbolic SInteger Source #

Evaluate a symbolic tree, obtaining a symbolic value. Note how we structure this evaluation so we impose extra constraints on what values square-root, divide etc. can take. This is the power of the symbolic approach: We can put arbitrary symbolic constraints as we evaluate the tree.

generate :: Integer -> T () () -> IO (Maybe (T BinOp UnOp)) Source #

In the query mode, find a filling of a given tree shape t, such that it evaluates to the requested number i. Note that we return back a concrete tree.

find :: Integer -> IO () Source #

Given an integer, walk through all possible tree shapes (at most 640 of them), and find a filling that solves the puzzle.

puzzle :: IO () Source #

Solution to the puzzle. When you run this puzzle, the solver can produce different results than what's shown here, but the expressions should still be all valid!

    ghci> puzzle
     0 [OK]: (4 - (4 + (4 - 4)))
     1 [OK]: (4 / (4 + (4 - 4)))
     2 [OK]: sqrt((4 + (4 * (4 - 4))))
     3 [OK]: (4 - (4 ^ (4 - 4)))
     4 [OK]: (4 + (4 * (4 - 4)))
     5 [OK]: (4 + (4 ^ (4 - 4)))
     6 [OK]: (4 + sqrt((4 * (4 / 4))))
     7 [OK]: (4 + (4 - (4 / 4)))
     8 [OK]: (4 - (4 - (4 + 4)))
     9 [OK]: (4 + (4 + (4 / 4)))
    10 [OK]: (4 + (4 + (4 - sqrt(4))))
    11 [OK]: (4 + ((4 + 4!) / 4))
    12 [OK]: (4 * (4 - (4 / 4)))
    13 [OK]: (4! + ((sqrt(4) - 4!) / sqrt(4)))
    14 [OK]: (4 + (4 + (4 + sqrt(4))))
    15 [OK]: (4 + ((4! - sqrt(4)) / sqrt(4)))
    16 [OK]: (4 * (4 * (4 / 4)))
    17 [OK]: (4 + ((sqrt(4) + 4!) / sqrt(4)))
    18 [OK]: -(4 + (4 - (sqrt(4) + 4!)))
    19 [OK]: -(4 - (4! - (4 / 4)))
    20 [OK]: (4 * (4 + (4 / 4)))