-- | run tests like this: "solve test2" import Prelude hiding ( not ) import Satchmo.Boolean hiding ( constant ) import Satchmo.Code import Satchmo.Binary.Op.Fixed -- import Satchmo.Binary.Op.Flexible import Satchmo.Solve assert_positive x = do n <- constant 0 e <- equals n x assert [ not e ] assert_equals x y = do e <- equals x y assert [ e ] assert_lt x y = do d <- number \$ width y assert_positive d xd <- add x d assert_equals xd y test1 = do x <- number 4 y <- constant 12 assert_equals x y return \$ decode (x,y) test2 = do x <- constant 3 y <- constant 9 z <- add x y return \$ decode [x,y,z] test3 = do x <- number 5 xx <- add x x xxx <- add xx x y <- constant 15 assert_equals xxx y return \$ decode [ x, y ] test4 = do x <- number 8 y <- number 8 xy <- times x y z <- constant 63 assert_equals xy z return \$ decode [x, y, z] test5 = do x <- number 10 y <- number 10 xy <- times x y z <- constant 1001 assert_equals xy z return \$ decode [x, y, z] ramanujan = do let bits = 11 a <- number bits b <- number bits c <- number bits d <- number bits assert_lt a c ; assert_lt c d ; assert_lt d b let cube x = do x2 <- times x x ; times x2 x a3 <- cube a; b3 <- cube b; ab <- add a3 b3 c3 <- cube c; d3 <- cube d; cd <- add c3 d3 assert_equals ab cd return \$ decode [a,b,c,d]