{-# 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 = seq :: forall a b. a -> b -> b
seq Integer
m forall a b. (a -> b) -> a -> b
$ (forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
LA.mapCoeff forall {a}. Integral a => Ratio a -> a
f Expr Rational
e, Integer
m)
  where
    f :: Ratio a -> a
f Ratio a
x = forall a. Ratio a -> a
numerator (forall a. Num a => Integer -> a
fromInteger Integer
m forall a. Num a => a -> a -> a
* Ratio a
x)
    m :: Integer
m = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall a. Integral a => a -> a -> a
lcm Integer
1 [forall a. Ratio a -> a
denominator Rational
c | (Rational
c,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) = forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
LA.mapCoeff (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) = forall x. VectorSpace x => x -> (Var -> x) -> Expr (Scalar x) -> x
LA.lift1 Rational
1 (Model Rational
model forall a. IntMap a -> Var -> a
IM.!) (forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
LA.mapCoeff forall a b. (Integral a, Num b) => a -> b
fromIntegral ExprZ
e) forall a. Fractional a => a -> a -> a
/ (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
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
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
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
Ord)

instance Variables Constr where
  vars :: Constr -> VarSet
vars (IsPos ExprZ
t) = forall a. Variables a => a -> VarSet
vars ExprZ
t
  vars (IsNonneg ExprZ
t) = forall a. Variables a => a -> VarSet
vars ExprZ
t
  vars (IsZero ExprZ
t) = 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 forall a b. (a -> b) -> a -> b
$ ExprZ -> ExprZ
normalizeExpr forall a b. (a -> b) -> a -> b
$ Integer
c forall v. VectorSpace v => Scalar v -> v -> v
*^ ExprZ
e2 forall v. AdditiveGroup v => v -> v -> v
^-^ Integer
d 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 forall a b. (a -> b) -> a -> b
$ ExprZ -> ExprZ
normalizeExpr forall a b. (a -> b) -> a -> b
$ Integer
c forall v. VectorSpace v => Scalar v -> v -> v
*^ ExprZ
e2 forall v. AdditiveGroup v => v -> v -> v
^-^ Integer
d forall v. VectorSpace v => Scalar v -> v -> v
*^ ExprZ
e1
geR :: Rat -> Rat -> Constr
geR = forall a b c. (a -> b -> c) -> b -> a -> c
flip Rat -> Rat -> Constr
leR
gtR :: Rat -> Rat -> Constr
gtR = 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 forall a b. (a -> b) -> a -> b
$ ExprZ -> ExprZ
normalizeExpr forall a b. (a -> b) -> a -> b
$ Integer
c forall v. VectorSpace v => Scalar v -> v -> v
*^ ExprZ
e2 forall v. AdditiveGroup v => v -> v -> v
^-^ Integer
d forall v. VectorSpace v => Scalar v -> v -> v
*^ ExprZ
e1

normalizeExpr :: ExprZ -> ExprZ
normalizeExpr :: ExprZ -> ExprZ
normalizeExpr ExprZ
e = forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
LA.mapCoeff (forall a. Integral a => a -> a -> a
`div` Integer
d) ExprZ
e
  where d :: Integer
d = forall a. Num a => a -> a
abs forall a b. (a -> b) -> a -> b
$ [Integer] -> Integer
gcd' forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr Rational -> Rat
toRat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. (Num r, Eq r) => Var -> Expr r -> Expr r -> Expr r
LA.applySubst1 Var
x Expr Rational
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
LA.mapCoeff 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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 ExprZ
e) =
      case forall r. Num r => Expr r -> Maybe r
LA.asConst ExprZ
e of
        Just Integer
x -> forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
x forall a. Ord a => a -> a -> Bool
> Integer
0) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return []
        Maybe Integer
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return [Constr
c]
    f c :: Constr
c@(IsNonneg ExprZ
e) =
      case forall r. Num r => Expr r -> Maybe r
LA.asConst ExprZ
e of
        Just Integer
x -> forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
x forall a. Ord a => a -> a -> Bool
>= Integer
0) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return []
        Maybe Integer
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return [Constr
c]
    f c :: Constr
c@(IsZero ExprZ
e) =
      case forall r. Num r => Expr r -> Maybe r
LA.asConst ExprZ
e of
        Just Integer
x -> forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
x forall a. Eq a => a -> a -> Bool
== Integer
0) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return []
        Maybe Integer
Nothing -> 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)    = forall m e v. Eval m e v => m -> e -> v
LA.eval Model Rational
m (forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
LA.mapCoeff forall a. Num a => Integer -> a
fromInteger ExprZ
t :: LA.Expr Rational) forall a. Ord a => a -> a -> Bool
> Rational
0
  eval Model Rational
m (IsNonneg ExprZ
t) = forall m e v. Eval m e v => m -> e -> v
LA.eval Model Rational
m (forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
LA.mapCoeff forall a. Num a => Integer -> a
fromInteger ExprZ
t :: LA.Expr Rational) forall a. Ord a => a -> a -> Bool
>= Rational
0
  eval Model Rational
m (IsZero ExprZ
t)   = forall m e v. Eval m e v => m -> e -> v
LA.eval Model Rational
m (forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
LA.mapCoeff forall a. Num a => Integer -> a
fromInteger ExprZ
t :: LA.Expr Rational) 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 -> forall lit. [[lit]] -> DNF lit
DNF [[Rat
a Rat -> Rat -> Constr
`leR` Rat
b]]
        RelOp
Lt -> forall lit. [[lit]] -> DNF lit
DNF [[Rat
a Rat -> Rat -> Constr
`ltR` Rat
b]]
        RelOp
Ge -> forall lit. [[lit]] -> DNF lit
DNF [[Rat
a Rat -> Rat -> Constr
`geR` Rat
b]]
        RelOp
Gt -> forall lit. [[lit]] -> DNF lit
DNF [[Rat
a Rat -> Rat -> Constr
`gtR` Rat
b]]
        RelOp
Eql -> forall lit. [[lit]] -> DNF lit
DNF [[Rat
a Rat -> Rat -> Constr
`eqR` Rat
b]]
        RelOp
NEq -> 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) = forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
LA.mapCoeff forall a. Num a => Integer -> a
fromInteger ExprZ
e forall e r. IsOrdRel e r => e -> e -> r
.>=. forall r. (Num r, Eq r) => r -> Expr r
LA.constant Rational
0
toLAAtom (IsPos ExprZ
e)    = forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
LA.mapCoeff forall a. Num a => Integer -> a
fromInteger ExprZ
e forall e r. IsOrdRel e r => e -> e -> r
.>.  forall r. (Num r, Eq r) => r -> Expr r
LA.constant Rational
0
toLAAtom (IsZero ExprZ
e)   = forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
LA.mapCoeff forall a. Num a => Integer -> a
fromInteger ExprZ
e forall e r. IsEqRel e r => e -> e -> r
.==. 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 = forall a. MonotoneBoolean a => [a] -> a
andB forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) =
  forall r. Ord r => [Interval r] -> Interval r
Interval.intersections forall a b. (a -> b) -> a -> b
$
    [ forall r. r -> Extended r
Finite (Model Rational -> Rat -> Rational
evalRat Model Rational
model Rat
x) forall r. Ord r => Extended r -> Extended r -> Interval r
<=..< forall r. Extended r
PosInf | Rat
x <- [Rat]
ls1 ] forall a. [a] -> [a] -> [a]
++
    [ forall r. r -> Extended r
Finite (Model Rational -> Rat -> Rational
evalRat Model Rational
model Rat
x) forall r. Ord r => Extended r -> Extended r -> Interval r
<..<  forall r. Extended r
PosInf | Rat
x <- [Rat]
ls2 ] forall a. [a] -> [a] -> [a]
++
    [ forall r. Extended r
NegInf forall r. Ord r => Extended r -> Extended r -> Interval r
<..<= forall r. r -> Extended r
Finite (Model Rational -> Rat -> Rational
evalRat Model Rational
model Rat
x) | Rat
x <- [Rat]
us1 ] forall a. [a] -> [a] -> [a]
++
    [ forall r. Extended r
NegInf forall r. Ord r => Extended r -> Extended r -> Interval r
<..<  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 forall a b. (a -> b) -> a -> b
$
  [ Rat
x Rat -> Rat -> Constr
`leR` Rat
y | Rat
x <- [Rat]
ls1, Rat
y <- [Rat]
us1 ] forall a. [a] -> [a] -> [a]
++
  [ Rat
x Rat -> Rat -> Constr
`ltR` Rat
y | Rat
x <- [Rat]
ls1, Rat
y <- [Rat]
us2 ] forall a. [a] -> [a] -> [a]
++
  [ Rat
x Rat -> Rat -> Constr
`ltR` Rat
y | Rat
x <- [Rat]
ls2, Rat
y <- [Rat]
us1 ] 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 = 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 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 forall a. a -> [a] -> [a]
: [Constr]
xs)
        Just (Integer
c,ExprZ
t') -> ((Rat
t'' forall a. a -> [a] -> [a]
: [Rat]
ls1, [Rat]
ls2, Rat
t'' forall a. a -> [a] -> [a]
: [Rat]
us1, [Rat]
us2), [Constr]
xs)
          where
            t'' :: Rat
t'' = (forall a. Num a => a -> a
signum Integer
c forall v. VectorSpace v => Scalar v -> v -> v
*^ forall v. AdditiveGroup v => v -> v
negateV ExprZ
t', 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 forall r. Num r => Var -> Expr r -> (r, Expr r)
LA.extract Var
v ExprZ
t of
        (Integer
c,ExprZ
t') ->
          case Integer
c forall a. Ord a => a -> a -> Ordering
`compare` Integer
0 of
            Ordering
EQ -> (Bounds
bnd, Constr
constr forall a. a -> [a] -> [a]
: [Constr]
xs)
            Ordering
GT ->
              if Bool
strict
              then (([Rat]
ls1, (forall v. AdditiveGroup v => v -> v
negateV ExprZ
t', Integer
c) forall a. a -> [a] -> [a]
: [Rat]
ls2, [Rat]
us1, [Rat]
us2), [Constr]
xs) -- 0 < cx + M ⇔ -M/c <  x
              else (((forall v. AdditiveGroup v => v -> v
negateV ExprZ
t', Integer
c) 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', forall a. Num a => a -> a
negate Integer
c) forall a. a -> [a] -> [a]
: [Rat]
us2), [Constr]
xs) -- 0 < cx + M ⇔ x < M/-c
              else (([Rat]
ls1, [Rat]
ls2, (ExprZ
t', forall a. Num a => a -> a
negate Integer
c) 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 <- forall lit. DNF lit -> [[lit]]
unDNF forall a b. (a -> b) -> a -> b
$ [Atom Rational] -> DNF Constr
constraintsToDNF [Atom Rational]
xs
  ([Constr]
zs, Model Rational -> Model Rational
mt) <- forall a. Maybe a -> [a]
maybeToList forall a b. (a -> b) -> a -> b
$ Var
-> [Constr] -> Maybe ([Constr], Model Rational -> Model Rational)
project' Var
v [Constr]
ys
  forall (m :: * -> *) a. Monad m => a -> m a
return (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 <- forall lit. DNF lit -> [[lit]]
unDNF forall a b. (a -> b) -> a -> b
$ [Atom Rational] -> DNF Constr
constraintsToDNF [Atom Rational]
xs
  ([Constr]
zs, Model Rational -> Model Rational
mt) <- forall a. Maybe a -> [a]
maybeToList forall a b. (a -> b) -> a -> b
$ VarSet
-> [Constr] -> Maybe ([Constr], Model Rational -> Model Rational)
projectN' VarSet
vs [Constr]
ys
  forall (m :: * -> *) a. Monad m => a -> m a
return (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 = forall (m :: * -> *) a. Monad m => a -> m a
return ([Constr]
xs, 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 = 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]
          forall (m :: * -> *) a. Monad m => a -> m a
return ([Constr]
zs, Model Rational -> Model Rational
mt1 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return ([Constr]
xs, 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 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  -> forall a. HasCallStack => String -> a
error String
"ToySolver.FourierMotzkin.project': should not happen"
                         Just Rational
val -> 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 forall a. [a] -> [a] -> [a]
++ [Constr]
cond)
                  forall (m :: * -> *) a. Monad m => a -> m a
return ([Constr]
ys, Model Rational -> Model Rational
mt1 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 = forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (Constr, [Constr]) -> Maybe (Var, Rat, [Constr])
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) forall a. a -> [a] -> [a]
: [(a
y,a
xforall a. a -> [a] -> [a]
:[a]
ys) | (a
y,[a]
ys) <- 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 (forall a. Variables a => a -> VarSet
vars ExprZ
e)
      forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not 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') = forall r. Num r => Var -> Expr r -> (r, Expr r)
LA.extract Var
v ExprZ
e
      forall (m :: * -> *) a. Monad m => a -> m a
return (Var
v, (forall v. AdditiveGroup v => v -> v
negateV ExprZ
e', Integer
c), [Constr]
cs)
    f (Constr, [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 = 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 <- 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 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 = forall a. IntMap a
IM.empty
  forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall m e v. Eval m e v => m -> e -> v
eval Model Rational
m) [Constr]
cs2
  forall (m :: * -> *) a. Monad m => a -> m a
return 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 = forall a. (a -> a -> a) -> [a] -> a
foldl1' forall a. Integral a => a -> a -> a
gcd [Integer]
xs

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