    {-# LANGUAGE BangPatterns, PatternGuards, Trustworthy, CPP #-}
    {-|
    This module implements a decision procedure for quantifier-free linear
    arithmetic.  The algorithm is based on the following paper:

      An Online Proof-Producing Decision Procedure for
      Mixed-Integer Linear Arithmetic
      by
      Sergey Berezin, Vijay Ganesh, and David L. Dill
    -}
    module Data.Integer.SAT
      ( PropSet
      , noProps
      , checkSat
      , assert
      , Prop(..)
      , Expr(..)
      , BoundType(..)
      , getExprBound
      , getExprRange
      , Name
      , toName
      , fromName
      -- * Iterators
      , allSolutions
      , slnCurrent
      , slnNextVal
      , slnNextVar
      , slnEnumerate

      -- * Debug
      , dotPropSet
      , sizePropSet
      , allInerts
      , ppInerts

      -- * For QuickCheck
      , iPickBounded
      , Bound(..)
      , tConst
      ) where

    import Debug.Trace

    import           Control.Applicative (Alternative (..), Applicative (..), (<$>))
    import           Control.Monad       (MonadPlus (..), ap, guard, liftM)
    import           Data.List           (partition)
    import           Data.Map            (Map)
    import qualified Data.Map            as Map
    #if MIN_VERSION_containers(0,6,0)
    import qualified Data.Map.Strict     as MapStrict
    #endif
    import           Data.Maybe          (fromMaybe, mapMaybe, maybeToList)
    import           Prelude             hiding ((<>))
    import           Text.PrettyPrint

    infixr 2 :||
    infixr 3 :&&
    infix  4 :==, :/=, :<, :<=, :>, :>=
    infixl 6 :+, :-
    infixl 7 :*

    --------------------------------------------------------------------------------
    -- Solver interface

    -- | A collection of propositions.
    newtype PropSet = State (Answer RW)
                      deriving Int -> PropSet -> ShowS
    [PropSet] -> ShowS
    PropSet -> String
    (Int -> PropSet -> ShowS)
    -> (PropSet -> String) -> ([PropSet] -> ShowS) -> Show PropSet
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [PropSet] -> ShowS
    $cshowList :: [PropSet] -> ShowS
    show :: PropSet -> String
    $cshow :: PropSet -> String
    showsPrec :: Int -> PropSet -> ShowS
    $cshowsPrec :: Int -> PropSet -> ShowS
    Show

    dotPropSet :: PropSet -> Doc
    dotPropSet :: PropSet -> Doc
    dotPropSet (State a :: Answer RW
    a) = (RW -> Doc) -> Answer RW -> Doc
    forall a. (a -> Doc) -> Answer a -> Doc
    dotAnswer (Inerts -> Doc
    ppInerts (Inerts -> Doc) -> (RW -> Inerts) -> RW -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RW -> Inerts
    inerts) Answer RW
    a

    sizePropSet :: PropSet -> (Integer,Integer,Integer)
    sizePropSet :: PropSet -> (Integer, Integer, Integer)
    sizePropSet (State a :: Answer RW
    a) = Answer RW -> (Integer, Integer, Integer)
    forall a. Answer a -> (Integer, Integer, Integer)
    answerSize Answer RW
    a

    -- | An empty collection of propositions.
    noProps :: PropSet
    noProps :: PropSet
    noProps = Answer RW -> PropSet
    State (Answer RW -> PropSet) -> Answer RW -> PropSet
    forall a b. (a -> b) -> a -> b
    $ RW -> Answer RW
    forall (m :: * -> *) a. Monad m => a -> m a
    return RW
    initRW

    -- | Add a new proposition to an existing collection.
    assert :: Prop -> PropSet -> PropSet
    assert :: Prop -> PropSet -> PropSet
    assert p :: Prop
    p (State rws :: Answer RW
    rws) = Answer RW -> PropSet
    State (Answer RW -> PropSet) -> Answer RW -> PropSet
    forall a b. (a -> b) -> a -> b
    $ (((), RW) -> RW) -> Answer ((), RW) -> Answer RW
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((), RW) -> RW
    forall a b. (a, b) -> b
    snd (Answer ((), RW) -> Answer RW) -> Answer ((), RW) -> Answer RW
    forall a b. (a -> b) -> a -> b
    $ RW -> Answer ((), RW)
    m (RW -> Answer ((), RW)) -> Answer RW -> Answer ((), RW)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Answer RW
    rws
      where S m :: RW -> Answer ((), RW)
    m = Prop -> S ()
    prop Prop
    p

    -- | Extract a model from a consistent set of propositions.
    -- Returns 'Nothing' if the assertions have no model.
    -- If a variable does not appear in the assignment, then it is 0 (?).
    checkSat :: PropSet -> Maybe [(Int,Integer)]
    checkSat :: PropSet -> Maybe [(Int, Integer)]
    checkSat (State m :: Answer RW
    m) = Answer RW -> Maybe [(Int, Integer)]
    forall (m :: * -> *).
    MonadPlus m =>
    Answer RW -> m [(Int, Integer)]
    go Answer RW
    m
      where
      go :: Answer RW -> m [(Int, Integer)]
    go None           = m [(Int, Integer)]
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
      go (One rw :: RW
    rw)       = [(Int, Integer)] -> m [(Int, Integer)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [ (Int
    x,Integer
    v) | (UserName x :: Int
    x, v :: Integer
    v) <- Inerts -> [(Name, Integer)]
    iModel (RW -> Inerts
    inerts RW
    rw) ]
      go (Choice m1 :: Answer RW
    m1 m2 :: Answer RW
    m2) = m [(Int, Integer)] -> m [(Int, Integer)] -> m [(Int, Integer)]
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    mplus (Answer RW -> m [(Int, Integer)]
    go Answer RW
    m1) (Answer RW -> m [(Int, Integer)]
    go Answer RW
    m2)

    allInerts :: PropSet -> [Inerts]
    allInerts :: PropSet -> [Inerts]
    allInerts (State m :: Answer RW
    m) = (RW -> Inerts) -> [RW] -> [Inerts]
    forall a b. (a -> b) -> [a] -> [b]
    map RW -> Inerts
    inerts (Answer RW -> [RW]
    forall a. Answer a -> [a]
    toList Answer RW
    m)

    allSolutions :: PropSet -> [Solutions]
    allSolutions :: PropSet -> [Solutions]
    allSolutions = (Inerts -> Solutions) -> [Inerts] -> [Solutions]
    forall a b. (a -> b) -> [a] -> [b]
    map Inerts -> Solutions
    startIter ([Inerts] -> [Solutions])
    -> (PropSet -> [Inerts]) -> PropSet -> [Solutions]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PropSet -> [Inerts]
    allInerts

    -- | Computes bounds on the expression that are compatible with the model.
    -- Returns `Nothing` if the bound is not known.
    getExprBound :: BoundType -> Expr -> PropSet -> Maybe Integer
    getExprBound :: BoundType -> Expr -> PropSet -> Maybe Integer
    getExprBound bt :: BoundType
    bt e :: Expr
    e (State s :: Answer RW
    s) =
      do let S m :: RW -> Answer (Term, RW)
    m          = Expr -> S Term
    expr Expr
    e
             check :: (Term, RW) -> Maybe Integer
    check (t :: Term
    t,s1 :: RW
    s1) = BoundType -> Term -> Inerts -> Maybe Integer
    iTermBound BoundType
    bt Term
    t (RW -> Inerts
    inerts RW
    s1)
         [Integer]
    bs <- ((Term, RW) -> Maybe Integer) -> [(Term, RW)] -> Maybe [Integer]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Term, RW) -> Maybe Integer
    check ([(Term, RW)] -> Maybe [Integer])
    -> [(Term, RW)] -> Maybe [Integer]
    forall a b. (a -> b) -> a -> b
    $ Answer (Term, RW) -> [(Term, RW)]
    forall a. Answer a -> [a]
    toList (Answer (Term, RW) -> [(Term, RW)])
    -> Answer (Term, RW) -> [(Term, RW)]
    forall a b. (a -> b) -> a -> b
    $ Answer RW
    s Answer RW -> (RW -> Answer (Term, RW)) -> Answer (Term, RW)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= RW -> Answer (Term, RW)
    m
         case [Integer]
    bs of
           [] -> Maybe Integer
    forall a. Maybe a
    Nothing
           _  -> Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just ([Integer] -> Integer
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    maximum [Integer]
    bs)

    -- | Compute the range of possible values for an expression.
    -- Returns `Nothing` if the bound is not known.
    getExprRange :: Expr -> PropSet -> Maybe [Integer]
    getExprRange :: Expr -> PropSet -> Maybe [Integer]
    getExprRange e :: Expr
    e (State s :: Answer RW
    s) =
      do let S m :: RW -> Answer (Term, RW)
    m          = Expr -> S Term
    expr Expr
    e
             check :: (Term, RW) -> Maybe (Integer, Integer)
    check (t :: Term
    t,s1 :: RW
    s1) = do Integer
    l <- BoundType -> Term -> Inerts -> Maybe Integer
    iTermBound BoundType
    Lower Term
    t (RW -> Inerts
    inerts RW
    s1)
                               Integer
    u <- BoundType -> Term -> Inerts -> Maybe Integer
    iTermBound BoundType
    Upper Term
    t (RW -> Inerts
    inerts RW
    s1)
                               (Integer, Integer) -> Maybe (Integer, Integer)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer
    l,Integer
    u)
         [(Integer, Integer)]
    bs <- ((Term, RW) -> Maybe (Integer, Integer))
    -> [(Term, RW)] -> Maybe [(Integer, Integer)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Term, RW) -> Maybe (Integer, Integer)
    check ([(Term, RW)] -> Maybe [(Integer, Integer)])
    -> [(Term, RW)] -> Maybe [(Integer, Integer)]
    forall a b. (a -> b) -> a -> b
    $ Answer (Term, RW) -> [(Term, RW)]
    forall a. Answer a -> [a]
    toList (Answer (Term, RW) -> [(Term, RW)])
    -> Answer (Term, RW) -> [(Term, RW)]
    forall a b. (a -> b) -> a -> b
    $ Answer RW
    s Answer RW -> (RW -> Answer (Term, RW)) -> Answer (Term, RW)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= RW -> Answer (Term, RW)
    m
         case [(Integer, Integer)]
    bs of
           [] -> Maybe [Integer]
    forall a. Maybe a
    Nothing
           _  -> let (ls :: [Integer]
    ls,us :: [Integer]
    us) = [(Integer, Integer)] -> ([Integer], [Integer])
    forall a b. [(a, b)] -> ([a], [b])
    unzip [(Integer, Integer)]
    bs
                 in [Integer] -> Maybe [Integer]
    forall a. a -> Maybe a
    Just [ Integer
    x | Integer
    x <- [ [Integer] -> Integer
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    minimum [Integer]
    ls .. [Integer] -> Integer
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    maximum [Integer]
    us ] ]

    -- | The type of proposition.
    data Prop = PTrue
              | PFalse
              | Prop :|| Prop
              | Prop :&& Prop
              | Not Prop
              | Expr :== Expr
              | Expr :/= Expr
              | Expr :<  Expr
              | Expr :>  Expr
              | Expr :<= Expr
              | Expr :>= Expr
                deriving (ReadPrec [Prop]
    ReadPrec Prop
    Int -> ReadS Prop
    ReadS [Prop]
    (Int -> ReadS Prop)
    -> ReadS [Prop] -> ReadPrec Prop -> ReadPrec [Prop] -> Read Prop
    forall a.
    (Int -> ReadS a)
    -> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
    readListPrec :: ReadPrec [Prop]
    $creadListPrec :: ReadPrec [Prop]
    readPrec :: ReadPrec Prop
    $creadPrec :: ReadPrec Prop
    readList :: ReadS [Prop]
    $creadList :: ReadS [Prop]
    readsPrec :: Int -> ReadS Prop
    $creadsPrec :: Int -> ReadS Prop
    Read,Int -> Prop -> ShowS
    [Prop] -> ShowS
    Prop -> String
    (Int -> Prop -> ShowS)
    -> (Prop -> String) -> ([Prop] -> ShowS) -> Show Prop
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Prop] -> ShowS
    $cshowList :: [Prop] -> ShowS
    show :: Prop -> String
    $cshow :: Prop -> String
    showsPrec :: Int -> Prop -> ShowS
    $cshowsPrec :: Int -> Prop -> ShowS
    Show)

    -- | The type of integer expressions.
    -- Variable names must be non-negative.
    data Expr = Expr :+ Expr          -- ^ Addition
              | Expr :- Expr          -- ^ Subtraction
              | Integer :* Expr       -- ^ Multiplication by a constant
              | Negate Expr           -- ^ Negation
              | Var Name              -- ^ Variable
              | K Integer             -- ^ Constant
              | If Prop Expr Expr     -- ^ A conditional expression
              | Div Expr Integer      -- ^ Division, rounds down
              | Mod Expr Integer      -- ^ Non-negative remainder
                deriving (ReadPrec [Expr]
    ReadPrec Expr
    Int -> ReadS Expr
    ReadS [Expr]
    (Int -> ReadS Expr)
    -> ReadS [Expr] -> ReadPrec Expr -> ReadPrec [Expr] -> Read Expr
    forall a.
    (Int -> ReadS a)
    -> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
    readListPrec :: ReadPrec [Expr]
    $creadListPrec :: ReadPrec [Expr]
    readPrec :: ReadPrec Expr
    $creadPrec :: ReadPrec Expr
    readList :: ReadS [Expr]
    $creadList :: ReadS [Expr]
    readsPrec :: Int -> ReadS Expr
    $creadsPrec :: Int -> ReadS Expr
    Read,Int -> Expr -> ShowS
    [Expr] -> ShowS
    Expr -> String
    (Int -> Expr -> ShowS)
    -> (Expr -> String) -> ([Expr] -> ShowS) -> Show Expr
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Expr] -> ShowS
    $cshowList :: [Expr] -> ShowS
    show :: Expr -> String
    $cshow :: Expr -> String
    showsPrec :: Int -> Expr -> ShowS
    $cshowsPrec :: Int -> Expr -> ShowS
    Show)

    prop :: Prop -> S ()
    prop :: Prop -> S ()
    prop PTrue       = () -> S ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
    prop PFalse      = S ()
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
    prop (p1 :: Prop
    p1 :|| p2 :: Prop
    p2) = Prop -> S ()
    prop Prop
    p1 S () -> S () -> S ()
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    `mplus` Prop -> S ()
    prop Prop
    p2
    prop (p1 :: Prop
    p1 :&& p2 :: Prop
    p2) = Prop -> S ()
    prop Prop
    p1 S () -> S () -> S ()
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Prop -> S ()
    prop Prop
    p2
    prop (Not p :: Prop
    p)     = Prop -> S ()
    prop (Prop -> Prop
    neg Prop
    p)
      where
      neg :: Prop -> Prop
    neg PTrue       = Prop
    PFalse
      neg PFalse      = Prop
    PTrue
      neg (p1 :: Prop
    p1 :&& p2 :: Prop
    p2) = Prop -> Prop
    neg Prop
    p1 Prop -> Prop -> Prop
    :|| Prop -> Prop
    neg Prop
    p2
      neg (p1 :: Prop
    p1 :|| p2 :: Prop
    p2) = Prop -> Prop
    neg Prop
    p1 Prop -> Prop -> Prop
    :&& Prop -> Prop
    neg Prop
    p2
      neg (Not q :: Prop
    q)     = Prop
    q
      neg (e1 :: Expr
    e1 :== e2 :: Expr
    e2) = Expr
    e1 Expr -> Expr -> Prop
    :/= Expr
    e2
      neg (e1 :: Expr
    e1 :/= e2 :: Expr
    e2) = Expr
    e1 Expr -> Expr -> Prop
    :== Expr
    e2
      neg (e1 :: Expr
    e1 :<  e2 :: Expr
    e2) = Expr
    e1 Expr -> Expr -> Prop
    :>= Expr
    e2
      neg (e1 :: Expr
    e1 :<= e2 :: Expr
    e2) = Expr
    e1 Expr -> Expr -> Prop
    :>  Expr
    e2
      neg (e1 :: Expr
    e1 :>  e2 :: Expr
    e2) = Expr
    e1 Expr -> Expr -> Prop
    :<= Expr
    e2
      neg (e1 :: Expr
    e1 :>= e2 :: Expr
    e2) = Expr
    e1 Expr -> Expr -> Prop
    :<  Expr
    e2

    prop (e1 :: Expr
    e1 :== e2 :: Expr
    e2) = do Term
    t1 <- Expr -> S Term
    expr Expr
    e1
                          Term
    t2 <- Expr -> S Term
    expr Expr
    e2
                          Term -> S ()
    solveIs0 (Term
    t1 Term -> Term -> Term
    |-| Term
    t2)

    prop (e1 :: Expr
    e1 :/= e2 :: Expr
    e2)  = do Term
    t1 <- Expr -> S Term
    expr Expr
    e1
                           Term
    t2 <- Expr -> S Term
    expr Expr
    e2
                           let t :: Term
    t = Term
    t1 Term -> Term -> Term
    |-| Term
    t2
                           Term -> S ()
    solveIsNeg Term
    t S () -> S () -> S ()
    `orElse` Term -> S ()
    solveIsNeg (Term -> Term
    tNeg Term
    t)

    prop (e1 :: Expr
    e1 :< e2 :: Expr
    e2)   = do Term
    t1 <- Expr -> S Term
    expr Expr
    e1
                           Term
    t2 <- Expr -> S Term
    expr Expr
    e2
                           Term -> S ()
    solveIsNeg (Term
    t1 Term -> Term -> Term
    |-| Term
    t2)

    prop (e1 :: Expr
    e1 :<= e2 :: Expr
    e2)  = do Term
    t1 <- Expr -> S Term
    expr Expr
    e1
                           Term
    t2 <- Expr -> S Term
    expr Expr
    e2
                           let t :: Term
    t = Term
    t1 Term -> Term -> Term
    |-| Term
    t2 Term -> Term -> Term
    |-| Integer -> Term
    tConst 1
                           Term -> S ()
    solveIsNeg Term
    t

    prop (e1 :: Expr
    e1 :> e2 :: Expr
    e2)   = Prop -> S ()
    prop (Expr
    e2 Expr -> Expr -> Prop
    :<  Expr
    e1)
    prop (e1 :: Expr
    e1 :>= e2 :: Expr
    e2)  = Prop -> S ()
    prop (Expr
    e2 Expr -> Expr -> Prop
    :<= Expr
    e1)

    expr :: Expr -> S Term
    expr :: Expr -> S Term
    expr (e1 :: Expr
    e1 :+ e2 :: Expr
    e2)   = Term -> Term -> Term
    (|+|)   (Term -> Term -> Term) -> S Term -> S (Term -> Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> S Term
    expr Expr
    e1 S (Term -> Term) -> S Term -> S Term
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr -> S Term
    expr Expr
    e2
    expr (e1 :: Expr
    e1 :- e2 :: Expr
    e2)   = Term -> Term -> Term
    (|-|)   (Term -> Term -> Term) -> S Term -> S (Term -> Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> S Term
    expr Expr
    e1 S (Term -> Term) -> S Term -> S Term
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr -> S Term
    expr Expr
    e2
    expr (k :: Integer
    k  :* e2 :: Expr
    e2)   = (Integer
    k Integer -> Term -> Term
    |*|) (Term -> Term) -> S Term -> S Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> S Term
    expr Expr
    e2
    expr (Negate e :: Expr
    e)   = Term -> Term
    tNeg    (Term -> Term) -> S Term -> S Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> S Term
    expr Expr
    e
    expr (Var x :: Name
    x)      = Term -> S Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Name -> Term
    tVar Name
    x)
    expr (K x :: Integer
    x)        = Term -> S Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Term
    tConst Integer
    x)
    expr (If p :: Prop
    p e1 :: Expr
    e1 e2 :: Expr
    e2) = do Name
    x <- S Name
    newVar
                           Prop -> S ()
    prop (Prop
    p Prop -> Prop -> Prop
    :&& Name -> Expr
    Var Name
    x Expr -> Expr -> Prop
    :== Expr
    e1 Prop -> Prop -> Prop
    :|| Prop -> Prop
    Not Prop
    p Prop -> Prop -> Prop
    :&& Name -> Expr
    Var Name
    x Expr -> Expr -> Prop
    :== Expr
    e2)
                           Term -> S Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Name -> Term
    tVar Name
    x)
    expr (Div e :: Expr
    e k :: Integer
    k)    = ((Term, Term) -> Term) -> S (Term, Term) -> S Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Term, Term) -> Term
    forall a b. (a, b) -> a
    fst (S (Term, Term) -> S Term) -> S (Term, Term) -> S Term
    forall a b. (a -> b) -> a -> b
    $ Expr -> Integer -> S (Term, Term)
    exprDivMod Expr
    e Integer
    k
    expr (Mod e :: Expr
    e k :: Integer
    k)    = ((Term, Term) -> Term) -> S (Term, Term) -> S Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Term, Term) -> Term
    forall a b. (a, b) -> b
    snd (S (Term, Term) -> S Term) -> S (Term, Term) -> S Term
    forall a b. (a -> b) -> a -> b
    $ Expr -> Integer -> S (Term, Term)
    exprDivMod Expr
    e Integer
    k

    exprDivMod :: Expr -> Integer -> S (Term,Term)
    exprDivMod :: Expr -> Integer -> S (Term, Term)
    exprDivMod e :: Expr
    e k :: Integer
    k =
      do Bool -> S ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Integer
    k Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    /= 0) -- Always unsat
         Name
    q <- S Name
    newVar
         Name
    r <- S Name
    newVar
         let er :: Expr
    er = Name -> Expr
    Var Name
    r
         Prop -> S ()
    prop (Integer
    k Integer -> Expr -> Expr
    :* Name -> Expr
    Var Name
    q Expr -> Expr -> Expr
    :+ Expr
    er Expr -> Expr -> Prop
    :== Expr
    e Prop -> Prop -> Prop
    :&& Expr
    er Expr -> Expr -> Prop
    :< Integer -> Expr
    K Integer
    k Prop -> Prop -> Prop
    :&& Integer -> Expr
    K 0 Expr -> Expr -> Prop
    :<= Expr
    er)
         (Term, Term) -> S (Term, Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Name -> Term
    tVar Name
    q, Name -> Term
    tVar Name
    r)

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

    data RW = RW { RW -> Int
    nameSource :: !Int
                 , RW -> Inerts
    inerts     :: Inerts
                 } deriving Int -> RW -> ShowS
    [RW] -> ShowS
    RW -> String
    (Int -> RW -> ShowS)
    -> (RW -> String) -> ([RW] -> ShowS) -> Show RW
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [RW] -> ShowS
    $cshowList :: [RW] -> ShowS
    show :: RW -> String
    $cshow :: RW -> String
    showsPrec :: Int -> RW -> ShowS
    $cshowsPrec :: Int -> RW -> ShowS
    Show

    initRW :: RW
    initRW :: RW
    initRW = $WRW :: Int -> Inerts -> RW
    RW { nameSource :: Int
    nameSource = 0, inerts :: Inerts
    inerts = Inerts
    iNone }

    --------------------------------------------------------------------------------
    -- Constraints and Bound on Variables

    ctLt :: Term -> Term -> Term
    ctLt :: Term -> Term -> Term
    ctLt t1 :: Term
    t1 t2 :: Term
    t2 = Term
    t1 Term -> Term -> Term
    |-| Term
    t2

    ctEq :: Term -> Term -> Term
    ctEq :: Term -> Term -> Term
    ctEq t1 :: Term
    t1 t2 :: Term
    t2 = Term
    t1 Term -> Term -> Term
    |-| Term
    t2

    data Bound      = Bound Integer Term  -- ^ The integer is strictly positive
                      deriving Int -> Bound -> ShowS
    [Bound] -> ShowS
    Bound -> String
    (Int -> Bound -> ShowS)
    -> (Bound -> String) -> ([Bound] -> ShowS) -> Show Bound
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Bound] -> ShowS
    $cshowList :: [Bound] -> ShowS
    show :: Bound -> String
    $cshow :: Bound -> String
    showsPrec :: Int -> Bound -> ShowS
    $cshowsPrec :: Int -> Bound -> ShowS
    Show

    data BoundType  = Lower | Upper
                      deriving Int -> BoundType -> ShowS
    [BoundType] -> ShowS
    BoundType -> String
    (Int -> BoundType -> ShowS)
    -> (BoundType -> String)
    -> ([BoundType] -> ShowS)
    -> Show BoundType
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [BoundType] -> ShowS
    $cshowList :: [BoundType] -> ShowS
    show :: BoundType -> String
    $cshow :: BoundType -> String
    showsPrec :: Int -> BoundType -> ShowS
    $cshowsPrec :: Int -> BoundType -> ShowS
    Show

    toCt :: BoundType -> Name -> Bound -> Term
    toCt :: BoundType -> Name -> Bound -> Term
    toCt Lower x :: Name
    x (Bound c :: Integer
    c t :: Term
    t) = Term -> Term -> Term
    ctLt Term
    t              (Integer
    c Integer -> Term -> Term
    |*| Name -> Term
    tVar Name
    x)
    toCt Upper x :: Name
    x (Bound c :: Integer
    c t :: Term
    t) = Term -> Term -> Term
    ctLt (Integer
    c Integer -> Term -> Term
    |*| Name -> Term
    tVar Name
    x) Term
    t

    --------------------------------------------------------------------------------
    -- Inert set

    -- | The inert contains the solver state on one possible path.
    data Inerts = Inerts
      { Inerts -> NameMap ([Bound], [Bound])
    bounds :: NameMap ([Bound],[Bound])
        -- ^ Known lower and upper bounds for variables.
        -- Each bound @(c,t)@ in the first list asserts that  @t < c * x@
        -- Each bound @(c,t)@ in the second list asserts that @c * x < t@

      , Inerts -> NameMap Term
    solved :: NameMap Term
        -- ^ Definitions for resolved variables.
        -- These form an idempotent substitution.
      } deriving Int -> Inerts -> ShowS
    [Inerts] -> ShowS
    Inerts -> String
    (Int -> Inerts -> ShowS)
    -> (Inerts -> String) -> ([Inerts] -> ShowS) -> Show Inerts
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Inerts] -> ShowS
    $cshowList :: [Inerts] -> ShowS
    show :: Inerts -> String
    $cshow :: Inerts -> String
    showsPrec :: Int -> Inerts -> ShowS
    $cshowsPrec :: Int -> Inerts -> ShowS
    Show

    ppInerts :: Inerts -> Doc
    ppInerts :: Inerts -> Doc
    ppInerts is :: Inerts
    is = [Doc] -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [ Name -> Bound -> Doc
    ppLower Name
    x Bound
    b | (x :: Name
    x,(ls :: [Bound]
    ls,_)) <- [(Name, ([Bound], [Bound]))]
    bnds, Bound
    b <- [Bound]
    ls ] [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++
                         [ Name -> Bound -> Doc
    ppUpper Name
    x Bound
    b | (x :: Name
    x,(_,us :: [Bound]
    us)) <- [(Name, ([Bound], [Bound]))]
    bnds, Bound
    b <- [Bound]
    us ] [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++
                         [ (Name, Term) -> Doc
    ppEq (Name, Term)
    e      | (Name, Term)
    e <- NameMap Term -> [(Name, Term)]
    forall k a. Map k a -> [(k, a)]
    Map.toList (Inerts -> NameMap Term
    solved Inerts
    is) ]
      where
      bnds :: [(Name, ([Bound], [Bound]))]
    bnds = NameMap ([Bound], [Bound]) -> [(Name, ([Bound], [Bound]))]
    forall k a. Map k a -> [(k, a)]
    Map.toList (Inerts -> NameMap ([Bound], [Bound])
    bounds Inerts
    is)

      ppT :: Integer -> Name -> Doc
    ppT c :: Integer
    c x :: Name
    x                = Term -> Doc
    ppTerm (Integer
    c Integer -> Term -> Term
    |*| Name -> Term
    tVar Name
    x)
      ppLower :: Name -> Bound -> Doc
    ppLower x :: Name
    x (Bound c :: Integer
    c t :: Term
    t)  = Term -> Doc
    ppTerm Term
    t Doc -> Doc -> Doc
    <+> String -> Doc
    text "<" Doc -> Doc -> Doc
    <+> Integer -> Name -> Doc
    ppT Integer
    c Name
    x
      ppUpper :: Name -> Bound -> Doc
    ppUpper x :: Name
    x (Bound c :: Integer
    c t :: Term
    t)  = Integer -> Name -> Doc
    ppT Integer
    c Name
    x  Doc -> Doc -> Doc
    <+> String -> Doc
    text "<" Doc -> Doc -> Doc
    <+> Term -> Doc
    ppTerm Term
    t
      ppEq :: (Name, Term) -> Doc
    ppEq (x :: Name
    x,t :: Term
    t)             = Name -> Doc
    ppName Name
    x Doc -> Doc -> Doc
    <+> String -> Doc
    text "=" Doc -> Doc -> Doc
    <+> Term -> Doc
    ppTerm Term
    t

    -- | An empty inert set.
    iNone :: Inerts
    iNone :: Inerts
    iNone = Inerts :: NameMap ([Bound], [Bound]) -> NameMap Term -> Inerts
    Inerts { bounds :: NameMap ([Bound], [Bound])
    bounds = NameMap ([Bound], [Bound])
    forall k a. Map k a
    Map.empty
                   , solved :: NameMap Term
    solved = NameMap Term
    forall k a. Map k a
    Map.empty
                   }

    -- | Rewrite a term using the definitions from an inert set.
    iApSubst :: Inerts -> Term -> Term
    iApSubst :: Inerts -> Term -> Term
    iApSubst i :: Inerts
    i t :: Term
    t = ((Name, Term) -> Term -> Term) -> Term -> [(Name, Term)] -> Term
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (Name, Term) -> Term -> Term
    apS Term
    t ([(Name, Term)] -> Term) -> [(Name, Term)] -> Term
    forall a b. (a -> b) -> a -> b
    $ NameMap Term -> [(Name, Term)]
    forall k a. Map k a -> [(k, a)]
    Map.toList (NameMap Term -> [(Name, Term)]) -> NameMap Term -> [(Name, Term)]
    forall a b. (a -> b) -> a -> b
    $ Inerts -> NameMap Term
    solved Inerts
    i
      where apS :: (Name, Term) -> Term -> Term
    apS (x :: Name
    x,t1 :: Term
    t1) t2 :: Term
    t2 = Name -> Term -> Term -> Term
    tLet Name
    x Term
    t1 Term
    t2

    -- | Add a definition.  Upper and lower bound constraints that mention
    -- the variable are "kicked-out" so that they can be reinserted in the
    -- context of the new knowledge.
    --
    --    * Assumes substitution has already been applied.
    --
    --    * The kicked-out constraints are NOT rewritten, this happens
    --      when they get inserted in the work queue.

    iSolved :: Name -> Term -> Inerts -> ([Term], Inerts)
    iSolved :: Name -> Term -> Inerts -> ([Term], Inerts)
    iSolved x :: Name
    x t :: Term
    t i :: Inerts
    i =
      ( [Term]
    kickedOut
      , Inerts :: NameMap ([Bound], [Bound]) -> NameMap Term -> Inerts
    Inerts { bounds :: NameMap ([Bound], [Bound])
    bounds = NameMap ([Bound], [Bound])
    otherBounds
               , solved :: NameMap Term
    solved = Name -> Term -> NameMap Term -> NameMap Term
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert Name
    x Term
    t (NameMap Term -> NameMap Term) -> NameMap Term -> NameMap Term
    forall a b. (a -> b) -> a -> b
    $ (Term -> Term) -> NameMap Term -> NameMap Term
    forall a b k. (a -> b) -> Map k a -> Map k b
    Map.map (Name -> Term -> Term -> Term
    tLet Name
    x Term
    t) (NameMap Term -> NameMap Term) -> NameMap Term -> NameMap Term
    forall a b. (a -> b) -> a -> b
    $ Inerts -> NameMap Term
    solved Inerts
    i
               }
      )
      where
      (kickedOut :: [Term]
    kickedOut, otherBounds :: NameMap ([Bound], [Bound])
    otherBounds) =

            -- First, we eliminate all entries for `x`
        let (mb :: Maybe ([Bound], [Bound])
    mb, mp1 :: NameMap ([Bound], [Bound])
    mp1) = (Name -> ([Bound], [Bound]) -> Maybe ([Bound], [Bound]))
    -> Name
    -> NameMap ([Bound], [Bound])
    -> (Maybe ([Bound], [Bound]), NameMap ([Bound], [Bound]))
    forall k a.
    Ord k =>
    (k -> a -> Maybe a) -> k -> Map k a -> (Maybe a, Map k a)
    Map.updateLookupWithKey (\_ _ -> Maybe ([Bound], [Bound])
    forall a. Maybe a
    Nothing) Name
    x (Inerts -> NameMap ([Bound], [Bound])
    bounds Inerts
    i)

            -- Next, we elminate all constraints that mentiond `x` in bounds
            mp2 :: Map Name (([Bound], [Bound]), [Term])
    mp2 = (Name -> ([Bound], [Bound]) -> (([Bound], [Bound]), [Term]))
    -> NameMap ([Bound], [Bound])
    -> Map Name (([Bound], [Bound]), [Term])
    forall k a b. (k -> a -> b) -> Map k a -> Map k b
    Map.mapWithKey Name -> ([Bound], [Bound]) -> (([Bound], [Bound]), [Term])
    extractBounds NameMap ([Bound], [Bound])
    mp1

        in ( [ Term
    ct | (lbs :: [Bound]
    lbs,ubs :: [Bound]
    ubs) <- Maybe ([Bound], [Bound]) -> [([Bound], [Bound])]
    forall a. Maybe a -> [a]
    maybeToList Maybe ([Bound], [Bound])
    mb
                  ,  Term
    ct <- (Bound -> Term) -> [Bound] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (BoundType -> Name -> Bound -> Term
    toCt BoundType
    Lower Name
    x) [Bound]
    lbs [Term] -> [Term] -> [Term]
    forall a. [a] -> [a] -> [a]
    ++ (Bound -> Term) -> [Bound] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (BoundType -> Name -> Bound -> Term
    toCt BoundType
    Upper Name
    x) [Bound]
    ubs ]
             [Term] -> [Term] -> [Term]
    forall a. [a] -> [a] -> [a]
    ++
             [ Term
    ct | (_,cts :: [Term]
    cts) <- Map Name (([Bound], [Bound]), [Term])
    -> [(([Bound], [Bound]), [Term])]
    forall k a. Map k a -> [a]
    Map.elems Map Name (([Bound], [Bound]), [Term])
    mp2, Term
    ct <- [Term]
    cts ]

           , ((([Bound], [Bound]), [Term]) -> ([Bound], [Bound]))
    -> Map Name (([Bound], [Bound]), [Term])
    -> NameMap ([Bound], [Bound])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (([Bound], [Bound]), [Term]) -> ([Bound], [Bound])
    forall a b. (a, b) -> a
    fst Map Name (([Bound], [Bound]), [Term])
    mp2
           )

      extractBounds :: Name -> ([Bound], [Bound]) -> (([Bound], [Bound]), [Term])
    extractBounds y :: Name
    y (lbs :: [Bound]
    lbs,ubs :: [Bound]
    ubs) =
        let (lbsStay :: [Bound]
    lbsStay, lbsKick :: [Bound]
    lbsKick) = (Bound -> Bool) -> [Bound] -> ([Bound], [Bound])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    partition Bound -> Bool
    stay [Bound]
    lbs
            (ubsStay :: [Bound]
    ubsStay, ubsKick :: [Bound]
    ubsKick) = (Bound -> Bool) -> [Bound] -> ([Bound], [Bound])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    partition Bound -> Bool
    stay [Bound]
    ubs
        in ( ([Bound]
    lbsStay,[Bound]
    ubsStay)
           , (Bound -> Term) -> [Bound] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (BoundType -> Name -> Bound -> Term
    toCt BoundType
    Lower Name
    y) [Bound]
    lbsKick [Term] -> [Term] -> [Term]
    forall a. [a] -> [a] -> [a]
    ++
             (Bound -> Term) -> [Bound] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (BoundType -> Name -> Bound -> Term
    toCt BoundType
    Upper Name
    y) [Bound]
    ubsKick
           )

      stay :: Bound -> Bool
    stay (Bound _ bnd :: Term
    bnd) = Bool -> Bool
    not (Name -> Term -> Bool
    tHasVar Name
    x Term
    bnd)

    -- | Given some lower and upper bounds, find the interval the satisfies them.
    -- Note the upper and lower bounds are strict (i.e., < and >)
    boundInterval :: [Bound] -> [Bound] -> Maybe (Maybe Integer, Maybe Integer)
    boundInterval :: [Bound] -> [Bound] -> Maybe (Maybe Integer, Maybe Integer)
    boundInterval lbs :: [Bound]
    lbs ubs :: [Bound]
    ubs =
      do [Integer]
    ls <- (Bound -> Maybe Integer) -> [Bound] -> Maybe [Integer]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (BoundType -> Bound -> Maybe Integer
    normBound BoundType
    Lower) [Bound]
    lbs
         [Integer]
    us <- (Bound -> Maybe Integer) -> [Bound] -> Maybe [Integer]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (BoundType -> Bound -> Maybe Integer
    normBound BoundType
    Upper) [Bound]
    ubs
         let lb :: Maybe Integer
    lb = case [Integer]
    ls of
                    [] -> Maybe Integer
    forall a. Maybe a
    Nothing
                    _  -> Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just ([Integer] -> Integer
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    maximum [Integer]
    ls Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + 1)
             ub :: Maybe Integer
    ub = case [Integer]
    us of
                    [] -> Maybe Integer
    forall a. Maybe a
    Nothing
                    _  -> Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just ([Integer] -> Integer
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    minimum [Integer]
    us Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - 1)
         case (Maybe Integer
    lb,Maybe Integer
    ub) of
           (Just l :: Integer
    l, Just u :: Integer
    u) -> Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Integer
    l Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    u)
           _                -> () -> Maybe ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
         (Maybe Integer, Maybe Integer)
    -> Maybe (Maybe Integer, Maybe Integer)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Integer
    lb,Maybe Integer
    ub)
      where
      normBound :: BoundType -> Bound -> Maybe Integer
    normBound Lower (Bound c :: Integer
    c t :: Term
    t) = do Integer
    k <- Term -> Maybe Integer
    isConst Term
    t
                                       Integer -> Maybe Integer
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    div (Integer
    k Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    c Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - 1) Integer
    c)
      normBound Upper (Bound c :: Integer
    c t :: Term
    t) = do Integer
    k <- Term -> Maybe Integer
    isConst Term
    t
                                       Integer -> Maybe Integer
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    div Integer
    k Integer
    c)

    data Solutions = Done
                   | TopVar Name Integer (Maybe Integer) (Maybe Integer) Inerts
                   | FixedVar Name Integer Solutions
                      deriving Int -> Solutions -> ShowS
    [Solutions] -> ShowS
    Solutions -> String
    (Int -> Solutions -> ShowS)
    -> (Solutions -> String)
    -> ([Solutions] -> ShowS)
    -> Show Solutions
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Solutions] -> ShowS
    $cshowList :: [Solutions] -> ShowS
    show :: Solutions -> String
    $cshow :: Solutions -> String
    showsPrec :: Int -> Solutions -> ShowS
    $cshowsPrec :: Int -> Solutions -> ShowS
    Show

    slnCurrent :: Solutions -> [(Int,Integer)]
    slnCurrent :: Solutions -> [(Int, Integer)]
    slnCurrent s :: Solutions
    s = [ (Int
    x,Integer
    v) | (UserName x :: Int
    x, v :: Integer
    v) <- Solutions -> [(Name, Integer)]
    go Solutions
    s ]
      where
      go :: Solutions -> [(Name, Integer)]
    go Done                = []
      go (TopVar x :: Name
    x v :: Integer
    v _ _ is :: Inerts
    is) = (Name
    x, Integer
    v) (Name, Integer) -> [(Name, Integer)] -> [(Name, Integer)]
    forall a. a -> [a] -> [a]
    : Inerts -> [(Name, Integer)]
    iModel (Name -> Integer -> Inerts -> Inerts
    iLet Name
    x Integer
    v Inerts
    is)
      go (FixedVar x :: Name
    x v :: Integer
    v i :: Solutions
    i)    = (Name
    x, Integer
    v) (Name, Integer) -> [(Name, Integer)] -> [(Name, Integer)]
    forall a. a -> [a] -> [a]
    : Solutions -> [(Name, Integer)]
    go Solutions
    i

    -- | Replace occurances of a variable with an integer.
    -- WARNING: The integer should be a valid value for the variable.
    iLet :: Name -> Integer -> Inerts -> Inerts
    iLet :: Name -> Integer -> Inerts -> Inerts
    iLet x :: Name
    x v :: Integer
    v is :: Inerts
    is = Inerts :: NameMap ([Bound], [Bound]) -> NameMap Term -> Inerts
    Inerts { bounds :: NameMap ([Bound], [Bound])
    bounds = (([Bound], [Bound]) -> ([Bound], [Bound]))
    -> NameMap ([Bound], [Bound]) -> NameMap ([Bound], [Bound])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ([Bound], [Bound]) -> ([Bound], [Bound])
    updBs (Inerts -> NameMap ([Bound], [Bound])
    bounds Inerts
    is)
                         , solved :: NameMap Term
    solved = (Term -> Term) -> NameMap Term -> NameMap Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Name -> Integer -> Term -> Term
    tLetNum Name
    x Integer
    v) (Inerts -> NameMap Term
    solved Inerts
    is) }
      where
      updB :: Bound -> Bound
    updB (Bound c :: Integer
    c t :: Term
    t) = Integer -> Term -> Bound
    Bound Integer
    c (Name -> Integer -> Term -> Term
    tLetNum Name
    x Integer
    v Term
    t)
      updBs :: ([Bound], [Bound]) -> ([Bound], [Bound])
    updBs (ls :: [Bound]
    ls,us :: [Bound]
    us)    = ((Bound -> Bound) -> [Bound] -> [Bound]
    forall a b. (a -> b) -> [a] -> [b]
    map Bound -> Bound
    updB [Bound]
    ls, (Bound -> Bound) -> [Bound] -> [Bound]
    forall a b. (a -> b) -> [a] -> [b]
    map Bound -> Bound
    updB [Bound]
    us)

    startIter :: Inerts -> Solutions
    startIter :: Inerts -> Solutions
    startIter is :: Inerts
    is =
      case NameMap ([Bound], [Bound])
    -> Maybe ((Name, ([Bound], [Bound])), NameMap ([Bound], [Bound]))
    forall k a. Map k a -> Maybe ((k, a), Map k a)
    Map.maxViewWithKey (Inerts -> NameMap ([Bound], [Bound])
    bounds Inerts
    is) of
        Nothing ->
          case NameMap Term -> Maybe ((Name, Term), NameMap Term)
    forall k a. Map k a -> Maybe ((k, a), Map k a)
    Map.maxViewWithKey (Inerts -> NameMap Term
    solved Inerts
    is) of
            Nothing -> Solutions
    Done
            Just ((x :: Name
    x,t :: Term
    t), mp1 :: NameMap Term
    mp1) ->
              case [ Name
    y | Name
    y <- Term -> [Name]
    tVarList Term
    t ] of
                y :: Name
    y : _ -> Name
    -> Integer -> Maybe Integer -> Maybe Integer -> Inerts -> Solutions
    TopVar Name
    y 0 Maybe Integer
    forall a. Maybe a
    Nothing Maybe Integer
    forall a. Maybe a
    Nothing Inerts
    is
                [] -> let v :: Integer
    v = Term -> Integer
    tConstPart Term
    t
                      in Name
    -> Integer -> Maybe Integer -> Maybe Integer -> Inerts -> Solutions
    TopVar Name
    x Integer
    v (Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    v) (Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    v) (Inerts -> Solutions) -> Inerts -> Solutions
    forall a b. (a -> b) -> a -> b
    $ Inerts
    is { solved :: NameMap Term
    solved = NameMap Term
    mp1 }
        Just ((x :: Name
    x,(lbs :: [Bound]
    lbs,ubs :: [Bound]
    ubs)), mp1 :: NameMap ([Bound], [Bound])
    mp1) ->
          case [ Name
    y | Bound _ t :: Term
    t <- [Bound]
    lbs [Bound] -> [Bound] -> [Bound]
    forall a. [a] -> [a] -> [a]
    ++ [Bound]
    ubs, Name
    y <- Term -> [Name]
    tVarList Term
    t ] of
            y :: Name
    y : _ -> Name
    -> Integer -> Maybe Integer -> Maybe Integer -> Inerts -> Solutions
    TopVar Name
    y 0 Maybe Integer
    forall a. Maybe a
    Nothing Maybe Integer
    forall a. Maybe a
    Nothing Inerts
    is
            [] -> case [Bound] -> [Bound] -> Maybe (Maybe Integer, Maybe Integer)
    boundInterval [Bound]
    lbs [Bound]
    ubs of
                    Nothing -> String -> Solutions
    forall a. HasCallStack => String -> a
    error "bug: cannot compute interval?"
                    Just (lb :: Maybe Integer
    lb,ub :: Maybe Integer
    ub) ->
                      let v :: Integer
    v = Integer -> Maybe Integer -> Integer
    forall a. a -> Maybe a -> a
    fromMaybe 0 (Maybe Integer -> Maybe Integer -> Maybe Integer
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    mplus Maybe Integer
    lb Maybe Integer
    ub)
                      in Name
    -> Integer -> Maybe Integer -> Maybe Integer -> Inerts -> Solutions
    TopVar Name
    x Integer
    v Maybe Integer
    lb Maybe Integer
    ub (Inerts -> Solutions) -> Inerts -> Solutions
    forall a b. (a -> b) -> a -> b
    $ Inerts
    is { bounds :: NameMap ([Bound], [Bound])
    bounds = NameMap ([Bound], [Bound])
    mp1 }

    slnEnumerate :: Solutions -> [ Solutions ]
    slnEnumerate :: Solutions -> [Solutions]
    slnEnumerate s0 :: Solutions
    s0 = Solutions -> [Solutions] -> [Solutions]
    go Solutions
    s0 []
      where
      go :: Solutions -> [Solutions] -> [Solutions]
    go s :: Solutions
    s k :: [Solutions]
    k  = case Solutions -> Maybe Solutions
    slnNextVar Solutions
    s of
                  Nothing -> Solutions -> [Solutions] -> [Solutions]
    hor Solutions
    s [Solutions]
    k
                  Just s1 :: Solutions
    s1 -> Solutions -> [Solutions] -> [Solutions]
    go Solutions
    s1 ([Solutions] -> [Solutions]) -> [Solutions] -> [Solutions]
    forall a b. (a -> b) -> a -> b
    $ case Solutions -> Maybe Solutions
    slnNextVal Solutions
    s of
                                       Nothing -> [Solutions]
    k
                                       Just s2 :: Solutions
    s2 -> Solutions -> [Solutions] -> [Solutions]
    go Solutions
    s2 [Solutions]
    k

      hor :: Solutions -> [Solutions] -> [Solutions]
    hor s :: Solutions
    s k :: [Solutions]
    k = Solutions
    s
              Solutions -> [Solutions] -> [Solutions]
    forall a. a -> [a] -> [a]
    : case Solutions -> Maybe Solutions
    slnNextVal Solutions
    s of
                  Nothing -> [Solutions]
    k
                  Just s1 :: Solutions
    s1 -> Solutions -> [Solutions] -> [Solutions]
    hor Solutions
    s1 [Solutions]
    k

    slnNextVal :: Solutions -> Maybe Solutions
    slnNextVal :: Solutions -> Maybe Solutions
    slnNextVal Done = Maybe Solutions
    forall a. Maybe a
    Nothing
    slnNextVal (FixedVar x :: Name
    x v :: Integer
    v i :: Solutions
    i) = Name -> Integer -> Solutions -> Solutions
    FixedVar Name
    x Integer
    v (Solutions -> Solutions) -> Maybe Solutions -> Maybe Solutions
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` Solutions -> Maybe Solutions
    slnNextVal Solutions
    i
    slnNextVal it :: Solutions
    it@(TopVar _ _ lb :: Maybe Integer
    lb _ _) =
      case Maybe Integer
    lb of
        Just _  -> (Integer -> Integer) -> Solutions -> Maybe Solutions
    slnNextValWith (Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +1) Solutions
    it
        Nothing -> (Integer -> Integer) -> Solutions -> Maybe Solutions
    slnNextValWith (Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    subtract 1) Solutions
    it

    slnNextValWith :: (Integer -> Integer) -> Solutions -> Maybe Solutions
    slnNextValWith :: (Integer -> Integer) -> Solutions -> Maybe Solutions
    slnNextValWith _ Done = Maybe Solutions
    forall a. Maybe a
    Nothing
    slnNextValWith f :: Integer -> Integer
    f (FixedVar x :: Name
    x v :: Integer
    v i :: Solutions
    i) = Name -> Integer -> Solutions -> Solutions
    FixedVar Name
    x Integer
    v (Solutions -> Solutions) -> Maybe Solutions -> Maybe Solutions
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` (Integer -> Integer) -> Solutions -> Maybe Solutions
    slnNextValWith Integer -> Integer
    f Solutions
    i
    slnNextValWith f :: Integer -> Integer
    f (TopVar x :: Name
    x v :: Integer
    v lb :: Maybe Integer
    lb ub :: Maybe Integer
    ub is :: Inerts
    is) =
      do let v1 :: Integer
    v1 = Integer -> Integer
    f Integer
    v
         case Maybe Integer
    lb of
           Just l :: Integer
    l  -> Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Integer
    l Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    v1)
           Nothing -> () -> Maybe ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
         case Maybe Integer
    ub of
           Just u :: Integer
    u  -> Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Integer
    v1 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    u)
           Nothing -> () -> Maybe ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
         Solutions -> Maybe Solutions
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Solutions -> Maybe Solutions) -> Solutions -> Maybe Solutions
    forall a b. (a -> b) -> a -> b
    $ Name
    -> Integer -> Maybe Integer -> Maybe Integer -> Inerts -> Solutions
    TopVar Name
    x Integer
    v1 Maybe Integer
    lb Maybe Integer
    ub Inerts
    is

    slnNextVar :: Solutions -> Maybe Solutions
    slnNextVar :: Solutions -> Maybe Solutions
    slnNextVar Done                = Maybe Solutions
    forall a. Maybe a
    Nothing
    slnNextVar (TopVar x :: Name
    x v :: Integer
    v _ _ is :: Inerts
    is) = Solutions -> Maybe Solutions
    forall a. a -> Maybe a
    Just (Solutions -> Maybe Solutions) -> Solutions -> Maybe Solutions
    forall a b. (a -> b) -> a -> b
    $ Name -> Integer -> Solutions -> Solutions
    FixedVar Name
    x Integer
    v (Solutions -> Solutions) -> Solutions -> Solutions
    forall a b. (a -> b) -> a -> b
    $ Inerts -> Solutions
    startIter (Inerts -> Solutions) -> Inerts -> Solutions
    forall a b. (a -> b) -> a -> b
    $ Name -> Integer -> Inerts -> Inerts
    iLet Name
    x Integer
    v Inerts
    is
    slnNextVar (FixedVar x :: Name
    x v :: Integer
    v i :: Solutions
    i)    = Name -> Integer -> Solutions -> Solutions
    FixedVar Name
    x Integer
    v (Solutions -> Solutions) -> Maybe Solutions -> Maybe Solutions
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` Solutions -> Maybe Solutions
    slnNextVar Solutions
    i

    -- Given a list of lower (resp. upper) bounds, compute the least (resp. largest)
    -- value that satisfies them all.
    iPickBounded :: BoundType -> [Bound] -> Maybe Integer
    iPickBounded :: BoundType -> [Bound] -> Maybe Integer
    iPickBounded _ [] = Maybe Integer
    forall a. Maybe a
    Nothing
    iPickBounded bt :: BoundType
    bt bs :: [Bound]
    bs =
      do [Integer]
    xs <- (Bound -> Maybe Integer) -> [Bound] -> Maybe [Integer]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (BoundType -> Bound -> Maybe Integer
    normBound BoundType
    bt) [Bound]
    bs
         Integer -> Maybe Integer
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer -> Maybe Integer) -> Integer -> Maybe Integer
    forall a b. (a -> b) -> a -> b
    $ case BoundType
    bt of
                    Lower -> [Integer] -> Integer
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    maximum [Integer]
    xs
                    Upper -> [Integer] -> Integer
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    minimum [Integer]
    xs
      where
      -- t < c*x
      -- <=> t+1 <= c*x
      -- <=> (t+1)/c <= x
      -- <=> ceil((t+1)/c) <= x
      -- <=> t `div` c + 1 <= x
      normBound :: BoundType -> Bound -> Maybe Integer
    normBound Lower (Bound c :: Integer
    c t :: Term
    t) = do Integer
    k <- Term -> Maybe Integer
    isConst Term
    t
                                       Integer -> Maybe Integer
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer
    k Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `div` Integer
    c Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + 1)
      -- c*x < t
      -- <=> c*x <= t-1
      -- <=> x   <= (t-1)/c
      -- <=> x   <= floor((t-1)/c)
      -- <=> x   <= (t-1) `div` c
      normBound Upper (Bound c :: Integer
    c t :: Term
    t) = do Integer
    k <- Term -> Maybe Integer
    isConst Term
    t
                                       Integer -> Maybe Integer
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    div (Integer
    kInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -1) Integer
    c)

    -- | The largest (resp. least) upper (resp. lower) bound on a term
    -- that will satisfy the model
    iTermBound :: BoundType -> Term -> Inerts -> Maybe Integer
    iTermBound :: BoundType -> Term -> Inerts -> Maybe Integer
    iTermBound bt :: BoundType
    bt (T k :: Integer
    k xs :: NameMap Integer
    xs) is :: Inerts
    is = do [Integer]
    ks <- ((Name, Integer) -> Maybe Integer)
    -> [(Name, Integer)] -> Maybe [Integer]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Name, Integer) -> Maybe Integer
    summand (NameMap Integer -> [(Name, Integer)]
    forall k a. Map k a -> [(k, a)]
    Map.toList NameMap Integer
    xs)
                                   Integer -> Maybe Integer
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer -> Maybe Integer) -> Integer -> Maybe Integer
    forall a b. (a -> b) -> a -> b
    $ [Integer] -> Integer
    forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
    sum ([Integer] -> Integer) -> [Integer] -> Integer
    forall a b. (a -> b) -> a -> b
    $ Integer
    k Integer -> [Integer] -> [Integer]
    forall a. a -> [a] -> [a]
    : [Integer]
    ks
      where
      summand :: (Name, Integer) -> Maybe Integer
    summand (x :: Name
    x,c :: Integer
    c) = (Integer -> Integer) -> Maybe Integer -> Maybe Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Integer
    c Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    *) (BoundType -> Name -> Inerts -> Maybe Integer
    iVarBound (Integer -> BoundType
    forall a. (Ord a, Num a) => a -> BoundType
    newBt Integer
    c) Name
    x Inerts
    is)
      newBt :: a -> BoundType
    newBt c :: a
    c = if a
    c a -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    > 0 then BoundType
    bt else case BoundType
    bt of
                                        Lower -> BoundType
    Upper
                                        Upper -> BoundType
    Lower

    -- | The largest (resp. least) upper (resp. lower) bound on a variable
    -- that will satisfy the model.
    iVarBound :: BoundType -> Name -> Inerts -> Maybe Integer
    iVarBound :: BoundType -> Name -> Inerts -> Maybe Integer
    iVarBound bt :: BoundType
    bt x :: Name
    x is :: Inerts
    is
      | Just t :: Term
    t <- Name -> NameMap Term -> Maybe Term
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    x (Inerts -> NameMap Term
    solved Inerts
    is) = BoundType -> Term -> Inerts -> Maybe Integer
    iTermBound BoundType
    bt Term
    t Inerts
    is

    iVarBound bt :: BoundType
    bt x :: Name
    x is :: Inerts
    is =
      do ([Bound], [Bound])
    both <- Name -> NameMap ([Bound], [Bound]) -> Maybe ([Bound], [Bound])
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    x (Inerts -> NameMap ([Bound], [Bound])
    bounds Inerts
    is)
         case (Bound -> Maybe Integer) -> [Bound] -> [Integer]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe Bound -> Maybe Integer
    fromBound (([Bound], [Bound]) -> [Bound]
    forall b. (b, b) -> b
    chooseBounds ([Bound], [Bound])
    both) of
           [] -> Maybe Integer
    forall a. Maybe a
    Nothing
           bs :: [Integer]
    bs -> Integer -> Maybe Integer
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Integer] -> Integer
    combineBounds [Integer]
    bs)
      where
      fromBound :: Bound -> Maybe Integer
    fromBound (Bound c :: Integer
    c t :: Term
    t) = (Integer -> Integer) -> Maybe Integer -> Maybe Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    scaleBound Integer
    c) (BoundType -> Term -> Inerts -> Maybe Integer
    iTermBound BoundType
    bt Term
    t Inerts
    is)

      combineBounds :: [Integer] -> Integer
    combineBounds = case BoundType
    bt of
                        Upper -> [Integer] -> Integer
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    minimum
                        Lower -> [Integer] -> Integer
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    maximum

      chooseBounds :: (b, b) -> b
    chooseBounds = case BoundType
    bt of
                       Upper -> (b, b) -> b
    forall a b. (a, b) -> b
    snd
                       Lower -> (b, b) -> b
    forall a b. (a, b) -> a
    fst

      scaleBound :: a -> a -> a
    scaleBound c :: a
    c b :: a
    b = case BoundType
    bt of
                         Upper -> a -> a -> a
    forall a. Integral a => a -> a -> a
    div (a
    ba -> a -> a
    forall a. Num a => a -> a -> a
    -1) a
    c
                         Lower -> a -> a -> a
    forall a. Integral a => a -> a -> a
    div a
    b a
    c a -> a -> a
    forall a. Num a => a -> a -> a
    + 1

    iModel :: Inerts -> [(Name,Integer)]
    iModel :: Inerts -> [(Name, Integer)]
    iModel i :: Inerts
    i = [(Name, Integer)]
    -> NameMap ([Bound], [Bound]) -> [(Name, Integer)]
    goBounds [] (Inerts -> NameMap ([Bound], [Bound])
    bounds Inerts
    i)
      where
      goBounds :: [(Name, Integer)]
    -> NameMap ([Bound], [Bound]) -> [(Name, Integer)]
    goBounds su :: [(Name, Integer)]
    su mp :: NameMap ([Bound], [Bound])
    mp =
        case NameMap ([Bound], [Bound])
    -> Maybe ((Name, ([Bound], [Bound])), NameMap ([Bound], [Bound]))
    forall k a. Map k a -> Maybe ((k, a), Map k a)
    Map.maxViewWithKey NameMap ([Bound], [Bound])
    mp of
          Nothing -> [(Name, Integer)] -> [(Name, Term)] -> [(Name, Integer)]
    goEqs [(Name, Integer)]
    su ([(Name, Term)] -> [(Name, Integer)])
    -> [(Name, Term)] -> [(Name, Integer)]
    forall a b. (a -> b) -> a -> b
    $ NameMap Term -> [(Name, Term)]
    forall k a. Map k a -> [(k, a)]
    Map.toList (NameMap Term -> [(Name, Term)]) -> NameMap Term -> [(Name, Term)]
    forall a b. (a -> b) -> a -> b
    $ Inerts -> NameMap Term
    solved Inerts
    i
          Just ((x :: Name
    x,(lbs0 :: [Bound]
    lbs0,ubs0 :: [Bound]
    ubs0)), mp1 :: NameMap ([Bound], [Bound])
    mp1) ->
            let lbs :: [Bound]
    lbs = [ Integer -> Term -> Bound
    Bound Integer
    c ([(Name, Integer)] -> Term -> Term
    tLetNums [(Name, Integer)]
    su Term
    t) | Bound c :: Integer
    c t :: Term
    t <- [Bound]
    lbs0 ]
                ubs :: [Bound]
    ubs = [ Integer -> Term -> Bound
    Bound Integer
    c ([(Name, Integer)] -> Term -> Term
    tLetNums [(Name, Integer)]
    su Term
    t) | Bound c :: Integer
    c t :: Term
    t <- [Bound]
    ubs0 ]
                sln :: Integer
    sln = Integer -> Maybe Integer -> Integer
    forall a. a -> Maybe a -> a
    fromMaybe 0
                    (Maybe Integer -> Integer) -> Maybe Integer -> Integer
    forall a b. (a -> b) -> a -> b
    $ Maybe Integer -> Maybe Integer -> Maybe Integer
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    mplus (BoundType -> [Bound] -> Maybe Integer
    iPickBounded BoundType
    Lower [Bound]
    lbs) (BoundType -> [Bound] -> Maybe Integer
    iPickBounded BoundType
    Upper [Bound]
    ubs)
            in [(Name, Integer)]
    -> NameMap ([Bound], [Bound]) -> [(Name, Integer)]
    goBounds ((Name
    x,Integer
    sln) (Name, Integer) -> [(Name, Integer)] -> [(Name, Integer)]
    forall a. a -> [a] -> [a]
    : [(Name, Integer)]
    su) NameMap ([Bound], [Bound])
    mp1

      goEqs :: [(Name, Integer)] -> [(Name, Term)] -> [(Name, Integer)]
    goEqs su :: [(Name, Integer)]
    su [] = [(Name, Integer)]
    su
      goEqs su :: [(Name, Integer)]
    su ((x :: Name
    x,t :: Term
    t) : more :: [(Name, Term)]
    more) =
        let t1 :: Term
    t1  = [(Name, Integer)] -> Term -> Term
    tLetNums [(Name, Integer)]
    su Term
    t
            vs :: [Name]
    vs  = Term -> [Name]
    tVarList Term
    t1
            su1 :: [(Name, Integer)]
    su1 = [ (Name
    v,0) | Name
    v <- [Name]
    vs ] [(Name, Integer)] -> [(Name, Integer)] -> [(Name, Integer)]
    forall a. [a] -> [a] -> [a]
    ++ (Name
    x,Term -> Integer
    tConstPart Term
    t1) (Name, Integer) -> [(Name, Integer)] -> [(Name, Integer)]
    forall a. a -> [a] -> [a]
    : [(Name, Integer)]
    su
        in [(Name, Integer)] -> [(Name, Term)] -> [(Name, Integer)]
    goEqs [(Name, Integer)]
    su1 [(Name, Term)]
    more

    --------------------------------------------------------------------------------
    -- Solving constraints

    solveIs0 :: Term -> S ()
    solveIs0 :: Term -> S ()
    solveIs0 t :: Term
    t = Term -> S ()
    solveIs0' (Term -> S ()) -> S Term -> S ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Term -> S Term
    apSubst Term
    t

    -- | Solve a constraint if the form @t = 0@.
    -- Assumes substitution has already been applied.
    solveIs0' :: Term -> S ()
    solveIs0' :: Term -> S ()
    solveIs0' t :: Term
    t

      -- A == 0
      | Just a :: Integer
    a <- Term -> Maybe Integer
    isConst Term
    t = Bool -> S ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Integer
    a Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0)

      -- A + B * x = 0
      | Just (a :: Integer
    a,b :: Integer
    b,x :: Name
    x) <- Term -> Maybe (Integer, Integer, Name)
    tIsOneVar Term
    t =
        case Integer -> Integer -> (Integer, Integer)
    forall a. Integral a => a -> a -> (a, a)
    divMod (-Integer
    a) Integer
    b of
          (q :: Integer
    q,0) -> Name -> Term -> S ()
    addDef Name
    x (Integer -> Term
    tConst Integer
    q)
          _     -> S ()
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

      --  x + S = 0
      -- -x + S = 0
      | Just (xc :: Integer
    xc,x :: Name
    x,s :: Term
    s) <- Term -> Maybe (Integer, Name, Term)
    tGetSimpleCoeff Term
    t =
        Name -> Term -> S ()
    addDef Name
    x (if Integer
    xc Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > 0 then Term -> Term
    tNeg Term
    s else Term
    s)

      -- A * S = 0
      | Just (_, s :: Term
    s) <- Term -> Maybe (Integer, Term)
    tFactor Term
    t  = Term -> S ()
    solveIs0 Term
    s

      -- See Section 3.1 of paper for details.
      -- We obtain an equivalent formulation but with smaller coefficients.
      | Just (ak :: Integer
    ak,xk :: Name
    xk,s :: Term
    s) <- Term -> Maybe (Integer, Name, Term)
    tLeastAbsCoeff Term
    t =
          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
    + 1
             Name
    v <- S Name
    newVar
             let sgn :: Integer
    sgn  = Integer -> Integer
    forall a. Num a => a -> a
    signum Integer
    ak
                 soln :: Term
    soln =     (Integer -> Integer
    forall a. Num a => a -> a
    negate Integer
    sgn Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    m) Integer -> Term -> Term
    |*| Name -> Term
    tVar Name
    v
                        Term -> Term -> Term
    |+| (Integer -> Integer) -> Term -> Term
    tMapCoeff (\c :: Integer
    c -> Integer
    sgn Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer -> Integer -> Integer
    modulus Integer
    c Integer
    m) Term
    s
             Name -> Term -> S ()
    addDef Name
    xk Term
    soln

             let upd :: Integer -> Integer
    upd i :: Integer
    i = Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    div (2Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    *Integer
    i Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    m) (2Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    *Integer
    m) Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer -> Integer -> Integer
    modulus Integer
    i Integer
    m
             Term -> S ()
    solveIs0 (Integer -> Integer
    forall a. Num a => a -> a
    negate (Integer -> Integer
    forall a. Num a => a -> a
    abs Integer
    ak) Integer -> Term -> Term
    |*| Name -> Term
    tVar Name
    v Term -> Term -> Term
    |+| (Integer -> Integer) -> Term -> Term
    tMapCoeff Integer -> Integer
    upd Term
    s)

      | Bool
    otherwise = String -> S ()
    forall a. HasCallStack => String -> a
    error "solveIs0: unreachable"

    modulus :: Integer -> Integer -> Integer
    modulus :: Integer -> Integer -> Integer
    modulus a :: Integer
    a m :: Integer
    m = Integer
    a Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    m Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    div (2 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    a Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    m) (2 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    m)

    solveIsNeg :: Term -> S ()
    solveIsNeg :: Term -> S ()
    solveIsNeg t :: Term
    t = Term -> S ()
    solveIsNeg' (Term -> S ()) -> S Term -> S ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Term -> S Term
    apSubst Term
    t

    -- | Solve a constraint of the form @t < 0@.
    -- Assumes that substitution has been applied
    solveIsNeg' :: Term -> S ()
    solveIsNeg' :: Term -> S ()
    solveIsNeg' t :: Term
    t

      -- A < 0
      | Just a :: Integer
    a <- Term -> Maybe Integer
    isConst Term
    t = Bool -> S ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Integer
    a Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < 0)

      -- A * S < 0
      | Just (_,s :: Term
    s) <- Term -> Maybe (Integer, Term)
    tFactor Term
    t = Term -> S ()
    solveIsNeg Term
    s

      -- See Section 5.1 of the paper
      | Just (xc :: Integer
    xc,x :: Name
    x,s :: Term
    s) <- Term -> Maybe (Integer, Name, Term)
    tLeastVar Term
    t =

        do [(Integer, Term, Integer, Term)]
    ctrs <- if Integer
    xc Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < 0
                   -- -XC*x + S < 0
                   -- S < XC*x
                   then do [Bound]
    ubs <- BoundType -> Name -> S [Bound]
    getBounds BoundType
    Upper Name
    x
                           let b :: Integer
    b    = Integer -> Integer
    forall a. Num a => a -> a
    negate Integer
    xc
                               beta :: Term
    beta = Term
    s
                           BoundType -> Name -> Bound -> S ()
    addBound BoundType
    Lower Name
    x (Integer -> Term -> Bound
    Bound Integer
    b Term
    beta)
                           [(Integer, Term, Integer, Term)]
    -> S [(Integer, Term, Integer, Term)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [ (Integer
    a,Term
    alpha,Integer
    b,Term
    beta) | Bound a :: Integer
    a alpha :: Term
    alpha <- [Bound]
    ubs ]
                   -- XC*x + S < 0
                   -- XC*x < -S
                   else do [Bound]
    lbs <- BoundType -> Name -> S [Bound]
    getBounds BoundType
    Lower Name
    x
                           let a :: Integer
    a     = Integer
    xc
                               alpha :: Term
    alpha = Term -> Term
    tNeg Term
    s
                           BoundType -> Name -> Bound -> S ()
    addBound BoundType
    Upper Name
    x (Integer -> Term -> Bound
    Bound Integer
    a Term
    alpha)
                           [(Integer, Term, Integer, Term)]
    -> S [(Integer, Term, Integer, Term)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [ (Integer
    a,Term
    alpha,Integer
    b,Term
    beta) | Bound b :: Integer
    b beta :: Term
    beta <- [Bound]
    lbs ]

          -- See Note [Shadows]
           ((Integer, Term, Integer, Term) -> S ())
    -> [(Integer, Term, Integer, Term)] -> S ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (\(a :: Integer
    a,alpha :: Term
    alpha,b :: Integer
    b,beta :: Term
    beta) ->
              do let real :: Term
    real = Term -> Term -> Term
    ctLt (Integer
    a Integer -> Term -> Term
    |*| Term
    beta) (Integer
    b Integer -> Term -> Term
    |*| Term
    alpha)
                     dark :: Term
    dark = Term -> Term -> Term
    ctLt (Integer -> Term
    tConst (Integer
    a Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    b)) (Integer
    b Integer -> Term -> Term
    |*| Term
    alpha Term -> Term -> Term
    |-| Integer
    a Integer -> Term -> Term
    |*| Term
    beta)
                     gray :: [Term]
    gray = [ Term -> Term -> Term
    ctEq (Integer
    b Integer -> Term -> Term
    |*| Name -> Term
    tVar Name
    x) (Integer -> Term
    tConst Integer
    i Term -> Term -> Term
    |+| Term
    beta)
                                                          | Integer
    i <- [ 1 .. Integer
    b Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - 1 ] ]
                 Term -> S ()
    solveIsNeg Term
    real
                 (S () -> S () -> S ()) -> S () -> [S ()] -> S ()
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl S () -> S () -> S ()
    orElse (Term -> S ()
    solveIsNeg Term
    dark) ((Term -> S ()) -> [Term] -> [S ()]
    forall a b. (a -> b) -> [a] -> [b]
    map Term -> S ()
    solveIs0 [Term]
    gray)
                 ) [(Integer, Term, Integer, Term)]
    ctrs

      | Bool
    otherwise = String -> S ()
    forall a. HasCallStack => String -> a
    error "solveIsNeg: unreachable"

    orElse :: S () -> S () -> S ()
    orElse :: S () -> S () -> S ()
    orElse x :: S ()
    x y :: S ()
    y = S () -> S () -> S ()
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    mplus S ()
    x S ()
    y

    {- Note [Shadows]

      P: beta < b * x
      Q: a * x < alpha

    real: a * beta < b * alpha

      beta     < b * x      -- from P
      a * beta < a * b * x  -- (a *)
      a * beta < b * alpha  -- comm. and Q

    dark: b * alpha - a * beta > a * b

    gray: b * x = beta + 1 \/
          b * x = beta + 2 \/
          ...
          b * x = beta + (b-1)

    We stop at @b - 1@ because if:

    > b * x                >= beta + b
    > a * b * x            >= a * (beta + b)     -- (a *)
    > a * b * x            >= a * beta + a * b   -- distrib.
    > b * alpha            >  a * beta + a * b   -- comm. and Q
    > b * alpha - a * beta > a * b               -- subtract (a * beta)

    which is covered by the dark shadow.
    -}

    --------------------------------------------------------------------------------
    -- Monads

    data Answer a = None | One a | Choice (Answer a) (Answer a)
                    deriving Int -> Answer a -> ShowS
    [Answer a] -> ShowS
    Answer a -> String
    (Int -> Answer a -> ShowS)
    -> (Answer a -> String) -> ([Answer a] -> ShowS) -> Show (Answer a)
    forall a. Show a => Int -> Answer a -> ShowS
    forall a. Show a => [Answer a] -> ShowS
    forall a. Show a => Answer a -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Answer a] -> ShowS
    $cshowList :: forall a. Show a => [Answer a] -> ShowS
    show :: Answer a -> String
    $cshow :: forall a. Show a => Answer a -> String
    showsPrec :: Int -> Answer a -> ShowS
    $cshowsPrec :: forall a. Show a => Int -> Answer a -> ShowS
    Show

    answerSize :: Answer a -> (Integer,Integer,Integer)
    answerSize :: Answer a -> (Integer, Integer, Integer)
    answerSize = Integer
    -> Integer -> Integer -> Answer a -> (Integer, Integer, Integer)
    forall t t t a.
    (Num t, Num t, Num t) =>
    t -> t -> t -> Answer a -> (t, t, t)
    go 0 0 0
      where
      go :: t -> t -> t -> Answer a -> (t, t, t)
    go !t
    n !t
    o !t
    c ans :: Answer a
    ans =
        case Answer a
    ans of
          None  -> (t
    nt -> t -> t
    forall a. Num a => a -> a -> a
    +1, t
    o, t
    c)
          One _ -> (t
    n, t
    o t -> t -> t
    forall a. Num a => a -> a -> a
    + 1, t
    c)
          Choice x :: Answer a
    x y :: Answer a
    y ->
            case t -> t -> t -> Answer a -> (t, t, t)
    go t
    n t
    o (t
    ct -> t -> t
    forall a. Num a => a -> a -> a
    +1) Answer a
    x of
              (n' :: t
    n',o' :: t
    o',c' :: t
    c') -> t -> t -> t -> Answer a -> (t, t, t)
    go t
    n' t
    o' t
    c' Answer a
    y

    dotAnswer :: (a -> Doc) -> Answer a -> Doc
    dotAnswer :: (a -> Doc) -> Answer a -> Doc
    dotAnswer pp :: a -> Doc
    pp g0 :: Answer a
    g0 = [Doc] -> Doc
    vcat [String -> Doc
    text "digraph {", Int -> Doc -> Doc
    nest 2 ((Doc, Integer) -> Doc
    forall a b. (a, b) -> a
    fst ((Doc, Integer) -> Doc) -> (Doc, Integer) -> Doc
    forall a b. (a -> b) -> a -> b
    $ Integer -> Answer a -> (Doc, Integer)
    go 0 Answer a
    g0), String -> Doc
    text "}"]
      where
      node :: Integer -> a -> Doc
    node x :: Integer
    x d :: a
    d            = Integer -> Doc
    integer Integer
    x Doc -> Doc -> Doc
    <+> Doc -> Doc
    brackets (String -> Doc
    text "label=" Doc -> Doc -> Doc
    <> String -> Doc
    text (a -> String
    forall a. Show a => a -> String
    show a
    d))
                                                                  Doc -> Doc -> Doc
    <> Doc
    semi
      edge :: Integer -> Integer -> Doc
    edge x :: Integer
    x y :: Integer
    y            = Integer -> Doc
    integer Integer
    x Doc -> Doc -> Doc
    <+> String -> Doc
    text "->" Doc -> Doc -> Doc
    <+> Integer -> Doc
    integer Integer
    y

      go :: Integer -> Answer a -> (Doc, Integer)
    go x :: Integer
    x None           = let x' :: Integer
    x' = Integer
    x Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + 1
                            in Integer -> (Doc, Integer) -> (Doc, Integer)
    forall a b. a -> b -> b
    seq Integer
    x' ( Integer -> String -> Doc
    forall a. Show a => Integer -> a -> Doc
    node Integer
    x "", Integer
    x' )
      go x :: Integer
    x (One a :: a
    a)        = let x' :: Integer
    x' = Integer
    x Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + 1
                            in Integer -> (Doc, Integer) -> (Doc, Integer)
    forall a b. a -> b -> b
    seq Integer
    x' ( Integer -> String -> Doc
    forall a. Show a => Integer -> a -> Doc
    node Integer
    x (Doc -> String
    forall a. Show a => a -> String
    show (a -> Doc
    pp a
    a)), Integer
    x' )
      go x :: Integer
    x (Choice c1 :: Answer a
    c1 c2 :: Answer a
    c2) = let x' :: Integer
    x'       = Integer
    x Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + 1
                                (ls1 :: Doc
    ls1,x1 :: Integer
    x1) = Integer -> Answer a -> (Doc, Integer)
    go Integer
    x' Answer a
    c1
                                (ls2 :: Doc
    ls2,x2 :: Integer
    x2) = Integer -> Answer a -> (Doc, Integer)
    go Integer
    x1    Answer a
    c2
                            in Integer -> (Doc, Integer) -> (Doc, Integer)
    forall a b. a -> b -> b
    seq Integer
    x'
                               ( [Doc] -> Doc
    vcat [ Integer -> String -> Doc
    forall a. Show a => Integer -> a -> Doc
    node Integer
    x "|"
                                      , Integer -> Integer -> Doc
    edge Integer
    x Integer
    x'
                                      , Integer -> Integer -> Doc
    edge Integer
    x Integer
    x1
                                      , Doc
    ls1
                                      , Doc
    ls2
                                      ], Integer
    x2 )
    toList :: Answer a -> [a]
    toList :: Answer a -> [a]
    toList a :: Answer a
    a = Answer a -> [a] -> [a]
    forall a. Answer a -> [a] -> [a]
    go Answer a
    a []
      where
      go :: Answer a -> [a] -> [a]
    go (Choice xs :: Answer a
    xs ys :: Answer a
    ys) zs :: [a]
    zs = Answer a -> [a] -> [a]
    go Answer a
    xs (Answer a -> [a] -> [a]
    go Answer a
    ys [a]
    zs)
      go (One x :: a
    x) xs :: [a]
    xs        = a
    x a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : [a]
    xs
      go None xs :: [a]
    xs           = [a]
    xs

    instance Monad Answer where
      return :: a -> Answer a
    return a :: a
    a           = a -> Answer a
    forall a. a -> Answer a
    One a
    a
      None >>= :: Answer a -> (a -> Answer b) -> Answer b
    >>= _         = Answer b
    forall a. Answer a
    None
      One a :: a
    a >>= k :: a -> Answer b
    k        = a -> Answer b
    k a
    a
      Choice m1 :: Answer a
    m1 m2 :: Answer a
    m2 >>= k :: a -> Answer b
    k = Answer b -> Answer b -> Answer b
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    mplus (Answer a
    m1 Answer a -> (a -> Answer b) -> Answer b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= a -> Answer b
    k) (Answer a
    m2 Answer a -> (a -> Answer b) -> Answer b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= a -> Answer b
    k)

    instance MonadFail Answer where
      fail :: String -> Answer a
    fail _             = Answer a
    forall a. Answer a
    None

    instance Alternative Answer where
      empty :: Answer a
    empty = Answer a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
      <|> :: Answer a -> Answer a -> Answer a
    (<|>) = Answer a -> Answer a -> Answer a
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    mplus

    instance MonadPlus Answer where
      mzero :: Answer a
    mzero                = Answer a
    forall a. Answer a
    None
      mplus :: Answer a -> Answer a -> Answer a
    mplus None x :: Answer a
    x = Answer a
    x
      -- mplus (Choice x y) z = mplus x (mplus y z)
      mplus x :: Answer a
    x y :: Answer a
    y    = Answer a -> Answer a -> Answer a
    forall a. Answer a -> Answer a -> Answer a
    Choice Answer a
    x Answer a
    y

    instance Functor Answer where
      fmap :: (a -> b) -> Answer a -> Answer b
    fmap _ None           = Answer b
    forall a. Answer a
    None
      fmap f :: a -> b
    f (One x :: a
    x)        = b -> Answer b
    forall a. a -> Answer a
    One (a -> b
    f a
    x)
      fmap f :: a -> b
    f (Choice x1 :: Answer a
    x1 x2 :: Answer a
    x2) = Answer b -> Answer b -> Answer b
    forall a. Answer a -> Answer a -> Answer a
    Choice ((a -> b) -> Answer a -> Answer b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> b
    f Answer a
    x1) ((a -> b) -> Answer a -> Answer b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> b
    f Answer a
    x2)

    instance Applicative Answer where
      pure :: a -> Answer a
    pure  = a -> Answer a
    forall (m :: * -> *) a. Monad m => a -> m a
    return
      <*> :: Answer (a -> b) -> Answer a -> Answer b
    (<*>) = Answer (a -> b) -> Answer a -> Answer b
    forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
    ap

    newtype S a = S (RW -> Answer (a,RW))

    instance Monad S where
      return :: a -> S a
    return a :: a
    a      = (RW -> Answer (a, RW)) -> S a
    forall a. (RW -> Answer (a, RW)) -> S a
    S ((RW -> Answer (a, RW)) -> S a) -> (RW -> Answer (a, RW)) -> S a
    forall a b. (a -> b) -> a -> b
    $ \s :: RW
    s -> (a, RW) -> Answer (a, RW)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a
    a,RW
    s)
      S m :: RW -> Answer (a, RW)
    m >>= :: S a -> (a -> S b) -> S b
    >>= k :: a -> S b
    k     = (RW -> Answer (b, RW)) -> S b
    forall a. (RW -> Answer (a, RW)) -> S a
    S ((RW -> Answer (b, RW)) -> S b) -> (RW -> Answer (b, RW)) -> S b
    forall a b. (a -> b) -> a -> b
    $ \s :: RW
    s -> do (a :: a
    a,s1 :: RW
    s1) <- RW -> Answer (a, RW)
    m RW
    s
                                   let S m1 :: RW -> Answer (b, RW)
    m1 = a -> S b
    k a
    a
                                   RW -> Answer (b, RW)
    m1 RW
    s1

    instance Alternative S where
      empty :: S a
    empty = S a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
      <|> :: S a -> S a -> S a
    (<|>) = S a -> S a -> S a
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    mplus

    instance MonadPlus S where
      mzero :: S a
    mzero               = (RW -> Answer (a, RW)) -> S a
    forall a. (RW -> Answer (a, RW)) -> S a
    S ((RW -> Answer (a, RW)) -> S a) -> (RW -> Answer (a, RW)) -> S a
    forall a b. (a -> b) -> a -> b
    $ \_ -> Answer (a, RW)
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
      mplus :: S a -> S a -> S a
    mplus (S m1 :: RW -> Answer (a, RW)
    m1) (S m2 :: RW -> Answer (a, RW)
    m2) = (RW -> Answer (a, RW)) -> S a
    forall a. (RW -> Answer (a, RW)) -> S a
    S ((RW -> Answer (a, RW)) -> S a) -> (RW -> Answer (a, RW)) -> S a
    forall a b. (a -> b) -> a -> b
    $ \s :: RW
    s -> Answer (a, RW) -> Answer (a, RW) -> Answer (a, RW)
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    mplus (RW -> Answer (a, RW)
    m1 RW
    s) (RW -> Answer (a, RW)
    m2 RW
    s)

    instance Functor S where
      fmap :: (a -> b) -> S a -> S b
    fmap = (a -> b) -> S a -> S b
    forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
    liftM

    instance Applicative S where
      pure :: a -> S a
    pure  = a -> S a
    forall (m :: * -> *) a. Monad m => a -> m a
    return
      <*> :: S (a -> b) -> S a -> S b
    (<*>) = S (a -> b) -> S a -> S b
    forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
    ap

    updS :: (RW -> (a,RW)) -> S a
    updS :: (RW -> (a, RW)) -> S a
    updS f :: RW -> (a, RW)
    f = (RW -> Answer (a, RW)) -> S a
    forall a. (RW -> Answer (a, RW)) -> S a
    S ((RW -> Answer (a, RW)) -> S a) -> (RW -> Answer (a, RW)) -> S a
    forall a b. (a -> b) -> a -> b
    $ \s :: RW
    s -> (a, RW) -> Answer (a, RW)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (RW -> (a, RW)
    f RW
    s)

    updS_ :: (RW -> RW) -> S ()
    updS_ :: (RW -> RW) -> S ()
    updS_ f :: RW -> RW
    f = (RW -> ((), RW)) -> S ()
    forall a. (RW -> (a, RW)) -> S a
    updS ((RW -> ((), RW)) -> S ()) -> (RW -> ((), RW)) -> S ()
    forall a b. (a -> b) -> a -> b
    $ \rw :: RW
    rw -> ((),RW -> RW
    f RW
    rw)

    get :: (RW -> a) -> S a
    get :: (RW -> a) -> S a
    get f :: RW -> a
    f = (RW -> (a, RW)) -> S a
    forall a. (RW -> (a, RW)) -> S a
    updS ((RW -> (a, RW)) -> S a) -> (RW -> (a, RW)) -> S a
    forall a b. (a -> b) -> a -> b
    $ \rw :: RW
    rw -> (RW -> a
    f RW
    rw, RW
    rw)

    newVar :: S Name
    newVar :: S Name
    newVar = (RW -> (Name, RW)) -> S Name
    forall a. (RW -> (a, RW)) -> S a
    updS ((RW -> (Name, RW)) -> S Name) -> (RW -> (Name, RW)) -> S Name
    forall a b. (a -> b) -> a -> b
    $ \rw :: RW
    rw -> ( Int -> Name
    SysName (RW -> Int
    nameSource RW
    rw)
                           , RW
    rw { nameSource :: Int
    nameSource = RW -> Int
    nameSource RW
    rw Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + 1 }
                           )

    -- | Get lower ('fst'), or upper ('snd') bounds for a variable.
    getBounds :: BoundType -> Name -> S [Bound]
    getBounds :: BoundType -> Name -> S [Bound]
    getBounds f :: BoundType
    f x :: Name
    x = (RW -> [Bound]) -> S [Bound]
    forall a. (RW -> a) -> S a
    get ((RW -> [Bound]) -> S [Bound]) -> (RW -> [Bound]) -> S [Bound]
    forall a b. (a -> b) -> a -> b
    $ \rw :: RW
    rw -> case Name -> NameMap ([Bound], [Bound]) -> Maybe ([Bound], [Bound])
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    x (NameMap ([Bound], [Bound]) -> Maybe ([Bound], [Bound]))
    -> NameMap ([Bound], [Bound]) -> Maybe ([Bound], [Bound])
    forall a b. (a -> b) -> a -> b
    $ Inerts -> NameMap ([Bound], [Bound])
    bounds (Inerts -> NameMap ([Bound], [Bound]))
    -> Inerts -> NameMap ([Bound], [Bound])
    forall a b. (a -> b) -> a -> b
    $ RW -> Inerts
    inerts RW
    rw of
                                   Nothing -> []
                                   Just bs :: ([Bound], [Bound])
    bs -> case BoundType
    f of
                                                Lower -> ([Bound], [Bound]) -> [Bound]
    forall a b. (a, b) -> a
    fst ([Bound], [Bound])
    bs
                                                Upper -> ([Bound], [Bound]) -> [Bound]
    forall a b. (a, b) -> b
    snd ([Bound], [Bound])
    bs

    addBound :: BoundType -> Name -> Bound -> S ()
    addBound :: BoundType -> Name -> Bound -> S ()
    addBound bt :: BoundType
    bt x :: Name
    x b :: Bound
    b = (RW -> RW) -> S ()
    updS_ ((RW -> RW) -> S ()) -> (RW -> RW) -> S ()
    forall a b. (a -> b) -> a -> b
    $ \rw :: RW
    rw ->
      let i :: Inerts
    i = RW -> Inerts
    inerts RW
    rw
          entry :: ([Bound], [Bound])
    entry = case BoundType
    bt of
                    Lower -> ([Bound
    b],[])
                    Upper -> ([],[Bound
    b])
          jn :: ([a], [a]) -> ([a], [a]) -> ([a], [a])
    jn (newL :: [a]
    newL,newU :: [a]
    newU) (oldL :: [a]
    oldL,oldU :: [a]
    oldU) = ([a]
    newL[a] -> [a] -> [a]
    forall a. [a] -> [a] -> [a]
    ++[a]
    oldL, [a]
    newU[a] -> [a] -> [a]
    forall a. [a] -> [a] -> [a]
    ++[a]
    oldU)
      in RW
    rw { inerts :: Inerts
    inerts = Inerts
    i { bounds :: NameMap ([Bound], [Bound])
    bounds = (([Bound], [Bound]) -> ([Bound], [Bound]) -> ([Bound], [Bound]))
    -> Name
    -> ([Bound], [Bound])
    -> NameMap ([Bound], [Bound])
    -> NameMap ([Bound], [Bound])
    forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
    Map.insertWith ([Bound], [Bound]) -> ([Bound], [Bound]) -> ([Bound], [Bound])
    forall a a. ([a], [a]) -> ([a], [a]) -> ([a], [a])
    jn Name
    x ([Bound], [Bound])
    entry (Inerts -> NameMap ([Bound], [Bound])
    bounds Inerts
    i) }}

    -- | Add a new definition.
    -- Assumes substitution has already been applied
    addDef :: Name -> Term -> S ()
    addDef :: Name -> Term -> S ()
    addDef x :: Name
    x t :: Term
    t =
      do [Term]
    newWork <- (RW -> ([Term], RW)) -> S [Term]
    forall a. (RW -> (a, RW)) -> S a
    updS ((RW -> ([Term], RW)) -> S [Term])
    -> (RW -> ([Term], RW)) -> S [Term]
    forall a b. (a -> b) -> a -> b
    $ \rw :: RW
    rw -> let (newWork :: [Term]
    newWork,newInerts :: Inerts
    newInerts) = Name -> Term -> Inerts -> ([Term], Inerts)
    iSolved Name
    x Term
    t (RW -> Inerts
    inerts RW
    rw)
                                  in ([Term]
    newWork, RW
    rw { inerts :: Inerts
    inerts = Inerts
    newInerts })
         (Term -> S ()) -> [Term] -> S ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Term -> S ()
    solveIsNeg [Term]
    newWork

    apSubst :: Term -> S Term
    apSubst :: Term -> S Term
    apSubst t :: Term
    t =
      do Inerts
    i <- (RW -> Inerts) -> S Inerts
    forall a. (RW -> a) -> S a
    get RW -> Inerts
    inerts
         Term -> S Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Inerts -> Term -> Term
    iApSubst Inerts
    i Term
    t)

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

    data Name = UserName !Int | SysName !Int
                deriving (ReadPrec [Name]
    ReadPrec Name
    Int -> ReadS Name
    ReadS [Name]
    (Int -> ReadS Name)
    -> ReadS [Name] -> ReadPrec Name -> ReadPrec [Name] -> Read Name
    forall a.
    (Int -> ReadS a)
    -> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
    readListPrec :: ReadPrec [Name]
    $creadListPrec :: ReadPrec [Name]
    readPrec :: ReadPrec Name
    $creadPrec :: ReadPrec Name
    readList :: ReadS [Name]
    $creadList :: ReadS [Name]
    readsPrec :: Int -> ReadS Name
    $creadsPrec :: Int -> ReadS Name
    Read,Int -> Name -> ShowS
    [Name] -> ShowS
    Name -> String
    (Int -> Name -> ShowS)
    -> (Name -> String) -> ([Name] -> ShowS) -> Show Name
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Name] -> ShowS
    $cshowList :: [Name] -> ShowS
    show :: Name -> String
    $cshow :: Name -> String
    showsPrec :: Int -> Name -> ShowS
    $cshowsPrec :: Int -> Name -> ShowS
    Show,Name -> Name -> Bool
    (Name -> Name -> Bool) -> (Name -> Name -> Bool) -> Eq Name
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Name -> Name -> Bool
    $c/= :: Name -> Name -> Bool
    == :: Name -> Name -> Bool
    $c== :: Name -> Name -> Bool
    Eq,Eq Name
    Eq Name =>
    (Name -> Name -> Ordering)
    -> (Name -> Name -> Bool)
    -> (Name -> Name -> Bool)
    -> (Name -> Name -> Bool)
    -> (Name -> Name -> Bool)
    -> (Name -> Name -> Name)
    -> (Name -> Name -> Name)
    -> Ord Name
    Name -> Name -> Bool
    Name -> Name -> Ordering
    Name -> Name -> Name
    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 :: Name -> Name -> Name
    $cmin :: Name -> Name -> Name
    max :: Name -> Name -> Name
    $cmax :: Name -> Name -> Name
    >= :: Name -> Name -> Bool
    $c>= :: Name -> Name -> Bool
    > :: Name -> Name -> Bool
    $c> :: Name -> Name -> Bool
    <= :: Name -> Name -> Bool
    $c<= :: Name -> Name -> Bool
    < :: Name -> Name -> Bool
    $c< :: Name -> Name -> Bool
    compare :: Name -> Name -> Ordering
    $ccompare :: Name -> Name -> Ordering
    $cp1Ord :: Eq Name
    Ord)

    ppName :: Name -> Doc
    ppName :: Name -> Doc
    ppName (UserName x :: Int
    x) = String -> Doc
    text "u" Doc -> Doc -> Doc
    <> Int -> Doc
    int Int
    x
    ppName (SysName x :: Int
    x)  = String -> Doc
    text "s" Doc -> Doc -> Doc
    <> Int -> Doc
    int Int
    x

    toName :: Int -> Name
    toName :: Int -> Name
    toName = Int -> Name
    UserName

    fromName :: Name -> Maybe Int
    fromName :: Name -> Maybe Int
    fromName (UserName x :: Int
    x) = Int -> Maybe Int
    forall a. a -> Maybe a
    Just Int
    x
    fromName (SysName _)  = Maybe Int
    forall a. Maybe a
    Nothing

    type NameMap = Map Name

    -- | The type of terms.  The integer is the constant part of the term,
    -- and the `Map` maps variables (represented by @Int@ to their coefficients).
    -- The term is a sum of its parts.
    -- INVARIANT: the `Map` does not map anything to 0.
    data Term = T !Integer (NameMap Integer)
                  deriving (Term -> Term -> Bool
    (Term -> Term -> Bool) -> (Term -> Term -> Bool) -> Eq Term
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Term -> Term -> Bool
    $c/= :: Term -> Term -> Bool
    == :: Term -> Term -> Bool
    $c== :: Term -> Term -> Bool
    Eq,Eq Term
    Eq Term =>
    (Term -> Term -> Ordering)
    -> (Term -> Term -> Bool)
    -> (Term -> Term -> Bool)
    -> (Term -> Term -> Bool)
    -> (Term -> Term -> Bool)
    -> (Term -> Term -> Term)
    -> (Term -> Term -> Term)
    -> Ord Term
    Term -> Term -> Bool
    Term -> Term -> Ordering
    Term -> Term -> Term
    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 :: Term -> Term -> Term
    $cmin :: Term -> Term -> Term
    max :: Term -> Term -> Term
    $cmax :: Term -> Term -> Term
    >= :: Term -> Term -> Bool
    $c>= :: Term -> Term -> Bool
    > :: Term -> Term -> Bool
    $c> :: Term -> Term -> Bool
    <= :: Term -> Term -> Bool
    $c<= :: Term -> Term -> Bool
    < :: Term -> Term -> Bool
    $c< :: Term -> Term -> Bool
    compare :: Term -> Term -> Ordering
    $ccompare :: Term -> Term -> Ordering
    $cp1Ord :: Eq Term
    Ord)

    infixl 6 |+|, |-|
    infixr 7 |*|

    -- | A constant term.
    tConst :: Integer -> Term
    tConst :: Integer -> Term
    tConst k :: Integer
    k = Integer -> NameMap Integer -> Term
    T Integer
    k NameMap Integer
    forall k a. Map k a
    Map.empty

    -- | Construct a term with a single variable.
    tVar :: Name -> Term
    tVar :: Name -> Term
    tVar x :: Name
    x = Integer -> NameMap Integer -> Term
    T 0 (Name -> Integer -> NameMap Integer
    forall k a. k -> a -> Map k a
    Map.singleton Name
    x 1)

    (|+|) :: Term -> Term -> Term
    T n1 :: Integer
    n1 m1 :: NameMap Integer
    m1 |+| :: Term -> Term -> Term
    |+| T n2 :: Integer
    n2 m2 :: NameMap Integer
    m2 = Integer -> NameMap Integer -> Term
    T (Integer
    n1 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    n2)
                        (NameMap Integer -> Term) -> NameMap Integer -> Term
    forall a b. (a -> b) -> a -> b
    $ if NameMap Integer -> Bool
    forall k a. Map k a -> Bool
    Map.null NameMap Integer
    m1 then NameMap Integer
    m2 else
                          if NameMap Integer -> Bool
    forall k a. Map k a -> Bool
    Map.null NameMap Integer
    m2 then NameMap Integer
    m1 else
                          (Integer -> Bool) -> NameMap Integer -> NameMap Integer
    forall a k. (a -> Bool) -> Map k a -> Map k a
    Map.filter (Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    /= 0) (NameMap Integer -> NameMap Integer)
    -> NameMap Integer -> NameMap Integer
    forall a b. (a -> b) -> a -> b
    $ (Integer -> Integer -> Integer)
    -> NameMap Integer -> NameMap Integer -> NameMap Integer
    forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
    Map.unionWith Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    (+) NameMap Integer
    m1 NameMap Integer
    m2

    (|*|) :: Integer -> Term -> Term
    0 |*| :: Integer -> Term -> Term
    |*| _     = Integer -> Term
    tConst 0
    1 |*| t :: Term
    t     = Term
    t
    k :: Integer
    k |*| T n :: Integer
    n m :: NameMap Integer
    m = Integer -> NameMap Integer -> Term
    T (Integer
    k Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    n) ((Integer -> Integer) -> NameMap Integer -> NameMap Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Integer
    k Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    *) NameMap Integer
    m)

    tNeg :: Term -> Term
    tNeg :: Term -> Term
    tNeg t :: Term
    t = (-1) Integer -> Term -> Term
    |*| Term
    t

    (|-|) :: Term -> Term -> Term
    t1 :: Term
    t1 |-| :: Term -> Term -> Term
    |-| t2 :: Term
    t2 = Term
    t1 Term -> Term -> Term
    |+| Term -> Term
    tNeg Term
    t2

    -- | Replace a variable with a term.
    tLet :: Name -> Term -> Term -> Term
    tLet :: Name -> Term -> Term -> Term
    tLet x :: Name
    x t1 :: Term
    t1 t2 :: Term
    t2 = let (a :: Integer
    a,t :: Term
    t) = Name -> Term -> (Integer, Term)
    tSplitVar Name
    x Term
    t2
                   in Integer
    a Integer -> Term -> Term
    |*| Term
    t1 Term -> Term -> Term
    |+| Term
    t

    -- | Replace a variable with a constant.
    tLetNum :: Name -> Integer -> Term -> Term
    tLetNum :: Name -> Integer -> Term -> Term
    tLetNum x :: Name
    x k :: Integer
    k t :: Term
    t = let (c :: Integer
    c,T n :: Integer
    n m :: NameMap Integer
    m) = Name -> Term -> (Integer, Term)
    tSplitVar Name
    x Term
    t
                    in Integer -> NameMap Integer -> Term
    T (Integer
    c Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    k Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    n) NameMap Integer
    m

    -- | Replace the given variables with constants.
    tLetNums :: [(Name,Integer)] -> Term -> Term
    tLetNums :: [(Name, Integer)] -> Term -> Term
    tLetNums xs :: [(Name, Integer)]
    xs t :: Term
    t = ((Name, Integer) -> Term -> Term)
    -> Term -> [(Name, Integer)] -> Term
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (\(x :: Name
    x,i :: Integer
    i) t1 :: Term
    t1 -> Name -> Integer -> Term -> Term
    tLetNum Name
    x Integer
    i Term
    t1) Term
    t [(Name, Integer)]
    xs

    instance Show Term where
      showsPrec :: Int -> Term -> ShowS
    showsPrec c :: Int
    c t :: Term
    t = Int -> String -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    c (Doc -> String
    forall a. Show a => a -> String
    show (Term -> Doc
    ppTerm Term
    t))

    ppTerm :: Term -> Doc
    ppTerm :: Term -> Doc
    ppTerm (T k :: Integer
    k m :: NameMap Integer
    m) =
      case NameMap Integer -> [(Name, Integer)]
    forall k a. Map k a -> [(k, a)]
    Map.toList NameMap Integer
    m of
        []     -> Integer -> Doc
    integer Integer
    k
        xs :: [(Name, Integer)]
    xs     | Integer
    k Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    /= 0 -> [Doc] -> Doc
    hsep (Integer -> Doc
    integer Integer
    k Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : ((Name, Integer) -> Doc) -> [(Name, Integer)] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name, Integer) -> Doc
    ppProd [(Name, Integer)]
    xs)
        x :: (Name, Integer)
    x : xs :: [(Name, Integer)]
    xs -> [Doc] -> Doc
    hsep ((Name, Integer) -> Doc
    ppFst (Name, Integer)
    x   Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : ((Name, Integer) -> Doc) -> [(Name, Integer)] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name, Integer) -> Doc
    ppProd [(Name, Integer)]
    xs)

      where
      ppFst :: (Name, Integer) -> Doc
    ppFst (x :: Name
    x,1)  = Name -> Doc
    ppName Name
    x
      ppFst (x :: Name
    x,-1) = String -> Doc
    text "-" Doc -> Doc -> Doc
    <> Name -> Doc
    ppName Name
    x
      ppFst (x :: Name
    x,n :: Integer
    n)  = Integer -> Name -> Doc
    ppMul Integer
    n Name
    x

      ppProd :: (Name, Integer) -> Doc
    ppProd (x :: Name
    x,1)  = String -> Doc
    text "+" Doc -> Doc -> Doc
    <+> Name -> Doc
    ppName Name
    x
      ppProd (x :: Name
    x,-1) = String -> Doc
    text "-" Doc -> Doc -> Doc
    <+> Name -> Doc
    ppName Name
    x
      ppProd (x :: Name
    x,n :: Integer
    n) | Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > 0      = String -> Doc
    text "+" Doc -> Doc -> Doc
    <+> Integer -> Name -> Doc
    ppMul Integer
    n Name
    x
                   | Bool
    otherwise  = String -> Doc
    text "-" Doc -> Doc -> Doc
    <+> Integer -> Name -> Doc
    ppMul (Integer -> Integer
    forall a. Num a => a -> a
    abs Integer
    n) Name
    x

      ppMul :: Integer -> Name -> Doc
    ppMul n :: Integer
    n x :: Name
    x = Integer -> Doc
    integer Integer
    n Doc -> Doc -> Doc
    <+> String -> Doc
    text "*" Doc -> Doc -> Doc
    <+> Name -> Doc
    ppName Name
    x

    -- | Remove a variable from the term, and return its coefficient.
    -- If the variable is not present in the term, the coefficient is 0.
    tSplitVar :: Name -> Term -> (Integer, Term)
    tSplitVar :: Name -> Term -> (Integer, Term)
    tSplitVar x :: Name
    x t :: Term
    t@(T n :: Integer
    n m :: NameMap Integer
    m) =
      case (Name -> Integer -> Maybe Integer)
    -> Name -> NameMap Integer -> (Maybe Integer, NameMap Integer)
    forall k a.
    Ord k =>
    (k -> a -> Maybe a) -> k -> Map k a -> (Maybe a, Map k a)
    Map.updateLookupWithKey (\_ _ -> Maybe Integer
    forall a. Maybe a
    Nothing) Name
    x NameMap Integer
    m of
        (Nothing,_) -> (0,Term
    t)
        (Just k :: Integer
    k,m1 :: NameMap Integer
    m1) -> (Integer
    k, Integer -> NameMap Integer -> Term
    T Integer
    n NameMap Integer
    m1)

    -- | Does the term contain this varibale?
    tHasVar :: Name -> Term -> Bool
    tHasVar :: Name -> Term -> Bool
    tHasVar x :: Name
    x (T _ m :: NameMap Integer
    m) = Name -> NameMap Integer -> Bool
    forall k a. Ord k => k -> Map k a -> Bool
    Map.member Name
    x NameMap Integer
    m

    -- | Is this terms just an integer.
    isConst :: Term -> Maybe Integer
    isConst :: Term -> Maybe Integer
    isConst (T n :: Integer
    n m :: NameMap Integer
    m)
      | NameMap Integer -> Bool
    forall k a. Map k a -> Bool
    Map.null NameMap Integer
    m  = Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    n
      | Bool
    otherwise   = Maybe Integer
    forall a. Maybe a
    Nothing

    tConstPart :: Term -> Integer
    tConstPart :: Term -> Integer
    tConstPart (T n :: Integer
    n _) = Integer
    n

    -- | Returns: @Just (a, b, x)@ if the term is the form: @a + b * x@
    tIsOneVar :: Term -> Maybe (Integer, Integer, Name)
    tIsOneVar :: Term -> Maybe (Integer, Integer, Name)
    tIsOneVar (T a :: Integer
    a m :: NameMap Integer
    m) = case NameMap Integer -> [(Name, Integer)]
    forall k a. Map k a -> [(k, a)]
    Map.toList NameMap Integer
    m of
                          [ (x :: Name
    x,b :: Integer
    b) ] -> (Integer, Integer, Name) -> Maybe (Integer, Integer, Name)
    forall a. a -> Maybe a
    Just (Integer
    a, Integer
    b, Name
    x)
                          _         -> Maybe (Integer, Integer, Name)
    forall a. Maybe a
    Nothing

    -- | Spots terms that contain variables with unit coefficients
    -- (i.e., of the form @x + t@ or @t - x@).
    -- Returns (coeff, var, rest of term)
    tGetSimpleCoeff :: Term -> Maybe (Integer, Name, Term)
    tGetSimpleCoeff :: Term -> Maybe (Integer, Name, Term)
    tGetSimpleCoeff (T a :: Integer
    a m :: NameMap Integer
    m) =
      do let (m1 :: NameMap Integer
    m1,m2 :: NameMap Integer
    m2) = (Integer -> Bool)
    -> NameMap Integer -> (NameMap Integer, NameMap Integer)
    forall a k. (a -> Bool) -> Map k a -> (Map k a, Map k a)
    Map.partition (\x :: Integer
    x -> Integer
    x Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == 1 Bool -> Bool -> Bool
    || Integer
    x Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == -1) NameMap Integer
    m
         ((x :: Name
    x,xc :: Integer
    xc), m3 :: NameMap Integer
    m3) <- NameMap Integer -> Maybe ((Name, Integer), NameMap Integer)
    forall k a. Map k a -> Maybe ((k, a), Map k a)
    Map.minViewWithKey NameMap Integer
    m1
         (Integer, Name, Term) -> Maybe (Integer, Name, Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer
    xc, Name
    x, Integer -> NameMap Integer -> Term
    T Integer
    a (NameMap Integer -> NameMap Integer -> NameMap Integer
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union NameMap Integer
    m3 NameMap Integer
    m2))

    tVarList :: Term -> [Name]
    tVarList :: Term -> [Name]
    tVarList (T _ m :: NameMap Integer
    m) = NameMap Integer -> [Name]
    forall k a. Map k a -> [k]
    Map.keys NameMap Integer
    m

    -- | Try to factor-out a common consant (> 1) from a term.
    -- For example, @2 + 4x@ becomes @2 * (1 + 2x)@.
    tFactor :: Term -> Maybe (Integer, Term)
    tFactor :: Term -> Maybe (Integer, Term)
    tFactor (T c :: Integer
    c m :: NameMap Integer
    m) =
      do Integer
    d <- [Integer] -> Maybe Integer
    common (Integer
    c Integer -> [Integer] -> [Integer]
    forall a. a -> [a] -> [a]
    : NameMap Integer -> [Integer]
    forall k a. Map k a -> [a]
    Map.elems NameMap Integer
    m)
         (Integer, Term) -> Maybe (Integer, Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer
    d, Integer -> NameMap Integer -> Term
    T (Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    div Integer
    c Integer
    d) ((Integer -> Integer) -> NameMap Integer -> NameMap Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `div` Integer
    d) NameMap Integer
    m))
      where
      common :: [Integer] -> Maybe Integer
      common :: [Integer] -> Maybe Integer
    common []  = Maybe Integer
    forall a. Maybe a
    Nothing
      common [x :: Integer
    x] = Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    x
      common (x :: Integer
    x : y :: Integer
    y : zs :: [Integer]
    zs) =
        case Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    gcd Integer
    x Integer
    y of
          1 -> Maybe Integer
    forall a. Maybe a
    Nothing
          n :: Integer
    n -> [Integer] -> Maybe Integer
    common (Integer
    n Integer -> [Integer] -> [Integer]
    forall a. a -> [a] -> [a]
    : [Integer]
    zs)

    -- | Extract a variable with a coefficient whose absolute value is minimal.
    tLeastAbsCoeff :: Term -> Maybe (Integer, Name, Term)
    #if MIN_VERSION_containers(0,6,0)
    tLeastAbsCoeff :: Term -> Maybe (Integer, Name, Term)
    tLeastAbsCoeff (T c :: Integer
    c m :: NameMap Integer
    m) = do (xc :: Integer
    xc,x :: Name
    x,m1 :: NameMap Integer
    m1) <- (Name
     -> Integer
     -> Maybe (Integer, Name, NameMap Integer)
     -> Maybe (Integer, Name, NameMap Integer))
    -> Maybe (Integer, Name, NameMap Integer)
    -> NameMap Integer
    -> Maybe (Integer, Name, NameMap Integer)
    forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
    MapStrict.foldrWithKey Name
    -> Integer
    -> Maybe (Integer, Name, NameMap Integer)
    -> Maybe (Integer, Name, NameMap Integer)
    forall a.
    (Ord a, Num a) =>
    Name
    -> a
    -> Maybe (a, Name, NameMap Integer)
    -> Maybe (a, Name, NameMap Integer)
    step Maybe (Integer, Name, NameMap Integer)
    forall a. Maybe a
    Nothing NameMap Integer
    m
    #else
    tLeastAbsCoeff (T c m) = do (xc,x,m1) <- Map.foldWithKey step Nothing m
    #endif
                                (Integer, Name, Term) -> Maybe (Integer, Name, Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer
    xc, Name
    x, Integer -> NameMap Integer -> Term
    T Integer
    c NameMap Integer
    m1)
      where
      step :: Name
    -> a
    -> Maybe (a, Name, NameMap Integer)
    -> Maybe (a, Name, NameMap Integer)
    step x :: Name
    x xc :: a
    xc Nothing   = (a, Name, NameMap Integer) -> Maybe (a, Name, NameMap Integer)
    forall a. a -> Maybe a
    Just (a
    xc, Name
    x, Name -> NameMap Integer -> NameMap Integer
    forall k a. Ord k => k -> Map k a -> Map k a
    Map.delete Name
    x NameMap Integer
    m)
      step x :: Name
    x xc :: a
    xc (Just (yc :: a
    yc,_,_))
        | a -> a
    forall a. Num a => a -> a
    abs a
    xc a -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    < a -> a
    forall a. Num a => a -> a
    abs a
    yc = (a, Name, NameMap Integer) -> Maybe (a, Name, NameMap Integer)
    forall a. a -> Maybe a
    Just (a
    xc, Name
    x, Name -> NameMap Integer -> NameMap Integer
    forall k a. Ord k => k -> Map k a -> Map k a
    Map.delete Name
    x NameMap Integer
    m)
      step _ _ it :: Maybe (a, Name, NameMap Integer)
    it         = Maybe (a, Name, NameMap Integer)
    it

    -- | Extract the least variable from a term
    tLeastVar :: Term -> Maybe (Integer, Name, Term)
    tLeastVar :: Term -> Maybe (Integer, Name, Term)
    tLeastVar (T c :: Integer
    c m :: NameMap Integer
    m) =
      do ((x :: Name
    x,xc :: Integer
    xc), m1 :: NameMap Integer
    m1) <- NameMap Integer -> Maybe ((Name, Integer), NameMap Integer)
    forall k a. Map k a -> Maybe ((k, a), Map k a)
    Map.minViewWithKey NameMap Integer
    m
         (Integer, Name, Term) -> Maybe (Integer, Name, Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer
    xc, Name
    x, Integer -> NameMap Integer -> Term
    T Integer
    c NameMap Integer
    m1)

    -- | Apply a function to all coefficients, including the constnat
    tMapCoeff :: (Integer -> Integer) -> Term -> Term
    tMapCoeff :: (Integer -> Integer) -> Term -> Term
    tMapCoeff f :: Integer -> Integer
    f (T c :: Integer
    c m :: NameMap Integer
    m) = Integer -> NameMap Integer -> Term
    T (Integer -> Integer
    f Integer
    c) ((Integer -> Integer) -> NameMap Integer -> NameMap Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Integer -> Integer
    f NameMap Integer
    m)