Skip to content

Instantly share code, notes, and snippets.

@LeventErkok
Created January 30, 2012 01:48
Show Gist options
  • Save LeventErkok/1701881 to your computer and use it in GitHub Desktop.
Save LeventErkok/1701881 to your computer and use it in GitHub Desktop.
import Data.SBV
import Data.List (partition)
sumSplit :: [Integer] -> IO (Maybe (Integer, [Integer], [Integer]))
sumSplit xs = do r <- satWith z3 $ do zs <- mkFreeVars (length xs)
let sums sofar [] = sofar
sums (i,o) ((f, v):rest) = sums (ite f (i+v, o) (i, o+v)) rest
(f, s) = sums (0, 0) $ zip zs (map literal xs)
return $ f .== s
case getModel r of
Left _ -> return Nothing
Right (_, bs) -> let (f, s) = partition fst $ zip bs xs
part1 = map snd f
part2 = map snd s
in return $ Just (sum part1, part1, part2)
-- Example calls in ghci:
-- *Main> sumSplit []
-- Just (0,[],[])
-- *Main> sumSplit [0]
-- Just (0,[],[0])
-- *Main> sumSplit [1]
-- Nothing
-- *Main> sumSplit [1,3,5,1,3,-1,2,0]
-- Just (7,[3,3,-1,2],[1,5,1,0])
-- *Main> sumSplit [1,3,5,1,3,-1,2,0,12]
-- Just (13,[-1,2,12],[1,3,5,1,3,0])
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment