{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE ScopedTypeVariables #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Arith.BoundsInference
-- Copyright   :  (c) Masahiro Sakai 2011
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- Tightening variable bounds by constraint propagation.
--
-----------------------------------------------------------------------------
module ToySolver.Arith.BoundsInference
  ( BoundsEnv
  , inferBounds
  , LA.computeInterval
  ) where

import Control.Monad
import qualified Data.IntMap as IM
import qualified Data.IntSet as IS
import Data.VectorSpace
import Data.Interval

import ToySolver.Data.OrdRel
import ToySolver.Data.LA (BoundsEnv)
import qualified ToySolver.Data.LA as LA
import ToySolver.Data.IntVar
import ToySolver.Internal.Util (isInteger)

type C r = (RelOp, LA.Expr r)

-- | tightening variable bounds by constraint propagation.
inferBounds :: forall r. (RealFrac r)
  => LA.BoundsEnv r -- ^ initial bounds
  -> [LA.Atom r]    -- ^ constraints
  -> VarSet         -- ^ integral variables
  -> Int            -- ^ limit of iterations
  -> LA.BoundsEnv r
inferBounds :: forall r.
RealFrac r =>
BoundsEnv r -> [Atom r] -> VarSet -> Int -> BoundsEnv r
inferBounds BoundsEnv r
bounds [Atom r]
constraints VarSet
ivs Int
limit = Int -> BoundsEnv r -> BoundsEnv r
loop Int
0 BoundsEnv r
bounds
  where
    cs :: VarMap [C r]
    cs :: VarMap [C r]
cs = forall a. (a -> a -> a) -> [(Int, a)] -> IntMap a
IM.fromListWith forall a. [a] -> [a] -> [a]
(++) forall a b. (a -> b) -> a -> b
$ do
      OrdRel Expr r
lhs RelOp
op Expr r
rhs <- [Atom r]
constraints
      let m :: IntMap r
m = forall r. Expr r -> IntMap r
LA.coeffMap (Expr r
lhs forall v. AdditiveGroup v => v -> v -> v
^-^ Expr r
rhs)
      (Int
v,r
c) <- forall a. IntMap a -> [(Int, a)]
IM.toList IntMap r
m
      forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ Int
v forall a. Eq a => a -> a -> Bool
/= Int
LA.unitVar
      let op' :: RelOp
op' = if r
c forall a. Ord a => a -> a -> Bool
< r
0 then RelOp -> RelOp
flipOp RelOp
op else RelOp
op
          rhs' :: Expr r
rhs' = (-r
1forall a. Fractional a => a -> a -> a
/r
c) forall v. VectorSpace v => Scalar v -> v -> v
*^ forall r. (Num r, Eq r) => IntMap r -> Expr r
LA.fromCoeffMap (forall a. Int -> IntMap a -> IntMap a
IM.delete Int
v IntMap r
m)
      forall (m :: * -> *) a. Monad m => a -> m a
return (Int
v, [(RelOp
op', Expr r
rhs')])

    loop  :: Int -> LA.BoundsEnv r -> LA.BoundsEnv r
    loop :: Int -> BoundsEnv r -> BoundsEnv r
loop !Int
i BoundsEnv r
b = if (Int
limitforall a. Ord a => a -> a -> Bool
>=Int
0 Bool -> Bool -> Bool
&& Int
iforall a. Ord a => a -> a -> Bool
>=Int
limit) Bool -> Bool -> Bool
|| BoundsEnv r
bforall a. Eq a => a -> a -> Bool
==BoundsEnv r
b' then BoundsEnv r
b else Int -> BoundsEnv r -> BoundsEnv r
loop (Int
iforall a. Num a => a -> a -> a
+Int
1) BoundsEnv r
b'
      where
        b' :: BoundsEnv r
b' = BoundsEnv r -> BoundsEnv r
refine BoundsEnv r
b

    refine :: LA.BoundsEnv r -> LA.BoundsEnv r
    refine :: BoundsEnv r -> BoundsEnv r
refine BoundsEnv r
b = forall a b. (Int -> a -> b) -> IntMap a -> IntMap b
IM.mapWithKey (\Int
v Interval r
i -> Int -> Interval r -> Interval r
tighten Int
v forall a b. (a -> b) -> a -> b
$ forall r.
(Real r, Fractional r) =>
BoundsEnv r -> [C r] -> Interval r -> Interval r
f BoundsEnv r
b (forall a. a -> Int -> IntMap a -> a
IM.findWithDefault [] Int
v VarMap [C r]
cs) Interval r
i) BoundsEnv r
b

    -- tighten bounds of integer variables
    tighten :: Var -> Interval r -> Interval r
    tighten :: Int -> Interval r -> Interval r
tighten Int
v Interval r
x =
      if Int
v Int -> VarSet -> Bool
`IS.notMember` VarSet
ivs
        then Interval r
x
        else forall r. RealFrac r => Interval r -> Interval r
tightenToInteger Interval r
x

f :: (Real r, Fractional r) => LA.BoundsEnv r -> [C r] -> Interval r -> Interval r
f :: forall r.
(Real r, Fractional r) =>
BoundsEnv r -> [C r] -> Interval r -> Interval r
f BoundsEnv r
b [C r]
cs Interval r
i = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall r. Ord r => Interval r -> Interval r -> Interval r
intersection Interval r
i forall a b. (a -> b) -> a -> b
$ do
  (RelOp
op, Expr r
rhs) <- [C r]
cs
  let i' :: Interval r
i' = forall r.
(Real r, Fractional r) =>
BoundsEnv r -> Expr r -> Interval r
LA.computeInterval BoundsEnv r
b Expr r
rhs
      lb :: (Extended r, Boundary)
lb = forall r. Interval r -> (Extended r, Boundary)
lowerBound' Interval r
i'
      ub :: (Extended r, Boundary)
ub = forall r. Interval r -> (Extended r, Boundary)
upperBound' Interval r
i'
  case RelOp
op of
    RelOp
Eql -> forall (m :: * -> *) a. Monad m => a -> m a
return Interval r
i'
    RelOp
Le -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
Ord r =>
(Extended r, Boundary) -> (Extended r, Boundary) -> Interval r
interval (forall r. Extended r
NegInf, Boundary
Open) (Extended r, Boundary)
ub
    RelOp
Ge -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
Ord r =>
(Extended r, Boundary) -> (Extended r, Boundary) -> Interval r
interval (Extended r, Boundary)
lb (forall r. Extended r
PosInf, Boundary
Open)
    RelOp
Lt -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
Ord r =>
(Extended r, Boundary) -> (Extended r, Boundary) -> Interval r
interval (forall r. Extended r
NegInf, Boundary
Open) (forall r. (Extended r, Boundary) -> (Extended r, Boundary)
strict (Extended r, Boundary)
ub)
    RelOp
Gt -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
Ord r =>
(Extended r, Boundary) -> (Extended r, Boundary) -> Interval r
interval (forall r. (Extended r, Boundary) -> (Extended r, Boundary)
strict (Extended r, Boundary)
ub) (forall r. Extended r
PosInf, Boundary
Open)
    RelOp
NEq -> []

strict :: (Extended r, Boundary) -> (Extended r, Boundary)
strict :: forall r. (Extended r, Boundary) -> (Extended r, Boundary)
strict (Extended r
x, Boundary
_) = (Extended r
x, Boundary
Open)

-- | tightening intervals by ceiling lower bounds and flooring upper bounds.
tightenToInteger :: forall r. (RealFrac r) => Interval r -> Interval r
tightenToInteger :: forall r. RealFrac r => Interval r -> Interval r
tightenToInteger Interval r
ival = forall r.
Ord r =>
(Extended r, Boundary) -> (Extended r, Boundary) -> Interval r
interval (Extended r, Boundary)
lb2 (Extended r, Boundary)
ub2
  where
    lb :: (Extended r, Boundary)
lb@(Extended r
x1, Boundary
in1) = forall r. Interval r -> (Extended r, Boundary)
lowerBound' Interval r
ival
    ub :: (Extended r, Boundary)
ub@(Extended r
x2, Boundary
in2) = forall r. Interval r -> (Extended r, Boundary)
upperBound' Interval r
ival
    lb2 :: (Extended r, Boundary)
lb2 =
      case Extended r
x1 of
        Finite r
x ->
          ( if forall a. RealFrac a => a -> Bool
isInteger r
x Bool -> Bool -> Bool
&& Boundary
in1 forall a. Eq a => a -> a -> Bool
== Boundary
Open
            then forall r. r -> Extended r
Finite (r
x forall a. Num a => a -> a -> a
+ r
1)
            else forall r. r -> Extended r
Finite (forall a. Num a => Integer -> a
fromInteger (forall a b. (RealFrac a, Integral b) => a -> b
ceiling r
x))
          , Boundary
Closed
          )
        Extended r
_ -> (Extended r, Boundary)
lb
    ub2 :: (Extended r, Boundary)
ub2 =
      case Extended r
x2 of
        Finite r
x ->
          ( if forall a. RealFrac a => a -> Bool
isInteger r
x Bool -> Bool -> Bool
&& Boundary
in2 forall a. Eq a => a -> a -> Bool
== Boundary
Open
            then forall r. r -> Extended r
Finite (r
x forall a. Num a => a -> a -> a
- r
1)
            else forall r. r -> Extended r
Finite (forall a. Num a => Integer -> a
fromInteger (forall a b. (RealFrac a, Integral b) => a -> b
floor r
x))
          , Boundary
Closed
          )
        Extended r
_ -> (Extended r, Boundary)
ub