module Satchmo.PolynomialSOS

(nonNegative, positive, strictlyMonotone)

where

import Prelude hiding (null,and)
import Control.Monad (foldM,replicateM)

import Satchmo.MonadSAT (MonadSAT)
import Satchmo.Polynomial 
    (NumPoly,Poly,times,add,polynomial,null,equals,constantTerm,derive)
import Satchmo.Boolean (Boolean,and)
import qualified Satchmo.BinaryTwosComplement.Op.Fixed as F

sqr :: MonadSAT m => NumPoly -> m NumPoly
sqr :: forall (m :: * -> *). MonadSAT m => NumPoly -> m NumPoly
sqr NumPoly
p = NumPoly
p NumPoly -> NumPoly -> m NumPoly
forall (m :: * -> *). MonadSAT m => NumPoly -> NumPoly -> m NumPoly
`times` NumPoly
p
  
sumOfSquares :: MonadSAT m => Int -> Int -> Int -> m NumPoly
sumOfSquares :: forall (m :: * -> *). MonadSAT m => Int -> Int -> Int -> m NumPoly
sumOfSquares Int
coefficientBitWidth Int
degree Int
numPoly = do
  [NumPoly]
sqrs <- Int -> m NumPoly -> m [NumPoly]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
numPoly 
          (m NumPoly -> m [NumPoly]) -> m NumPoly -> m [NumPoly]
forall a b. (a -> b) -> a -> b
$ Int -> Int -> m NumPoly
forall (m :: * -> *). MonadSAT m => Int -> Int -> m NumPoly
polynomial Int
coefficientBitWidth Int
degree m NumPoly -> (NumPoly -> m NumPoly) -> m NumPoly
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= NumPoly -> m NumPoly
forall (m :: * -> *). MonadSAT m => NumPoly -> m NumPoly
sqr
  (NumPoly -> NumPoly -> m NumPoly)
-> NumPoly -> [NumPoly] -> m NumPoly
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM NumPoly -> NumPoly -> m NumPoly
forall (m :: * -> *). MonadSAT m => NumPoly -> NumPoly -> m NumPoly
add NumPoly
forall a. Poly a
null [NumPoly]
sqrs

nonNegative :: MonadSAT m => Int -- ^ Bit width of coefficients
            -> Int -- ^ Maximum degree
            -> Int -- ^ Maximum number of polynomials
            -> NumPoly -> m Boolean
nonNegative :: forall (m :: * -> *).
MonadSAT m =>
Int -> Int -> Int -> NumPoly -> m Boolean
nonNegative Int
coefficientBitWidth Int
degree Int
numPoly NumPoly
p = do
  NumPoly
sos <- Int -> Int -> Int -> m NumPoly
forall (m :: * -> *). MonadSAT m => Int -> Int -> Int -> m NumPoly
sumOfSquares Int
coefficientBitWidth Int
degree Int
numPoly
  NumPoly -> NumPoly -> m Boolean
forall (m :: * -> *). MonadSAT m => NumPoly -> NumPoly -> m Boolean
equals NumPoly
sos NumPoly
p
  
positive :: MonadSAT m => Int -- ^ Bit width of coefficients
            -> Int -- ^ Maximum degree
            -> Int -- ^ Maximum number of polynomials
            -> NumPoly -> m Boolean
positive :: forall (m :: * -> *).
MonadSAT m =>
Int -> Int -> Int -> NumPoly -> m Boolean
positive Int
coefficientBitWidth Int
degree Int
numPoly NumPoly
p = do
  NumPoly
sos <- Int -> Int -> Int -> m NumPoly
forall (m :: * -> *). MonadSAT m => Int -> Int -> Int -> m NumPoly
sumOfSquares Int
coefficientBitWidth Int
degree Int
numPoly
  Boolean
e1 <- NumPoly -> NumPoly -> m Boolean
forall (m :: * -> *). MonadSAT m => NumPoly -> NumPoly -> m Boolean
equals NumPoly
sos NumPoly
p
  Boolean
e2 <- Number -> m Boolean
forall (m :: * -> *). MonadSAT m => Number -> m Boolean
F.positive (Number -> m Boolean) -> Number -> m Boolean
forall a b. (a -> b) -> a -> b
$ NumPoly -> Number
forall a. Poly a -> a
constantTerm NumPoly
sos 
  [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [Boolean
e1, Boolean
e2]

strictlyMonotone :: MonadSAT m => Int -- ^ Bit width of coefficients
            -> Int -- ^ Maximum degree
            -> Int -- ^ Maximum number of polynomials
            -> NumPoly -> m Boolean
strictlyMonotone :: forall (m :: * -> *).
MonadSAT m =>
Int -> Int -> Int -> NumPoly -> m Boolean
strictlyMonotone Int
coefficientBitWidth Int
degree Int
numPoly NumPoly
p = do
  NumPoly
p' <- NumPoly -> m NumPoly
forall (m :: * -> *). MonadSAT m => NumPoly -> m NumPoly
derive NumPoly
p
  Int -> Int -> Int -> NumPoly -> m Boolean
forall (m :: * -> *).
MonadSAT m =>
Int -> Int -> Int -> NumPoly -> m Boolean
positive Int
coefficientBitWidth Int
degree Int
numPoly NumPoly
p'