{-# 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 = ([C r] -> [C r] -> [C r]) -> [(Int, [C r])] -> VarMap [C r]
forall a. (a -> a -> a) -> [(Int, a)] -> IntMap a
IM.fromListWith [C r] -> [C r] -> [C r]
forall a. [a] -> [a] -> [a]
(++) ([(Int, [C r])] -> VarMap [C r]) -> [(Int, [C r])] -> VarMap [C r]
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 = Expr r -> IntMap r
forall r. Expr r -> IntMap r
LA.coeffMap (Expr r
lhs Expr r -> Expr r -> Expr r
forall v. AdditiveGroup v => v -> v -> v
^-^ Expr r
rhs)
      (Int
v,r
c) <- IntMap r -> [(Int, r)]
forall a. IntMap a -> [(Int, a)]
IM.toList IntMap r
m
      Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ Int
v Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
LA.unitVar
      let op' :: RelOp
op' = if r
c r -> r -> Bool
forall a. Ord a => a -> a -> Bool
< r
0 then RelOp -> RelOp
flipOp RelOp
op else RelOp
op
          rhs' :: Expr r
rhs' = (-r
1r -> r -> r
forall a. Fractional a => a -> a -> a
/r
c) Scalar (Expr r) -> Expr r -> Expr r
forall v. VectorSpace v => Scalar v -> v -> v
*^ IntMap r -> Expr r
forall r. (Num r, Eq r) => IntMap r -> Expr r
LA.fromCoeffMap (Int -> IntMap r -> IntMap r
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
v IntMap r
m)
      (Int, [C r]) -> [(Int, [C r])]
forall a. a -> [a]
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
limitInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>=Int
0 Bool -> Bool -> Bool
&& Int
iInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>=Int
limit) Bool -> Bool -> Bool
|| BoundsEnv r
bBoundsEnv r -> BoundsEnv r -> Bool
forall a. Eq a => a -> a -> Bool
==BoundsEnv r
b' then BoundsEnv r
b else Int -> BoundsEnv r -> BoundsEnv r
loop (Int
iInt -> Int -> Int
forall 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 = (Int -> Interval r -> Interval r) -> BoundsEnv r -> BoundsEnv r
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 (Interval r -> Interval r) -> Interval r -> Interval r
forall a b. (a -> b) -> a -> b
$ BoundsEnv r -> [C r] -> Interval r -> Interval r
forall r.
(Real r, Fractional r) =>
BoundsEnv r -> [C r] -> Interval r -> Interval r
f BoundsEnv r
b ([C r] -> Int -> VarMap [C r] -> [C r]
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 Interval r -> Interval r
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 = (Interval r -> Interval r -> Interval r)
-> Interval r -> [Interval r] -> Interval r
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Interval r -> Interval r -> Interval r
forall r. Ord r => Interval r -> Interval r -> Interval r
intersection Interval r
i ([Interval r] -> Interval r) -> [Interval r] -> Interval r
forall a b. (a -> b) -> a -> b
$ do
  (RelOp
op, Expr r
rhs) <- [C r]
cs
  let i' :: Interval r
i' = BoundsEnv r -> Expr r -> Interval r
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 = Interval r -> (Extended r, Boundary)
forall r. Interval r -> (Extended r, Boundary)
lowerBound' Interval r
i'
      ub :: (Extended r, Boundary)
ub = Interval r -> (Extended r, Boundary)
forall r. Interval r -> (Extended r, Boundary)
upperBound' Interval r
i'
  case RelOp
op of
    RelOp
Eql -> Interval r -> [Interval r]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return Interval r
i'
    RelOp
Le -> Interval r -> [Interval r]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Interval r -> [Interval r]) -> Interval r -> [Interval r]
forall a b. (a -> b) -> a -> b
$ (Extended r, Boundary) -> (Extended r, Boundary) -> Interval r
forall r.
Ord r =>
(Extended r, Boundary) -> (Extended r, Boundary) -> Interval r
interval (Extended r
forall r. Extended r
NegInf, Boundary
Open) (Extended r, Boundary)
ub
    RelOp
Ge -> Interval r -> [Interval r]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Interval r -> [Interval r]) -> Interval r -> [Interval r]
forall a b. (a -> b) -> a -> b
$ (Extended r, Boundary) -> (Extended r, Boundary) -> Interval r
forall r.
Ord r =>
(Extended r, Boundary) -> (Extended r, Boundary) -> Interval r
interval (Extended r, Boundary)
lb (Extended r
forall r. Extended r
PosInf, Boundary
Open)
    RelOp
Lt -> Interval r -> [Interval r]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Interval r -> [Interval r]) -> Interval r -> [Interval r]
forall a b. (a -> b) -> a -> b
$ (Extended r, Boundary) -> (Extended r, Boundary) -> Interval r
forall r.
Ord r =>
(Extended r, Boundary) -> (Extended r, Boundary) -> Interval r
interval (Extended r
forall r. Extended r
NegInf, Boundary
Open) ((Extended r, Boundary) -> (Extended r, Boundary)
forall r. (Extended r, Boundary) -> (Extended r, Boundary)
strict (Extended r, Boundary)
ub)
    RelOp
Gt -> Interval r -> [Interval r]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Interval r -> [Interval r]) -> Interval r -> [Interval r]
forall a b. (a -> b) -> a -> b
$ (Extended r, Boundary) -> (Extended r, Boundary) -> Interval r
forall r.
Ord r =>
(Extended r, Boundary) -> (Extended r, Boundary) -> Interval r
interval ((Extended r, Boundary) -> (Extended r, Boundary)
forall r. (Extended r, Boundary) -> (Extended r, Boundary)
strict (Extended r, Boundary)
ub) (Extended r
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 = (Extended r, Boundary) -> (Extended r, Boundary) -> Interval r
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) = Interval r -> (Extended r, Boundary)
forall r. Interval r -> (Extended r, Boundary)
lowerBound' Interval r
ival
    ub :: (Extended r, Boundary)
ub@(Extended r
x2, Boundary
in2) = Interval r -> (Extended r, Boundary)
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 r -> Bool
forall a. RealFrac a => a -> Bool
isInteger r
x Bool -> Bool -> Bool
&& Boundary
in1 Boundary -> Boundary -> Bool
forall a. Eq a => a -> a -> Bool
== Boundary
Open
            then r -> Extended r
forall r. r -> Extended r
Finite (r
x r -> r -> r
forall a. Num a => a -> a -> a
+ r
1)
            else r -> Extended r
forall r. r -> Extended r
Finite (Integer -> r
forall a. Num a => Integer -> a
fromInteger (r -> Integer
forall b. Integral b => r -> b
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 r -> Bool
forall a. RealFrac a => a -> Bool
isInteger r
x Bool -> Bool -> Bool
&& Boundary
in2 Boundary -> Boundary -> Bool
forall a. Eq a => a -> a -> Bool
== Boundary
Open
            then r -> Extended r
forall r. r -> Extended r
Finite (r
x r -> r -> r
forall a. Num a => a -> a -> a
- r
1)
            else r -> Extended r
forall r. r -> Extended r
Finite (Integer -> r
forall a. Num a => Integer -> a
fromInteger (r -> Integer
forall b. Integral b => r -> b
forall a b. (RealFrac a, Integral b) => a -> b
floor r
x))
          , Boundary
Closed
          )
        Extended r
_ -> (Extended r, Boundary)
ub