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
-> Int
-> Int
-> 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
-> Int
-> Int
-> 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
-> Int
-> Int
-> 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'