{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Arith.OmegaTest.Base
-- Copyright   :  (c) Masahiro Sakai 2011
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- (incomplete) implementation of Omega Test
--
-- References:
--
-- * William Pugh. The Omega test: a fast and practical integer
--   programming algorithm for dependence analysis. In Proceedings of
--   the 1991 ACM/IEEE conference on Supercomputing (1991), pp. 4-13.
--
-- * <http://users.cecs.anu.edu.au/~michaeln/pubs/arithmetic-dps.pdf>
--
-- See also:
--
-- * <http://hackage.haskell.org/package/Omega>
--
-----------------------------------------------------------------------------
module ToySolver.Arith.OmegaTest.Base
    ( Model
    , solve
    , solveQFLIRAConj
    , Options (..)
    , checkRealNoCheck
    , checkRealByFM

    -- * Exported just for testing
    , zmod
    ) where

import Control.Exception (assert)
import Control.Monad
import Data.Default.Class
import Data.List
import Data.Maybe
import Data.Ord
import Data.Ratio
import qualified Data.IntMap as IM
import qualified Data.IntSet as IS
import Data.VectorSpace

import ToySolver.Data.OrdRel
import ToySolver.Data.Boolean
import ToySolver.Data.DNF
import qualified ToySolver.Data.LA as LA
import ToySolver.Data.IntVar
import ToySolver.Internal.Util (combineMaybe)
import qualified ToySolver.Arith.FourierMotzkin as FM

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

-- | Options for solving.
--
-- The default option can be obtained by 'def'.
data Options
  = Options
  { Options -> VarSet -> [Atom (Ratio Integer)] -> Bool
optCheckReal :: VarSet -> [LA.Atom Rational] -> Bool
  -- ^ optCheckReal is used for checking whether real shadow is satisfiable.
  --
  -- * If it returns @True@, the real shadow may or may not be satisfiable.
  --
  -- * If it returns @False@, the real shadow must be unsatisfiable
  }

instance Default Options where
  def :: Options
def =
    Options
    { optCheckReal :: VarSet -> [Atom (Ratio Integer)] -> Bool
optCheckReal =
        -- checkRealNoCheck
        VarSet -> [Atom (Ratio Integer)] -> Bool
checkRealByFM
    }

checkRealNoCheck :: VarSet -> [LA.Atom Rational] -> Bool
checkRealNoCheck :: VarSet -> [Atom (Ratio Integer)] -> Bool
checkRealNoCheck VarSet
_ [Atom (Ratio Integer)]
_ = Bool
True

checkRealByFM :: VarSet -> [LA.Atom Rational] -> Bool
checkRealByFM :: VarSet -> [Atom (Ratio Integer)] -> Bool
checkRealByFM VarSet
vs [Atom (Ratio Integer)]
as = Maybe (Model (Ratio Integer)) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Model (Ratio Integer)) -> Bool)
-> Maybe (Model (Ratio Integer)) -> Bool
forall a b. (a -> b) -> a -> b
$ VarSet -> [Atom (Ratio Integer)] -> Maybe (Model (Ratio Integer))
FM.solve VarSet
vs [Atom (Ratio Integer)]
as

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

type ExprZ = LA.Expr Integer

-- | Atomic constraint
data Constr
  = IsNonneg ExprZ
  -- ^ e ≥ 0
  | IsZero ExprZ
  -- ^ e = 0
  deriving (Int -> Constr -> ShowS
[Constr] -> ShowS
Constr -> String
(Int -> Constr -> ShowS)
-> (Constr -> String) -> ([Constr] -> ShowS) -> Show Constr
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Constr -> ShowS
showsPrec :: Int -> 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 (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

-- 制約集合の単純化
-- 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 constr :: Constr
constr@(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
constr]
    f constr :: Constr
constr@(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
constr]

leZ, ltZ, geZ, gtZ, eqZ :: ExprZ -> ExprZ -> Constr
-- Note that constants may be floored by division
leZ :: ExprZ -> ExprZ -> Constr
leZ ExprZ
e1 ExprZ
e2 = ExprZ -> Constr
IsNonneg ((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
    e :: ExprZ
e = ExprZ
e2 ExprZ -> ExprZ -> ExprZ
forall v. AdditiveGroup v => v -> v -> v
^-^ ExprZ
e1
    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
c | (Integer
c,Int
v) <- ExprZ -> [(Integer, Int)]
forall r. Expr r -> [(r, Int)]
LA.terms ExprZ
e, Int
v Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
LA.unitVar]
ltZ :: ExprZ -> ExprZ -> Constr
ltZ ExprZ
e1 ExprZ
e2 = (ExprZ
e1 ExprZ -> ExprZ -> ExprZ
forall v. AdditiveGroup v => v -> v -> v
^+^ Integer -> ExprZ
forall r. (Num r, Eq r) => r -> Expr r
LA.constant Integer
1) ExprZ -> ExprZ -> Constr
`leZ` ExprZ
e2
geZ :: ExprZ -> ExprZ -> Constr
geZ = (ExprZ -> ExprZ -> Constr) -> ExprZ -> ExprZ -> Constr
forall a b c. (a -> b -> c) -> b -> a -> c
flip ExprZ -> ExprZ -> Constr
leZ
gtZ :: ExprZ -> ExprZ -> Constr
gtZ = (ExprZ -> ExprZ -> Constr) -> ExprZ -> ExprZ -> Constr
forall a b c. (a -> b -> c) -> b -> a -> c
flip ExprZ -> ExprZ -> Constr
ltZ
eqZ :: ExprZ -> ExprZ -> Constr
eqZ ExprZ
e1 ExprZ
e2 =
  case ExprZ -> Maybe Constr
isZero (ExprZ
e1 ExprZ -> ExprZ -> ExprZ
forall v. AdditiveGroup v => v -> v -> v
^-^ ExprZ
e2) of
    Just Constr
c -> Constr
c
    Maybe Constr
Nothing -> ExprZ -> Constr
IsZero (Integer -> ExprZ
forall r. (Num r, Eq r) => r -> Expr r
LA.constant Integer
1) -- unsatisfiable

isZero :: ExprZ -> Maybe Constr
isZero :: ExprZ -> Maybe Constr
isZero ExprZ
e
  = if Int -> ExprZ -> Integer
forall r. Num r => Int -> Expr r -> r
LA.coeff Int
LA.unitVar ExprZ
e Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
d Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0
    then Constr -> Maybe Constr
forall a. a -> Maybe a
Just (Constr -> Maybe Constr) -> Constr -> Maybe Constr
forall a b. (a -> b) -> a -> b
$ ExprZ -> Constr
IsZero (ExprZ -> Constr) -> ExprZ -> Constr
forall a b. (a -> b) -> a -> b
$ (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
    else Maybe Constr
forall a. Maybe a
Nothing
  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
c | (Integer
c,Int
v) <- ExprZ -> [(Integer, Int)]
forall r. Expr r -> [(r, Int)]
LA.terms ExprZ
e, Int
v Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
LA.unitVar]

applySubst1Constr :: Var -> ExprZ -> Constr -> Constr
applySubst1Constr :: Int -> ExprZ -> Constr -> Constr
applySubst1Constr Int
v ExprZ
e (IsNonneg ExprZ
e2) = Int -> ExprZ -> ExprZ -> ExprZ
forall r. (Num r, Eq r) => Int -> Expr r -> Expr r -> Expr r
LA.applySubst1 Int
v ExprZ
e ExprZ
e2 ExprZ -> ExprZ -> Constr
`geZ` Integer -> ExprZ
forall r. (Num r, Eq r) => r -> Expr r
LA.constant Integer
0
applySubst1Constr Int
v ExprZ
e (IsZero ExprZ
e2)   = Int -> ExprZ -> ExprZ -> ExprZ
forall r. (Num r, Eq r) => Int -> Expr r -> Expr r -> Expr r
LA.applySubst1 Int
v ExprZ
e ExprZ
e2 ExprZ -> ExprZ -> Constr
`eqZ` Integer -> ExprZ
forall r. (Num r, Eq r) => r -> Expr r
LA.constant Integer
0

instance Eval (Model Integer) Constr Bool where
  eval :: Model Integer -> Constr -> Bool
eval Model Integer
m (IsNonneg ExprZ
t) = Model Integer -> ExprZ -> Integer
forall m e v. Eval m e v => m -> e -> v
LA.eval Model Integer
m ExprZ
t Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0
  eval Model Integer
m (IsZero ExprZ
t)   = Model Integer -> ExprZ -> Integer
forall m e v. Eval m e v => m -> e -> v
LA.eval Model Integer
m ExprZ
t Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0

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

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

{-
(ls,us) represents
{ x | ∀(M,c)∈ls. M/c≤x, ∀(M,c)∈us. x≤M/c }
-}
type BoundsZ = ([Rat],[Rat])

evalBoundsZ :: Model Integer -> BoundsZ -> IntervalZ
evalBoundsZ :: Model Integer -> BoundsZ -> IntervalZ
evalBoundsZ Model Integer
model ([Rat]
ls,[Rat]
us) =
  (IntervalZ -> IntervalZ -> IntervalZ)
-> IntervalZ -> [IntervalZ] -> IntervalZ
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' IntervalZ -> IntervalZ -> IntervalZ
intersectZ IntervalZ
univZ ([IntervalZ] -> IntervalZ) -> [IntervalZ] -> IntervalZ
forall a b. (a -> b) -> a -> b
$
    [ (Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Ratio Integer -> Integer
forall b. Integral b => Ratio Integer -> b
forall a b. (RealFrac a, Integral b) => a -> b
ceiling (Model Integer -> ExprZ -> Integer
forall m e v. Eval m e v => m -> e -> v
LA.eval Model Integer
model ExprZ
x Integer -> Integer -> Ratio Integer
forall a. Integral a => a -> a -> Ratio a
% Integer
c)), Maybe Integer
forall a. Maybe a
Nothing) | (ExprZ
x,Integer
c) <- [Rat]
ls ] [IntervalZ] -> [IntervalZ] -> [IntervalZ]
forall a. [a] -> [a] -> [a]
++
    [ (Maybe Integer
forall a. Maybe a
Nothing, Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Ratio Integer -> Integer
forall b. Integral b => Ratio Integer -> b
forall a b. (RealFrac a, Integral b) => a -> b
floor (Model Integer -> ExprZ -> Integer
forall m e v. Eval m e v => m -> e -> v
LA.eval Model Integer
model ExprZ
x Integer -> Integer -> Ratio Integer
forall a. Integral a => a -> a -> Ratio a
% Integer
c))) | (ExprZ
x,Integer
c) <- [Rat]
us ]

collectBoundsZ :: Var -> [Constr] -> (BoundsZ, [Constr])
collectBoundsZ :: Int -> [Constr] -> (BoundsZ, [Constr])
collectBoundsZ Int
v = (Constr -> (BoundsZ, [Constr]) -> (BoundsZ, [Constr]))
-> (BoundsZ, [Constr]) -> [Constr] -> (BoundsZ, [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 -> (BoundsZ, [Constr]) -> (BoundsZ, [Constr])
phi (([],[]),[])
  where
    phi :: Constr -> (BoundsZ,[Constr]) -> (BoundsZ,[Constr])
    phi :: Constr -> (BoundsZ, [Constr]) -> (BoundsZ, [Constr])
phi constr :: Constr
constr@(IsNonneg ExprZ
t) (([Rat]
ls,[Rat]
us),[Constr]
xs) =
      case Int -> ExprZ -> (Integer, ExprZ)
forall r. Num r => Int -> Expr r -> (r, Expr r)
LA.extract Int
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 -> (([Rat]
ls, [Rat]
us), Constr
constr Constr -> [Constr] -> [Constr]
forall a. a -> [a] -> [a]
: [Constr]
xs)
            Ordering
GT -> (((ExprZ -> ExprZ
forall v. AdditiveGroup v => v -> v
negateV ExprZ
t', Integer
c) Rat -> [Rat] -> [Rat]
forall a. a -> [a] -> [a]
: [Rat]
ls, [Rat]
us), [Constr]
xs) -- 0 ≤ cx + M ⇔ -M/c ≤ x
            Ordering
LT -> (([Rat]
ls, (ExprZ
t', Integer -> Integer
forall a. Num a => a -> a
negate Integer
c) Rat -> [Rat] -> [Rat]
forall a. a -> [a] -> [a]
: [Rat]
us), [Constr]
xs)   -- 0 ≤ cx + M ⇔ x ≤ M/-c
    phi constr :: Constr
constr@(IsZero ExprZ
_) (BoundsZ
bnd,[Constr]
xs) = (BoundsZ
bnd, Constr
constr Constr -> [Constr] -> [Constr]
forall a. a -> [a] -> [a]
: [Constr]
xs) -- we assume v does not appear in constr

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

solve' :: Options -> VarSet -> [Constr] -> Maybe (Model Integer)
solve' :: Options -> VarSet -> [Constr] -> Maybe (Model Integer)
solve' Options
opt VarSet
vs2 [Constr]
xs = [Constr] -> Maybe [Constr]
simplify [Constr]
xs Maybe [Constr]
-> ([Constr] -> Maybe (Model Integer)) -> Maybe (Model Integer)
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= VarSet -> [Constr] -> Maybe (Model Integer)
go VarSet
vs2
  where
    go :: VarSet -> [Constr] -> Maybe (Model Integer)
    go :: VarSet -> [Constr] -> Maybe (Model Integer)
go VarSet
vs [Constr]
cs | VarSet -> Bool
IS.null VarSet
vs = do
      let m :: Model Integer
          m :: Model Integer
m = Model Integer
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 Integer -> Constr -> Bool
forall m e v. Eval m e v => m -> e -> v
eval Model Integer
m) [Constr]
cs
      Model Integer -> Maybe (Model Integer)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Model Integer
m
    go VarSet
vs [Constr]
cs | Just (ExprZ
e,[Constr]
cs2) <- [Constr] -> Maybe (ExprZ, [Constr])
extractEq [Constr]
cs = do
      (VarSet
vs',[Constr]
cs3, Model Integer -> Model Integer
mt) <- ExprZ
-> VarSet
-> [Constr]
-> Maybe (VarSet, [Constr], Model Integer -> Model Integer)
eliminateEq ExprZ
e VarSet
vs [Constr]
cs2
      Model Integer
m <- VarSet -> [Constr] -> Maybe (Model Integer)
go VarSet
vs' ([Constr] -> Maybe (Model Integer))
-> Maybe [Constr] -> Maybe (Model Integer)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Constr] -> Maybe [Constr]
simplify [Constr]
cs3
      Model Integer -> Maybe (Model Integer)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Model Integer -> Model Integer
mt Model Integer
m)
    go VarSet
vs [Constr]
cs = do
      Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Options -> VarSet -> [Atom (Ratio Integer)] -> Bool
optCheckReal Options
opt VarSet
vs ((Constr -> Atom (Ratio Integer))
-> [Constr] -> [Atom (Ratio Integer)]
forall a b. (a -> b) -> [a] -> [b]
map Constr -> Atom (Ratio Integer)
toLAAtom [Constr]
cs)
      if BoundsZ -> Bool
isExact BoundsZ
bnd then
        Maybe (Model Integer)
case1
      else
        Maybe (Model Integer)
case1 Maybe (Model Integer)
-> Maybe (Model Integer) -> Maybe (Model Integer)
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Maybe (Model Integer)
case2

      where
        (Int
v,VarSet
vs',bnd :: BoundsZ
bnd@([Rat]
ls,[Rat]
us),[Constr]
rest) = VarSet -> [Constr] -> (Int, VarSet, BoundsZ, [Constr])
chooseVariable VarSet
vs [Constr]
cs

        case1 :: Maybe (Model Integer)
case1 = do
          let zs :: [Constr]
zs = [ Integer -> ExprZ
forall r. (Num r, Eq r) => r -> Expr r
LA.constant ((Integer
aInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*(Integer
bInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)) ExprZ -> ExprZ -> Constr
`leZ` (Integer
Scalar ExprZ
a Scalar ExprZ -> ExprZ -> ExprZ
forall v. VectorSpace v => Scalar v -> v -> v
*^ ExprZ
d ExprZ -> ExprZ -> ExprZ
forall v. AdditiveGroup v => v -> v -> v
^-^ Integer
Scalar ExprZ
b Scalar ExprZ -> ExprZ -> ExprZ
forall v. VectorSpace v => Scalar v -> v -> v
*^ ExprZ
c)
                   | (ExprZ
c,Integer
a)<-[Rat]
ls , (ExprZ
d,Integer
b)<-[Rat]
us ]
          Model Integer
model <- VarSet -> [Constr] -> Maybe (Model Integer)
go VarSet
vs' ([Constr] -> Maybe (Model Integer))
-> Maybe [Constr] -> Maybe (Model Integer)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Constr] -> Maybe [Constr]
simplify ([Constr]
zs [Constr] -> [Constr] -> [Constr]
forall a. [a] -> [a] -> [a]
++ [Constr]
rest)
          case IntervalZ -> Maybe Integer
pickupZ (Model Integer -> BoundsZ -> IntervalZ
evalBoundsZ Model Integer
model BoundsZ
bnd) of
            Maybe Integer
Nothing  -> String -> Maybe (Model Integer)
forall a. HasCallStack => String -> a
error String
"ToySolver.OmegaTest.solve': should not happen"
            Just Integer
val -> Model Integer -> Maybe (Model Integer)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Model Integer -> Maybe (Model Integer))
-> Model Integer -> Maybe (Model Integer)
forall a b. (a -> b) -> a -> b
$ Int -> Integer -> Model Integer -> Model Integer
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
v Integer
val Model Integer
model

        case2 :: Maybe (Model Integer)
case2 = [Maybe (Model Integer)] -> Maybe (Model Integer)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
          [ do Constr
c <- ExprZ -> Maybe Constr
isZero (ExprZ -> Maybe Constr) -> ExprZ -> Maybe Constr
forall a b. (a -> b) -> a -> b
$ Integer
Scalar ExprZ
a' Scalar ExprZ -> ExprZ -> ExprZ
forall v. VectorSpace v => Scalar v -> v -> v
*^ Int -> ExprZ
forall r. Num r => Int -> Expr r
LA.var Int
v ExprZ -> ExprZ -> ExprZ
forall v. AdditiveGroup v => v -> v -> v
^-^ (ExprZ
c' ExprZ -> ExprZ -> ExprZ
forall v. AdditiveGroup v => v -> v -> v
^+^ Integer -> ExprZ
forall r. (Num r, Eq r) => r -> Expr r
LA.constant Integer
k)
               Model Integer
model <- VarSet -> [Constr] -> Maybe (Model Integer)
go VarSet
vs (Constr
c Constr -> [Constr] -> [Constr]
forall a. a -> [a] -> [a]
: [Constr]
cs)
               Model Integer -> Maybe (Model Integer)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Model Integer
model
          | let m :: Integer
m = [Integer] -> Integer
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [Integer
b | (ExprZ
_,Integer
b)<-[Rat]
us]
          , (ExprZ
c',Integer
a') <- [Rat]
ls
          , Integer
k <- [Integer
0 .. (Integer
mInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
a'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
a'Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
m) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
m]
          ]

isExact :: BoundsZ -> Bool
isExact :: BoundsZ -> Bool
isExact ([Rat]
ls,[Rat]
us) = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Integer
aInteger -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
==Integer
1 Bool -> Bool -> Bool
|| Integer
bInteger -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
==Integer
1 | (ExprZ
_,Integer
a)<-[Rat]
ls , (ExprZ
_,Integer
b)<-[Rat]
us]

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

chooseVariable :: VarSet -> [Constr] -> (Var, VarSet, BoundsZ, [Constr])
chooseVariable :: VarSet -> [Constr] -> (Int, VarSet, BoundsZ, [Constr])
chooseVariable VarSet
vs [Constr]
xs = [(Int, VarSet, BoundsZ, [Constr])]
-> (Int, VarSet, BoundsZ, [Constr])
forall a. HasCallStack => [a] -> a
head ([(Int, VarSet, BoundsZ, [Constr])]
 -> (Int, VarSet, BoundsZ, [Constr]))
-> [(Int, VarSet, BoundsZ, [Constr])]
-> (Int, VarSet, BoundsZ, [Constr])
forall a b. (a -> b) -> a -> b
$ [(Int, VarSet, BoundsZ, [Constr])
e | e :: (Int, VarSet, BoundsZ, [Constr])
e@(Int
_,VarSet
_,BoundsZ
bnd,[Constr]
_) <- [(Int, VarSet, BoundsZ, [Constr])]
table, BoundsZ -> Bool
isExact BoundsZ
bnd] [(Int, VarSet, BoundsZ, [Constr])]
-> [(Int, VarSet, BoundsZ, [Constr])]
-> [(Int, VarSet, BoundsZ, [Constr])]
forall a. [a] -> [a] -> [a]
++ [(Int, VarSet, BoundsZ, [Constr])]
table
  where
    table :: [(Int, VarSet, BoundsZ, [Constr])]
table = [ (Int
v, [Int] -> VarSet
IS.fromAscList [Int]
vs', BoundsZ
bnd, [Constr]
rest)
            | (Int
v,[Int]
vs') <- [Int] -> [(Int, [Int])]
forall a. [a] -> [(a, [a])]
pickup (VarSet -> [Int]
IS.toAscList VarSet
vs), let (BoundsZ
bnd, [Constr]
rest) = Int -> [Constr] -> (BoundsZ, [Constr])
collectBoundsZ Int
v [Constr]
xs
            ]

-- Find an equality constraint (e==0) and extract e with rest of constraints.
extractEq :: [Constr] -> Maybe (ExprZ, [Constr])
extractEq :: [Constr] -> Maybe (ExprZ, [Constr])
extractEq = [Maybe (ExprZ, [Constr])] -> Maybe (ExprZ, [Constr])
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([Maybe (ExprZ, [Constr])] -> Maybe (ExprZ, [Constr]))
-> ([Constr] -> [Maybe (ExprZ, [Constr])])
-> [Constr]
-> Maybe (ExprZ, [Constr])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Constr, [Constr]) -> Maybe (ExprZ, [Constr]))
-> [(Constr, [Constr])] -> [Maybe (ExprZ, [Constr])]
forall a b. (a -> b) -> [a] -> [b]
map (Constr, [Constr]) -> Maybe (ExprZ, [Constr])
f ([(Constr, [Constr])] -> [Maybe (ExprZ, [Constr])])
-> ([Constr] -> [(Constr, [Constr])])
-> [Constr]
-> [Maybe (ExprZ, [Constr])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Constr] -> [(Constr, [Constr])]
forall a. [a] -> [(a, [a])]
pickup
  where
    f :: (Constr, [Constr]) -> Maybe (ExprZ, [Constr])
    f :: (Constr, [Constr]) -> Maybe (ExprZ, [Constr])
f (IsZero ExprZ
e, [Constr]
ls) = (ExprZ, [Constr]) -> Maybe (ExprZ, [Constr])
forall a. a -> Maybe a
Just (ExprZ
e, [Constr]
ls)
    f (Constr, [Constr])
_ = Maybe (ExprZ, [Constr])
forall a. Maybe a
Nothing

-- Eliminate an equality equality constraint (e==0).
eliminateEq :: ExprZ -> VarSet -> [Constr] -> Maybe (VarSet, [Constr], Model Integer -> Model Integer)
eliminateEq :: ExprZ
-> VarSet
-> [Constr]
-> Maybe (VarSet, [Constr], Model Integer -> Model Integer)
eliminateEq ExprZ
e VarSet
vs [Constr]
cs | Just Integer
c <- ExprZ -> Maybe Integer
forall r. Num r => Expr r -> Maybe r
LA.asConst ExprZ
e = Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
cInteger -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
==Integer
0) Maybe ()
-> Maybe (VarSet, [Constr], Model Integer -> Model Integer)
-> Maybe (VarSet, [Constr], Model Integer -> Model Integer)
forall a b. Maybe a -> Maybe b -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (VarSet, [Constr], Model Integer -> Model Integer)
-> Maybe (VarSet, [Constr], Model Integer -> Model Integer)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (VarSet
vs, [Constr]
cs, Model Integer -> Model Integer
forall a. a -> a
id)
eliminateEq ExprZ
e VarSet
vs [Constr]
cs = do
  let (Integer
ak,Int
xk) = ((Integer, Int) -> (Integer, Int) -> Ordering)
-> [(Integer, Int)] -> (Integer, Int)
forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
minimumBy (((Integer, Int) -> Integer)
-> (Integer, Int) -> (Integer, Int) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Integer -> Integer
forall a. Num a => a -> a
abs (Integer -> Integer)
-> ((Integer, Int) -> Integer) -> (Integer, Int) -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer, Int) -> Integer
forall a b. (a, b) -> a
fst)) [(Integer
a,Int
x) | (Integer
a,Int
x) <- ExprZ -> [(Integer, Int)]
forall r. Expr r -> [(r, Int)]
LA.terms ExprZ
e, Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
LA.unitVar]
  if Integer -> Integer
forall a. Num a => a -> a
abs Integer
ak Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1 then
    case Int -> ExprZ -> (Integer, ExprZ)
forall r. Num r => Int -> Expr r -> (r, Expr r)
LA.extract Int
xk ExprZ
e of
      (Integer
_, ExprZ
e') -> do
        let xk_def :: ExprZ
xk_def = Integer -> Integer
forall a. Num a => a -> a
signum Integer
ak Scalar ExprZ -> ExprZ -> ExprZ
forall v. VectorSpace v => Scalar v -> v -> v
*^ ExprZ -> ExprZ
forall v. AdditiveGroup v => v -> v
negateV ExprZ
e'
        (VarSet, [Constr], Model Integer -> Model Integer)
-> Maybe (VarSet, [Constr], Model Integer -> Model Integer)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ((VarSet, [Constr], Model Integer -> Model Integer)
 -> Maybe (VarSet, [Constr], Model Integer -> Model Integer))
-> (VarSet, [Constr], Model Integer -> Model Integer)
-> Maybe (VarSet, [Constr], Model Integer -> Model Integer)
forall a b. (a -> b) -> a -> b
$
           ( Int -> VarSet -> VarSet
IS.delete Int
xk VarSet
vs
           , [Int -> ExprZ -> Constr -> Constr
applySubst1Constr Int
xk ExprZ
xk_def Constr
c | Constr
c <- [Constr]
cs]
           , \Model Integer
model -> Int -> Integer -> Model Integer -> Model Integer
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
xk (Model Integer -> ExprZ -> Integer
forall m e v. Eval m e v => m -> e -> v
LA.eval Model Integer
model ExprZ
xk_def) Model Integer
model
           )
  else do
    let m :: Integer
m = Integer -> Integer
forall a. Num a => a -> a
abs Integer
ak Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
    Bool -> Maybe () -> Maybe ()
forall a. HasCallStack => Bool -> a -> a
assert (Integer
ak Integer -> Integer -> Integer
`zmod` Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== - Integer -> Integer
forall a. Num a => a -> a
signum Integer
ak) (Maybe () -> Maybe ()) -> Maybe () -> Maybe ()
forall a b. (a -> b) -> a -> b
$ () -> Maybe ()
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    let -- sigma is a fresh variable
        sigma :: Int
sigma = if VarSet -> Bool
IS.null VarSet
vs then Int
0 else VarSet -> Int
IS.findMax VarSet
vs Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
        -- m *^ LA.var sigma == LA.fromTerms [(a `zmod` m, x) | (a,x) <- LA.terms e]
        -- m *^ LA.var sigma == LA.fromTerms [(a `zmod` m, x) | (a,x) <- LA.terms e, x /= xk] ^+^ (ak `zmod` m) *^ LA.var xk
        -- m *^ LA.var sigma == LA.fromTerms [(a `zmod` m, x) | (a,x) <- LA.terms e, x /= xk] ^+^ (- signum ak) *^ LA.var xk
        -- LA.var xk == (- signum ak * m) *^ LA.var sigma ^+^ LA.fromTerms [(signum ak * (a `zmod` m), x) | (a,x) <- LA.terms e, x /= xk]
        xk_def :: ExprZ
xk_def = (- Integer -> Integer
forall a. Num a => a -> a
signum Integer
ak Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
m) Scalar ExprZ -> ExprZ -> ExprZ
forall v. VectorSpace v => Scalar v -> v -> v
*^ Int -> ExprZ
forall r. Num r => Int -> Expr r
LA.var Int
sigma ExprZ -> ExprZ -> ExprZ
forall v. AdditiveGroup v => v -> v -> v
^+^
                   [(Integer, Int)] -> ExprZ
forall r. (Num r, Eq r) => [(r, Int)] -> Expr r
LA.fromTerms [(Integer -> Integer
forall a. Num a => a -> a
signum Integer
ak Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* (Integer
a Integer -> Integer -> Integer
`zmod` Integer
m), Int
x) | (Integer
a,Int
x) <- ExprZ -> [(Integer, Int)]
forall r. Expr r -> [(r, Int)]
LA.terms ExprZ
e, Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
xk]
        -- e2 is normalized version of (LA.applySubst1 xk xk_def e).
        e2 :: ExprZ
e2 = (- Integer -> Integer
forall a. Num a => a -> a
abs Integer
ak) Scalar ExprZ -> ExprZ -> ExprZ
forall v. VectorSpace v => Scalar v -> v -> v
*^ Int -> ExprZ
forall r. Num r => Int -> Expr r
LA.var Int
sigma ExprZ -> ExprZ -> ExprZ
forall v. AdditiveGroup v => v -> v -> v
^+^
                [(Integer, Int)] -> ExprZ
forall r. (Num r, Eq r) => [(r, Int)] -> Expr r
LA.fromTerms [((Ratio Integer -> Integer
forall b. Integral b => Ratio Integer -> b
forall a b. (RealFrac a, Integral b) => a -> b
floor (Integer
aInteger -> Integer -> Ratio Integer
forall a. Integral a => a -> a -> Ratio a
%Integer
m Ratio Integer -> Ratio Integer -> Ratio Integer
forall a. Num a => a -> a -> a
+ Ratio Integer
1Ratio Integer -> Ratio Integer -> Ratio Integer
forall a. Fractional a => a -> a -> a
/Ratio Integer
2) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ (Integer
a Integer -> Integer -> Integer
`zmod` Integer
m)), Int
x) | (Integer
a,Int
x) <- ExprZ -> [(Integer, Int)]
forall r. Expr r -> [(r, Int)]
LA.terms ExprZ
e, Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
xk]
    Bool -> Maybe () -> Maybe ()
forall a. HasCallStack => Bool -> a -> a
assert (Integer
Scalar ExprZ
m Scalar ExprZ -> ExprZ -> ExprZ
forall v. VectorSpace v => Scalar v -> v -> v
*^ ExprZ
e2 ExprZ -> ExprZ -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> ExprZ -> ExprZ -> ExprZ
forall r. (Num r, Eq r) => Int -> Expr r -> Expr r -> Expr r
LA.applySubst1 Int
xk ExprZ
xk_def ExprZ
e) (Maybe () -> Maybe ()) -> Maybe () -> Maybe ()
forall a b. (a -> b) -> a -> b
$ () -> Maybe ()
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    let mt :: Model Integer -> Model Integer
        mt :: Model Integer -> Model Integer
mt Model Integer
model = Int -> Model Integer -> Model Integer
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
sigma (Model Integer -> Model Integer) -> Model Integer -> Model Integer
forall a b. (a -> b) -> a -> b
$ Int -> Integer -> Model Integer -> Model Integer
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
xk (Model Integer -> ExprZ -> Integer
forall m e v. Eval m e v => m -> e -> v
LA.eval Model Integer
model ExprZ
xk_def) Model Integer
model
    Constr
c <- ExprZ -> Maybe Constr
isZero ExprZ
e2
    (VarSet, [Constr], Model Integer -> Model Integer)
-> Maybe (VarSet, [Constr], Model Integer -> Model Integer)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> VarSet -> VarSet
IS.insert Int
sigma (Int -> VarSet -> VarSet
IS.delete Int
xk VarSet
vs), Constr
c Constr -> [Constr] -> [Constr]
forall a. a -> [a] -> [a]
: [Int -> ExprZ -> Constr -> Constr
applySubst1Constr Int
xk ExprZ
xk_def Constr
c | Constr
c <- [Constr]
cs], Model Integer -> Model Integer
mt)

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

type IntervalZ = (Maybe Integer, Maybe Integer)

univZ :: IntervalZ
univZ :: IntervalZ
univZ = (Maybe Integer
forall a. Maybe a
Nothing, Maybe Integer
forall a. Maybe a
Nothing)

intersectZ :: IntervalZ -> IntervalZ -> IntervalZ
intersectZ :: IntervalZ -> IntervalZ -> IntervalZ
intersectZ (Maybe Integer
l1,Maybe Integer
u1) (Maybe Integer
l2,Maybe Integer
u2) = ((Integer -> Integer -> Integer)
-> Maybe Integer -> Maybe Integer -> Maybe Integer
forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
combineMaybe Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Maybe Integer
l1 Maybe Integer
l2, (Integer -> Integer -> Integer)
-> Maybe Integer -> Maybe Integer -> Maybe Integer
forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
combineMaybe Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Maybe Integer
u1 Maybe Integer
u2)

pickupZ :: IntervalZ -> Maybe Integer
pickupZ :: IntervalZ -> Maybe Integer
pickupZ (Maybe Integer
Nothing,Maybe Integer
Nothing) = Integer -> Maybe Integer
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
0
pickupZ (Just Integer
x, Maybe Integer
Nothing) = Integer -> Maybe Integer
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
x
pickupZ (Maybe Integer
Nothing, Just Integer
x) = Integer -> Maybe Integer
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
x
pickupZ (Just Integer
x, Just Integer
y) = if Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
y then Integer -> Maybe Integer
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
x else Maybe Integer
forall a. Maybe a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

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

-- | @'solve' opt {x1,…,xn} φ@ returns @Just M@ that @M ⊧_LIA φ@ when
-- such @M@ exists, returns @Nothing@ otherwise.
--
-- @FV(φ)@ must be a subset of @{x1,…,xn}@.
--
solve :: Options -> VarSet -> [LA.Atom Rational] -> Maybe (Model Integer)
solve :: Options
-> VarSet -> [Atom (Ratio Integer)] -> Maybe (Model Integer)
solve Options
opt VarSet
vs [Atom (Ratio Integer)]
cs = [Maybe (Model Integer)] -> Maybe (Model Integer)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [Options -> VarSet -> [Constr] -> Maybe (Model Integer)
solve' Options
opt VarSet
vs [Constr]
cs | [Constr]
cs <- DNF Constr -> [[Constr]]
forall lit. DNF lit -> [[lit]]
unDNF DNF Constr
dnf]
  where
    dnf :: DNF Constr
dnf = [DNF Constr] -> DNF Constr
forall a. MonotoneBoolean a => [a] -> a
andB ((Atom (Ratio Integer) -> DNF Constr)
-> [Atom (Ratio Integer)] -> [DNF Constr]
forall a b. (a -> b) -> [a] -> [b]
map Atom (Ratio Integer) -> DNF Constr
f [Atom (Ratio Integer)]
cs)
    f :: Atom (Ratio Integer) -> DNF Constr
f (OrdRel Expr (Ratio Integer)
lhs RelOp
op Expr (Ratio Integer)
rhs) =
      case RelOp
op of
        RelOp
Lt  -> [[Constr]] -> DNF Constr
forall lit. [[lit]] -> DNF lit
DNF [[ExprZ
a ExprZ -> ExprZ -> Constr
`ltZ` ExprZ
b]]
        RelOp
Le  -> [[Constr]] -> DNF Constr
forall lit. [[lit]] -> DNF lit
DNF [[ExprZ
a ExprZ -> ExprZ -> Constr
`leZ` ExprZ
b]]
        RelOp
Gt  -> [[Constr]] -> DNF Constr
forall lit. [[lit]] -> DNF lit
DNF [[ExprZ
a ExprZ -> ExprZ -> Constr
`gtZ` ExprZ
b]]
        RelOp
Ge  -> [[Constr]] -> DNF Constr
forall lit. [[lit]] -> DNF lit
DNF [[ExprZ
a ExprZ -> ExprZ -> Constr
`geZ` ExprZ
b]]
        RelOp
Eql -> [[Constr]] -> DNF Constr
forall lit. [[lit]] -> DNF lit
DNF [[ExprZ
a ExprZ -> ExprZ -> Constr
`eqZ` ExprZ
b]]
        RelOp
NEq -> [[Constr]] -> DNF Constr
forall lit. [[lit]] -> DNF lit
DNF [[ExprZ
a ExprZ -> ExprZ -> Constr
`ltZ` ExprZ
b], [ExprZ
a ExprZ -> ExprZ -> Constr
`gtZ` ExprZ
b]]
      where
        (ExprZ
e1,Integer
c1) = Expr (Ratio Integer) -> Rat
g Expr (Ratio Integer)
lhs
        (ExprZ
e2,Integer
c2) = Expr (Ratio Integer) -> Rat
g Expr (Ratio Integer)
rhs
        a :: ExprZ
a = Integer
Scalar ExprZ
c2 Scalar ExprZ -> ExprZ -> ExprZ
forall v. VectorSpace v => Scalar v -> v -> v
*^ ExprZ
e1
        b :: ExprZ
b = Integer
Scalar ExprZ
c1 Scalar ExprZ -> ExprZ -> ExprZ
forall v. VectorSpace v => Scalar v -> v -> v
*^ ExprZ
e2
    g :: LA.Expr Rational -> (ExprZ, Integer)
    g :: Expr (Ratio Integer) -> Rat
g Expr (Ratio Integer)
a = ((Ratio Integer -> Integer) -> Expr (Ratio Integer) -> ExprZ
forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
LA.mapCoeff (\Ratio Integer
c -> Ratio Integer -> Integer
forall b. Integral b => Ratio Integer -> b
forall a b. (RealFrac a, Integral b) => a -> b
floor (Ratio Integer
c Ratio Integer -> Ratio Integer -> Ratio Integer
forall a. Num a => a -> a -> a
* Integer -> Ratio Integer
forall a. Num a => Integer -> a
fromInteger Integer
d)) Expr (Ratio Integer)
a, Integer
d)
      where
        d :: Integer
d = (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 [Ratio Integer -> Integer
forall a. Ratio a -> a
denominator Ratio Integer
c | (Ratio Integer
c,Int
_) <- Expr (Ratio Integer) -> [(Ratio Integer, Int)]
forall r. Expr r -> [(r, Int)]
LA.terms Expr (Ratio Integer)
a]

-- | @'solveQFLIRAConj' {x1,…,xn} φ I@ returns @Just M@ that @M ⊧_LIRA φ@ when
-- such @M@ exists, returns @Nothing@ otherwise.
--
-- * @FV(φ)@ must be a subset of @{x1,…,xn}@.
--
-- * @I@ is a set of integer variables and must be a subset of @{x1,…,xn}@.
--
solveQFLIRAConj :: Options -> VarSet -> [LA.Atom Rational] -> VarSet -> Maybe (Model Rational)
solveQFLIRAConj :: Options
-> VarSet
-> [Atom (Ratio Integer)]
-> VarSet
-> Maybe (Model (Ratio Integer))
solveQFLIRAConj Options
opt VarSet
vs [Atom (Ratio Integer)]
cs VarSet
ivs = [Model (Ratio Integer)] -> Maybe (Model (Ratio Integer))
forall a. [a] -> Maybe a
listToMaybe ([Model (Ratio Integer)] -> Maybe (Model (Ratio Integer)))
-> [Model (Ratio Integer)] -> Maybe (Model (Ratio Integer))
forall a b. (a -> b) -> a -> b
$ do
  ([Atom (Ratio Integer)]
cs2, Model (Ratio Integer) -> Model (Ratio Integer)
mt) <- VarSet
-> [Atom (Ratio Integer)]
-> [([Atom (Ratio Integer)],
     Model (Ratio Integer) -> Model (Ratio Integer))]
FM.projectN VarSet
rvs [Atom (Ratio Integer)]
cs
  Model Integer
m <- Maybe (Model Integer) -> [Model Integer]
forall a. Maybe a -> [a]
maybeToList (Maybe (Model Integer) -> [Model Integer])
-> Maybe (Model Integer) -> [Model Integer]
forall a b. (a -> b) -> a -> b
$ Options
-> VarSet -> [Atom (Ratio Integer)] -> Maybe (Model Integer)
solve Options
opt VarSet
ivs [Atom (Ratio Integer)]
cs2
  Model (Ratio Integer) -> [Model (Ratio Integer)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Model (Ratio Integer) -> [Model (Ratio Integer)])
-> Model (Ratio Integer) -> [Model (Ratio Integer)]
forall a b. (a -> b) -> a -> b
$ Model (Ratio Integer) -> Model (Ratio Integer)
mt (Model (Ratio Integer) -> Model (Ratio Integer))
-> Model (Ratio Integer) -> Model (Ratio Integer)
forall a b. (a -> b) -> a -> b
$ (Integer -> Ratio Integer)
-> Model Integer -> Model (Ratio Integer)
forall a b. (a -> b) -> IntMap a -> IntMap b
IM.map Integer -> Ratio Integer
forall a. Num a => Integer -> a
fromInteger Model Integer
m
  where
    rvs :: VarSet
rvs = VarSet
vs VarSet -> VarSet -> VarSet
`IS.difference` VarSet
ivs

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

zmod :: Integer -> Integer -> Integer
Integer
a zmod :: Integer -> Integer -> Integer
`zmod` Integer
b = Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
b Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Ratio Integer -> Integer
forall b. Integral b => Ratio Integer -> b
forall a b. (RealFrac a, Integral b) => a -> b
floor (Integer
a Integer -> Integer -> Ratio Integer
forall a. Integral a => a -> a -> Ratio a
% Integer
b Ratio Integer -> Ratio Integer -> Ratio Integer
forall a. Num a => a -> a -> a
+ Ratio Integer
1 Ratio Integer -> Ratio Integer -> Ratio Integer
forall a. Fractional a => a -> a -> a
/ Ratio Integer
2)

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

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]

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