Copyright	(c) Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
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

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

Eq BinOp Source #
Methods (==) :: BinOp -> BinOp -> Bool # (/=) :: BinOp -> BinOp -> Bool #
Data BinOp Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BinOp -> c BinOp # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BinOp # toConstr :: BinOp -> Constr # dataTypeOf :: BinOp -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c BinOp) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BinOp) # gmapT :: (forall b. Data b => b -> b) -> BinOp -> BinOp # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BinOp -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BinOp -> r # gmapQ :: (forall d. Data d => d -> u) -> BinOp -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> BinOp -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> BinOp -> m BinOp # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BinOp -> m BinOp # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BinOp -> m BinOp #
Ord BinOp Source #
Methods compare :: BinOp -> BinOp -> Ordering # (<) :: BinOp -> BinOp -> Bool # (<=) :: BinOp -> BinOp -> Bool # (>) :: BinOp -> BinOp -> Bool # (>=) :: BinOp -> BinOp -> Bool # max :: BinOp -> BinOp -> BinOp # min :: BinOp -> BinOp -> BinOp #
Read BinOp Source #
Methods readsPrec :: Int -> ReadS BinOp # readList :: ReadS [BinOp] # readPrec :: ReadPrec BinOp # readListPrec :: ReadPrec [BinOp] #
Show BinOp Source #
Methods showsPrec :: Int -> BinOp -> ShowS # show :: BinOp -> String # showList :: [BinOp] -> ShowS #
HasKind BinOp Source #
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 # isInteger :: BinOp -> Bool Source # isUninterpreted :: BinOp -> Bool Source # isChar :: BinOp -> Bool Source # isString :: BinOp -> Bool Source # showType :: BinOp -> String Source #
SymWord BinOp Source #
Methods forall :: String -> Symbolic (SBV BinOp) Source # forall_ :: Symbolic (SBV BinOp) Source # mkForallVars :: Int -> Symbolic [SBV BinOp] Source # exists :: String -> Symbolic (SBV BinOp) Source # exists_ :: Symbolic (SBV BinOp) Source # mkExistVars :: Int -> Symbolic [SBV BinOp] Source # free :: String -> Symbolic (SBV BinOp) Source # free_ :: Symbolic (SBV BinOp) Source # mkFreeVars :: Int -> Symbolic [SBV BinOp] Source # symbolic :: String -> Symbolic (SBV BinOp) Source # symbolics :: [String] -> Symbolic [SBV BinOp] Source # literal :: BinOp -> SBV BinOp Source # unliteral :: SBV BinOp -> Maybe BinOp Source # fromCW :: CW -> BinOp Source # isConcrete :: SBV BinOp -> Bool Source # isSymbolic :: SBV BinOp -> Bool Source # isConcretely :: SBV BinOp -> (BinOp -> Bool) -> Bool Source # mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV BinOp) Source #
SatModel BinOp Source #	Make `BinOp` a symbolic value.
Methods parseCWs :: [CW] -> Maybe (BinOp, [CW]) Source # cvtModel :: (BinOp -> Maybe b) -> Maybe (BinOp, [CW]) -> Maybe (b, [CW]) Source #
SMTValue BinOp Source #
Methods sexprToVal :: SExpr -> Maybe BinOp Source #
Show (T BinOp UnOp) Source #	A rudimentary `Show` instance for trees, nothing fancy.
Methods showsPrec :: Int -> T BinOp UnOp -> ShowS # show :: T BinOp UnOp -> String # showList :: [T BinOp UnOp] -> ShowS #

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

Eq UnOp Source #
Methods (==) :: UnOp -> UnOp -> Bool # (/=) :: UnOp -> UnOp -> Bool #
Data UnOp Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> UnOp -> c UnOp # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c UnOp # toConstr :: UnOp -> Constr # dataTypeOf :: UnOp -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c UnOp) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UnOp) # gmapT :: (forall b. Data b => b -> b) -> UnOp -> UnOp # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UnOp -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UnOp -> r # gmapQ :: (forall d. Data d => d -> u) -> UnOp -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> UnOp -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> UnOp -> m UnOp # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UnOp -> m UnOp # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UnOp -> m UnOp #
Ord UnOp Source #
Methods compare :: UnOp -> UnOp -> Ordering # (<) :: UnOp -> UnOp -> Bool # (<=) :: UnOp -> UnOp -> Bool # (>) :: UnOp -> UnOp -> Bool # (>=) :: UnOp -> UnOp -> Bool # max :: UnOp -> UnOp -> UnOp # min :: UnOp -> UnOp -> UnOp #
Read UnOp Source #
Methods readsPrec :: Int -> ReadS UnOp # readList :: ReadS [UnOp] # readPrec :: ReadPrec UnOp # readListPrec :: ReadPrec [UnOp] #
Show UnOp Source #
Methods showsPrec :: Int -> UnOp -> ShowS # show :: UnOp -> String # showList :: [UnOp] -> ShowS #
HasKind UnOp Source #
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 # isInteger :: UnOp -> Bool Source # isUninterpreted :: UnOp -> Bool Source # isChar :: UnOp -> Bool Source # isString :: UnOp -> Bool Source # showType :: UnOp -> String Source #
SymWord UnOp Source #
Methods forall :: String -> Symbolic (SBV UnOp) Source # forall_ :: Symbolic (SBV UnOp) Source # mkForallVars :: Int -> Symbolic [SBV UnOp] Source # exists :: String -> Symbolic (SBV UnOp) Source # exists_ :: Symbolic (SBV UnOp) Source # mkExistVars :: Int -> Symbolic [SBV UnOp] Source # free :: String -> Symbolic (SBV UnOp) Source # free_ :: Symbolic (SBV UnOp) Source # mkFreeVars :: Int -> Symbolic [SBV UnOp] Source # symbolic :: String -> Symbolic (SBV UnOp) Source # symbolics :: [String] -> Symbolic [SBV UnOp] Source # literal :: UnOp -> SBV UnOp Source # unliteral :: SBV UnOp -> Maybe UnOp Source # fromCW :: CW -> UnOp Source # isConcrete :: SBV UnOp -> Bool Source # isSymbolic :: SBV UnOp -> Bool Source # isConcretely :: SBV UnOp -> (UnOp -> Bool) -> Bool Source # mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV UnOp) Source #
SatModel UnOp Source #	Make `UnOp` a symbolic value.
Methods parseCWs :: [CW] -> Maybe (UnOp, [CW]) Source # cvtModel :: (UnOp -> Maybe b) -> Maybe (UnOp, [CW]) -> Maybe (b, [CW]) Source #
SMTValue UnOp Source #
Methods sexprToVal :: SExpr -> Maybe UnOp Source #
Show (T BinOp UnOp) Source #	A rudimentary `Show` instance for trees, nothing fancy.
Methods showsPrec :: Int -> T BinOp UnOp -> ShowS # show :: T BinOp UnOp -> String # showList :: [T BinOp UnOp] -> ShowS #

type SBinOp = SBV BinOp Source #

Symbolic variant of BinOp.

type SUnOp = SBV UnOp Source #

Symbolic variant of UnOp.

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

Show (T BinOp UnOp) Source #	A rudimentary `Show` instance for trees, nothing fancy.
Methods showsPrec :: Int -> T BinOp UnOp -> ShowS # show :: T BinOp UnOp -> String # showList :: [T BinOp UnOp] -> ShowS #

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 :: (SymWord 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 evalutes 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)))