module Satchmo.SMT.Exotic.Arctic.Integer where
import Satchmo.SMT.Exotic.Dict
import qualified Satchmo.SMT.Exotic.Domain
import qualified Data.Map as M
import qualified Satchmo.Unary.Op.Flexible as X
import qualified Satchmo.Unary as N
import qualified Satchmo.Boolean as B
import Satchmo.Code
import Satchmo.SAT.Mini (SAT)
import Control.Monad (forM, guard, when)
import qualified Satchmo.SMT.Exotic.Semiring.Arctic as A
data Arctic = Arctic { contents :: N.Number
, shift :: Int
}
minus_infinite = B.not . head . N.bits . contents
not_minus_infinite = head . N.bits . contents
instance ( Decode m B.Boolean Bool )
=> Decode m Arctic ( A.Arctic Integer ) where
decode a = do
c <- decode $ contents a
return $ if 0 == c
then A.Minus_Infinite
else A.Finite $ fromIntegral (c shift a)
constant :: Int -> A.Arctic Integer
-> SAT Arctic
constant bits a = case a of
A.Minus_Infinite -> do
cs <- forM [ negate bits + 1 .. bits ] $ \ _ ->
B.constant False
make bits $ N.make cs
A.Finite f -> do
cs <- forM [ negate bits + 1 .. bits ] $ \ i ->
B.constant ( i <= fromIntegral f )
make bits $ N.make cs
make s c = do
return $ Arctic { contents = c, shift = s }
dict :: Int
-> Dict SAT Arctic B.Boolean
dict bits = Dict
{ domain = Satchmo.SMT.Exotic.Domain.Arctic
, fresh = do
c <- N.number $ 2 * bits
make bits c
, finite = \ x ->
return $ N.bits (contents x) !! (shift x 1)
, ge = \ l r -> N.ge ( contents l ) ( contents r )
, gg = \ l r ->
B.monadic B.or [ return $ minus_infinite r
, N.gt ( contents l ) ( contents r )
]
, plus = \ xs -> do
c <- X.maximum $ map contents xs
make bits c
, times = \ [s,t] -> do
m <- B.or [ minus_infinite s
, minus_infinite t ]
let a = contents s ; b = contents t
pairs <- sequence $ do
(i,x) <- zip [negate bits + 1 .. ] $ N.bits a
(j,y) <- zip [negate bits + 1 .. ] $ N.bits b
guard $ i+j > negate bits
guard $ i+j <= bits
return $ do
z <- B.and [x,y, B.not m]
return (i+j, [z])
cs <- forM ( map snd $ M.toAscList
$ M.fromListWith (++) pairs ) B.or
B.assert [ m, head cs ]
B.assert [ B.not $ last cs ]
make bits $ N.make $ init cs
}