Documentation.SBV.Examples.Queries.FourFours

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.

Documentation

data BinOp

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

Defined in Documentation.SBV.Examples.Queries.FourFours

Methods

(==) :: BinOp -> BinOp -> Bool

(/=) :: BinOp -> BinOp -> Bool

Data BinOp

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

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 :: forall r r'. (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

Defined in Documentation.SBV.Examples.Queries.FourFours

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

Defined in Documentation.SBV.Examples.Queries.FourFours

Methods

readsPrec :: Int -> ReadS BinOp

readList :: ReadS [BinOp]

readPrec :: ReadPrec BinOp

readListPrec :: ReadPrec [BinOp]

Show BinOp

Defined in Documentation.SBV.Examples.Queries.FourFours

Methods

showsPrec :: Int -> BinOp -> ShowS

show :: BinOp -> String

showList :: [BinOp] -> ShowS

HasKind BinOp

Defined in Documentation.SBV.Examples.Queries.FourFours

Methods

kindOf :: BinOp -> Kind

hasSign :: BinOp -> Bool

intSizeOf :: BinOp -> Int

isBoolean :: BinOp -> Bool

isBounded :: BinOp -> Bool

isReal :: BinOp -> Bool

isFloat :: BinOp -> Bool

isDouble :: BinOp -> Bool

isRational :: BinOp -> Bool

isFP :: BinOp -> Bool

isUnbounded :: BinOp -> Bool

isUserSort :: BinOp -> Bool

isChar :: BinOp -> Bool

isString :: BinOp -> Bool

isList :: BinOp -> Bool

isSet :: BinOp -> Bool

isTuple :: BinOp -> Bool

isMaybe :: BinOp -> Bool

isEither :: BinOp -> Bool

showType :: BinOp -> String

SymVal BinOp

Defined in Documentation.SBV.Examples.Queries.FourFours

Methods

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

literal :: BinOp -> SBV BinOp

fromCV :: CV -> BinOp

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

forall :: MonadSymbolic m => String -> m (SBV BinOp)

forall_ :: MonadSymbolic m => m (SBV BinOp)

mkForallVars :: MonadSymbolic m => Int -> m [SBV BinOp]

exists :: MonadSymbolic m => String -> m (SBV BinOp)

exists_ :: MonadSymbolic m => m (SBV BinOp)

mkExistVars :: MonadSymbolic m => Int -> m [SBV BinOp]

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

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

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

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

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

unliteral :: SBV BinOp -> Maybe BinOp

isConcrete :: SBV BinOp -> Bool

isSymbolic :: SBV BinOp -> Bool

SatModel BinOp

Defined in Documentation.SBV.Examples.Queries.FourFours

Methods

parseCVs :: [CV] -> Maybe (BinOp, [CV])

cvtModel :: (BinOp -> Maybe b) -> Maybe (BinOp, [CV]) -> Maybe (b, [CV])

Show (T BinOp UnOp)

A rudimentary Show instance for trees, nothing fancy.

Defined in Documentation.SBV.Examples.Queries.FourFours

Methods

showsPrec :: Int -> T BinOp UnOp -> ShowS

show :: T BinOp UnOp -> String

showList :: [T BinOp UnOp] -> ShowS

type SBinOp = SBV BinOp

Make BinOp a symbolic value.

sExpt :: SBV BinOp

sDivide :: SBV BinOp

sTimes :: SBV BinOp

sMinus :: SBV BinOp

sPlus :: SBV BinOp

data UnOp

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

Defined in Documentation.SBV.Examples.Queries.FourFours

Methods

(==) :: UnOp -> UnOp -> Bool

(/=) :: UnOp -> UnOp -> Bool

Data UnOp

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

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 :: forall r r'. (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

Defined in Documentation.SBV.Examples.Queries.FourFours

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

Defined in Documentation.SBV.Examples.Queries.FourFours

Methods

readsPrec :: Int -> ReadS UnOp

readList :: ReadS [UnOp]

readPrec :: ReadPrec UnOp

readListPrec :: ReadPrec [UnOp]

Show UnOp

Defined in Documentation.SBV.Examples.Queries.FourFours

Methods

showsPrec :: Int -> UnOp -> ShowS

show :: UnOp -> String

showList :: [UnOp] -> ShowS

HasKind UnOp

Defined in Documentation.SBV.Examples.Queries.FourFours

Methods

kindOf :: UnOp -> Kind

hasSign :: UnOp -> Bool

intSizeOf :: UnOp -> Int

isBoolean :: UnOp -> Bool

isBounded :: UnOp -> Bool

isReal :: UnOp -> Bool

isFloat :: UnOp -> Bool

isDouble :: UnOp -> Bool

isRational :: UnOp -> Bool

isFP :: UnOp -> Bool

isUnbounded :: UnOp -> Bool

isUserSort :: UnOp -> Bool

isChar :: UnOp -> Bool

isString :: UnOp -> Bool

isList :: UnOp -> Bool

isSet :: UnOp -> Bool

isTuple :: UnOp -> Bool

isMaybe :: UnOp -> Bool

isEither :: UnOp -> Bool

showType :: UnOp -> String

SymVal UnOp

Defined in Documentation.SBV.Examples.Queries.FourFours

Methods

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

literal :: UnOp -> SBV UnOp

fromCV :: CV -> UnOp

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

forall :: MonadSymbolic m => String -> m (SBV UnOp)

forall_ :: MonadSymbolic m => m (SBV UnOp)

mkForallVars :: MonadSymbolic m => Int -> m [SBV UnOp]

exists :: MonadSymbolic m => String -> m (SBV UnOp)

exists_ :: MonadSymbolic m => m (SBV UnOp)

mkExistVars :: MonadSymbolic m => Int -> m [SBV UnOp]

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

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

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

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

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

unliteral :: SBV UnOp -> Maybe UnOp

isConcrete :: SBV UnOp -> Bool

isSymbolic :: SBV UnOp -> Bool

SatModel UnOp

Defined in Documentation.SBV.Examples.Queries.FourFours

Methods

parseCVs :: [CV] -> Maybe (UnOp, [CV])

cvtModel :: (UnOp -> Maybe b) -> Maybe (UnOp, [CV]) -> Maybe (b, [CV])

Show (T BinOp UnOp)

A rudimentary Show instance for trees, nothing fancy.

Defined in Documentation.SBV.Examples.Queries.FourFours

Methods

showsPrec :: Int -> T BinOp UnOp -> ShowS

show :: T BinOp UnOp -> String

showList :: [T BinOp UnOp] -> ShowS

type SUnOp = SBV UnOp

Make UnOp a symbolic value.

sFactorial :: SBV UnOp

sSqrt :: SBV UnOp

sNegate :: SBV UnOp

data T b u

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)

A rudimentary Show instance for trees, nothing fancy.

Defined in Documentation.SBV.Examples.Queries.FourFours

Methods

showsPrec :: Int -> T BinOp UnOp -> ShowS

show :: T BinOp UnOp -> String

showList :: [T BinOp UnOp] -> ShowS

allPossibleTrees :: [T () ()]

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)

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

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

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

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

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

puzzle :: IO ()

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