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


-- | Use SMT solvers to solve linear systems over integers and rationals
--   
--   Solve linear systems of equations over integers and rationals, using
--   an SMT solver.
--   
--   linearEqSolver is hosted at GitHub:
--   <a>http://github.com/LeventErkok/linearEqSolver</a>. Comments, bug
--   reports, and patches are always welcome.
--   
--   Release notes can be seen at:
--   <a>http://github.com/LeventErkok/linearEqSolver/blob/master/CHANGES.md</a>
@package linearEqSolver
@version 2.3


-- | (The linear equation solver library is hosted at
--   <a>http://github.com/LeventErkok/linearEqSolver</a>. Comments, bug
--   reports, and patches are always welcome.)
--   
--   Solvers for linear equations over integers and rationals. Both single
--   solution and all solution variants are supported.
module Math.LinearEquationSolver

-- | Solvers that SBV is aware of
data Solver
Z3 :: Solver
Yices :: Solver
Boolector :: Solver
CVC4 :: Solver
MathSAT :: Solver
ABC :: Solver

-- | Solve a system of linear integer equations. The first argument is the
--   matrix of coefficients, known as <tt>A</tt>, of size <tt>mxn</tt>. The
--   second argument is the vector of results, known as <tt>b</tt>, of size
--   <tt>mx1</tt>. The result will be either <a>Nothing</a>, if there is no
--   solution, or <tt>Just x</tt> -- such that <tt>Ax = b</tt> holds.
--   (Naturally, the result <tt>x</tt> will be a vector of size
--   <tt>nx1</tt> in this case.)
--   
--   Here's an example call, to solve the following system of equations:
--   
--   <pre>
--   2x + 3y + 4z = 20
--   6x - 3y + 9z = -6
--   2x      +  z = 8
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; solveIntegerLinearEqs Z3 [[2, 3, 4],[6, -3, 9],[2, 0, 1]] [20, -6, 8]
--   Just [5,6,-2]
--   </pre>
--   
--   The first argument picks the SMT solver to use. Valid values are
--   <a>z3</a> and <a>cvc4</a>. Naturally, you should have the chosen
--   solver installed on your system.
--   
--   In case there are no solutions, we will get <a>Nothing</a>:
--   
--   <pre>
--   &gt;&gt;&gt; solveIntegerLinearEqs Z3 [[1], [1]] [2, 3]
--   Nothing
--   </pre>
--   
--   Note that there are no solutions to this second system as it
--   stipulates the unknown is equal to both 2 and 3. (Overspecified.)
solveIntegerLinearEqs :: Solver -> [[Integer]] -> [Integer] -> IO (Maybe [Integer])

-- | Similar to <a>solveIntegerLinearEqs</a>, except in case the system has
--   an infinite number of solutions, then it will return the number of
--   solutions requested. (Note that if the system is underspecified, then
--   there are an infinite number of solutions.) So, the result can be
--   empty, a singleton, or precisely the number requested, last of which
--   indicates there are an infinite number of solutions.
--   
--   Here's an example call, where we underspecify the system and hence
--   there are multiple (in this case an infinite number of) solutions.
--   Here, we ask for the first 3 elements for testing purposes.
--   
--   <pre>
--   2x + 3y + 4z = 20
--   6x - 3y + 9z = -6
--   </pre>
--   
--   We have:
--   
--   <pre>
--   &gt;&gt;&gt; solveIntegerLinearEqsAll Z3 3 [[2, 3, 4],[6, -3, 9]] [20, -6]
--   [[-47,-2,30],[-34,0,22],[-21,2,14]]
--   </pre>
--   
--   The solutions you get might differ, depending on what the solver
--   returns. (Though they'll be correct!)
solveIntegerLinearEqsAll :: Solver -> Int -> [[Integer]] -> [Integer] -> IO [[Integer]]

-- | Solve a system of linear equations over rationals. Same as the integer
--   version <a>solveIntegerLinearEqs</a>, except it takes rational
--   coefficients and returns rational results.
--   
--   Here's an example call, to solve the following system of equations:
--   
--   <pre>
--   2.4x + 3.6y = 12
--   7.2x - 5y   = -8.5
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; solveRationalLinearEqs Z3 [[2.4, 3.6],[7.2, -5]] [12, -8.5]
--   Just [245 % 316,445 % 158]
--   </pre>
solveRationalLinearEqs :: Solver -> [[Rational]] -> [Rational] -> IO (Maybe [Rational])

-- | Solve a system of linear equations over rationals. Similar to
--   <a>solveRationalLinearEqs</a>, except if the system is underspecified,
--   then returns the number of solutions requested.
--   
--   Example system:
--   
--   <pre>
--   2.4x + 3.6y = 12
--   </pre>
--   
--   In this case, the system has infinitely many solutions. We can compute
--   three of them as follows:
--   
--   <pre>
--   &gt;&gt;&gt; solveRationalLinearEqsAll Z3 3 [[2.4, 3.6]] [12]
--   [[0 % 1,10 % 3],[3 % 4,17 % 6],[3 % 2,7 % 3]]
--   </pre>
--   
--   The solutions you get might differ, depending on what the solver
--   returns. (Though they'll be correct!)
solveRationalLinearEqsAll :: Solver -> Int -> [[Rational]] -> [Rational] -> IO [[Rational]]