{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE ScopedTypeVariables #-}
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)
inferBounds :: forall r. (RealFrac r)
=> LA.BoundsEnv r
-> [LA.Atom r]
-> VarSet
-> Int
-> 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 :: 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)
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