{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Arith.FourierMotzkin.Base
-- Copyright   :  (c) Masahiro Sakai 2011-2013
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- Naïve implementation of Fourier-Motzkin Variable Elimination
--
-- Reference:
--
-- * <http://users.cecs.anu.edu.au/~michaeln/pubs/arithmetic-dps.pdf>
--
-----------------------------------------------------------------------------
module ToySolver.Arith.FourierMotzkin.Base
    (
    -- * Primitive constraints
      Constr (..)
    , eqR
    , ExprZ
    , fromLAAtom
    , toLAAtom
    , constraintsToDNF
    , simplify

    -- * Bounds
    , Bounds
    , evalBounds
    , boundsToConstrs
    , collectBounds

    -- * Projection
    , project
    , project'
    , projectN
    , projectN'

    -- * Solving
    , solve
    , solve'

    -- * Utilities used by other modules
    , Rat
    , toRat
    ) where

import Control.Monad
import Data.List
import Data.Maybe
import Data.Ratio
import qualified Data.IntMap as IM
import qualified Data.IntSet as IS
import Data.VectorSpace hiding (project)
import qualified Data.Interval as Interval
import Data.Interval (Interval, Extended (..), (<=..<), (<..<=), (<..<))

import ToySolver.Data.OrdRel
import ToySolver.Data.Boolean
import ToySolver.Data.DNF
import qualified ToySolver.Data.LA as LA
import ToySolver.Data.IntVar

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

type ExprZ = LA.Expr Integer

-- | (t,c) represents t/c, and c must be >0.
type Rat = (ExprZ, Integer)

toRat :: LA.Expr Rational -> Rat
toRat :: Expr Rational -> Rat
toRat Expr Rational
e = Integer -> Rat -> Rat
seq Integer
m (Rat -> Rat) -> Rat -> Rat
forall a b. (a -> b) -> a -> b
$ ((Rational -> Integer) -> Expr Rational -> Expr Integer
forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
LA.mapCoeff Rational -> Integer
forall a. Integral a => Ratio a -> a
f Expr Rational
e, Integer
m)
  where
    f :: Ratio a -> a
f Ratio a
x = Ratio a -> a
forall a. Ratio a -> a
numerator (Integer -> Ratio a
forall a. Num a => Integer -> a
fromInteger Integer
m Ratio a -> Ratio a -> Ratio a
forall a. Num a => a -> a -> a
* Ratio a
x)
    m :: Integer
m = (Integer -> Integer -> Integer) -> Integer -> [Integer] -> Integer
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
lcm Integer
1 [Rational -> Integer
forall a. Ratio a -> a
denominator Rational
c | (Rational
c,Var
_) <- Expr Rational -> [(Rational, Var)]
forall r. Expr r -> [(r, Var)]
LA.terms Expr Rational
e]

fromRat :: Rat -> LA.Expr Rational
fromRat :: Rat -> Expr Rational
fromRat (Expr Integer
e,Integer
c) = (Integer -> Rational) -> Expr Integer -> Expr Rational
forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
LA.mapCoeff (Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
c) Expr Integer
e

evalRat :: Model Rational -> Rat -> Rational
evalRat :: Model Rational -> Rat -> Rational
evalRat Model Rational
model (Expr Integer
e, Integer
d) = Rational -> (Var -> Rational) -> Expr (Scalar Rational) -> Rational
forall x. VectorSpace x => x -> (Var -> x) -> Expr (Scalar x) -> x
LA.lift1 Rational
1 (Model Rational
model Model Rational -> Var -> Rational
forall a. IntMap a -> Var -> a
IM.!) ((Integer -> Rational) -> Expr Integer -> Expr Rational
forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
LA.mapCoeff Integer -> Rational
forall a b. (Integral a, Num b) => a -> b
fromIntegral Expr Integer
e) Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ (Integer -> Rational
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
d)

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

-- | Atomic constraint
data Constr
  = IsNonneg ExprZ
  -- ^ e ≥ 0
  | IsPos ExprZ
  -- ^ e > 0
  | IsZero ExprZ
  -- ^ e = 0
  deriving (Var -> Constr -> ShowS
[Constr] -> ShowS
Constr -> String
(Var -> Constr -> ShowS)
-> (Constr -> String) -> ([Constr] -> ShowS) -> Show Constr
forall a.
(Var -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Constr] -> ShowS
$cshowList :: [Constr] -> ShowS
show :: Constr -> String
$cshow :: Constr -> String
showsPrec :: Var -> Constr -> ShowS
$cshowsPrec :: Var -> Constr -> ShowS
Show, Constr -> Constr -> Bool
(Constr -> Constr -> Bool)
-> (Constr -> Constr -> Bool) -> Eq Constr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Constr -> Constr -> Bool
$c/= :: Constr -> Constr -> Bool
== :: Constr -> Constr -> Bool
$c== :: Constr -> Constr -> Bool
Eq, Eq Constr
Eq Constr
-> (Constr -> Constr -> Ordering)
-> (Constr -> Constr -> Bool)
-> (Constr -> Constr -> Bool)
-> (Constr -> Constr -> Bool)
-> (Constr -> Constr -> Bool)
-> (Constr -> Constr -> Constr)
-> (Constr -> Constr -> Constr)
-> Ord Constr
Constr -> Constr -> Bool
Constr -> Constr -> Ordering
Constr -> Constr -> Constr
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
min :: Constr -> Constr -> Constr
$cmin :: Constr -> Constr -> Constr
max :: Constr -> Constr -> Constr
$cmax :: Constr -> Constr -> Constr
>= :: Constr -> Constr -> Bool
$c>= :: Constr -> Constr -> Bool
> :: Constr -> Constr -> Bool
$c> :: Constr -> Constr -> Bool
<= :: Constr -> Constr -> Bool
$c<= :: Constr -> Constr -> Bool
< :: Constr -> Constr -> Bool
$c< :: Constr -> Constr -> Bool
compare :: Constr -> Constr -> Ordering
$ccompare :: Constr -> Constr -> Ordering
$cp1Ord :: Eq Constr
Ord)

instance Variables Constr where
  vars :: Constr -> VarSet
vars (IsPos Expr Integer
t) = Expr Integer -> VarSet
forall a. Variables a => a -> VarSet
vars Expr Integer
t
  vars (IsNonneg Expr Integer
t) = Expr Integer -> VarSet
forall a. Variables a => a -> VarSet
vars Expr Integer
t
  vars (IsZero Expr Integer
t) = Expr Integer -> VarSet
forall a. Variables a => a -> VarSet
vars Expr Integer
t

leR, ltR, geR, gtR, eqR :: Rat -> Rat -> Constr
leR :: Rat -> Rat -> Constr
leR (Expr Integer
e1,Integer
c) (Expr Integer
e2,Integer
d) = Expr Integer -> Constr
IsNonneg (Expr Integer -> Constr) -> Expr Integer -> Constr
forall a b. (a -> b) -> a -> b
$ Expr Integer -> Expr Integer
normalizeExpr (Expr Integer -> Expr Integer) -> Expr Integer -> Expr Integer
forall a b. (a -> b) -> a -> b
$ Integer
Scalar (Expr Integer)
c Scalar (Expr Integer) -> Expr Integer -> Expr Integer
forall v. VectorSpace v => Scalar v -> v -> v
*^ Expr Integer
e2 Expr Integer -> Expr Integer -> Expr Integer
forall v. AdditiveGroup v => v -> v -> v
^-^ Integer
Scalar (Expr Integer)
d Scalar (Expr Integer) -> Expr Integer -> Expr Integer
forall v. VectorSpace v => Scalar v -> v -> v
*^ Expr Integer
e1
ltR :: Rat -> Rat -> Constr
ltR (Expr Integer
e1,Integer
c) (Expr Integer
e2,Integer
d) = Expr Integer -> Constr
IsPos (Expr Integer -> Constr) -> Expr Integer -> Constr
forall a b. (a -> b) -> a -> b
$ Expr Integer -> Expr Integer
normalizeExpr (Expr Integer -> Expr Integer) -> Expr Integer -> Expr Integer
forall a b. (a -> b) -> a -> b
$ Integer
Scalar (Expr Integer)
c Scalar (Expr Integer) -> Expr Integer -> Expr Integer
forall v. VectorSpace v => Scalar v -> v -> v
*^ Expr Integer
e2 Expr Integer -> Expr Integer -> Expr Integer
forall v. AdditiveGroup v => v -> v -> v
^-^ Integer
Scalar (Expr Integer)
d Scalar (Expr Integer) -> Expr Integer -> Expr Integer
forall v. VectorSpace v => Scalar v -> v -> v
*^ Expr Integer
e1
geR :: Rat -> Rat -> Constr
geR = (Rat -> Rat -> Constr) -> Rat -> Rat -> Constr
forall a b c. (a -> b -> c) -> b -> a -> c
flip Rat -> Rat -> Constr
leR
gtR :: Rat -> Rat -> Constr
gtR = (Rat -> Rat -> Constr) -> Rat -> Rat -> Constr
forall a b c. (a -> b -> c) -> b -> a -> c
flip Rat -> Rat -> Constr
ltR
eqR :: Rat -> Rat -> Constr
eqR (Expr Integer
e1,Integer
c) (Expr Integer
e2,Integer
d) = Expr Integer -> Constr
IsZero (Expr Integer -> Constr) -> Expr Integer -> Constr
forall a b. (a -> b) -> a -> b
$ Expr Integer -> Expr Integer
normalizeExpr (Expr Integer -> Expr Integer) -> Expr Integer -> Expr Integer
forall a b. (a -> b) -> a -> b
$ Integer
Scalar (Expr Integer)
c Scalar (Expr Integer) -> Expr Integer -> Expr Integer
forall v. VectorSpace v => Scalar v -> v -> v
*^ Expr Integer
e2 Expr Integer -> Expr Integer -> Expr Integer
forall v. AdditiveGroup v => v -> v -> v
^-^ Integer
Scalar (Expr Integer)
d Scalar (Expr Integer) -> Expr Integer -> Expr Integer
forall v. VectorSpace v => Scalar v -> v -> v
*^ Expr Integer
e1

normalizeExpr :: ExprZ -> ExprZ
normalizeExpr :: Expr Integer -> Expr Integer
normalizeExpr Expr Integer
e = (Integer -> Integer) -> Expr Integer -> Expr Integer
forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
LA.mapCoeff (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
d) Expr Integer
e
  where d :: Integer
d = Integer -> Integer
forall a. Num a => a -> a
abs (Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ [Integer] -> Integer
gcd' ([Integer] -> Integer) -> [Integer] -> Integer
forall a b. (a -> b) -> a -> b
$ ((Integer, Var) -> Integer) -> [(Integer, Var)] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map (Integer, Var) -> Integer
forall a b. (a, b) -> a
fst ([(Integer, Var)] -> [Integer]) -> [(Integer, Var)] -> [Integer]
forall a b. (a -> b) -> a -> b
$ Expr Integer -> [(Integer, Var)]
forall r. Expr r -> [(r, Var)]
LA.terms Expr Integer
e

-- "subst1Constr x t c" computes c[t/x]
subst1Constr :: Var -> LA.Expr Rational -> Constr -> Constr
subst1Constr :: Var -> Expr Rational -> Constr -> Constr
subst1Constr Var
x Expr Rational
t Constr
c =
  case Constr
c of
    IsPos Expr Integer
e    -> Expr Integer -> Constr
IsPos (Expr Integer -> Expr Integer
f Expr Integer
e)
    IsNonneg Expr Integer
e -> Expr Integer -> Constr
IsNonneg (Expr Integer -> Expr Integer
f Expr Integer
e)
    IsZero Expr Integer
e   -> Expr Integer -> Constr
IsZero (Expr Integer -> Expr Integer
f Expr Integer
e)
  where
    f :: ExprZ -> ExprZ
    f :: Expr Integer -> Expr Integer
f = Expr Integer -> Expr Integer
normalizeExpr (Expr Integer -> Expr Integer)
-> (Expr Integer -> Expr Integer) -> Expr Integer -> Expr Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rat -> Expr Integer
forall a b. (a, b) -> a
fst (Rat -> Expr Integer)
-> (Expr Integer -> Rat) -> Expr Integer -> Expr Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr Rational -> Rat
toRat (Expr Rational -> Rat)
-> (Expr Integer -> Expr Rational) -> Expr Integer -> Rat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Expr Rational -> Expr Rational -> Expr Rational
forall r. (Num r, Eq r) => Var -> Expr r -> Expr r -> Expr r
LA.applySubst1 Var
x Expr Rational
t (Expr Rational -> Expr Rational)
-> (Expr Integer -> Expr Rational) -> Expr Integer -> Expr Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> Rational) -> Expr Integer -> Expr Rational
forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
LA.mapCoeff Integer -> Rational
forall a. Num a => Integer -> a
fromInteger

-- | Simplify conjunction of 'Constr's.
-- It returns 'Nothing' when a inconsistency is detected.
simplify :: [Constr] -> Maybe [Constr]
simplify :: [Constr] -> Maybe [Constr]
simplify = ([[Constr]] -> [Constr]) -> Maybe [[Constr]] -> Maybe [Constr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[Constr]] -> [Constr]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Maybe [[Constr]] -> Maybe [Constr])
-> ([Constr] -> Maybe [[Constr]]) -> [Constr] -> Maybe [Constr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Constr -> Maybe [Constr]) -> [Constr] -> Maybe [[Constr]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Constr -> Maybe [Constr]
f
  where
    f :: Constr -> Maybe [Constr]
    f :: Constr -> Maybe [Constr]
f c :: Constr
c@(IsPos Expr Integer
e) =
      case Expr Integer -> Maybe Integer
forall r. Num r => Expr r -> Maybe r
LA.asConst Expr Integer
e of
        Just Integer
x -> Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0) Maybe () -> Maybe [Constr] -> Maybe [Constr]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Constr] -> Maybe [Constr]
forall (m :: * -> *) a. Monad m => a -> m a
return []
        Maybe Integer
Nothing -> [Constr] -> Maybe [Constr]
forall (m :: * -> *) a. Monad m => a -> m a
return [Constr
c]
    f c :: Constr
c@(IsNonneg Expr Integer
e) =
      case Expr Integer -> Maybe Integer
forall r. Num r => Expr r -> Maybe r
LA.asConst Expr Integer
e of
        Just Integer
x -> Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0) Maybe () -> Maybe [Constr] -> Maybe [Constr]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Constr] -> Maybe [Constr]
forall (m :: * -> *) a. Monad m => a -> m a
return []
        Maybe Integer
Nothing -> [Constr] -> Maybe [Constr]
forall (m :: * -> *) a. Monad m => a -> m a
return [Constr
c]
    f c :: Constr
c@(IsZero Expr Integer
e) =
      case Expr Integer -> Maybe Integer
forall r. Num r => Expr r -> Maybe r
LA.asConst Expr Integer
e of
        Just Integer
x -> Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0) Maybe () -> Maybe [Constr] -> Maybe [Constr]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Constr] -> Maybe [Constr]
forall (m :: * -> *) a. Monad m => a -> m a
return []
        Maybe Integer
Nothing -> [Constr] -> Maybe [Constr]
forall (m :: * -> *) a. Monad m => a -> m a
return [Constr
c]

instance Eval (Model Rational) Constr Bool where
  eval :: Model Rational -> Constr -> Bool
eval Model Rational
m (IsPos Expr Integer
t)    = Model Rational -> Expr Rational -> Rational
forall m e v. Eval m e v => m -> e -> v
LA.eval Model Rational
m ((Integer -> Rational) -> Expr Integer -> Expr Rational
forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
LA.mapCoeff Integer -> Rational
forall a. Num a => Integer -> a
fromInteger Expr Integer
t :: LA.Expr Rational) Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
0
  eval Model Rational
m (IsNonneg Expr Integer
t) = Model Rational -> Expr Rational -> Rational
forall m e v. Eval m e v => m -> e -> v
LA.eval Model Rational
m ((Integer -> Rational) -> Expr Integer -> Expr Rational
forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
LA.mapCoeff Integer -> Rational
forall a. Num a => Integer -> a
fromInteger Expr Integer
t :: LA.Expr Rational) Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
>= Rational
0
  eval Model Rational
m (IsZero Expr Integer
t)   = Model Rational -> Expr Rational -> Rational
forall m e v. Eval m e v => m -> e -> v
LA.eval Model Rational
m ((Integer -> Rational) -> Expr Integer -> Expr Rational
forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
LA.mapCoeff Integer -> Rational
forall a. Num a => Integer -> a
fromInteger Expr Integer
t :: LA.Expr Rational) Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
0

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

fromLAAtom :: LA.Atom Rational -> DNF Constr
fromLAAtom :: Atom Rational -> DNF Constr
fromLAAtom (OrdRel Expr Rational
a RelOp
op Expr Rational
b) = RelOp -> Rat -> Rat -> DNF Constr
atomR' RelOp
op (Expr Rational -> Rat
toRat Expr Rational
a) (Expr Rational -> Rat
toRat Expr Rational
b)
  where
    atomR' :: RelOp -> Rat -> Rat -> DNF Constr
    atomR' :: RelOp -> Rat -> Rat -> DNF Constr
atomR' RelOp
op Rat
a Rat
b =
      case RelOp
op of
        RelOp
Le -> [[Constr]] -> DNF Constr
forall lit. [[lit]] -> DNF lit
DNF [[Rat
a Rat -> Rat -> Constr
`leR` Rat
b]]
        RelOp
Lt -> [[Constr]] -> DNF Constr
forall lit. [[lit]] -> DNF lit
DNF [[Rat
a Rat -> Rat -> Constr
`ltR` Rat
b]]
        RelOp
Ge -> [[Constr]] -> DNF Constr
forall lit. [[lit]] -> DNF lit
DNF [[Rat
a Rat -> Rat -> Constr
`geR` Rat
b]]
        RelOp
Gt -> [[Constr]] -> DNF Constr
forall lit. [[lit]] -> DNF lit
DNF [[Rat
a Rat -> Rat -> Constr
`gtR` Rat
b]]
        RelOp
Eql -> [[Constr]] -> DNF Constr
forall lit. [[lit]] -> DNF lit
DNF [[Rat
a Rat -> Rat -> Constr
`eqR` Rat
b]]
        RelOp
NEq -> [[Constr]] -> DNF Constr
forall lit. [[lit]] -> DNF lit
DNF [[Rat
a Rat -> Rat -> Constr
`ltR` Rat
b], [Rat
a Rat -> Rat -> Constr
`gtR` Rat
b]]

toLAAtom :: Constr -> LA.Atom Rational
toLAAtom :: Constr -> Atom Rational
toLAAtom (IsNonneg Expr Integer
e) = (Integer -> Rational) -> Expr Integer -> Expr Rational
forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
LA.mapCoeff Integer -> Rational
forall a. Num a => Integer -> a
fromInteger Expr Integer
e Expr Rational -> Expr Rational -> Atom Rational
forall e r. IsOrdRel e r => e -> e -> r
.>=. Rational -> Expr Rational
forall r. (Num r, Eq r) => r -> Expr r
LA.constant Rational
0
toLAAtom (IsPos Expr Integer
e)    = (Integer -> Rational) -> Expr Integer -> Expr Rational
forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
LA.mapCoeff Integer -> Rational
forall a. Num a => Integer -> a
fromInteger Expr Integer
e Expr Rational -> Expr Rational -> Atom Rational
forall e r. IsOrdRel e r => e -> e -> r
.>.  Rational -> Expr Rational
forall r. (Num r, Eq r) => r -> Expr r
LA.constant Rational
0
toLAAtom (IsZero Expr Integer
e)   = (Integer -> Rational) -> Expr Integer -> Expr Rational
forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
LA.mapCoeff Integer -> Rational
forall a. Num a => Integer -> a
fromInteger Expr Integer
e Expr Rational -> Expr Rational -> Atom Rational
forall e r. IsEqRel e r => e -> e -> r
.==. Rational -> Expr Rational
forall r. (Num r, Eq r) => r -> Expr r
LA.constant Rational
0

constraintsToDNF :: [LA.Atom Rational] -> DNF Constr
constraintsToDNF :: [Atom Rational] -> DNF Constr
constraintsToDNF = [DNF Constr] -> DNF Constr
forall a. MonotoneBoolean a => [a] -> a
andB ([DNF Constr] -> DNF Constr)
-> ([Atom Rational] -> [DNF Constr])
-> [Atom Rational]
-> DNF Constr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Atom Rational -> DNF Constr) -> [Atom Rational] -> [DNF Constr]
forall a b. (a -> b) -> [a] -> [b]
map Atom Rational -> DNF Constr
fromLAAtom

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

{-
(ls1,ls2,us1,us2) represents
{ x | ∀(M,c)∈ls1. M/c≤x, ∀(M,c)∈ls2. M/c<x, ∀(M,c)∈us1. x≤M/c, ∀(M,c)∈us2. x<M/c }
-}
type Bounds = ([Rat], [Rat], [Rat], [Rat])

evalBounds :: Model Rational -> Bounds -> Interval Rational
evalBounds :: Model Rational -> Bounds -> Interval Rational
evalBounds Model Rational
model ([Rat]
ls1,[Rat]
ls2,[Rat]
us1,[Rat]
us2) =
  [Interval Rational] -> Interval Rational
forall r. Ord r => [Interval r] -> Interval r
Interval.intersections ([Interval Rational] -> Interval Rational)
-> [Interval Rational] -> Interval Rational
forall a b. (a -> b) -> a -> b
$
    [ Rational -> Extended Rational
forall r. r -> Extended r
Finite (Model Rational -> Rat -> Rational
evalRat Model Rational
model Rat
x) Extended Rational -> Extended Rational -> Interval Rational
forall r. Ord r => Extended r -> Extended r -> Interval r
<=..< Extended Rational
forall r. Extended r
PosInf | Rat
x <- [Rat]
ls1 ] [Interval Rational] -> [Interval Rational] -> [Interval Rational]
forall a. [a] -> [a] -> [a]
++
    [ Rational -> Extended Rational
forall r. r -> Extended r
Finite (Model Rational -> Rat -> Rational
evalRat Model Rational
model Rat
x) Extended Rational -> Extended Rational -> Interval Rational
forall r. Ord r => Extended r -> Extended r -> Interval r
<..<  Extended Rational
forall r. Extended r
PosInf | Rat
x <- [Rat]
ls2 ] [Interval Rational] -> [Interval Rational] -> [Interval Rational]
forall a. [a] -> [a] -> [a]
++
    [ Extended Rational
forall r. Extended r
NegInf Extended Rational -> Extended Rational -> Interval Rational
forall r. Ord r => Extended r -> Extended r -> Interval r
<..<= Rational -> Extended Rational
forall r. r -> Extended r
Finite (Model Rational -> Rat -> Rational
evalRat Model Rational
model Rat
x) | Rat
x <- [Rat]
us1 ] [Interval Rational] -> [Interval Rational] -> [Interval Rational]
forall a. [a] -> [a] -> [a]
++
    [ Extended Rational
forall r. Extended r
NegInf Extended Rational -> Extended Rational -> Interval Rational
forall r. Ord r => Extended r -> Extended r -> Interval r
<..<  Rational -> Extended Rational
forall r. r -> Extended r
Finite (Model Rational -> Rat -> Rational
evalRat Model Rational
model Rat
x) | Rat
x <- [Rat]
us2 ]

boundsToConstrs :: Bounds -> Maybe [Constr]
boundsToConstrs :: Bounds -> Maybe [Constr]
boundsToConstrs  ([Rat]
ls1, [Rat]
ls2, [Rat]
us1, [Rat]
us2) = [Constr] -> Maybe [Constr]
simplify ([Constr] -> Maybe [Constr]) -> [Constr] -> Maybe [Constr]
forall a b. (a -> b) -> a -> b
$
  [ Rat
x Rat -> Rat -> Constr
`leR` Rat
y | Rat
x <- [Rat]
ls1, Rat
y <- [Rat]
us1 ] [Constr] -> [Constr] -> [Constr]
forall a. [a] -> [a] -> [a]
++
  [ Rat
x Rat -> Rat -> Constr
`ltR` Rat
y | Rat
x <- [Rat]
ls1, Rat
y <- [Rat]
us2 ] [Constr] -> [Constr] -> [Constr]
forall a. [a] -> [a] -> [a]
++
  [ Rat
x Rat -> Rat -> Constr
`ltR` Rat
y | Rat
x <- [Rat]
ls2, Rat
y <- [Rat]
us1 ] [Constr] -> [Constr] -> [Constr]
forall a. [a] -> [a] -> [a]
++
  [ Rat
x Rat -> Rat -> Constr
`ltR` Rat
y | Rat
x <- [Rat]
ls2, Rat
y <- [Rat]
us2 ]

collectBounds :: Var -> [Constr] -> (Bounds, [Constr])
collectBounds :: Var -> [Constr] -> (Bounds, [Constr])
collectBounds Var
v = (Constr -> (Bounds, [Constr]) -> (Bounds, [Constr]))
-> (Bounds, [Constr]) -> [Constr] -> (Bounds, [Constr])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Constr -> (Bounds, [Constr]) -> (Bounds, [Constr])
phi (([],[],[],[]),[])
  where
    phi :: Constr -> (Bounds, [Constr]) -> (Bounds, [Constr])
    phi :: Constr -> (Bounds, [Constr]) -> (Bounds, [Constr])
phi constr :: Constr
constr@(IsNonneg Expr Integer
t) (Bounds, [Constr])
x = Bool
-> Constr
-> Expr Integer
-> (Bounds, [Constr])
-> (Bounds, [Constr])
f Bool
False Constr
constr Expr Integer
t (Bounds, [Constr])
x
    phi constr :: Constr
constr@(IsPos Expr Integer
t) (Bounds, [Constr])
x = Bool
-> Constr
-> Expr Integer
-> (Bounds, [Constr])
-> (Bounds, [Constr])
f Bool
True Constr
constr Expr Integer
t (Bounds, [Constr])
x
    phi constr :: Constr
constr@(IsZero Expr Integer
t) (bnd :: Bounds
bnd@([Rat]
ls1,[Rat]
ls2,[Rat]
us1,[Rat]
us2), [Constr]
xs) =
      case Var -> Expr Integer -> Maybe (Integer, Expr Integer)
forall r. Num r => Var -> Expr r -> Maybe (r, Expr r)
LA.extractMaybe Var
v Expr Integer
t of
        Maybe (Integer, Expr Integer)
Nothing -> (Bounds
bnd, Constr
constr Constr -> [Constr] -> [Constr]
forall a. a -> [a] -> [a]
: [Constr]
xs)
        Just (Integer
c,Expr Integer
t') -> ((Rat
t'' Rat -> [Rat] -> [Rat]
forall a. a -> [a] -> [a]
: [Rat]
ls1, [Rat]
ls2, Rat
t'' Rat -> [Rat] -> [Rat]
forall a. a -> [a] -> [a]
: [Rat]
us1, [Rat]
us2), [Constr]
xs)
          where
            t'' :: Rat
t'' = (Integer -> Integer
forall a. Num a => a -> a
signum Integer
c Scalar (Expr Integer) -> Expr Integer -> Expr Integer
forall v. VectorSpace v => Scalar v -> v -> v
*^ Expr Integer -> Expr Integer
forall v. AdditiveGroup v => v -> v
negateV Expr Integer
t', Integer -> Integer
forall a. Num a => a -> a
abs Integer
c)

    f :: Bool -> Constr -> ExprZ -> (Bounds, [Constr]) -> (Bounds, [Constr])
    f :: Bool
-> Constr
-> Expr Integer
-> (Bounds, [Constr])
-> (Bounds, [Constr])
f Bool
strict Constr
constr Expr Integer
t (bnd :: Bounds
bnd@([Rat]
ls1,[Rat]
ls2,[Rat]
us1,[Rat]
us2), [Constr]
xs) =
      case Var -> Expr Integer -> (Integer, Expr Integer)
forall r. Num r => Var -> Expr r -> (r, Expr r)
LA.extract Var
v Expr Integer
t of
        (Integer
c,Expr Integer
t') ->
          case Integer
c Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Integer
0 of
            Ordering
EQ -> (Bounds
bnd, Constr
constr Constr -> [Constr] -> [Constr]
forall a. a -> [a] -> [a]
: [Constr]
xs)
            Ordering
GT ->
              if Bool
strict
              then (([Rat]
ls1, (Expr Integer -> Expr Integer
forall v. AdditiveGroup v => v -> v
negateV Expr Integer
t', Integer
c) Rat -> [Rat] -> [Rat]
forall a. a -> [a] -> [a]
: [Rat]
ls2, [Rat]
us1, [Rat]
us2), [Constr]
xs) -- 0 < cx + M ⇔ -M/c <  x
              else (((Expr Integer -> Expr Integer
forall v. AdditiveGroup v => v -> v
negateV Expr Integer
t', Integer
c) Rat -> [Rat] -> [Rat]
forall a. a -> [a] -> [a]
: [Rat]
ls1, [Rat]
ls2, [Rat]
us1, [Rat]
us2), [Constr]
xs) -- 0 ≤ cx + M ⇔ -M/c ≤ x
            Ordering
LT ->
              if Bool
strict
              then (([Rat]
ls1, [Rat]
ls2, [Rat]
us1, (Expr Integer
t', Integer -> Integer
forall a. Num a => a -> a
negate Integer
c) Rat -> [Rat] -> [Rat]
forall a. a -> [a] -> [a]
: [Rat]
us2), [Constr]
xs) -- 0 < cx + M ⇔ x < M/-c
              else (([Rat]
ls1, [Rat]
ls2, (Expr Integer
t', Integer -> Integer
forall a. Num a => a -> a
negate Integer
c) Rat -> [Rat] -> [Rat]
forall a. a -> [a] -> [a]
: [Rat]
us1, [Rat]
us2), [Constr]
xs) -- 0 ≤ cx + M ⇔ x ≤ M/-c

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

{-| @'project' x φ@ returns @[(ψ_1, lift_1), …, (ψ_m, lift_m)]@ such that:

* @⊢_LRA ∀y1, …, yn. (∃x. φ) ↔ (ψ_1 ∨ … ∨ φ_m)@ where @{y1, …, yn} = FV(φ) \\ {x}@, and

* if @M ⊧_LRA ψ_i@ then @lift_i M ⊧_LRA φ@.
-}
project :: Var -> [LA.Atom Rational] -> [([LA.Atom Rational], Model Rational -> Model Rational)]
project :: Var
-> [Atom Rational]
-> [([Atom Rational], Model Rational -> Model Rational)]
project Var
v [Atom Rational]
xs = do
  [Constr]
ys <- DNF Constr -> [[Constr]]
forall lit. DNF lit -> [[lit]]
unDNF (DNF Constr -> [[Constr]]) -> DNF Constr -> [[Constr]]
forall a b. (a -> b) -> a -> b
$ [Atom Rational] -> DNF Constr
constraintsToDNF [Atom Rational]
xs
  ([Constr]
zs, Model Rational -> Model Rational
mt) <- Maybe ([Constr], Model Rational -> Model Rational)
-> [([Constr], Model Rational -> Model Rational)]
forall a. Maybe a -> [a]
maybeToList (Maybe ([Constr], Model Rational -> Model Rational)
 -> [([Constr], Model Rational -> Model Rational)])
-> Maybe ([Constr], Model Rational -> Model Rational)
-> [([Constr], Model Rational -> Model Rational)]
forall a b. (a -> b) -> a -> b
$ Var
-> [Constr] -> Maybe ([Constr], Model Rational -> Model Rational)
project' Var
v [Constr]
ys
  ([Atom Rational], Model Rational -> Model Rational)
-> [([Atom Rational], Model Rational -> Model Rational)]
forall (m :: * -> *) a. Monad m => a -> m a
return ((Constr -> Atom Rational) -> [Constr] -> [Atom Rational]
forall a b. (a -> b) -> [a] -> [b]
map Constr -> Atom Rational
toLAAtom [Constr]
zs, Model Rational -> Model Rational
mt)

project' :: Var -> [Constr] -> Maybe ([Constr], Model Rational -> Model Rational)
project' :: Var
-> [Constr] -> Maybe ([Constr], Model Rational -> Model Rational)
project' Var
v [Constr]
cs = VarSet
-> [Constr] -> Maybe ([Constr], Model Rational -> Model Rational)
projectN' (Var -> VarSet
IS.singleton Var
v) [Constr]
cs

{-| @'projectN' {x1,…,xm} φ@ returns @[(ψ_1, lift_1), …, (ψ_n, lift_n)]@ such that:

* @⊢_LRA ∀y1, …, yp. (∃x. φ) ↔ (ψ_1 ∨ … ∨ φ_n)@ where @{y1, …, yp} = FV(φ) \\ {x1,…,xm}@, and

* if @M ⊧_LRA ψ_i@ then @lift_i M ⊧_LRA φ@.
-}
projectN :: VarSet -> [LA.Atom Rational] -> [([LA.Atom Rational], Model Rational -> Model Rational)]
projectN :: VarSet
-> [Atom Rational]
-> [([Atom Rational], Model Rational -> Model Rational)]
projectN VarSet
vs [Atom Rational]
xs = do
  [Constr]
ys <- DNF Constr -> [[Constr]]
forall lit. DNF lit -> [[lit]]
unDNF (DNF Constr -> [[Constr]]) -> DNF Constr -> [[Constr]]
forall a b. (a -> b) -> a -> b
$ [Atom Rational] -> DNF Constr
constraintsToDNF [Atom Rational]
xs
  ([Constr]
zs, Model Rational -> Model Rational
mt) <- Maybe ([Constr], Model Rational -> Model Rational)
-> [([Constr], Model Rational -> Model Rational)]
forall a. Maybe a -> [a]
maybeToList (Maybe ([Constr], Model Rational -> Model Rational)
 -> [([Constr], Model Rational -> Model Rational)])
-> Maybe ([Constr], Model Rational -> Model Rational)
-> [([Constr], Model Rational -> Model Rational)]
forall a b. (a -> b) -> a -> b
$ VarSet
-> [Constr] -> Maybe ([Constr], Model Rational -> Model Rational)
projectN' VarSet
vs [Constr]
ys
  ([Atom Rational], Model Rational -> Model Rational)
-> [([Atom Rational], Model Rational -> Model Rational)]
forall (m :: * -> *) a. Monad m => a -> m a
return ((Constr -> Atom Rational) -> [Constr] -> [Atom Rational]
forall a b. (a -> b) -> [a] -> [b]
map Constr -> Atom Rational
toLAAtom [Constr]
zs, Model Rational -> Model Rational
mt)

projectN' :: VarSet -> [Constr] -> Maybe ([Constr], Model Rational -> Model Rational)
projectN' :: VarSet
-> [Constr] -> Maybe ([Constr], Model Rational -> Model Rational)
projectN' = VarSet
-> [Constr] -> Maybe ([Constr], Model Rational -> Model Rational)
f
  where
    f :: VarSet
-> [Constr] -> Maybe ([Constr], Model Rational -> Model Rational)
f VarSet
vs [Constr]
xs
      | VarSet -> Bool
IS.null VarSet
vs = ([Constr], Model Rational -> Model Rational)
-> Maybe ([Constr], Model Rational -> Model Rational)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Constr]
xs, Model Rational -> Model Rational
forall a. a -> a
id)
      | Just (Var
v,Rat
vdef,[Constr]
ys) <- VarSet -> [Constr] -> Maybe (Var, Rat, [Constr])
findEq VarSet
vs [Constr]
xs = do
          let mt1 :: Model Rational -> Model Rational
mt1 Model Rational
m = Var -> Rational -> Model Rational -> Model Rational
forall a. Var -> a -> IntMap a -> IntMap a
IM.insert Var
v (Model Rational -> Rat -> Rational
evalRat Model Rational
m Rat
vdef) Model Rational
m
          ([Constr]
zs, Model Rational -> Model Rational
mt2) <- VarSet
-> [Constr] -> Maybe ([Constr], Model Rational -> Model Rational)
f (Var -> VarSet -> VarSet
IS.delete Var
v VarSet
vs) [Var -> Expr Rational -> Constr -> Constr
subst1Constr Var
v (Rat -> Expr Rational
fromRat Rat
vdef) Constr
c | Constr
c <- [Constr]
ys]
          ([Constr], Model Rational -> Model Rational)
-> Maybe ([Constr], Model Rational -> Model Rational)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Constr]
zs, Model Rational -> Model Rational
mt1 (Model Rational -> Model Rational)
-> (Model Rational -> Model Rational)
-> Model Rational
-> Model Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Model Rational -> Model Rational
mt2)
      | Bool
otherwise =
          case VarSet -> Maybe (Var, VarSet)
IS.minView VarSet
vs of
            Maybe (Var, VarSet)
Nothing -> ([Constr], Model Rational -> Model Rational)
-> Maybe ([Constr], Model Rational -> Model Rational)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Constr]
xs, Model Rational -> Model Rational
forall a. a -> a
id) -- should not happen
            Just (Var
v,VarSet
vs') ->
              case Var -> [Constr] -> (Bounds, [Constr])
collectBounds Var
v [Constr]
xs of
                (Bounds
bnd, [Constr]
rest) -> do
                  [Constr]
cond <- Bounds -> Maybe [Constr]
boundsToConstrs Bounds
bnd
                  let mt1 :: Model Rational -> Model Rational
mt1 Model Rational
m =
                       case Interval Rational -> Maybe Rational
forall r. RealFrac r => Interval r -> Maybe Rational
Interval.simplestRationalWithin (Model Rational -> Bounds -> Interval Rational
evalBounds Model Rational
m Bounds
bnd) of
                         Maybe Rational
Nothing  -> String -> Model Rational
forall a. HasCallStack => String -> a
error String
"ToySolver.FourierMotzkin.project': should not happen"
                         Just Rational
val -> Var -> Rational -> Model Rational -> Model Rational
forall a. Var -> a -> IntMap a -> IntMap a
IM.insert Var
v Rational
val Model Rational
m
                  ([Constr]
ys, Model Rational -> Model Rational
mt2) <- VarSet
-> [Constr] -> Maybe ([Constr], Model Rational -> Model Rational)
f VarSet
vs' ([Constr]
rest [Constr] -> [Constr] -> [Constr]
forall a. [a] -> [a] -> [a]
++ [Constr]
cond)
                  ([Constr], Model Rational -> Model Rational)
-> Maybe ([Constr], Model Rational -> Model Rational)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Constr]
ys, Model Rational -> Model Rational
mt1 (Model Rational -> Model Rational)
-> (Model Rational -> Model Rational)
-> Model Rational
-> Model Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Model Rational -> Model Rational
mt2)

findEq :: VarSet -> [Constr] -> Maybe (Var, Rat, [Constr])
findEq :: VarSet -> [Constr] -> Maybe (Var, Rat, [Constr])
findEq VarSet
vs = [Maybe (Var, Rat, [Constr])] -> Maybe (Var, Rat, [Constr])
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([Maybe (Var, Rat, [Constr])] -> Maybe (Var, Rat, [Constr]))
-> ([Constr] -> [Maybe (Var, Rat, [Constr])])
-> [Constr]
-> Maybe (Var, Rat, [Constr])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Constr, [Constr]) -> Maybe (Var, Rat, [Constr]))
-> [(Constr, [Constr])] -> [Maybe (Var, Rat, [Constr])]
forall a b. (a -> b) -> [a] -> [b]
map (Constr, [Constr]) -> Maybe (Var, Rat, [Constr])
f ([(Constr, [Constr])] -> [Maybe (Var, Rat, [Constr])])
-> ([Constr] -> [(Constr, [Constr])])
-> [Constr]
-> [Maybe (Var, Rat, [Constr])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Constr] -> [(Constr, [Constr])]
forall a. [a] -> [(a, [a])]
pickup
  where
    pickup :: [a] -> [(a,[a])]
    pickup :: [a] -> [(a, [a])]
pickup [] = []
    pickup (a
x:[a]
xs) = (a
x,[a]
xs) (a, [a]) -> [(a, [a])] -> [(a, [a])]
forall a. a -> [a] -> [a]
: [(a
y,a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
ys) | (a
y,[a]
ys) <- [a] -> [(a, [a])]
forall a. [a] -> [(a, [a])]
pickup [a]
xs]

    f :: (Constr, [Constr]) -> Maybe (Var, Rat, [Constr])
    f :: (Constr, [Constr]) -> Maybe (Var, Rat, [Constr])
f (IsZero Expr Integer
e, [Constr]
cs) = do
      let vs2 :: VarSet
vs2 = VarSet -> VarSet -> VarSet
IS.intersection VarSet
vs (Expr Integer -> VarSet
forall a. Variables a => a -> VarSet
vars Expr Integer
e)
      Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ VarSet -> Bool
IS.null VarSet
vs2
      let v :: Var
v = VarSet -> Var
IS.findMin VarSet
vs2
          (Integer
c, Expr Integer
e') = Var -> Expr Integer -> (Integer, Expr Integer)
forall r. Num r => Var -> Expr r -> (r, Expr r)
LA.extract Var
v Expr Integer
e
      (Var, Rat, [Constr]) -> Maybe (Var, Rat, [Constr])
forall (m :: * -> *) a. Monad m => a -> m a
return (Var
v, (Expr Integer -> Expr Integer
forall v. AdditiveGroup v => v -> v
negateV Expr Integer
e', Integer
c), [Constr]
cs)
    f (Constr, [Constr])
_ = Maybe (Var, Rat, [Constr])
forall a. Maybe a
Nothing

-- | @'solve' {x1,…,xn} φ@ returns @Just M@ that @M ⊧_LRA φ@ when
-- such @M@ exists, returns @Nothing@ otherwise.
--
-- @FV(φ)@ must be a subset of @{x1,…,xn}@.
--
solve :: VarSet -> [LA.Atom Rational] -> Maybe (Model Rational)
solve :: VarSet -> [Atom Rational] -> Maybe (Model Rational)
solve VarSet
vs [Atom Rational]
cs = [Maybe (Model Rational)] -> Maybe (Model Rational)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [VarSet -> [Constr] -> Maybe (Model Rational)
solve' VarSet
vs [Constr]
cs2 | [Constr]
cs2 <- DNF Constr -> [[Constr]]
forall lit. DNF lit -> [[lit]]
unDNF ([Atom Rational] -> DNF Constr
constraintsToDNF [Atom Rational]
cs)]

solve' :: VarSet -> [Constr] -> Maybe (Model Rational)
solve' :: VarSet -> [Constr] -> Maybe (Model Rational)
solve' VarSet
vs [Constr]
cs = do
  ([Constr]
cs2,Model Rational -> Model Rational
mt) <- VarSet
-> [Constr] -> Maybe ([Constr], Model Rational -> Model Rational)
projectN' VarSet
vs ([Constr] -> Maybe ([Constr], Model Rational -> Model Rational))
-> Maybe [Constr]
-> Maybe ([Constr], Model Rational -> Model Rational)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Constr] -> Maybe [Constr]
simplify [Constr]
cs
  let m :: Model Rational
      m :: Model Rational
m = Model Rational
forall a. IntMap a
IM.empty
  Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ (Constr -> Bool) -> [Constr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Model Rational -> Constr -> Bool
forall m e v. Eval m e v => m -> e -> v
eval Model Rational
m) [Constr]
cs2
  Model Rational -> Maybe (Model Rational)
forall (m :: * -> *) a. Monad m => a -> m a
return (Model Rational -> Maybe (Model Rational))
-> Model Rational -> Maybe (Model Rational)
forall a b. (a -> b) -> a -> b
$ Model Rational -> Model Rational
mt Model Rational
m

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

gcd' :: [Integer] -> Integer
gcd' :: [Integer] -> Integer
gcd' [] = Integer
1
gcd' [Integer]
xs = (Integer -> Integer -> Integer) -> [Integer] -> Integer
forall a. (a -> a -> a) -> [a] -> a
foldl1' Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
gcd [Integer]
xs

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