-- Try running the convex hull algorithm.
--import Abs.Domain.SparsePolyhedra
--import Abs.Domain.SparsePolyhedra.Constraints
--import Abs.Domain.SparsePolyhedra.Types
--import Abs.Domain.SparsePolyhedra.Simplex
--
import Fake
import System.Environment (getArgs)
import Data.List (sort, sortBy)
import Control.Monad (replicateM, replicateM_, liftM, unless) 

-- Domain variables.

-- | Size of the buffer
s :: DomVar

-- | The character read
c :: DomVar

-- | The NUL position
sn :: DomVar

-- | The pointer offset of u
u :: DomVar

-- | The NUL position of v
vn :: DomVar

-- | The NUL position of p
tn :: DomVar

-- | A flag determining if sn = 4 or 6
f :: DomVar

-- | The pointer offset of p
p :: DomVar

(s:c:sn:u:tn:p:f:vn:_) = [1..] :: [DomVar]

main = do
  let size = 8
      initial = set u 0 $
		top size
  replicateM_ 1000 $ do
    res1 <- fixpoint initial bottom bottom vn 1
    unless (res1 `subset` res1) $ putStrLn "something's wrong"
    res2 <- fixpoint initial bottom bottom vn 1
    unless (res2 `subset` res2) $ putStrLn "something's wrong"


fixpoint :: Poly -> Poly -> Poly -> DomVar -> Integer -> IO Poly
fixpoint sU sT oldR sn fval = do
  let sR = join sU sT
  --putStrLn ("R:\n"++show sR)
  let sV = meetAsym [Constraint (Terms [(1,u)]) 8] sR
  if minimum [i+j | i <- [1..100], j <- [1..100]]<3 && sR `subset` sR then
    return sV else error "not reached" {-do
  let sT = assign 1 u (Constraint (Terms [(1,u)]) 1) sV
  fixpoint sU sT sR sn fval-}