module Satchmo.Polynomial
( Number ()
, number, constant
, iszero, equals, ge, gt
, add, times
)
where
import Data.Map ( Map )
import qualified Data.Map as M
import Satchmo.SAT
import Satchmo.Boolean hiding ( constant )
import qualified Satchmo.Boolean
import Satchmo.Code
import qualified Satchmo.Binary.Op.Fixed as F
import Control.Monad ( forM )
data Poly a = Poly [a] deriving ( Eq, Ord, Show )
type Number = Poly F.Number
instance Decode a Integer => Decode ( Poly a ) Integer where
decode ( Poly xs ) = do
ys <- forM xs decode
let base = 1000
return $ if all ( < base ) ys
then foldr ( \ y o -> o * base + y ) 0 ys
else error "Satchmo.Polynomial.decode"
degree :: Poly a -> Int
degree ( Poly xs ) = pred $ length xs
number :: MonadSAT m
=> Int
-> Int
-> m ( Poly F.Number )
number bits deg = do
xs <- forM [ 0 .. deg ] $ \ i -> F.number bits
return $ Poly xs
constant :: MonadSAT m
=> Integer
-> m ( Poly F.Number )
constant 0 = return $ Poly []
constant c = do
z <- F.constant 0
o <- F.constant c
return $ Poly [ z, o ]
iszero ( Poly xs ) = do
ns <- forM xs $ F.iszero
Satchmo.Boolean.and ns
equals ( Poly xs ) ( Poly ys ) = do
z <- F.constant 0
let n = max ( length xs ) ( length ys )
fill xs = take n $ xs ++ repeat z
let handle xs ys = case ( xs, ys ) of
( [], [] ) -> Satchmo.Boolean.constant True
(x:xs, y:ys) -> do
e <- F.equals x y
later <- handle xs ys
Satchmo.Boolean.and [ e, later ]
handle ( reverse $ fill xs ) ( reverse $ fill ys )
ge ( Poly xs ) ( Poly ys ) = do
z <- F.constant 0
let n = max ( length xs ) ( length ys )
fill xs = take n $ xs ++ repeat z
let handle xs ys = case ( xs, ys ) of
( [], [] ) -> Satchmo.Boolean.constant True
(x:xs, y:ys) -> do
gt <- F.gt x y
e <- F.equals x y
later <- handle xs ys
monadic Satchmo.Boolean.or
[ return gt
, Satchmo.Boolean.and [ e, later ]
]
handle ( reverse $ fill xs ) ( reverse $ fill ys )
gt ( Poly xs ) ( Poly ys ) = do
z <- F.constant 0
let n = max ( length xs ) ( length ys )
fill xs = take n $ xs ++ repeat z
let handle xs ys = case ( xs, ys ) of
( [], [] ) -> Satchmo.Boolean.constant False
(x:xs, y:ys) -> do
gt <- F.gt x y
e <- F.equals x y
later <- handle xs ys
monadic Satchmo.Boolean.or
[ return gt
, Satchmo.Boolean.and [ e, later ]
]
handle ( reverse $ fill xs ) ( reverse $ fill ys )
add ( Poly xs ) ( Poly ys ) = do
let handle xs ys = case ( xs, ys ) of
( [] , ys ) -> return ys
( xs, [] ) -> return xs
(x:xs, y:ys) -> do
z <- F.add x y
zs <- handle xs ys
return $ z : zs
zs <- handle xs ys
return $ Poly zs
times p q = do
let handle ( Poly xs ) ( Poly ys ) =
case ( xs, ys ) of
( [], ys ) -> return $ Poly []
( xs, [] ) -> return $ Poly []
( x : xs, ys ) -> do
Poly zs <- handle ( Poly xs ) ( Poly ys )
f : fs <- forM ys $ F.times x
Poly rest <- add ( Poly zs ) ( Poly fs )
return $ Poly $ f : rest
handle p q