{-# 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
forall a b. a -> b -> b
seq Integer
m (Rat -> Rat) -> Rat -> Rat
forall a b. (a -> b) -> a -> b
$ ((Rational -> Integer) -> Expr Rational -> ExprZ
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 b a. (b -> a -> b) -> b -> [a] -> b
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 (ExprZ
e,Integer
c) = (Integer -> Rational) -> ExprZ -> 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) ExprZ
e

evalRat :: Model Rational -> Rat -> Rational
evalRat :: Model Rational -> Rat -> Rational
evalRat Model Rational
model (ExprZ
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) -> ExprZ -> 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 ExprZ
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
$cshowsPrec :: Var -> Constr -> ShowS
showsPrec :: Var -> Constr -> ShowS
$cshow :: Constr -> String
show :: Constr -> String
$cshowList :: [Constr] -> ShowS
showList :: [Constr] -> ShowS
Show, Constr -> Constr -> Bool
(Constr -> Constr -> Bool)
-> (Constr -> Constr -> Bool) -> Eq Constr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Constr -> Constr -> Bool
== :: Constr -> Constr -> Bool
$c/= :: Constr -> Constr -> Bool
/= :: 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
$ccompare :: Constr -> Constr -> Ordering
compare :: Constr -> Constr -> Ordering
$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
>= :: Constr -> Constr -> Bool
$cmax :: Constr -> Constr -> Constr
max :: Constr -> Constr -> Constr
$cmin :: Constr -> Constr -> Constr
min :: Constr -> Constr -> Constr
Ord)

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

leR, ltR, geR, gtR, eqR :: Rat -> Rat -> Constr
leR :: Rat -> Rat -> Constr
leR (ExprZ
e1,Integer
c) (ExprZ
e2,Integer
d) = ExprZ -> Constr
IsNonneg (ExprZ -> Constr) -> ExprZ -> Constr
forall a b. (a -> b) -> a -> b
$ ExprZ -> ExprZ
normalizeExpr (ExprZ -> ExprZ) -> ExprZ -> ExprZ
forall a b. (a -> b) -> a -> b
$ Integer
Scalar ExprZ
c Scalar ExprZ -> ExprZ -> ExprZ
forall v. VectorSpace v => Scalar v -> v -> v
*^ ExprZ
e2 ExprZ -> ExprZ -> ExprZ
forall v. AdditiveGroup v => v -> v -> v
^-^ Integer
Scalar ExprZ
d Scalar ExprZ -> ExprZ -> ExprZ
forall v. VectorSpace v => Scalar v -> v -> v
*^ ExprZ
e1
ltR :: Rat -> Rat -> Constr
ltR (ExprZ
e1,Integer
c) (ExprZ
e2,Integer
d) = ExprZ -> Constr
IsPos (ExprZ -> Constr) -> ExprZ -> Constr
forall a b. (a -> b) -> a -> b
$ ExprZ -> ExprZ
normalizeExpr (ExprZ -> ExprZ) -> ExprZ -> ExprZ
forall a b. (a -> b) -> a -> b
$ Integer
Scalar ExprZ
c Scalar ExprZ -> ExprZ -> ExprZ
forall v. VectorSpace v => Scalar v -> v -> v
*^ ExprZ
e2 ExprZ -> ExprZ -> ExprZ
forall v. AdditiveGroup v => v -> v -> v
^-^ Integer
Scalar ExprZ
d Scalar ExprZ -> ExprZ -> ExprZ
forall v. VectorSpace v => Scalar v -> v -> v
*^ ExprZ
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 (ExprZ
e1,Integer
c) (ExprZ
e2,Integer
d) = ExprZ -> Constr
IsZero (ExprZ -> Constr) -> ExprZ -> Constr
forall a b. (a -> b) -> a -> b
$ ExprZ -> ExprZ
normalizeExpr (ExprZ -> ExprZ) -> ExprZ -> ExprZ
forall a b. (a -> b) -> a -> b
$ Integer
Scalar ExprZ
c Scalar ExprZ -> ExprZ -> ExprZ
forall v. VectorSpace v => Scalar v -> v -> v
*^ ExprZ
e2 ExprZ -> ExprZ -> ExprZ
forall v. AdditiveGroup v => v -> v -> v
^-^ Integer
Scalar ExprZ
d Scalar ExprZ -> ExprZ -> ExprZ
forall v. VectorSpace v => Scalar v -> v -> v
*^ ExprZ
e1

normalizeExpr :: ExprZ -> ExprZ
normalizeExpr :: ExprZ -> ExprZ
normalizeExpr ExprZ
e = (Integer -> Integer) -> ExprZ -> ExprZ
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) ExprZ
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
$ ExprZ -> [(Integer, Var)]
forall r. Expr r -> [(r, Var)]
LA.terms ExprZ
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 ExprZ
e    -> ExprZ -> Constr
IsPos (ExprZ -> ExprZ
f ExprZ
e)
    IsNonneg ExprZ
e -> ExprZ -> Constr
IsNonneg (ExprZ -> ExprZ
f ExprZ
e)
    IsZero ExprZ
e   -> ExprZ -> Constr
IsZero (ExprZ -> ExprZ
f ExprZ
e)
  where
    f :: ExprZ -> ExprZ
    f :: ExprZ -> ExprZ
f = ExprZ -> ExprZ
normalizeExpr (ExprZ -> ExprZ) -> (ExprZ -> ExprZ) -> ExprZ -> ExprZ
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rat -> ExprZ
forall a b. (a, b) -> a
fst (Rat -> ExprZ) -> (ExprZ -> Rat) -> ExprZ -> ExprZ
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr Rational -> Rat
toRat (Expr Rational -> Rat) -> (ExprZ -> Expr Rational) -> ExprZ -> 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)
-> (ExprZ -> Expr Rational) -> ExprZ -> Expr Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> Rational) -> ExprZ -> 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 a b. (a -> b) -> Maybe a -> Maybe b
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Constr -> Maybe [Constr]
f
  where
    f :: Constr -> Maybe [Constr]
    f :: Constr -> Maybe [Constr]
f c :: Constr
c@(IsPos ExprZ
e) =
      case ExprZ -> Maybe Integer
forall r. Num r => Expr r -> Maybe r
LA.asConst ExprZ
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 a b. Maybe a -> Maybe b -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Constr] -> Maybe [Constr]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return []
        Maybe Integer
Nothing -> [Constr] -> Maybe [Constr]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return [Constr
c]
    f c :: Constr
c@(IsNonneg ExprZ
e) =
      case ExprZ -> Maybe Integer
forall r. Num r => Expr r -> Maybe r
LA.asConst ExprZ
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 a b. Maybe a -> Maybe b -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Constr] -> Maybe [Constr]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return []
        Maybe Integer
Nothing -> [Constr] -> Maybe [Constr]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return [Constr
c]
    f c :: Constr
c@(IsZero ExprZ
e) =
      case ExprZ -> Maybe Integer
forall r. Num r => Expr r -> Maybe r
LA.asConst ExprZ
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 a b. Maybe a -> Maybe b -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Constr] -> Maybe [Constr]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return []
        Maybe Integer
Nothing -> [Constr] -> Maybe [Constr]
forall a. a -> Maybe a
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 ExprZ
t)    = Model Rational -> Expr Rational -> Rational
forall m e v. Eval m e v => m -> e -> v
LA.eval Model Rational
m ((Integer -> Rational) -> ExprZ -> 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 ExprZ
t :: LA.Expr Rational) Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
0
  eval Model Rational
m (IsNonneg ExprZ
t) = Model Rational -> Expr Rational -> Rational
forall m e v. Eval m e v => m -> e -> v
LA.eval Model Rational
m ((Integer -> Rational) -> ExprZ -> 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 ExprZ
t :: LA.Expr Rational) Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
>= Rational
0
  eval Model Rational
m (IsZero ExprZ
t)   = Model Rational -> Expr Rational -> Rational
forall m e v. Eval m e v => m -> e -> v
LA.eval Model Rational
m ((Integer -> Rational) -> ExprZ -> 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 ExprZ
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 ExprZ
e) = (Integer -> Rational) -> ExprZ -> 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 ExprZ
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 ExprZ
e)    = (Integer -> Rational) -> ExprZ -> 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 ExprZ
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 ExprZ
e)   = (Integer -> Rational) -> ExprZ -> 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 ExprZ
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 a b. (a -> b -> b) -> b -> [a] -> b
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 ExprZ
t) (Bounds, [Constr])
x = Bool -> Constr -> ExprZ -> (Bounds, [Constr]) -> (Bounds, [Constr])
f Bool
False Constr
constr ExprZ
t (Bounds, [Constr])
x
    phi constr :: Constr
constr@(IsPos ExprZ
t) (Bounds, [Constr])
x = Bool -> Constr -> ExprZ -> (Bounds, [Constr]) -> (Bounds, [Constr])
f Bool
True Constr
constr ExprZ
t (Bounds, [Constr])
x
    phi constr :: Constr
constr@(IsZero ExprZ
t) (bnd :: Bounds
bnd@([Rat]
ls1,[Rat]
ls2,[Rat]
us1,[Rat]
us2), [Constr]
xs) =
      case Var -> ExprZ -> Maybe (Integer, ExprZ)
forall r. Num r => Var -> Expr r -> Maybe (r, Expr r)
LA.extractMaybe Var
v ExprZ
t of
        Maybe (Integer, ExprZ)
Nothing -> (Bounds
bnd, Constr
constr Constr -> [Constr] -> [Constr]
forall a. a -> [a] -> [a]
: [Constr]
xs)
        Just (Integer
c,ExprZ
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 ExprZ -> ExprZ -> ExprZ
forall v. VectorSpace v => Scalar v -> v -> v
*^ ExprZ -> ExprZ
forall v. AdditiveGroup v => v -> v
negateV ExprZ
t', Integer -> Integer
forall a. Num a => a -> a
abs Integer
c)

    f :: Bool -> Constr -> ExprZ -> (Bounds, [Constr]) -> (Bounds, [Constr])
    f :: Bool -> Constr -> ExprZ -> (Bounds, [Constr]) -> (Bounds, [Constr])
f Bool
strict Constr
constr ExprZ
t (bnd :: Bounds
bnd@([Rat]
ls1,[Rat]
ls2,[Rat]
us1,[Rat]
us2), [Constr]
xs) =
      case Var -> ExprZ -> (Integer, ExprZ)
forall r. Num r => Var -> Expr r -> (r, Expr r)
LA.extract Var
v ExprZ
t of
        (Integer
c,ExprZ
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, (ExprZ -> ExprZ
forall v. AdditiveGroup v => v -> v
negateV ExprZ
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 (((ExprZ -> ExprZ
forall v. AdditiveGroup v => v -> v
negateV ExprZ
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, (ExprZ
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, (ExprZ
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 a. a -> [a]
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 a. a -> [a]
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 a. a -> Maybe a
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 a. a -> Maybe a
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 a. a -> Maybe a
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 a. a -> Maybe a
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 :: forall a. [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 ExprZ
e, [Constr]
cs) = do
      let vs2 :: VarSet
vs2 = VarSet -> VarSet -> VarSet
IS.intersection VarSet
vs (ExprZ -> VarSet
forall a. Variables a => a -> VarSet
vars ExprZ
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, ExprZ
e') = Var -> ExprZ -> (Integer, ExprZ)
forall r. Num r => Var -> Expr r -> (r, Expr r)
LA.extract Var
v ExprZ
e
      (Var, Rat, [Constr]) -> Maybe (Var, Rat, [Constr])
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Var
v, (ExprZ -> ExprZ
forall v. AdditiveGroup v => v -> v
negateV ExprZ
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 a. a -> Maybe a
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. HasCallStack => (a -> a -> a) -> [a] -> a
foldl1' Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
gcd [Integer]
xs

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