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 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 <- forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
numPoly 
          forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadSAT m => Int -> Int -> m NumPoly
polynomial Int
coefficientBitWidth Int
degree forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *). MonadSAT m => NumPoly -> m NumPoly
sqr
  forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM forall (m :: * -> *). MonadSAT m => NumPoly -> NumPoly -> m NumPoly
add 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 <- forall (m :: * -> *). MonadSAT m => Int -> Int -> Int -> m NumPoly
sumOfSquares Int
coefficientBitWidth Int
degree Int
numPoly
  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 <- forall (m :: * -> *). MonadSAT m => Int -> Int -> Int -> m NumPoly
sumOfSquares Int
coefficientBitWidth Int
degree Int
numPoly
  Boolean
e1 <- forall (m :: * -> *). MonadSAT m => NumPoly -> NumPoly -> m Boolean
equals NumPoly
sos NumPoly
p
  Boolean
e2 <- forall (m :: * -> *). MonadSAT m => Number -> m Boolean
F.positive forall a b. (a -> b) -> a -> b
$ forall a. Poly a -> a
constantTerm NumPoly
sos 
  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' <- forall (m :: * -> *). MonadSAT m => NumPoly -> m NumPoly
derive NumPoly
p
  forall (m :: * -> *).
MonadSAT m =>
Int -> Int -> Int -> NumPoly -> m Boolean
positive Int
coefficientBitWidth Int
degree Int
numPoly NumPoly
p'