picosat fails with stack overflow

[mmaroti]

If you create a large problem, then picosat fails with stack overflow. It actually creates and solves the problem, but fails in getSolution while going through the results with forM. Here is a test program and a new version of forM which would work for arbitrary large problems (as long as you have heap space). It returns the solution list in the same order as before, but if you remove the "reverse" in the mapM', then it would still work but return the result in the opposite order (and would be slightly faster).

module Main where
import Control.Monad (forM)
import Picosat

vars :: Int
vars = 1000000
clauses :: [[Int]]
clauses = fmap (\x -> [x]) [1 .. vars]

main :: IO ()
main = do
    putStrLn "Running new forM':"
    sol1 <- forM' [1 .. vars] return
    print $ last sol1
--  putStrLn "Running old forM:"
--  sol2 <- forM [1 .. vars] return
--  print $ last sol2
    putStrLn $ "Running Picosat with " ++ show (length clauses) ++ " clauses:"
    sol <- Picosat.solve clauses
    putStrLn $ show sol

mapM' :: Monad m => (a -> m b) -> [a] -> [b] -> m [b]
mapM' _ [] ys = return (reverse ys)
mapM' f (x : xs) ys = f x >>= \y -> mapM' f xs (y : ys)

forM' :: Monad m => [a] -> (a -> m b) -> m [b]
forM' xs f = mapM' f xs []