-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/

-- | A decision procedure for quantifier-free linear arithmetic.
--   
--   The decision procedure is based on the algorithm used in CVC4, which
--   is itself based on the Omega test.
@package presburger
@version 1.3.1

-- | 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

-- | A collection of propositions.
data PropSet

-- | An empty collection of propositions.
noProps :: PropSet

-- | 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)]

-- | Add a new proposition to an existing collection.
assert :: Prop -> PropSet -> PropSet

-- | The type of proposition.
data Prop
PTrue :: Prop
PFalse :: Prop
(:||) :: Prop -> Prop -> Prop
(:&&) :: Prop -> Prop -> Prop
Not :: Prop -> Prop
(:==) :: Expr -> Expr -> Prop
(:/=) :: Expr -> Expr -> Prop
(:<) :: Expr -> Expr -> Prop
(:>) :: Expr -> Expr -> Prop
(:<=) :: Expr -> Expr -> Prop
(:>=) :: Expr -> Expr -> Prop
infixr 2 :||
infixr 3 :&&
infix 4 :==
infix 4 :/=
infix 4 :<
infix 4 :<=
infix 4 :>
infix 4 :>=

-- | The type of integer expressions. Variable names must be non-negative.
data Expr

-- | Addition
(:+) :: Expr -> Expr -> Expr

-- | Subtraction
(:-) :: Expr -> Expr -> Expr

-- | Multiplication by a constant
(:*) :: Integer -> Expr -> Expr

-- | Negation
Negate :: Expr -> Expr

-- | Variable
Var :: Name -> Expr

-- | Constant
K :: Integer -> Expr

-- | A conditional expression
If :: Prop -> Expr -> Expr -> Expr

-- | Division, rounds down
Div :: Expr -> Integer -> Expr

-- | Non-negative remainder
Mod :: Expr -> Integer -> Expr
infixl 6 :+
infixl 6 :-
infixl 7 :*
data BoundType
Lower :: BoundType
Upper :: BoundType

-- | 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

-- | Compute the range of possible values for an expression. Returns
--   Nothing if the bound is not known.
getExprRange :: Expr -> PropSet -> Maybe [Integer]
data Name
toName :: Int -> Name
fromName :: Name -> Maybe Int
allSolutions :: PropSet -> [Solutions]
slnCurrent :: Solutions -> [(Int, Integer)]
slnNextVal :: Solutions -> Maybe Solutions
slnNextVar :: Solutions -> Maybe Solutions
slnEnumerate :: Solutions -> [Solutions]
dotPropSet :: PropSet -> Doc
sizePropSet :: PropSet -> (Integer, Integer, Integer)
allInerts :: PropSet -> [Inerts]
ppInerts :: Inerts -> Doc
iPickBounded :: BoundType -> [Bound] -> Maybe Integer
data Bound

-- | The integer is strictly positive
Bound :: Integer -> Term -> Bound

-- | A constant term.
tConst :: Integer -> Term
instance GHC.Show.Show Data.Integer.SAT.PropSet
instance GHC.Show.Show Data.Integer.SAT.RW
instance GHC.Show.Show Data.Integer.SAT.Solutions
instance GHC.Show.Show Data.Integer.SAT.Inerts
instance GHC.Show.Show Data.Integer.SAT.Bound
instance GHC.Classes.Ord Data.Integer.SAT.Term
instance GHC.Classes.Eq Data.Integer.SAT.Term
instance GHC.Show.Show Data.Integer.SAT.Prop
instance GHC.Read.Read Data.Integer.SAT.Prop
instance GHC.Show.Show Data.Integer.SAT.Expr
instance GHC.Read.Read Data.Integer.SAT.Expr
instance GHC.Classes.Ord Data.Integer.SAT.Name
instance GHC.Classes.Eq Data.Integer.SAT.Name
instance GHC.Show.Show Data.Integer.SAT.Name
instance GHC.Read.Read Data.Integer.SAT.Name
instance GHC.Show.Show a => GHC.Show.Show (Data.Integer.SAT.Answer a)
instance GHC.Show.Show Data.Integer.SAT.BoundType
instance GHC.Base.Monad Data.Integer.SAT.S
instance GHC.Base.Alternative Data.Integer.SAT.S
instance GHC.Base.MonadPlus Data.Integer.SAT.S
instance GHC.Base.Functor Data.Integer.SAT.S
instance GHC.Base.Applicative Data.Integer.SAT.S
instance GHC.Show.Show Data.Integer.SAT.Term
instance GHC.Base.Monad Data.Integer.SAT.Answer
instance Control.Monad.Fail.MonadFail Data.Integer.SAT.Answer
instance GHC.Base.Alternative Data.Integer.SAT.Answer
instance GHC.Base.MonadPlus Data.Integer.SAT.Answer
instance GHC.Base.Functor Data.Integer.SAT.Answer
instance GHC.Base.Applicative Data.Integer.SAT.Answer
