Skip to content

Commit

Permalink
a bit more safe coding
Browse files Browse the repository at this point in the history
  • Loading branch information
LeventErkok committed Nov 5, 2024
1 parent 89fd5b2 commit 86b1063
Showing 1 changed file with 14 additions and 6 deletions.
20 changes: 14 additions & 6 deletions Documentation/SBV/Examples/Puzzles/DieHard.hs
Original file line number Diff line number Diff line change
Expand Up @@ -56,12 +56,20 @@ type CState = State Integer Action
instance Queriable IO SState where
type QueryResult SState = CState

create = State <$> freshVar_ <*> freshVar_ <*> freshVar_
project State{big, small, action} = State <$> getValue big <*> getValue small <*> getValue action
embed State{big, small, action} = pure $ State { big = literal big
, small = literal small
, action = literal action
}
create = State <$> freshVar_ <*> freshVar_ <*> freshVar_

project State{big, small, action} = do b <- getValue big
s <- getValue small
a <- getValue action
pure $ State { big = b
, small = s
, action = a
}

embed State{big, small, action} = pure $ State { big = literal big
, small = literal small
, action = literal action
}

-- | Solve the problem using a BMC search. We have:
--
Expand Down

0 comments on commit 86b1063

Please sign in to comment.