{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
module ToySolver.Arith.FourierMotzkin.Base
(
Constr (..)
, eqR
, ExprZ
, fromLAAtom
, toLAAtom
, constraintsToDNF
, simplify
, Bounds
, evalBounds
, boundsToConstrs
, collectBounds
, project
, project'
, projectN
, projectN'
, solve
, solve'
, 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
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)
data Constr
= IsNonneg ExprZ
| IsPos ExprZ
| IsZero ExprZ
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 :: 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 :: [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
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)
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)
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)
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)
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 :: 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)
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 :: 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