{-# 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 vs as = isJust $ CAD.solve vs2 (map (fmap f) as)
  where
    vs2 = Set.fromAscList $ IS.toAscList vs

    f :: LA.Expr Rational -> P.Polynomial Rational Int
    f t = sum [ if x == LA.unitVar
                then P.constant c
                else P.constant c * P.var x
              | (c,x) <- LA.terms t ]

checkRealByVS :: VarSet -> [LA.Atom Rational] -> Bool
checkRealByVS vs as = isJust $ VS.solve vs as

checkRealBySimplex :: VarSet -> [LA.Atom Rational] -> Bool
checkRealBySimplex vs as = runST $ do
  solver <- Simplex.newSolver
  s <- liftM IM.fromAscList $ forM (IS.toAscList vs) $ \v -> do
    v2 <- Simplex.newVar solver
    return (v, LA.var v2)
  forM_ as $ \a -> do
    Simplex.assertAtomEx solver (fmap (LA.applySubst s) a)
  Simplex.check solver