{-# OPTIONS_GHC -Wall #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Arith.OmegaTest
-- Copyright   :  (c) Masahiro Sakai 2011
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  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
    (
    -- * Solving
      Model
    , solve
    , solveQFLIRAConj
    -- * Options for solving
    , Options (..)
    , checkRealNoCheck
    , checkRealByFM
    , checkRealByCAD
    , checkRealByVS
    , checkRealBySimplex
    ) where

import Control.Monad
import Control.Monad.ST
import qualified Data.IntMap as IM
import qualified Data.IntSet as IS
import Data.Maybe
import qualified Data.Set as Set

import qualified ToySolver.Data.LA as LA
import qualified ToySolver.Data.Polynomial as P
import ToySolver.Data.IntVar
import qualified ToySolver.Arith.CAD as CAD
import qualified ToySolver.Arith.Simplex as Simplex
import qualified ToySolver.Arith.VirtualSubstitution as VS
import ToySolver.Arith.OmegaTest.Base

checkRealByCAD :: VarSet -> [LA.Atom Rational] -> Bool
checkRealByCAD :: VarSet -> [Atom Rational] -> Bool
checkRealByCAD VarSet
vs [Atom Rational]
as = Maybe (Model Int) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Model Int) -> Bool) -> Maybe (Model Int) -> Bool
forall a b. (a -> b) -> a -> b
$ Set Int -> [OrdRel (Polynomial Rational Int)] -> Maybe (Model Int)
forall v.
(Ord v, Show v, PrettyVar v) =>
Set v -> [OrdRel (Polynomial Rational v)] -> Maybe (Model v)
CAD.solve Set Int
vs2 ((Atom Rational -> OrdRel (Polynomial Rational Int))
-> [Atom Rational] -> [OrdRel (Polynomial Rational Int)]
forall a b. (a -> b) -> [a] -> [b]
map ((Expr Rational -> Polynomial Rational Int)
-> Atom Rational -> OrdRel (Polynomial Rational Int)
forall a b. (a -> b) -> OrdRel a -> OrdRel b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr Rational -> Polynomial Rational Int
f) [Atom Rational]
as)
  where
    vs2 :: Set Int
vs2 = [Int] -> Set Int
forall a. Eq a => [a] -> Set a
Set.fromAscList ([Int] -> Set Int) -> [Int] -> Set Int
forall a b. (a -> b) -> a -> b
$ VarSet -> [Int]
IS.toAscList VarSet
vs

    f :: LA.Expr Rational -> P.Polynomial Rational Int
    f :: Expr Rational -> Polynomial Rational Int
f Expr Rational
t = [Polynomial Rational Int] -> Polynomial Rational Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [ if Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
LA.unitVar
                then Rational -> Polynomial Rational Int
forall k v. (Eq k, Num k) => k -> Polynomial k v
P.constant Rational
c
                else Rational -> Polynomial Rational Int
forall k v. (Eq k, Num k) => k -> Polynomial k v
P.constant Rational
c Polynomial Rational Int
-> Polynomial Rational Int -> Polynomial Rational Int
forall a. Num a => a -> a -> a
* Int -> Polynomial Rational Int
forall a v. Var a v => v -> a
P.var Int
x
              | (Rational
c,Int
x) <- Expr Rational -> [(Rational, Int)]
forall r. Expr r -> [(r, Int)]
LA.terms Expr Rational
t ]

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

checkRealBySimplex :: VarSet -> [LA.Atom Rational] -> Bool
checkRealBySimplex :: VarSet -> [Atom Rational] -> Bool
checkRealBySimplex VarSet
vs [Atom Rational]
as = (forall s. ST s Bool) -> Bool
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s Bool) -> Bool) -> (forall s. ST s Bool) -> Bool
forall a b. (a -> b) -> a -> b
$ do
  GenericSolverM (ST s) (Delta Rational)
solver <- ST s (GenericSolverM (ST s) (Delta Rational))
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
m (GenericSolverM m v)
Simplex.newSolver
  IntMap (Expr Rational)
s <- ([(Int, Expr Rational)] -> IntMap (Expr Rational))
-> ST s [(Int, Expr Rational)] -> ST s (IntMap (Expr Rational))
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [(Int, Expr Rational)] -> IntMap (Expr Rational)
forall a. [(Int, a)] -> IntMap a
IM.fromAscList (ST s [(Int, Expr Rational)] -> ST s (IntMap (Expr Rational)))
-> ST s [(Int, Expr Rational)] -> ST s (IntMap (Expr Rational))
forall a b. (a -> b) -> a -> b
$ [Int]
-> (Int -> ST s (Int, Expr Rational))
-> ST s [(Int, Expr Rational)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (VarSet -> [Int]
IS.toAscList VarSet
vs) ((Int -> ST s (Int, Expr Rational)) -> ST s [(Int, Expr Rational)])
-> (Int -> ST s (Int, Expr Rational))
-> ST s [(Int, Expr Rational)]
forall a b. (a -> b) -> a -> b
$ \Int
v -> do
    Int
v2 <- GenericSolverM (ST s) (Delta Rational) -> ST s Int
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m Int
Simplex.newVar GenericSolverM (ST s) (Delta Rational)
solver
    (Int, Expr Rational) -> ST s (Int, Expr Rational)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
v, Int -> Expr Rational
forall r. Num r => Int -> Expr r
LA.var Int
v2)
  [Atom Rational] -> (Atom Rational -> ST s ()) -> ST s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Atom Rational]
as ((Atom Rational -> ST s ()) -> ST s ())
-> (Atom Rational -> ST s ()) -> ST s ()
forall a b. (a -> b) -> a -> b
$ \Atom Rational
a -> do
    GenericSolverM (ST s) (Delta Rational) -> Atom Rational -> ST s ()
forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m (Delta Rational) -> Atom Rational -> m ()
Simplex.assertAtomEx GenericSolverM (ST s) (Delta Rational)
solver ((Expr Rational -> Expr Rational) -> Atom Rational -> Atom Rational
forall a b. (a -> b) -> OrdRel a -> OrdRel b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IntMap (Expr Rational) -> Expr Rational -> Expr Rational
forall r. (Num r, Eq r) => VarMap (Expr r) -> Expr r -> Expr r
LA.applySubst IntMap (Expr Rational)
s) Atom Rational
a)
  GenericSolverM (ST s) (Delta Rational) -> ST s Bool
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m Bool
Simplex.check GenericSolverM (ST s) (Delta Rational)
solver