{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeSynonymInstances #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Data.LA
-- Copyright   :  (c) Masahiro Sakai 2011
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- Some definition for Theory of Linear Arithmetics.
--
-----------------------------------------------------------------------------
module ToySolver.Data.LA
  (
  -- * Expression of linear arithmetics
    Expr
  , Var

  -- ** Conversion
  , var
  , constant
  , terms
  , fromTerms
  , coeffMap
  , fromCoeffMap
  , unitVar
  , asConst

  -- ** Query
  , coeff
  , lookupCoeff
  , extract
  , extractMaybe

  -- ** Operations
  , mapCoeff
  , mapCoeffWithVar
  , evalLinear
  , lift1
  , applySubst
  , applySubst1
  , showExpr

  -- * Atomic formula of linear arithmetics
  , Atom (..)
  , showAtom
  , applySubstAtom
  , applySubst1Atom
  , solveFor
  , module ToySolver.Data.OrdRel

  -- * Evaluation of expression and atomic formula
  , Eval (..)

  -- * misc
  , BoundsEnv
  , computeInterval
  ) where

import Control.Monad
import Control.DeepSeq
import Data.List
import Data.Maybe
import Data.IntMap.Strict (IntMap)
import qualified Data.IntMap.Strict as IntMap
import qualified Data.IntSet as IntSet
import Data.Interval
import Data.VectorSpace

import qualified ToySolver.Data.OrdRel as OrdRel
import ToySolver.Data.OrdRel
import ToySolver.Data.IntVar

-----------------------------------------------------------------------------

-- | Linear combination of variables and constants.
-- Non-negative keys are used for variables's coefficients.
-- key 'unitVar' is used for constants.
newtype Expr r
  = Expr
  { -- | a mapping from variables to coefficients
    forall r. Expr r -> IntMap r
coeffMap :: IntMap r
  } deriving (Expr r -> Expr r -> Bool
(Expr r -> Expr r -> Bool)
-> (Expr r -> Expr r -> Bool) -> Eq (Expr r)
forall r. Eq r => Expr r -> Expr r -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall r. Eq r => Expr r -> Expr r -> Bool
== :: Expr r -> Expr r -> Bool
$c/= :: forall r. Eq r => Expr r -> Expr r -> Bool
/= :: Expr r -> Expr r -> Bool
Eq, Eq (Expr r)
Eq (Expr r) =>
(Expr r -> Expr r -> Ordering)
-> (Expr r -> Expr r -> Bool)
-> (Expr r -> Expr r -> Bool)
-> (Expr r -> Expr r -> Bool)
-> (Expr r -> Expr r -> Bool)
-> (Expr r -> Expr r -> Expr r)
-> (Expr r -> Expr r -> Expr r)
-> Ord (Expr r)
Expr r -> Expr r -> Bool
Expr r -> Expr r -> Ordering
Expr r -> Expr r -> Expr r
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall r. Ord r => Eq (Expr r)
forall r. Ord r => Expr r -> Expr r -> Bool
forall r. Ord r => Expr r -> Expr r -> Ordering
forall r. Ord r => Expr r -> Expr r -> Expr r
$ccompare :: forall r. Ord r => Expr r -> Expr r -> Ordering
compare :: Expr r -> Expr r -> Ordering
$c< :: forall r. Ord r => Expr r -> Expr r -> Bool
< :: Expr r -> Expr r -> Bool
$c<= :: forall r. Ord r => Expr r -> Expr r -> Bool
<= :: Expr r -> Expr r -> Bool
$c> :: forall r. Ord r => Expr r -> Expr r -> Bool
> :: Expr r -> Expr r -> Bool
$c>= :: forall r. Ord r => Expr r -> Expr r -> Bool
>= :: Expr r -> Expr r -> Bool
$cmax :: forall r. Ord r => Expr r -> Expr r -> Expr r
max :: Expr r -> Expr r -> Expr r
$cmin :: forall r. Ord r => Expr r -> Expr r -> Expr r
min :: Expr r -> Expr r -> Expr r
Ord)

-- | Create a @Expr@ from a mapping from variables to coefficients.
fromCoeffMap :: (Num r, Eq r) => IntMap r -> Expr r
fromCoeffMap :: forall r. (Num r, Eq r) => IntMap r -> Expr r
fromCoeffMap IntMap r
m = Expr r -> Expr r
forall r. (Num r, Eq r) => Expr r -> Expr r
normalizeExpr (IntMap r -> Expr r
forall r. IntMap r -> Expr r
Expr IntMap r
m)

-- | terms contained in the expression.
terms :: Expr r -> [(r,Var)]
terms :: forall r. Expr r -> [(r, Var)]
terms (Expr IntMap r
m) = [(r
c,Var
v) | (Var
v,r
c) <- IntMap r -> [(Var, r)]
forall a. IntMap a -> [(Var, a)]
IntMap.toList IntMap r
m]

-- | Create a @Expr@ from a list of terms.
fromTerms :: (Num r, Eq r) => [(r,Var)] -> Expr r
fromTerms :: forall r. (Num r, Eq r) => [(r, Var)] -> Expr r
fromTerms [(r, Var)]
ts = IntMap r -> Expr r
forall r. (Num r, Eq r) => IntMap r -> Expr r
fromCoeffMap (IntMap r -> Expr r) -> IntMap r -> Expr r
forall a b. (a -> b) -> a -> b
$ (r -> r -> r) -> [(Var, r)] -> IntMap r
forall a. (a -> a -> a) -> [(Var, a)] -> IntMap a
IntMap.fromListWith r -> r -> r
forall a. Num a => a -> a -> a
(+) [(Var
x,r
c) | (r
c,Var
x) <- [(r, Var)]
ts]

instance Variables (Expr r) where
  vars :: Expr r -> VarSet
vars (Expr IntMap r
m) = Var -> VarSet -> VarSet
IntSet.delete Var
unitVar (IntMap r -> VarSet
forall a. IntMap a -> VarSet
IntMap.keysSet IntMap r
m)

instance Show r => Show (Expr r) where
  showsPrec :: Var -> Expr r -> ShowS
showsPrec Var
d Expr r
m  = Bool -> ShowS -> ShowS
showParen (Var
d Var -> Var -> Bool
forall a. Ord a => a -> a -> Bool
> Var
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    String -> ShowS
showString String
"fromTerms " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(r, Var)] -> ShowS
forall a. Show a => a -> ShowS
shows (Expr r -> [(r, Var)]
forall r. Expr r -> [(r, Var)]
terms Expr r
m)

instance (Num r, Eq r, Read r) => Read (Expr r) where
  readsPrec :: Var -> ReadS (Expr r)
readsPrec Var
p = Bool -> ReadS (Expr r) -> ReadS (Expr r)
forall a. Bool -> ReadS a -> ReadS a
readParen (Var
p Var -> Var -> Bool
forall a. Ord a => a -> a -> Bool
> Var
10) (ReadS (Expr r) -> ReadS (Expr r))
-> ReadS (Expr r) -> ReadS (Expr r)
forall a b. (a -> b) -> a -> b
$ \ String
r -> do
    (String
"fromTerms",String
s) <- ReadS String
lex String
r
    ([(r, Var)]
xs,String
t) <- ReadS [(r, Var)]
forall a. Read a => ReadS a
reads String
s
    (Expr r, String) -> [(Expr r, String)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(r, Var)] -> Expr r
forall r. (Num r, Eq r) => [(r, Var)] -> Expr r
fromTerms [(r, Var)]
xs, String
t)

instance NFData r => NFData (Expr r) where
  rnf :: Expr r -> ()
rnf (Expr IntMap r
m) = IntMap r -> ()
forall a. NFData a => a -> ()
rnf IntMap r
m

-- | Special variable that should always be evaluated to 1.
unitVar :: Var
unitVar :: Var
unitVar = -Var
1

asConst :: Num r => Expr r -> Maybe r
asConst :: forall r. Num r => Expr r -> Maybe r
asConst (Expr IntMap r
m) =
  case IntMap r -> [(Var, r)]
forall a. IntMap a -> [(Var, a)]
IntMap.toList IntMap r
m of
    [] -> r -> Maybe r
forall a. a -> Maybe a
Just r
0
    [(Var
v,r
x)] | Var
vVar -> Var -> Bool
forall a. Eq a => a -> a -> Bool
==Var
unitVar -> r -> Maybe r
forall a. a -> Maybe a
Just r
x
    [(Var, r)]
_ -> Maybe r
forall a. Maybe a
Nothing

normalizeExpr :: (Num r, Eq r) => Expr r -> Expr r
normalizeExpr :: forall r. (Num r, Eq r) => Expr r -> Expr r
normalizeExpr (Expr IntMap r
t) = IntMap r -> Expr r
forall r. IntMap r -> Expr r
Expr (IntMap r -> Expr r) -> IntMap r -> Expr r
forall a b. (a -> b) -> a -> b
$ (r -> Bool) -> IntMap r -> IntMap r
forall a. (a -> Bool) -> IntMap a -> IntMap a
IntMap.filter (r
0r -> r -> Bool
forall a. Eq a => a -> a -> Bool
/=) IntMap r
t

-- | variable
var :: Num r => Var -> Expr r
var :: forall r. Num r => Var -> Expr r
var Var
v = IntMap r -> Expr r
forall r. IntMap r -> Expr r
Expr (IntMap r -> Expr r) -> IntMap r -> Expr r
forall a b. (a -> b) -> a -> b
$ Var -> r -> IntMap r
forall a. Var -> a -> IntMap a
IntMap.singleton Var
v r
1

-- | constant
constant :: (Num r, Eq r) => r -> Expr r
constant :: forall r. (Num r, Eq r) => r -> Expr r
constant r
c = Expr r -> Expr r
forall r. (Num r, Eq r) => Expr r -> Expr r
normalizeExpr (Expr r -> Expr r) -> Expr r -> Expr r
forall a b. (a -> b) -> a -> b
$ IntMap r -> Expr r
forall r. IntMap r -> Expr r
Expr (IntMap r -> Expr r) -> IntMap r -> Expr r
forall a b. (a -> b) -> a -> b
$ Var -> r -> IntMap r
forall a. Var -> a -> IntMap a
IntMap.singleton Var
unitVar r
c

-- | map coefficients.
mapCoeff :: (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
mapCoeff :: forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
mapCoeff a -> b
f (Expr IntMap a
t) = IntMap b -> Expr b
forall r. IntMap r -> Expr r
Expr (IntMap b -> Expr b) -> IntMap b -> Expr b
forall a b. (a -> b) -> a -> b
$ (a -> Maybe b) -> IntMap a -> IntMap b
forall a b. (a -> Maybe b) -> IntMap a -> IntMap b
IntMap.mapMaybe a -> Maybe b
g IntMap a
t
  where
    g :: a -> Maybe b
g a
c = if b
c' b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
0 then Maybe b
forall a. Maybe a
Nothing else b -> Maybe b
forall a. a -> Maybe a
Just b
c'
      where c' :: b
c' = a -> b
f a
c

-- | map coefficients.
mapCoeffWithVar :: (Num b, Eq b) => (a -> Var -> b) -> Expr a -> Expr b
mapCoeffWithVar :: forall b a. (Num b, Eq b) => (a -> Var -> b) -> Expr a -> Expr b
mapCoeffWithVar a -> Var -> b
f (Expr IntMap a
t) = IntMap b -> Expr b
forall r. IntMap r -> Expr r
Expr (IntMap b -> Expr b) -> IntMap b -> Expr b
forall a b. (a -> b) -> a -> b
$ (Var -> a -> Maybe b) -> IntMap a -> IntMap b
forall a b. (Var -> a -> Maybe b) -> IntMap a -> IntMap b
IntMap.mapMaybeWithKey Var -> a -> Maybe b
g IntMap a
t
  where
    g :: Var -> a -> Maybe b
g Var
v a
c = if b
c' b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
0 then Maybe b
forall a. Maybe a
Nothing else b -> Maybe b
forall a. a -> Maybe a
Just b
c'
      where c' :: b
c' = a -> Var -> b
f a
c Var
v

instance (Num r, Eq r) => AdditiveGroup (Expr r) where
  Expr IntMap r
t ^+^ :: Expr r -> Expr r -> Expr r
^+^ Expr r
e2 | IntMap r -> Bool
forall a. IntMap a -> Bool
IntMap.null IntMap r
t = Expr r
e2
  Expr r
e1 ^+^ Expr IntMap r
t | IntMap r -> Bool
forall a. IntMap a -> Bool
IntMap.null IntMap r
t = Expr r
e1
  Expr r
e1 ^+^ Expr r
e2 = Expr r -> Expr r
forall r. (Num r, Eq r) => Expr r -> Expr r
normalizeExpr (Expr r -> Expr r) -> Expr r -> Expr r
forall a b. (a -> b) -> a -> b
$ Expr r -> Expr r -> Expr r
forall r. Num r => Expr r -> Expr r -> Expr r
plus Expr r
e1 Expr r
e2
  zeroV :: Expr r
zeroV = IntMap r -> Expr r
forall r. IntMap r -> Expr r
Expr (IntMap r -> Expr r) -> IntMap r -> Expr r
forall a b. (a -> b) -> a -> b
$ IntMap r
forall a. IntMap a
IntMap.empty
  negateV :: Expr r -> Expr r
negateV = ((-r
1) Scalar (Expr r) -> Expr r -> Expr r
forall v. VectorSpace v => Scalar v -> v -> v
*^)

instance (Num r, Eq r) => VectorSpace (Expr r) where
  type Scalar (Expr r) = r
  Scalar (Expr r)
1 *^ :: Scalar (Expr r) -> Expr r -> Expr r
*^ Expr r
e = Expr r
e
  Scalar (Expr r)
0 *^ Expr r
e = Expr r
forall v. AdditiveGroup v => v
zeroV
  Scalar (Expr r)
c *^ Expr r
e = (r -> r) -> Expr r -> Expr r
forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
mapCoeff (r
Scalar (Expr r)
cr -> r -> r
forall a. Num a => a -> a -> a
*) Expr r
e

plus :: Num r => Expr r -> Expr r -> Expr r
plus :: forall r. Num r => Expr r -> Expr r -> Expr r
plus (Expr IntMap r
t1) (Expr IntMap r
t2) = IntMap r -> Expr r
forall r. IntMap r -> Expr r
Expr (IntMap r -> Expr r) -> IntMap r -> Expr r
forall a b. (a -> b) -> a -> b
$ (r -> r -> r) -> IntMap r -> IntMap r -> IntMap r
forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IntMap.unionWith r -> r -> r
forall a. Num a => a -> a -> a
(+) IntMap r
t1 IntMap r
t2

instance Num r => Eval (Model r) (Expr r) r where
  eval :: Model r -> Expr r -> r
eval Model r
m (Expr Model r
t) = [r] -> r
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [(Model r
m' Model r -> Var -> r
forall a. IntMap a -> Var -> a
IntMap.! Var
v) r -> r -> r
forall a. Num a => a -> a -> a
* r
c | (Var
v,r
c) <- Model r -> [(Var, r)]
forall a. IntMap a -> [(Var, a)]
IntMap.toList Model r
t]
    where m' :: Model r
m' = Var -> r -> Model r -> Model r
forall a. Var -> a -> IntMap a -> IntMap a
IntMap.insert Var
unitVar r
1 Model r
m

-- | evaluate the expression under the model.
evalLinear :: VectorSpace a => Model a -> a -> Expr (Scalar a) -> a
evalLinear :: forall a. VectorSpace a => Model a -> a -> Expr (Scalar a) -> a
evalLinear Model a
m a
u (Expr IntMap (Scalar a)
t) = [a] -> a
forall (f :: * -> *) v. (Foldable f, AdditiveGroup v) => f v -> v
sumV [Scalar a
c Scalar a -> a -> a
forall v. VectorSpace v => Scalar v -> v -> v
*^ (Model a
m' Model a -> Var -> a
forall a. IntMap a -> Var -> a
IntMap.! Var
v) | (Var
v,Scalar a
c) <- IntMap (Scalar a) -> [(Var, Scalar a)]
forall a. IntMap a -> [(Var, a)]
IntMap.toList IntMap (Scalar a)
t]
  where m' :: Model a
m' = Var -> a -> Model a -> Model a
forall a. Var -> a -> IntMap a -> IntMap a
IntMap.insert Var
unitVar a
u Model a
m

lift1 :: VectorSpace x => x -> (Var -> x) -> Expr (Scalar x) -> x
lift1 :: forall x. VectorSpace x => x -> (Var -> x) -> Expr (Scalar x) -> x
lift1 x
unit Var -> x
f (Expr IntMap (Scalar x)
t) = [x] -> x
forall (f :: * -> *) v. (Foldable f, AdditiveGroup v) => f v -> v
sumV [Scalar x
c Scalar x -> x -> x
forall v. VectorSpace v => Scalar v -> v -> v
*^ (Var -> x
g Var
v) | (Var
v,Scalar x
c) <- IntMap (Scalar x) -> [(Var, Scalar x)]
forall a. IntMap a -> [(Var, a)]
IntMap.toList IntMap (Scalar x)
t]
  where
    g :: Var -> x
g Var
v
      | Var
vVar -> Var -> Bool
forall a. Eq a => a -> a -> Bool
==Var
unitVar = x
unit
      | Bool
otherwise   = Var -> x
f Var
v

applySubst :: (Num r, Eq r) => VarMap (Expr r) -> Expr r -> Expr r
applySubst :: forall r. (Num r, Eq r) => VarMap (Expr r) -> Expr r -> Expr r
applySubst VarMap (Expr r)
s (Expr IntMap r
m) = [Expr r] -> Expr r
forall (f :: * -> *) v. (Foldable f, AdditiveGroup v) => f v -> v
sumV (((Var, r) -> Expr r) -> [(Var, r)] -> [Expr r]
forall a b. (a -> b) -> [a] -> [b]
map (Var, r) -> Expr r
f (IntMap r -> [(Var, r)]
forall a. IntMap a -> [(Var, a)]
IntMap.toList IntMap r
m))
  where
    f :: (Var, r) -> Expr r
f (Var
v,r
c) = r
Scalar (Expr r)
c Scalar (Expr r) -> Expr r -> Expr r
forall v. VectorSpace v => Scalar v -> v -> v
*^ (
      case Var -> VarMap (Expr r) -> Maybe (Expr r)
forall a. Var -> IntMap a -> Maybe a
IntMap.lookup Var
v VarMap (Expr r)
s of
        Just Expr r
tm -> Expr r
tm
        Maybe (Expr r)
Nothing -> Var -> Expr r
forall r. Num r => Var -> Expr r
var Var
v)

-- | applySubst1 x e e1 == e1[e/x]
applySubst1 :: (Num r, Eq r) => Var -> Expr r -> Expr r -> Expr r
applySubst1 :: forall r. (Num r, Eq r) => Var -> Expr r -> Expr r -> Expr r
applySubst1 Var
x Expr r
e Expr r
e1 =
  case Var -> Expr r -> Maybe (r, Expr r)
forall r. Num r => Var -> Expr r -> Maybe (r, Expr r)
extractMaybe Var
x Expr r
e1 of
    Maybe (r, Expr r)
Nothing -> Expr r
e1
    Just (r
c,Expr r
e2) -> r
Scalar (Expr r)
c Scalar (Expr r) -> Expr r -> Expr r
forall v. VectorSpace v => Scalar v -> v -> v
*^ Expr r
e Expr r -> Expr r -> Expr r
forall v. AdditiveGroup v => v -> v -> v
^+^ Expr r
e2

-- | lookup a coefficient of the variable.
-- @
--   coeff v e == fst (extract v e)
-- @
coeff :: Num r => Var -> Expr r -> r
coeff :: forall r. Num r => Var -> Expr r -> r
coeff Var
v (Expr IntMap r
m) = r -> Var -> IntMap r -> r
forall a. a -> Var -> IntMap a -> a
IntMap.findWithDefault r
0 Var
v IntMap r
m

-- | lookup a coefficient of the variable.
-- It returns @Nothing@ if the expression does not contain @v@.
-- @
--   lookupCoeff v e == fmap fst (extractMaybe v e)
-- @
lookupCoeff :: Num r => Var -> Expr r -> Maybe r
lookupCoeff :: forall r. Num r => Var -> Expr r -> Maybe r
lookupCoeff Var
v (Expr IntMap r
m) = Var -> IntMap r -> Maybe r
forall a. Var -> IntMap a -> Maybe a
IntMap.lookup Var
v IntMap r
m

-- | @extract v e@ returns @(c, e')@ such that @e == c *^ v ^+^ e'@
extract :: Num r => Var -> Expr r -> (r, Expr r)
extract :: forall r. Num r => Var -> Expr r -> (r, Expr r)
extract Var
v (Expr IntMap r
m) = (r -> Var -> IntMap r -> r
forall a. a -> Var -> IntMap a -> a
IntMap.findWithDefault r
0 Var
v IntMap r
m, IntMap r -> Expr r
forall r. IntMap r -> Expr r
Expr (Var -> IntMap r -> IntMap r
forall a. Var -> IntMap a -> IntMap a
IntMap.delete Var
v IntMap r
m))
{-
-- Alternative implementation which may be faster but allocte more memory
extract v (Expr m) =
  case IntMap.updateLookupWithKey (\_ _ -> Nothing) v m of
    (Nothing, _) -> (0, Expr m)
    (Just c, m2) -> (c, Expr m2)
-}

-- | @extractMaybe v e@ returns @Just (c, e')@ such that @e == c *^ v ^+^ e'@
-- if @e@ contains v, and returns @Nothing@ otherwise.
extractMaybe :: Num r => Var -> Expr r -> Maybe (r, Expr r)
extractMaybe :: forall r. Num r => Var -> Expr r -> Maybe (r, Expr r)
extractMaybe Var
v (Expr IntMap r
m) =
  case Var -> IntMap r -> Maybe r
forall a. Var -> IntMap a -> Maybe a
IntMap.lookup Var
v IntMap r
m of
    Maybe r
Nothing -> Maybe (r, Expr r)
forall a. Maybe a
Nothing
    Just r
c -> (r, Expr r) -> Maybe (r, Expr r)
forall a. a -> Maybe a
Just (r
c, IntMap r -> Expr r
forall r. IntMap r -> Expr r
Expr (Var -> IntMap r -> IntMap r
forall a. Var -> IntMap a -> IntMap a
IntMap.delete Var
v IntMap r
m))
{-
-- Alternative implementation which may be faster but allocte more memory
extractMaybe v (Expr m) =
  case IntMap.updateLookupWithKey (\_ _ -> Nothing) v m of
    (Nothing, _) -> Nothing
    (Just c, m2) -> Just (c, Expr m2)
-}

showExpr :: (Num r, Eq r, Show r) => Expr r -> String
showExpr :: forall r. (Num r, Eq r, Show r) => Expr r -> String
showExpr = (Var -> String) -> Expr r -> String
forall r.
(Num r, Show r, Eq r) =>
(Var -> String) -> Expr r -> String
showExprWith Var -> String
forall {a}. Show a => a -> String
f
  where
    f :: a -> String
f a
x = String
"x" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall {a}. Show a => a -> String
show a
x

showExprWith :: (Num r, Show r, Eq r) => (Var -> String) -> Expr r -> String
showExprWith :: forall r.
(Num r, Show r, Eq r) =>
(Var -> String) -> Expr r -> String
showExprWith Var -> String
env (Expr IntMap r
m) = (ShowS -> ShowS -> ShowS) -> ShowS -> [ShowS] -> ShowS
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) ShowS
forall a. a -> a
id [ShowS]
xs String
""
  where
    xs :: [ShowS]
xs = ShowS -> [ShowS] -> [ShowS]
forall a. a -> [a] -> [a]
intersperse (String -> ShowS
showString String
" + ") [ShowS]
ts
    ts :: [ShowS]
ts = [if r
cr -> r -> Bool
forall a. Eq a => a -> a -> Bool
==r
1
            then String -> ShowS
showString (Var -> String
env Var
x)
            else Var -> r -> ShowS
forall a. Show a => Var -> a -> ShowS
showsPrec Var
8 r
c ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
"*" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString (Var -> String
env Var
x)
          | (Var
x,r
c) <- IntMap r -> [(Var, r)]
forall a. IntMap a -> [(Var, a)]
IntMap.toList IntMap r
m, Var
x Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
/= Var
unitVar] [ShowS] -> [ShowS] -> [ShowS]
forall a. [a] -> [a] -> [a]
++
         [Var -> r -> ShowS
forall a. Show a => Var -> a -> ShowS
showsPrec Var
7 r
c | r
c <- Maybe r -> [r]
forall a. Maybe a -> [a]
maybeToList (Var -> IntMap r -> Maybe r
forall a. Var -> IntMap a -> Maybe a
IntMap.lookup Var
unitVar IntMap r
m)]

-----------------------------------------------------------------------------

-- | Atomic Formula of Linear Arithmetics
type Atom r = OrdRel (Expr r)

showAtom :: (Num r, Eq r, Show r) => Atom r -> String
showAtom :: forall r. (Num r, Eq r, Show r) => Atom r -> String
showAtom (OrdRel Expr r
lhs RelOp
op Expr r
rhs) = Expr r -> String
forall r. (Num r, Eq r, Show r) => Expr r -> String
showExpr Expr r
lhs String -> ShowS
forall a. [a] -> [a] -> [a]
++ RelOp -> String
showOp RelOp
op String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr r -> String
forall r. (Num r, Eq r, Show r) => Expr r -> String
showExpr Expr r
rhs

applySubstAtom :: (Num r, Eq r) => VarMap (Expr r) -> Atom r -> Atom r
applySubstAtom :: forall r. (Num r, Eq r) => VarMap (Expr r) -> Atom r -> Atom r
applySubstAtom VarMap (Expr r)
s (OrdRel Expr r
lhs RelOp
op Expr r
rhs) = Expr r -> RelOp -> Expr r -> OrdRel (Expr r)
forall e. e -> RelOp -> e -> OrdRel e
OrdRel (VarMap (Expr r) -> Expr r -> Expr r
forall r. (Num r, Eq r) => VarMap (Expr r) -> Expr r -> Expr r
applySubst VarMap (Expr r)
s Expr r
lhs) RelOp
op (VarMap (Expr r) -> Expr r -> Expr r
forall r. (Num r, Eq r) => VarMap (Expr r) -> Expr r -> Expr r
applySubst VarMap (Expr r)
s Expr r
rhs)

-- | applySubst1 x e phi == phi[e/x]
applySubst1Atom :: (Num r, Eq r) => Var -> Expr r -> Atom r -> Atom r
applySubst1Atom :: forall r. (Num r, Eq r) => Var -> Expr r -> Atom r -> Atom r
applySubst1Atom Var
x Expr r
e (OrdRel Expr r
lhs RelOp
op Expr r
rhs) = Expr r -> RelOp -> Expr r -> OrdRel (Expr r)
forall e. e -> RelOp -> e -> OrdRel e
OrdRel (Var -> Expr r -> Expr r -> Expr r
forall r. (Num r, Eq r) => Var -> Expr r -> Expr r -> Expr r
applySubst1 Var
x Expr r
e Expr r
lhs) RelOp
op (Var -> Expr r -> Expr r -> Expr r
forall r. (Num r, Eq r) => Var -> Expr r -> Expr r -> Expr r
applySubst1 Var
x Expr r
e Expr r
rhs)

-- | Solve linear (in)equation for the given variable.
--
-- @solveFor a v@ returns @Just (op, e)@ such that @Atom v op e@
-- is equivalent to @a@.
solveFor :: (Real r, Fractional r) => Atom r -> Var -> Maybe (RelOp, Expr r)
solveFor :: forall r.
(Real r, Fractional r) =>
Atom r -> Var -> Maybe (RelOp, Expr r)
solveFor (OrdRel Expr r
lhs RelOp
op Expr r
rhs) Var
v = do
  (r
c,Expr r
e) <- Var -> Expr r -> Maybe (r, Expr r)
forall r. Num r => Var -> Expr r -> Maybe (r, Expr r)
extractMaybe Var
v (Expr r
lhs Expr r -> Expr r -> Expr r
forall v. AdditiveGroup v => v -> v -> v
^-^ Expr r
rhs)
  (RelOp, Expr r) -> Maybe (RelOp, Expr r)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ( if r
c r -> r -> Bool
forall a. Ord a => a -> a -> Bool
< r
0 then RelOp -> RelOp
flipOp RelOp
op else RelOp
op
         , (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
*^ Expr r -> Expr r
forall v. AdditiveGroup v => v -> v
negateV Expr r
e
         )

-----------------------------------------------------------------------------

type BoundsEnv r = VarMap (Interval r)

-- | compute bounds for a @Expr@ with respect to @BoundsEnv@.
computeInterval :: (Real r, Fractional r) => BoundsEnv r -> Expr r -> Interval r
computeInterval :: forall r.
(Real r, Fractional r) =>
BoundsEnv r -> Expr r -> Interval r
computeInterval BoundsEnv r
b = BoundsEnv r -> Expr (Interval r) -> Interval r
forall m e v. Eval m e v => m -> e -> v
eval BoundsEnv r
b (Expr (Interval r) -> Interval r)
-> (Expr r -> Expr (Interval r)) -> Expr r -> Interval r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (r -> Interval r) -> Expr r -> Expr (Interval r)
forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
mapCoeff r -> Interval r
forall r. Ord r => r -> Interval r
Data.Interval.singleton

-----------------------------------------------------------------------------